Step | Hyp | Ref
| Expression |
1 | | mrsubvr.v |
. . . 4
β’ π = (mVRβπ) |
2 | | mrsubvr.r |
. . . 4
β’ π
= (mRExβπ) |
3 | | mrsubvr.s |
. . . 4
β’ π = (mRSubstβπ) |
4 | 1, 2, 3 | mrsubff 34170 |
. . 3
β’ (π β π β π:(π
βpm π)βΆ(π
βm π
)) |
5 | | mapsspm 8820 |
. . . 4
β’ (π
βm π) β (π
βpm π) |
6 | 5 | a1i 11 |
. . 3
β’ (π β π β (π
βm π) β (π
βpm π)) |
7 | 4, 6 | fssresd 6713 |
. 2
β’ (π β π β (π βΎ (π
βm π)):(π
βm π)βΆ(π
βm π
)) |
8 | | fveq1 6845 |
. . . . . 6
β’ ((πβπ) = (πβπ) β ((πβπ)ββ¨βπ£ββ©) = ((πβπ)ββ¨βπ£ββ©)) |
9 | | simplrl 776 |
. . . . . . . . 9
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β π β (π
βm π)) |
10 | | elmapi 8793 |
. . . . . . . . 9
β’ (π β (π
βm π) β π:πβΆπ
) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β π:πβΆπ
) |
12 | | ssidd 3971 |
. . . . . . . 8
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β π β π) |
13 | | simpr 486 |
. . . . . . . 8
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β π£ β π) |
14 | 1, 2, 3 | mrsubvr 34169 |
. . . . . . . 8
β’ ((π:πβΆπ
β§ π β π β§ π£ β π) β ((πβπ)ββ¨βπ£ββ©) = (πβπ£)) |
15 | 11, 12, 13, 14 | syl3anc 1372 |
. . . . . . 7
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β ((πβπ)ββ¨βπ£ββ©) = (πβπ£)) |
16 | | simplrr 777 |
. . . . . . . . 9
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β π β (π
βm π)) |
17 | | elmapi 8793 |
. . . . . . . . 9
β’ (π β (π
βm π) β π:πβΆπ
) |
18 | 16, 17 | syl 17 |
. . . . . . . 8
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β π:πβΆπ
) |
19 | 1, 2, 3 | mrsubvr 34169 |
. . . . . . . 8
β’ ((π:πβΆπ
β§ π β π β§ π£ β π) β ((πβπ)ββ¨βπ£ββ©) = (πβπ£)) |
20 | 18, 12, 13, 19 | syl3anc 1372 |
. . . . . . 7
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β ((πβπ)ββ¨βπ£ββ©) = (πβπ£)) |
21 | 15, 20 | eqeq12d 2749 |
. . . . . 6
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β (((πβπ)ββ¨βπ£ββ©) = ((πβπ)ββ¨βπ£ββ©) β (πβπ£) = (πβπ£))) |
22 | 8, 21 | imbitrid 243 |
. . . . 5
β’ (((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β§ π£ β π) β ((πβπ) = (πβπ) β (πβπ£) = (πβπ£))) |
23 | 22 | ralrimdva 3148 |
. . . 4
β’ ((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β ((πβπ) = (πβπ) β βπ£ β π (πβπ£) = (πβπ£))) |
24 | | fvres 6865 |
. . . . . 6
β’ (π β (π
βm π) β ((π βΎ (π
βm π))βπ) = (πβπ)) |
25 | | fvres 6865 |
. . . . . 6
β’ (π β (π
βm π) β ((π βΎ (π
βm π))βπ) = (πβπ)) |
26 | 24, 25 | eqeqan12d 2747 |
. . . . 5
β’ ((π β (π
βm π) β§ π β (π
βm π)) β (((π βΎ (π
βm π))βπ) = ((π βΎ (π
βm π))βπ) β (πβπ) = (πβπ))) |
27 | 26 | adantl 483 |
. . . 4
β’ ((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β (((π βΎ (π
βm π))βπ) = ((π βΎ (π
βm π))βπ) β (πβπ) = (πβπ))) |
28 | | ffn 6672 |
. . . . . . 7
β’ (π:πβΆπ
β π Fn π) |
29 | | ffn 6672 |
. . . . . . 7
β’ (π:πβΆπ
β π Fn π) |
30 | | eqfnfv 6986 |
. . . . . . 7
β’ ((π Fn π β§ π Fn π) β (π = π β βπ£ β π (πβπ£) = (πβπ£))) |
31 | 28, 29, 30 | syl2an 597 |
. . . . . 6
β’ ((π:πβΆπ
β§ π:πβΆπ
) β (π = π β βπ£ β π (πβπ£) = (πβπ£))) |
32 | 10, 17, 31 | syl2an 597 |
. . . . 5
β’ ((π β (π
βm π) β§ π β (π
βm π)) β (π = π β βπ£ β π (πβπ£) = (πβπ£))) |
33 | 32 | adantl 483 |
. . . 4
β’ ((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β (π = π β βπ£ β π (πβπ£) = (πβπ£))) |
34 | 23, 27, 33 | 3imtr4d 294 |
. . 3
β’ ((π β π β§ (π β (π
βm π) β§ π β (π
βm π))) β (((π βΎ (π
βm π))βπ) = ((π βΎ (π
βm π))βπ) β π = π)) |
35 | 34 | ralrimivva 3194 |
. 2
β’ (π β π β βπ β (π
βm π)βπ β (π
βm π)(((π βΎ (π
βm π))βπ) = ((π βΎ (π
βm π))βπ) β π = π)) |
36 | | dff13 7206 |
. 2
β’ ((π βΎ (π
βm π)):(π
βm π)β1-1β(π
βm π
) β ((π βΎ (π
βm π)):(π
βm π)βΆ(π
βm π
) β§ βπ β (π
βm π)βπ β (π
βm π)(((π βΎ (π
βm π))βπ) = ((π βΎ (π
βm π))βπ) β π = π))) |
37 | 7, 35, 36 | sylanbrc 584 |
1
β’ (π β π β (π βΎ (π
βm π)):(π
βm π)β1-1β(π
βm π
)) |