Step | Hyp | Ref
| Expression |
1 | | ismtyval 36305 |
. . 3
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (π Ismty π) = {π β£ (π:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πβπ₯)π(πβπ¦)))}) |
2 | 1 | eleq2d 2820 |
. 2
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β πΉ β {π β£ (π:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πβπ₯)π(πβπ¦)))})) |
3 | | f1of 6785 |
. . . . . . 7
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβΆπ) |
4 | 3 | adantr 482 |
. . . . . 6
β’ ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β πΉ:πβΆπ) |
5 | | elfvdm 6880 |
. . . . . 6
β’ (π β (βMetβπ) β π β dom βMet) |
6 | | elfvdm 6880 |
. . . . . 6
β’ (π β (βMetβπ) β π β dom βMet) |
7 | | fex2 7871 |
. . . . . 6
β’ ((πΉ:πβΆπ β§ π β dom βMet β§ π β dom βMet) β
πΉ β
V) |
8 | 4, 5, 6, 7 | syl3an 1161 |
. . . . 5
β’ (((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β§ π β (βMetβπ) β§ π β (βMetβπ)) β πΉ β V) |
9 | 8 | 3expib 1123 |
. . . 4
β’ ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β ((π β (βMetβπ) β§ π β (βMetβπ)) β πΉ β V)) |
10 | 9 | com12 32 |
. . 3
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β ((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β πΉ β V)) |
11 | | f1oeq1 6773 |
. . . . 5
β’ (π = πΉ β (π:πβ1-1-ontoβπ β πΉ:πβ1-1-ontoβπ)) |
12 | | fveq1 6842 |
. . . . . . . 8
β’ (π = πΉ β (πβπ₯) = (πΉβπ₯)) |
13 | | fveq1 6842 |
. . . . . . . 8
β’ (π = πΉ β (πβπ¦) = (πΉβπ¦)) |
14 | 12, 13 | oveq12d 7376 |
. . . . . . 7
β’ (π = πΉ β ((πβπ₯)π(πβπ¦)) = ((πΉβπ₯)π(πΉβπ¦))) |
15 | 14 | eqeq2d 2744 |
. . . . . 6
β’ (π = πΉ β ((π₯ππ¦) = ((πβπ₯)π(πβπ¦)) β (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) |
16 | 15 | 2ralbidv 3209 |
. . . . 5
β’ (π = πΉ β (βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πβπ₯)π(πβπ¦)) β βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦)))) |
17 | 11, 16 | anbi12d 632 |
. . . 4
β’ (π = πΉ β ((π:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πβπ₯)π(πβπ¦))) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
18 | 17 | elab3g 3638 |
. . 3
β’ (((πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))) β πΉ β V) β (πΉ β {π β£ (π:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πβπ₯)π(πβπ¦)))} β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
19 | 10, 18 | syl 17 |
. 2
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β {π β£ (π:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πβπ₯)π(πβπ¦)))} β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |
20 | 2, 19 | bitrd 279 |
1
β’ ((π β (βMetβπ) β§ π β (βMetβπ)) β (πΉ β (π Ismty π) β (πΉ:πβ1-1-ontoβπ β§ βπ₯ β π βπ¦ β π (π₯ππ¦) = ((πΉβπ₯)π(πΉβπ¦))))) |