Step | Hyp | Ref
| Expression |
1 | | n0i 4297 |
. . . . 5
β’ (πΉ β ran π β Β¬ ran π = β
) |
2 | | mrsubccat.s |
. . . . . 6
β’ π = (mRSubstβπ) |
3 | 2 | rnfvprc 6840 |
. . . . 5
β’ (Β¬
π β V β ran π = β
) |
4 | 1, 3 | nsyl2 141 |
. . . 4
β’ (πΉ β ran π β π β V) |
5 | | mrsubcn.v |
. . . . 5
β’ π = (mVRβπ) |
6 | | mrsubccat.r |
. . . . 5
β’ π
= (mRExβπ) |
7 | 5, 6, 2 | mrsubff 34170 |
. . . 4
β’ (π β V β π:(π
βpm π)βΆ(π
βm π
)) |
8 | | ffun 6675 |
. . . 4
β’ (π:(π
βpm π)βΆ(π
βm π
) β Fun π) |
9 | 4, 7, 8 | 3syl 18 |
. . 3
β’ (πΉ β ran π β Fun π) |
10 | 5, 6, 2 | mrsubrn 34171 |
. . . . 5
β’ ran π = (π β (π
βm π)) |
11 | 10 | eleq2i 2826 |
. . . 4
β’ (πΉ β ran π β πΉ β (π β (π
βm π))) |
12 | 11 | biimpi 215 |
. . 3
β’ (πΉ β ran π β πΉ β (π β (π
βm π))) |
13 | | fvelima 6912 |
. . 3
β’ ((Fun
π β§ πΉ β (π β (π
βm π))) β βπ β (π
βm π)(πβπ) = πΉ) |
14 | 9, 12, 13 | syl2anc 585 |
. 2
β’ (πΉ β ran π β βπ β (π
βm π)(πβπ) = πΉ) |
15 | | elmapi 8793 |
. . . . . . 7
β’ (π β (π
βm π) β π:πβΆπ
) |
16 | 15 | adantl 483 |
. . . . . 6
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β π:πβΆπ
) |
17 | | ssidd 3971 |
. . . . . 6
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β π β π) |
18 | | eldifi 4090 |
. . . . . . . 8
β’ (π β (πΆ β π) β π β πΆ) |
19 | | elun1 4140 |
. . . . . . . 8
β’ (π β πΆ β π β (πΆ βͺ π)) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (π β (πΆ β π) β π β (πΆ βͺ π)) |
21 | 20 | adantr 482 |
. . . . . 6
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β π β (πΆ βͺ π)) |
22 | | mrsubcn.c |
. . . . . . 7
β’ πΆ = (mCNβπ) |
23 | 22, 5, 6, 2 | mrsubcv 34168 |
. . . . . 6
β’ ((π:πβΆπ
β§ π β π β§ π β (πΆ βͺ π)) β ((πβπ)ββ¨βπββ©) = if(π β π, (πβπ), β¨βπββ©)) |
24 | 16, 17, 21, 23 | syl3anc 1372 |
. . . . 5
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β ((πβπ)ββ¨βπββ©) = if(π β π, (πβπ), β¨βπββ©)) |
25 | | eldifn 4091 |
. . . . . . 7
β’ (π β (πΆ β π) β Β¬ π β π) |
26 | 25 | adantr 482 |
. . . . . 6
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β Β¬ π β π) |
27 | 26 | iffalsed 4501 |
. . . . 5
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β if(π β π, (πβπ), β¨βπββ©) = β¨βπββ©) |
28 | 24, 27 | eqtrd 2773 |
. . . 4
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β ((πβπ)ββ¨βπββ©) = β¨βπββ©) |
29 | | fveq1 6845 |
. . . . 5
β’ ((πβπ) = πΉ β ((πβπ)ββ¨βπββ©) = (πΉββ¨βπββ©)) |
30 | 29 | eqeq1d 2735 |
. . . 4
β’ ((πβπ) = πΉ β (((πβπ)ββ¨βπββ©) = β¨βπββ© β (πΉββ¨βπββ©) =
β¨βπββ©)) |
31 | 28, 30 | syl5ibcom 244 |
. . 3
β’ ((π β (πΆ β π) β§ π β (π
βm π)) β ((πβπ) = πΉ β (πΉββ¨βπββ©) = β¨βπββ©)) |
32 | 31 | rexlimdva 3149 |
. 2
β’ (π β (πΆ β π) β (βπ β (π
βm π)(πβπ) = πΉ β (πΉββ¨βπββ©) = β¨βπββ©)) |
33 | 14, 32 | mpan9 508 |
1
β’ ((πΉ β ran π β§ π β (πΆ β π)) β (πΉββ¨βπββ©) = β¨βπββ©) |