Step | Hyp | Ref
| Expression |
1 | | mrsubvr.v |
. . . . . . 7
β’ π = (mVRβπ) |
2 | | mrsubvr.r |
. . . . . . 7
β’ π
= (mRExβπ) |
3 | | mrsubvr.s |
. . . . . . 7
β’ π = (mRSubstβπ) |
4 | 1, 2, 3 | mrsubff 34170 |
. . . . . 6
β’ (π β V β π:(π
βpm π)βΆ(π
βm π
)) |
5 | 4 | ffnd 6673 |
. . . . 5
β’ (π β V β π Fn (π
βpm π)) |
6 | | eleq1w 2817 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π£ β (π₯ β dom π β π£ β dom π)) |
7 | | fveq2 6846 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π£ β (πβπ₯) = (πβπ£)) |
8 | | s1eq 14497 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ = π£ β β¨βπ₯ββ© = β¨βπ£ββ©) |
9 | 6, 7, 8 | ifbieq12d 4518 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ = π£ β if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©) = if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) |
10 | | eqid 2733 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)) = (π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)) |
11 | | fvex 6859 |
. . . . . . . . . . . . . . . . . 18
β’ (πβπ£) β V |
12 | | s1cli 14502 |
. . . . . . . . . . . . . . . . . . 19
β’
β¨βπ£ββ© β Word V |
13 | 12 | elexi 3466 |
. . . . . . . . . . . . . . . . . 18
β’
β¨βπ£ββ© β V |
14 | 11, 13 | ifex 4540 |
. . . . . . . . . . . . . . . . 17
β’ if(π£ β dom π, (πβπ£), β¨βπ£ββ©) β V |
15 | 9, 10, 14 | fvmpt 6952 |
. . . . . . . . . . . . . . . 16
β’ (π£ β π β ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£) = if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) |
16 | 15 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β V β§ π β (π
βpm π)) β§ π£ β π) β ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£) = if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) |
17 | 16 | ifeq1da 4521 |
. . . . . . . . . . . . . 14
β’ ((π β V β§ π β (π
βpm π)) β if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©) = if(π£ β π, if(π£ β dom π, (πβπ£), β¨βπ£ββ©), β¨βπ£ββ©)) |
18 | | ifan 4543 |
. . . . . . . . . . . . . 14
β’ if((π£ β π β§ π£ β dom π), (πβπ£), β¨βπ£ββ©) = if(π£ β π, if(π£ β dom π, (πβπ£), β¨βπ£ββ©), β¨βπ£ββ©) |
19 | 17, 18 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ ((π β V β§ π β (π
βpm π)) β if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©) = if((π£ β π β§ π£ β dom π), (πβπ£), β¨βπ£ββ©)) |
20 | | elpmi 8790 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π
βpm π) β (π:dom πβΆπ
β§ dom π β π)) |
21 | 20 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β V β§ π β (π
βpm π)) β (π:dom πβΆπ
β§ dom π β π)) |
22 | 21 | simprd 497 |
. . . . . . . . . . . . . . . . 17
β’ ((π β V β§ π β (π
βpm π)) β dom π β π) |
23 | 22 | sseld 3947 |
. . . . . . . . . . . . . . . 16
β’ ((π β V β§ π β (π
βpm π)) β (π£ β dom π β π£ β π)) |
24 | 23 | pm4.71rd 564 |
. . . . . . . . . . . . . . 15
β’ ((π β V β§ π β (π
βpm π)) β (π£ β dom π β (π£ β π β§ π£ β dom π))) |
25 | 24 | bicomd 222 |
. . . . . . . . . . . . . 14
β’ ((π β V β§ π β (π
βpm π)) β ((π£ β π β§ π£ β dom π) β π£ β dom π)) |
26 | 25 | ifbid 4513 |
. . . . . . . . . . . . 13
β’ ((π β V β§ π β (π
βpm π)) β if((π£ β π β§ π£ β dom π), (πβπ£), β¨βπ£ββ©) = if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) |
27 | 19, 26 | eqtr2d 2774 |
. . . . . . . . . . . 12
β’ ((π β V β§ π β (π
βpm π)) β if(π£ β dom π, (πβπ£), β¨βπ£ββ©) = if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©)) |
28 | 27 | mpteq2dv 5211 |
. . . . . . . . . . 11
β’ ((π β V β§ π β (π
βpm π)) β (π£ β ((mCNβπ) βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) = (π£ β ((mCNβπ) βͺ π) β¦ if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©))) |
29 | 28 | coeq1d 5821 |
. . . . . . . . . 10
β’ ((π β V β§ π β (π
βpm π)) β ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π) = ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©)) β π)) |
30 | 29 | oveq2d 7377 |
. . . . . . . . 9
β’ ((π β V β§ π β (π
βpm π)) β ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)) = ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©)) β π))) |
31 | 30 | mpteq2dv 5211 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β (π β π
β¦ ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π))) = (π β π
β¦ ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©)) β π)))) |
32 | | eqid 2733 |
. . . . . . . . . 10
β’
(mCNβπ) =
(mCNβπ) |
33 | | eqid 2733 |
. . . . . . . . . 10
β’
(freeMndβ((mCNβπ) βͺ π)) = (freeMndβ((mCNβπ) βͺ π)) |
34 | 32, 1, 2, 3, 33 | mrsubfval 34166 |
. . . . . . . . 9
β’ ((π:dom πβΆπ
β§ dom π β π) β (πβπ) = (π β π
β¦ ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)))) |
35 | 21, 34 | syl 17 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β (πβπ) = (π β π
β¦ ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β dom π, (πβπ£), β¨βπ£ββ©)) β π)))) |
36 | 21 | simpld 496 |
. . . . . . . . . . . . 13
β’ ((π β V β§ π β (π
βpm π)) β π:dom πβΆπ
) |
37 | 36 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β V β§ π β (π
βpm π)) β§ π₯ β π) β π:dom πβΆπ
) |
38 | 37 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((((π β V β§ π β (π
βpm π)) β§ π₯ β π) β§ π₯ β dom π) β (πβπ₯) β π
) |
39 | | elun2 4141 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β π₯ β ((mCNβπ) βͺ π)) |
40 | 39 | ad2antlr 726 |
. . . . . . . . . . . . 13
β’ ((((π β V β§ π β (π
βpm π)) β§ π₯ β π) β§ Β¬ π₯ β dom π) β π₯ β ((mCNβπ) βͺ π)) |
41 | 40 | s1cld 14500 |
. . . . . . . . . . . 12
β’ ((((π β V β§ π β (π
βpm π)) β§ π₯ β π) β§ Β¬ π₯ β dom π) β β¨βπ₯ββ© β Word ((mCNβπ) βͺ π)) |
42 | 32, 1, 2 | mrexval 34159 |
. . . . . . . . . . . . 13
β’ (π β V β π
= Word ((mCNβπ) βͺ π)) |
43 | 42 | ad3antrrr 729 |
. . . . . . . . . . . 12
β’ ((((π β V β§ π β (π
βpm π)) β§ π₯ β π) β§ Β¬ π₯ β dom π) β π
= Word ((mCNβπ) βͺ π)) |
44 | 41, 43 | eleqtrrd 2837 |
. . . . . . . . . . 11
β’ ((((π β V β§ π β (π
βpm π)) β§ π₯ β π) β§ Β¬ π₯ β dom π) β β¨βπ₯ββ© β π
) |
45 | 38, 44 | ifclda 4525 |
. . . . . . . . . 10
β’ (((π β V β§ π β (π
βpm π)) β§ π₯ β π) β if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©) β π
) |
46 | 45 | fmpttd 7067 |
. . . . . . . . 9
β’ ((π β V β§ π β (π
βpm π)) β (π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)):πβΆπ
) |
47 | | ssid 3970 |
. . . . . . . . 9
β’ π β π |
48 | 32, 1, 2, 3, 33 | mrsubfval 34166 |
. . . . . . . . 9
β’ (((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)):πβΆπ
β§ π β π) β (πβ(π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))) = (π β π
β¦ ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©)) β π)))) |
49 | 46, 47, 48 | sylancl 587 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β (πβ(π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))) = (π β π
β¦ ((freeMndβ((mCNβπ) βͺ π)) Ξ£g ((π£ β ((mCNβπ) βͺ π) β¦ if(π£ β π, ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))βπ£), β¨βπ£ββ©)) β π)))) |
50 | 31, 35, 49 | 3eqtr4d 2783 |
. . . . . . 7
β’ ((π β V β§ π β (π
βpm π)) β (πβπ) = (πβ(π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)))) |
51 | 5 | adantr 482 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β π Fn (π
βpm π)) |
52 | | mapsspm 8820 |
. . . . . . . . 9
β’ (π
βm π) β (π
βpm π) |
53 | 52 | a1i 11 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β (π
βm π) β (π
βpm π)) |
54 | 2 | fvexi 6860 |
. . . . . . . . . 10
β’ π
β V |
55 | 1 | fvexi 6860 |
. . . . . . . . . 10
β’ π β V |
56 | 54, 55 | elmap 8815 |
. . . . . . . . 9
β’ ((π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)) β (π
βm π) β (π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)):πβΆπ
) |
57 | 46, 56 | sylibr 233 |
. . . . . . . 8
β’ ((π β V β§ π β (π
βpm π)) β (π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)) β (π
βm π)) |
58 | | fnfvima 7187 |
. . . . . . . 8
β’ ((π Fn (π
βpm π) β§ (π
βm π) β (π
βpm π) β§ (π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©)) β (π
βm π)) β (πβ(π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))) β (π β (π
βm π))) |
59 | 51, 53, 57, 58 | syl3anc 1372 |
. . . . . . 7
β’ ((π β V β§ π β (π
βpm π)) β (πβ(π₯ β π β¦ if(π₯ β dom π, (πβπ₯), β¨βπ₯ββ©))) β (π β (π
βm π))) |
60 | 50, 59 | eqeltrd 2834 |
. . . . . 6
β’ ((π β V β§ π β (π
βpm π)) β (πβπ) β (π β (π
βm π))) |
61 | 60 | ralrimiva 3140 |
. . . . 5
β’ (π β V β βπ β (π
βpm π)(πβπ) β (π β (π
βm π))) |
62 | | ffnfv 7070 |
. . . . 5
β’ (π:(π
βpm π)βΆ(π β (π
βm π)) β (π Fn (π
βpm π) β§ βπ β (π
βpm π)(πβπ) β (π β (π
βm π)))) |
63 | 5, 61, 62 | sylanbrc 584 |
. . . 4
β’ (π β V β π:(π
βpm π)βΆ(π β (π
βm π))) |
64 | 63 | frnd 6680 |
. . 3
β’ (π β V β ran π β (π β (π
βm π))) |
65 | 3 | rnfvprc 6840 |
. . . 4
β’ (Β¬
π β V β ran π = β
) |
66 | | 0ss 4360 |
. . . 4
β’ β
β (π β (π
βm π)) |
67 | 65, 66 | eqsstrdi 4002 |
. . 3
β’ (Β¬
π β V β ran π β (π β (π
βm π))) |
68 | 64, 67 | pm2.61i 182 |
. 2
β’ ran π β (π β (π
βm π)) |
69 | | imassrn 6028 |
. 2
β’ (π β (π
βm π)) β ran π |
70 | 68, 69 | eqssi 3964 |
1
β’ ran π = (π β (π
βm π)) |