Step | Hyp | Ref
| Expression |
1 | | msubff.v |
. . . . . 6
⊢ 𝑉 = (mVR‘𝑇) |
2 | | msubff.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
3 | | msubff.s |
. . . . . 6
⊢ 𝑆 = (mSubst‘𝑇) |
4 | | eqid 2622 |
. . . . . 6
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
5 | | eqid 2622 |
. . . . . 6
⊢
(mRSubst‘𝑇) =
(mRSubst‘𝑇) |
6 | 1, 2, 3, 4, 5 | msubffval 31420 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉))) |
7 | 6 | rneqd 5353 |
. . . 4
⊢ (𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉))) |
8 | 1, 2, 5 | mrsubff 31409 |
. . . . . . . . . 10
⊢ (𝑇 ∈ V →
(mRSubst‘𝑇):(𝑅 ↑pm
𝑉)⟶(𝑅 ↑𝑚
𝑅)) |
9 | 8 | adantr 481 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅)) |
10 | | ffun 6048 |
. . . . . . . . 9
⊢
((mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅) → Fun
(mRSubst‘𝑇)) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → Fun
(mRSubst‘𝑇)) |
12 | | ffn 6045 |
. . . . . . . . . . 11
⊢
((mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅) → (mRSubst‘𝑇) Fn (𝑅 ↑pm 𝑉)) |
13 | 8, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝑇 ∈ V →
(mRSubst‘𝑇) Fn (𝑅 ↑pm
𝑉)) |
14 | | fnfvelrn 6356 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)
Fn (𝑅
↑pm 𝑉) ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇)) |
15 | 13, 14 | sylan 488 |
. . . . . . . . 9
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇)) |
16 | 1, 2, 5 | mrsubrn 31410 |
. . . . . . . . 9
⊢ ran
(mRSubst‘𝑇) =
((mRSubst‘𝑇) “
(𝑅
↑𝑚 𝑉)) |
17 | 15, 16 | syl6eleq 2711 |
. . . . . . . 8
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑𝑚 𝑉))) |
18 | | fvelima 6248 |
. . . . . . . 8
⊢ ((Fun
(mRSubst‘𝑇) ∧
((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑𝑚 𝑉))) → ∃𝑔 ∈ (𝑅 ↑𝑚 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓)) |
19 | 11, 17, 18 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → ∃𝑔 ∈ (𝑅 ↑𝑚 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓)) |
20 | | elmapi 7879 |
. . . . . . . . . . . . 13
⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → 𝑔:𝑉⟶𝑅) |
21 | 20 | adantl 482 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑔:𝑉⟶𝑅) |
22 | | ssid 3624 |
. . . . . . . . . . . 12
⊢ 𝑉 ⊆ 𝑉 |
23 | 1, 2, 3, 4, 5 | msubfval 31421 |
. . . . . . . . . . . 12
⊢ ((𝑔:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉)) |
24 | 21, 22, 23 | sylancl 694 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉)) |
25 | | fvex 6201 |
. . . . . . . . . . . . . . . 16
⊢
(mEx‘𝑇) ∈
V |
26 | 25 | mptex 6486 |
. . . . . . . . . . . . . . 15
⊢ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑒),
(((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈
V |
27 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) |
28 | 26, 27 | fnmpti 6022 |
. . . . . . . . . . . . . 14
⊢ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) Fn (𝑅 ↑pm 𝑉) |
29 | 6 | fneq1d 5981 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ V → (𝑆 Fn (𝑅 ↑pm 𝑉) ↔ (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) Fn (𝑅 ↑pm 𝑉))) |
30 | 28, 29 | mpbiri 248 |
. . . . . . . . . . . . 13
⊢ (𝑇 ∈ V → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
31 | 30 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑆 Fn (𝑅 ↑pm 𝑉)) |
32 | | mapsspm 7891 |
. . . . . . . . . . . . 13
⊢ (𝑅 ↑𝑚
𝑉) ⊆ (𝑅 ↑pm
𝑉) |
33 | 32 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑅 ↑𝑚 𝑉) ⊆ (𝑅 ↑pm 𝑉)) |
34 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) |
35 | | fnfvima 6496 |
. . . . . . . . . . . 12
⊢ ((𝑆 Fn (𝑅 ↑pm 𝑉) ∧ (𝑅 ↑𝑚 𝑉) ⊆ (𝑅 ↑pm 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
36 | 31, 33, 34, 35 | syl3anc 1326 |
. . . . . . . . . . 11
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
37 | 24, 36 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
38 | 37 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
39 | | fveq1 6190 |
. . . . . . . . . . . 12
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒)) = (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))) |
40 | 39 | opeq2d 4409 |
. . . . . . . . . . 11
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒),
(((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) |
41 | 40 | mpteq2dv 4745 |
. . . . . . . . . 10
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) = (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) |
42 | 41 | eleq1d 2686 |
. . . . . . . . 9
⊢
(((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → ((𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉)) ↔ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉)))) |
43 | 38, 42 | syl5ibcom 235 |
. . . . . . . 8
⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉)))) |
44 | 43 | rexlimdva 3031 |
. . . . . . 7
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (∃𝑔 ∈ (𝑅 ↑𝑚 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉)))) |
45 | 19, 44 | mpd 15 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑pm 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉) ∈ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
46 | 45, 27 | fmptd 6385 |
. . . . 5
⊢ (𝑇 ∈ V → (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)):(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑𝑚 𝑉))) |
47 | | frn 6053 |
. . . . 5
⊢ ((𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)):(𝑅 ↑pm 𝑉)⟶(𝑆 “ (𝑅 ↑𝑚 𝑉)) → ran (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
48 | 46, 47 | syl 17 |
. . . 4
⊢ (𝑇 ∈ V → ran (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘𝑒))〉)) ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
49 | 7, 48 | eqsstrd 3639 |
. . 3
⊢ (𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
50 | | fvprc 6185 |
. . . . . . 7
⊢ (¬
𝑇 ∈ V →
(mSubst‘𝑇) =
∅) |
51 | 3, 50 | syl5eq 2668 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
52 | 51 | rneqd 5353 |
. . . . 5
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ran ∅) |
53 | | rn0 5377 |
. . . . 5
⊢ ran
∅ = ∅ |
54 | 52, 53 | syl6eq 2672 |
. . . 4
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ∅) |
55 | | 0ss 3972 |
. . . 4
⊢ ∅
⊆ (𝑆 “ (𝑅 ↑𝑚
𝑉)) |
56 | 54, 55 | syl6eqss 3655 |
. . 3
⊢ (¬
𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉))) |
57 | 49, 56 | pm2.61i 176 |
. 2
⊢ ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑𝑚 𝑉)) |
58 | | imassrn 5477 |
. 2
⊢ (𝑆 “ (𝑅 ↑𝑚 𝑉)) ⊆ ran 𝑆 |
59 | 57, 58 | eqssi 3619 |
1
⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑𝑚 𝑉)) |