Step | Hyp | Ref
| Expression |
1 | | msubff.v |
. . . . . 6
⊢ 𝑉 = (mVR‘𝑇) |
2 | | msubff.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
3 | | msubff.s |
. . . . . 6
⊢ 𝑆 = (mSubst‘𝑇) |
4 | | eqid 2759 |
. . . . . 6
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
5 | | eqid 2759 |
. . . . . 6
⊢
(mRSubst‘𝑇) =
(mRSubst‘𝑇) |
6 | 1, 2, 3, 4, 5 | msubffval 33015 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉))) |
7 | 6 | rneqd 5785 |
. . . 4
⊢ (𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉))) |
8 | 1, 2, 5 | mrsubff 33004 |
. . . . . . . . . 10
⊢ (𝑇 ∈ V →
(mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) |
9 | 8 | adantr 484 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑m 𝑅)) |
10 | 9 | ffund 6508 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → Fun (mRSubst‘𝑇)) |
11 | 8 | ffnd 6505 |
. . . . . . . . . 10
⊢ (𝑇 ∈ V →
(mRSubst‘𝑇) Fn (𝑅 ↑pm 𝑉)) |
12 | | fnfvelrn 6846 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)
Fn (𝑅 ↑pm
𝑉) ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇)) |
13 | 11, 12 | sylan 583 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇)) |
14 | 1, 2, 5 | mrsubrn 33005 |
. . . . . . . . 9
⊢ ran
(mRSubst‘𝑇) =
((mRSubst‘𝑇) “
(𝑅 ↑m 𝑉)) |
15 | 13, 14 | eleqtrdi 2863 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑m 𝑉))) |
16 | | fvelima 6725 |
. . . . . . . 8
⊢ ((Fun
(mRSubst‘𝑇) ∧
((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑m 𝑉))) → ∃𝑔 ∈ (𝑅 ↑m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓)) |
17 | 10, 15, 16 | syl2anc 587 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ∃𝑔 ∈ (𝑅 ↑m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓)) |
18 | | elmapi 8445 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝑅 ↑m 𝑉) → 𝑔:𝑉⟶𝑅) |
19 | 18 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → 𝑔:𝑉⟶𝑅) |
20 | | ssid 3917 |
. . . . . . . . . . . 12
⊢ 𝑉 ⊆ 𝑉 |
21 | 1, 2, 3, 4, 5 | msubfval 33016 |
. . . . . . . . . . . 12
⊢ ((𝑔:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉)) |
22 | 19, 20, 21 | sylancl 589 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉)) |
23 | | fvex 6677 |
. . . . . . . . . . . . . . . 16
⊢
(mEx‘𝑇) ∈
V |
24 | 23 | mptex 6984 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑒),
(((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈
V |
25 | | eqid 2759 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) |
26 | 24, 25 | fnmpti 6480 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) Fn (𝑅 ↑pm 𝑉) |
27 | 6 | fneq1d 6433 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → (𝑆 Fn (𝑅 ↑pm 𝑉) ↔ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) Fn (𝑅 ↑pm 𝑉))) |
28 | 26, 27 | mpbiri 261 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
29 | 28 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
30 | | mapsspm 8472 |
. . . . . . . . . . . . 13
⊢ (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉) |
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉)) |
32 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → 𝑔 ∈ (𝑅 ↑m 𝑉)) |
33 | | fnfvima 6994 |
. . . . . . . . . . . 12
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑅 ↑m 𝑉) ⊆ (𝑅 ↑pm 𝑉) ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
34 | 29, 31, 32, 33 | syl3anc 1369 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
35 | 22, 34 | eqeltrrd 2854 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
36 | 35 | adantlr 714 |
. . . . . . . . 9
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉))) |
37 | | fveq1 6663 |
. . . . . . . . . . . 12
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒)) = (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))) |
38 | 37 | opeq2d 4774 |
. . . . . . . . . . 11
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒),
(((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) |
39 | 38 | mpteq2dv 5133 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) |
40 | 39 | eleq1d 2837 |
. . . . . . . . 9
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → ((𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉)) ↔ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉)))) |
41 | 36, 40 | syl5ibcom 248 |
. . . . . . . 8
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑m 𝑉)) → (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑m 𝑉)))) |
42 | 41 | rexlimdva 3209 |
. . . . . . 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 6877 |
. . . . 5
⊢ (𝑇 ∈ V → (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)):(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑m 𝑉))) |
45 | 44 | frnd 6511 |
. . . 4
⊢ (𝑇 ∈ V → ran (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
46 | 7, 45 | eqsstrd 3933 |
. . 3
⊢ (𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
47 | 3 | rnfvprc 6658 |
. . . 4
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
48 | | 0ss 4296 |
. . . 4
⊢ ∅
⊆ (𝑆 “ (𝑅 ↑m 𝑉)) |
49 | 47, 48 | eqsstrdi 3949 |
. . 3
⊢ (¬
𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉))) |
50 | 46, 49 | pm2.61i 185 |
. 2
⊢ ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑m 𝑉)) |
51 | | imassrn 5918 |
. 2
⊢ (𝑆 “ (𝑅 ↑m 𝑉)) ⊆ ran 𝑆 |
52 | 50, 51 | eqssi 3911 |
1
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑m 𝑉)) |