Step | Hyp | Ref
| Expression |
1 | | msubff1.v |
. . . 4
⊢ 𝑉 = (mVR‘𝑇) |
2 | | msubff1.r |
. . . 4
⊢ 𝑅 = (mREx‘𝑇) |
3 | | msubff1.s |
. . . 4
⊢ 𝑆 = (mSubst‘𝑇) |
4 | | msubff1.e |
. . . 4
⊢ 𝐸 = (mEx‘𝑇) |
5 | 1, 2, 3, 4 | msubff 30681 |
. . 3
⊢ (𝑇 ∈ mFS → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑𝑚 𝐸)) |
6 | | mapsspm 7777 |
. . . 4
⊢ (𝑅 ↑𝑚
𝑉) ⊆ (𝑅 ↑pm
𝑉) |
7 | 6 | a1i 11 |
. . 3
⊢ (𝑇 ∈ mFS → (𝑅 ↑𝑚
𝑉) ⊆ (𝑅 ↑pm
𝑉)) |
8 | 5, 7 | fssresd 5984 |
. 2
⊢ (𝑇 ∈ mFS → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)⟶(𝐸 ↑𝑚 𝐸)) |
9 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(mRSubst‘𝑇) =
(mRSubst‘𝑇) |
10 | 1, 2, 9 | mrsubff 30663 |
. . . . . . . . . . . 12
⊢ (𝑇 ∈ mFS →
(mRSubst‘𝑇):(𝑅 ↑pm
𝑉)⟶(𝑅 ↑𝑚
𝑅)) |
11 | 10 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → (mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
12 | | simplrl 796 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑓 ∈ (𝑅 ↑𝑚 𝑉)) |
13 | 6, 12 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑓 ∈ (𝑅 ↑pm 𝑉)) |
14 | 11, 13 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑓) ∈ (𝑅 ↑𝑚 𝑅)) |
15 | | elmapi 7765 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑓) ∈ (𝑅 ↑𝑚 𝑅) → ((mRSubst‘𝑇)‘𝑓):𝑅⟶𝑅) |
16 | | ffn 5958 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑓):𝑅⟶𝑅 → ((mRSubst‘𝑇)‘𝑓) Fn 𝑅) |
17 | 14, 15, 16 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑓) Fn 𝑅) |
18 | | simplrr 797 |
. . . . . . . . . . . 12
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) |
19 | 6, 18 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑔 ∈ (𝑅 ↑pm 𝑉)) |
20 | 11, 19 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑔) ∈ (𝑅 ↑𝑚 𝑅)) |
21 | | elmapi 7765 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑔) ∈ (𝑅 ↑𝑚 𝑅) → ((mRSubst‘𝑇)‘𝑔):𝑅⟶𝑅) |
22 | | ffn 5958 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑔):𝑅⟶𝑅 → ((mRSubst‘𝑇)‘𝑔) Fn 𝑅) |
23 | 20, 21, 22 | 3syl 18 |
. . . . . . . . 9
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑔) Fn 𝑅) |
24 | | simplrr 797 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (𝑆‘𝑓) = (𝑆‘𝑔)) |
25 | 24 | fveq1d 6105 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((𝑆‘𝑓)‘〈((mType‘𝑇)‘𝑣), 𝑟〉) = ((𝑆‘𝑔)‘〈((mType‘𝑇)‘𝑣), 𝑟〉)) |
26 | 12 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑓 ∈ (𝑅 ↑𝑚 𝑉)) |
27 | | elmapi 7765 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → 𝑓:𝑉⟶𝑅) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑓:𝑉⟶𝑅) |
29 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ 𝑉 ⊆ 𝑉 |
30 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑉 ⊆ 𝑉) |
31 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(mTC‘𝑇) =
(mTC‘𝑇) |
32 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(mType‘𝑇) =
(mType‘𝑇) |
33 | 1, 31, 32 | mtyf2 30702 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑇 ∈ mFS →
(mType‘𝑇):𝑉⟶(mTC‘𝑇)) |
34 | 33 | ad3antrrr 762 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (mType‘𝑇):𝑉⟶(mTC‘𝑇)) |
35 | | simplrl 796 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑣 ∈ 𝑉) |
36 | 34, 35 | ffvelrnd 6268 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((mType‘𝑇)‘𝑣) ∈ (mTC‘𝑇)) |
37 | | opelxpi 5072 |
. . . . . . . . . . . . . . 15
⊢
((((mType‘𝑇)‘𝑣) ∈ (mTC‘𝑇) ∧ 𝑟 ∈ 𝑅) → 〈((mType‘𝑇)‘𝑣), 𝑟〉 ∈ ((mTC‘𝑇) × 𝑅)) |
38 | 36, 37 | sylancom 698 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 〈((mType‘𝑇)‘𝑣), 𝑟〉 ∈ ((mTC‘𝑇) × 𝑅)) |
39 | 31, 4, 2 | mexval 30653 |
. . . . . . . . . . . . . 14
⊢ 𝐸 = ((mTC‘𝑇) × 𝑅) |
40 | 38, 39 | syl6eleqr 2699 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 〈((mType‘𝑇)‘𝑣), 𝑟〉 ∈ 𝐸) |
41 | 1, 2, 3, 4, 9 | msubval 30676 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 〈((mType‘𝑇)‘𝑣), 𝑟〉 ∈ 𝐸) → ((𝑆‘𝑓)‘〈((mType‘𝑇)‘𝑣), 𝑟〉) = 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉) |
42 | 28, 30, 40, 41 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((𝑆‘𝑓)‘〈((mType‘𝑇)‘𝑣), 𝑟〉) = 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉) |
43 | 18 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) |
44 | | elmapi 7765 |
. . . . . . . . . . . . . 14
⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → 𝑔:𝑉⟶𝑅) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑔:𝑉⟶𝑅) |
46 | 1, 2, 3, 4, 9 | msubval 30676 |
. . . . . . . . . . . . 13
⊢ ((𝑔:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 〈((mType‘𝑇)‘𝑣), 𝑟〉 ∈ 𝐸) → ((𝑆‘𝑔)‘〈((mType‘𝑇)‘𝑣), 𝑟〉) = 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉) |
47 | 45, 30, 40, 46 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((𝑆‘𝑔)‘〈((mType‘𝑇)‘𝑣), 𝑟〉) = 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉) |
48 | 25, 42, 47 | 3eqtr3d 2652 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉 = 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉) |
49 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(1st ‘〈((mType‘𝑇)‘𝑣), 𝑟〉) ∈ V |
50 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢
(((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉)) ∈ V |
51 | 49, 50 | opth 4871 |
. . . . . . . . . . . 12
⊢
(〈(1st ‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉 = 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉 ↔ ((1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉) = (1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉) ∧ (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉)) = (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉)))) |
52 | 51 | simprbi 479 |
. . . . . . . . . . 11
⊢
(〈(1st ‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉 = 〈(1st
‘〈((mType‘𝑇)‘𝑣), 𝑟〉), (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))〉 → (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉)) = (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))) |
53 | 48, 52 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉)) = (((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉))) |
54 | | fvex 6113 |
. . . . . . . . . . . 12
⊢
((mType‘𝑇)‘𝑣) ∈ V |
55 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑟 ∈ V |
56 | 54, 55 | op2nd 7068 |
. . . . . . . . . . 11
⊢
(2nd ‘〈((mType‘𝑇)‘𝑣), 𝑟〉) = 𝑟 |
57 | 56 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑓)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉)) = (((mRSubst‘𝑇)‘𝑓)‘𝑟) |
58 | 56 | fveq2i 6106 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑔)‘(2nd
‘〈((mType‘𝑇)‘𝑣), 𝑟〉)) = (((mRSubst‘𝑇)‘𝑔)‘𝑟) |
59 | 53, 57, 58 | 3eqtr3g 2667 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (((mRSubst‘𝑇)‘𝑓)‘𝑟) = (((mRSubst‘𝑇)‘𝑔)‘𝑟)) |
60 | 17, 23, 59 | eqfnfvd 6222 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔)) |
61 | 1, 2, 9 | mrsubff1 30665 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ mFS →
((mRSubst‘𝑇) ↾
(𝑅
↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝑅 ↑𝑚 𝑅)) |
62 | | f1fveq 6420 |
. . . . . . . . . . 11
⊢
((((mRSubst‘𝑇)
↾ (𝑅
↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝑅 ↑𝑚 𝑅) ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) →
((((mRSubst‘𝑇)
↾ (𝑅
↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ 𝑓 = 𝑔)) |
63 | 61, 62 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) →
((((mRSubst‘𝑇)
↾ (𝑅
↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ 𝑓 = 𝑔)) |
64 | | fvres 6117 |
. . . . . . . . . . . 12
⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((mRSubst‘𝑇)‘𝑓)) |
65 | | fvres 6117 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) = ((mRSubst‘𝑇)‘𝑔)) |
66 | 64, 65 | eqeqan12d 2626 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) →
((((mRSubst‘𝑇)
↾ (𝑅
↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔))) |
67 | 66 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) →
((((mRSubst‘𝑇)
↾ (𝑅
↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔))) |
68 | 63, 67 | bitr3d 269 |
. . . . . . . . 9
⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑓 = 𝑔 ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔))) |
69 | 68 | adantr 480 |
. . . . . . . 8
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → (𝑓 = 𝑔 ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔))) |
70 | 60, 69 | mpbird 246 |
. . . . . . 7
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑓 = 𝑔) |
71 | 70 | fveq1d 6105 |
. . . . . 6
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → (𝑓‘𝑣) = (𝑔‘𝑣)) |
72 | 71 | expr 641 |
. . . . 5
⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑓) = (𝑆‘𝑔) → (𝑓‘𝑣) = (𝑔‘𝑣))) |
73 | 72 | ralrimdva 2952 |
. . . 4
⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝑆‘𝑓) = (𝑆‘𝑔) → ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
74 | | fvres 6117 |
. . . . . 6
⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = (𝑆‘𝑓)) |
75 | | fvres 6117 |
. . . . . 6
⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) = (𝑆‘𝑔)) |
76 | 74, 75 | eqeqan12d 2626 |
. . . . 5
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ (𝑆‘𝑓) = (𝑆‘𝑔))) |
77 | 76 | adantl 481 |
. . . 4
⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ (𝑆‘𝑓) = (𝑆‘𝑔))) |
78 | | ffn 5958 |
. . . . . . 7
⊢ (𝑓:𝑉⟶𝑅 → 𝑓 Fn 𝑉) |
79 | | ffn 5958 |
. . . . . . 7
⊢ (𝑔:𝑉⟶𝑅 → 𝑔 Fn 𝑉) |
80 | | eqfnfv 6219 |
. . . . . . 7
⊢ ((𝑓 Fn 𝑉 ∧ 𝑔 Fn 𝑉) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
81 | 78, 79, 80 | syl2an 493 |
. . . . . 6
⊢ ((𝑓:𝑉⟶𝑅 ∧ 𝑔:𝑉⟶𝑅) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
82 | 27, 44, 81 | syl2an 493 |
. . . . 5
⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
83 | 82 | adantl 481 |
. . . 4
⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣))) |
84 | 73, 77, 83 | 3imtr4d 282 |
. . 3
⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔)) |
85 | 84 | ralrimivva 2954 |
. 2
⊢ (𝑇 ∈ mFS → ∀𝑓 ∈ (𝑅 ↑𝑚 𝑉)∀𝑔 ∈ (𝑅 ↑𝑚 𝑉)(((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔)) |
86 | | dff13 6416 |
. 2
⊢ ((𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝐸 ↑𝑚 𝐸) ↔ ((𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)⟶(𝐸 ↑𝑚 𝐸) ∧ ∀𝑓 ∈ (𝑅 ↑𝑚 𝑉)∀𝑔 ∈ (𝑅 ↑𝑚 𝑉)(((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔))) |
87 | 8, 85, 86 | sylanbrc 695 |
1
⊢ (𝑇 ∈ mFS → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝐸 ↑𝑚 𝐸)) |