Step | Hyp | Ref
| Expression |
1 | | iscn 13190 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (( I βΎ π) β (π½ Cn πΎ) β (( I βΎ π):πβΆπ β§ βπ₯ β πΎ (β‘(
I βΎ π) β π₯) β π½))) |
2 | | f1oi 5491 |
. . . . 5
β’ ( I
βΎ π):πβ1-1-ontoβπ |
3 | | f1of 5453 |
. . . . 5
β’ (( I
βΎ π):πβ1-1-ontoβπ β ( I βΎ π):πβΆπ) |
4 | 2, 3 | ax-mp 5 |
. . . 4
β’ ( I
βΎ π):πβΆπ |
5 | 4 | biantrur 303 |
. . 3
β’
(βπ₯ β
πΎ (β‘( I βΎ π) β π₯) β π½ β (( I βΎ π):πβΆπ β§ βπ₯ β πΎ (β‘(
I βΎ π) β π₯) β π½)) |
6 | 1, 5 | bitr4di 198 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (( I βΎ π) β (π½ Cn πΎ) β βπ₯ β πΎ (β‘(
I βΎ π) β π₯) β π½)) |
7 | | cnvresid 5282 |
. . . . . . 7
β’ β‘( I βΎ π) = ( I βΎ π) |
8 | 7 | imaeq1i 4960 |
. . . . . 6
β’ (β‘( I βΎ π) β π₯) = (( I βΎ π) β π₯) |
9 | | elssuni 3833 |
. . . . . . . . 9
β’ (π₯ β πΎ β π₯ β βͺ πΎ) |
10 | 9 | adantl 277 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β πΎ) β π₯ β βͺ πΎ) |
11 | | toponuni 13006 |
. . . . . . . . 9
β’ (πΎ β (TopOnβπ) β π = βͺ πΎ) |
12 | 11 | ad2antlr 489 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β πΎ) β π = βͺ πΎ) |
13 | 10, 12 | sseqtrrd 3192 |
. . . . . . 7
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β πΎ) β π₯ β π) |
14 | | resiima 4979 |
. . . . . . 7
β’ (π₯ β π β (( I βΎ π) β π₯) = π₯) |
15 | 13, 14 | syl 14 |
. . . . . 6
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β πΎ) β (( I βΎ π) β π₯) = π₯) |
16 | 8, 15 | eqtrid 2220 |
. . . . 5
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β πΎ) β (β‘( I βΎ π) β π₯) = π₯) |
17 | 16 | eleq1d 2244 |
. . . 4
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ π₯ β πΎ) β ((β‘( I βΎ π) β π₯) β π½ β π₯ β π½)) |
18 | 17 | ralbidva 2471 |
. . 3
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (βπ₯ β πΎ (β‘(
I βΎ π) β π₯) β π½ β βπ₯ β πΎ π₯ β π½)) |
19 | | dfss3 3143 |
. . 3
β’ (πΎ β π½ β βπ₯ β πΎ π₯ β π½) |
20 | 18, 19 | bitr4di 198 |
. 2
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (βπ₯ β πΎ (β‘(
I βΎ π) β π₯) β π½ β πΎ β π½)) |
21 | 6, 20 | bitrd 188 |
1
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (( I βΎ π) β (π½ Cn πΎ) β πΎ β π½)) |