Step | Hyp | Ref
| Expression |
1 | | msubff.v |
. . . . . 6
⊢ 𝑉 = (mVR‘𝑇) |
2 | | msubff.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
3 | | msubff.s |
. . . . . 6
⊢ 𝑆 = (mSubst‘𝑇) |
4 | | eqid 2733 |
. . . . . 6
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
5 | | eqid 2733 |
. . . . . 6
⊢
(mRSubst‘𝑇) =
(mRSubst‘𝑇) |
6 | 1, 2, 3, 4, 5 | msubffval 34503 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉))) |
7 | 6 | rneqd 5936 |
. . . 4
⊢ (𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉))) |
8 | 1, 2, 5 | mrsubff 34492 |
. . . . . . . . . 10
⊢ (𝑇 ∈ V →
(mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) |
9 | 8 | adantr 482 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) |
10 | 9 | ffund 6719 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → Fun (mRSubst‘𝑇)) |
11 | 8 | ffnd 6716 |
. . . . . . . . . 10
⊢ (𝑇 ∈ V →
(mRSubst‘𝑇) Fn (𝑅 ↑pm 𝑉)) |
12 | | fnfvelrn 7080 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)
Fn (𝑅 ↑pm
𝑉) ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇)) |
13 | 11, 12 | sylan 581 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇)) |
14 | 1, 2, 5 | mrsubrn 34493 |
. . . . . . . . 9
⊢ ran
(mRSubst‘𝑇) =
((mRSubst‘𝑇) “
(𝑅 ↑m 𝑉)) |
15 | 13, 14 | eleqtrdi 2844 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑m 𝑉))) |
16 | | fvelima 6955 |
. . . . . . . 8
⊢ ((Fun
(mRSubst‘𝑇) ∧
((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑m 𝑉))) → ∃𝑔 ∈ (𝑅 ↑m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓)) |
17 | 10, 15, 16 | syl2anc 585 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ∃𝑔 ∈ (𝑅 ↑m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓)) |
18 | | elmapi 8840 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝑅 ↑m 𝑉) → 𝑔:𝑉⟶𝑅) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → 𝑔:𝑉⟶𝑅) |
20 | | ssid 4004 |
. . . . . . . . . . . 12
⊢ 𝑉 ⊆ 𝑉 |
21 | 1, 2, 3, 4, 5 | msubfval 34504 |
. . . . . . . . . . . 12
⊢ ((𝑔:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉)) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉)) |
23 | | fvex 6902 |
. . . . . . . . . . . . . . . 16
⊢
(mEx‘𝑇) ∈
V |
24 | 23 | mptex 7222 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑒),
(((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈
V |
25 | | eqid 2733 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) |
26 | 24, 25 | fnmpti 6691 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) Fn (𝑅 ↑pm 𝑉) |
27 | 6 | fneq1d 6640 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → (𝑆 Fn (𝑅 ↑pm 𝑉) ↔ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) Fn (𝑅 ↑pm 𝑉))) |
28 | 26, 27 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
29 | 28 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
30 | | mapsspm 8867 |
. . . . . . . . . . . . 13
⊢ (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉) |
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉)) |
32 | | simpr 486 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → 𝑔 ∈ (𝑅 ↑m 𝑉)) |
33 | | fnfvima 7232 |
. . . . . . . . . . . 12
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉) ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
34 | 29, 31, 32, 33 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
35 | 22, 34 | eqeltrrd 2835 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
36 | 35 | adantlr 714 |
. . . . . . . . 9
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
37 | | fveq1 6888 |
. . . . . . . . . . . 12
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒)) = (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))) |
38 | 37 | opeq2d 4880 |
. . . . . . . . . . 11
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒),
(((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) |
39 | 38 | mpteq2dv 5250 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) |
40 | 39 | eleq1d 2819 |
. . . . . . . . 9
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → ((𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉)) ↔ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉)))) |
41 | 36, 40 | syl5ibcom 244 |
. . . . . . . 8
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉)))) |
42 | 41 | rexlimdva 3156 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (∃𝑔 ∈ (𝑅 ↑m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉)))) |
43 | 17, 42 | mpd 15 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
44 | 43 | fmpttd 7112 |
. . . . 5
⊢ (𝑇 ∈ V → (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)):(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑m 𝑉))) |
45 | 44 | frnd 6723 |
. . . 4
⊢ (𝑇 ∈ V → ran (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
46 | 7, 45 | eqsstrd 4020 |
. . 3
⊢ (𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
47 | 3 | rnfvprc 6883 |
. . . 4
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
48 | | 0ss 4396 |
. . . 4
⊢ ∅
⊆ (𝑆 “ (𝑅 ↑m 𝑉)) |
49 | 47, 48 | eqsstrdi 4036 |
. . 3
⊢ (¬
𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
50 | 46, 49 | pm2.61i 182 |
. 2
⊢ ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉)) |
51 | | imassrn 6069 |
. 2
⊢ (𝑆 “ (𝑅 ↑m 𝑉)) ⊆ ran 𝑆 |
52 | 50, 51 | eqssi 3998 |
1
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑m 𝑉)) |