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 34545 |
. . . . 5
β’ (π β V β π = (π β (π
βpm π) β¦ (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©))) |
7 | 6 | rneqd 5938 |
. . . 4
β’ (π β V β ran π = ran (π β (π
βpm π) β¦ (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©))) |
8 | 1, 2, 5 | mrsubff 34534 |
. . . . . . . . . 10
β’ (π β V β
(mRSubstβπ):(π
βpm π)βΆ(π
βm π
)) |
9 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((π β V β§ π β (π
βpm π)) β (mRSubstβπ):(π
βpm π)βΆ(π
βm π
)) |
10 | 9 | ffund 6722 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β Fun (mRSubstβπ)) |
11 | 8 | ffnd 6719 |
. . . . . . . . . 10
β’ (π β V β
(mRSubstβπ) Fn (π
βpm π)) |
12 | | fnfvelrn 7083 |
. . . . . . . . . 10
β’
(((mRSubstβπ)
Fn (π
βpm
π) β§ π β (π
βpm π)) β ((mRSubstβπ)βπ) β ran (mRSubstβπ)) |
13 | 11, 12 | sylan 581 |
. . . . . . . . 9
β’ ((π β V β§ π β (π
βpm π)) β ((mRSubstβπ)βπ) β ran (mRSubstβπ)) |
14 | 1, 2, 5 | mrsubrn 34535 |
. . . . . . . . 9
β’ ran
(mRSubstβπ) =
((mRSubstβπ) β
(π
βm π)) |
15 | 13, 14 | eleqtrdi 2844 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β ((mRSubstβπ)βπ) β ((mRSubstβπ) β (π
βm π))) |
16 | | fvelima 6958 |
. . . . . . . 8
β’ ((Fun
(mRSubstβπ) β§
((mRSubstβπ)βπ) β ((mRSubstβπ) β (π
βm π))) β βπ β (π
βm π)((mRSubstβπ)βπ) = ((mRSubstβπ)βπ)) |
17 | 10, 15, 16 | syl2anc 585 |
. . . . . . 7
β’ ((π β V β§ π β (π
βpm π)) β βπ β (π
βm π)((mRSubstβπ)βπ) = ((mRSubstβπ)βπ)) |
18 | | elmapi 8843 |
. . . . . . . . . . . . 13
β’ (π β (π
βm π) β π:πβΆπ
) |
19 | 18 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β V β§ π β (π
βm π)) β π:πβΆπ
) |
20 | | ssid 4005 |
. . . . . . . . . . . 12
β’ π β π |
21 | 1, 2, 3, 4, 5 | msubfval 34546 |
. . . . . . . . . . . 12
β’ ((π:πβΆπ
β§ π β π) β (πβπ) = (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)) |
22 | 19, 20, 21 | sylancl 587 |
. . . . . . . . . . 11
β’ ((π β V β§ π β (π
βm π)) β (πβπ) = (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)) |
23 | | fvex 6905 |
. . . . . . . . . . . . . . . 16
β’
(mExβπ) β
V |
24 | 23 | mptex 7225 |
. . . . . . . . . . . . . . 15
β’ (π β (mExβπ) β¦ β¨(1st
βπ),
(((mRSubstβπ)βπ)β(2nd βπ))β©) β
V |
25 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π β (π
βpm π) β¦ (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)) = (π β (π
βpm π) β¦ (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)) |
26 | 24, 25 | fnmpti 6694 |
. . . . . . . . . . . . . 14
β’ (π β (π
βpm π) β¦ (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)) Fn (π
βpm π) |
27 | 6 | fneq1d 6643 |
. . . . . . . . . . . . . 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 8870 |
. . . . . . . . . . . . 13
β’ (π
βm π) β (π
βpm π) |
31 | 30 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β V β§ π β (π
βm π)) β (π
βm π) β (π
βpm π)) |
32 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((π β V β§ π β (π
βm π)) β π β (π
βm π)) |
33 | | fnfvima 7235 |
. . . . . . . . . . . 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 6891 |
. . . . . . . . . . . 12
β’
(((mRSubstβπ)βπ) = ((mRSubstβπ)βπ) β (((mRSubstβπ)βπ)β(2nd βπ)) = (((mRSubstβπ)βπ)β(2nd βπ))) |
38 | 37 | opeq2d 4881 |
. . . . . . . . . . 11
β’
(((mRSubstβπ)βπ) = ((mRSubstβπ)βπ) β β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β© = β¨(1st
βπ),
(((mRSubstβπ)βπ)β(2nd βπ))β©) |
39 | 38 | mpteq2dv 5251 |
. . . . . . . . . 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 7115 |
. . . . 5
β’ (π β V β (π β (π
βpm π) β¦ (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)):(π
βpm π)βΆ(π β (π
βm π))) |
45 | 44 | frnd 6726 |
. . . 4
β’ (π β V β ran (π β (π
βpm π) β¦ (π β (mExβπ) β¦ β¨(1st βπ), (((mRSubstβπ)βπ)β(2nd βπ))β©)) β (π β (π
βm π))) |
46 | 7, 45 | eqsstrd 4021 |
. . 3
β’ (π β V β ran π β (π β (π
βm π))) |
47 | 3 | rnfvprc 6886 |
. . . 4
β’ (Β¬
π β V β ran π = β
) |
48 | | 0ss 4397 |
. . . 4
β’ β
β (π β (π
βm π)) |
49 | 47, 48 | eqsstrdi 4037 |
. . 3
β’ (Β¬
π β V β ran π β (π β (π
βm π))) |
50 | 46, 49 | pm2.61i 182 |
. 2
β’ ran π β (π β (π
βm π)) |
51 | | imassrn 6071 |
. 2
β’ (π β (π
βm π)) β ran π |
52 | 50, 51 | eqssi 3999 |
1
β’ ran π = (π β (π
βm π)) |