Step | Hyp | Ref
| Expression |
1 | | bren 8896 |
. 2
β’ (π΄ β π΅ β βπ π:π΄β1-1-ontoβπ΅) |
2 | | f1of 6785 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β π:π΄βΆπ΅) |
3 | | f1odm 6789 |
. . . . . . . . . 10
β’ (π:π΄β1-1-ontoβπ΅ β dom π = π΄) |
4 | | vex 3448 |
. . . . . . . . . . 11
β’ π β V |
5 | 4 | dmex 7849 |
. . . . . . . . . 10
β’ dom π β V |
6 | 3, 5 | eqeltrrdi 2843 |
. . . . . . . . 9
β’ (π:π΄β1-1-ontoβπ΅ β π΄ β V) |
7 | | f1ofo 6792 |
. . . . . . . . 9
β’ (π:π΄β1-1-ontoβπ΅ β π:π΄βontoβπ΅) |
8 | | focdmex 7889 |
. . . . . . . . 9
β’ (π΄ β V β (π:π΄βontoβπ΅ β π΅ β V)) |
9 | 6, 7, 8 | sylc 65 |
. . . . . . . 8
β’ (π:π΄β1-1-ontoβπ΅ β π΅ β V) |
10 | 9, 6 | elmapd 8782 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β (π β (π΅ βm π΄) β π:π΄βΆπ΅)) |
11 | 2, 10 | mpbird 257 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β π β (π΅ βm π΄)) |
12 | | indistopon 22367 |
. . . . . . . 8
β’ (π΄ β V β {β
, π΄} β (TopOnβπ΄)) |
13 | 6, 12 | syl 17 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β {β
, π΄} β (TopOnβπ΄)) |
14 | | cnindis 22659 |
. . . . . . 7
β’
(({β
, π΄}
β (TopOnβπ΄)
β§ π΅ β V) β
({β
, π΄} Cn {β
,
π΅}) = (π΅ βm π΄)) |
15 | 13, 9, 14 | syl2anc 585 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β ({β
, π΄} Cn {β
, π΅}) = (π΅ βm π΄)) |
16 | 11, 15 | eleqtrrd 2837 |
. . . . 5
β’ (π:π΄β1-1-ontoβπ΅ β π β ({β
, π΄} Cn {β
, π΅})) |
17 | | f1ocnv 6797 |
. . . . . . . 8
β’ (π:π΄β1-1-ontoβπ΅ β β‘π:π΅β1-1-ontoβπ΄) |
18 | | f1of 6785 |
. . . . . . . 8
β’ (β‘π:π΅β1-1-ontoβπ΄ β β‘π:π΅βΆπ΄) |
19 | 17, 18 | syl 17 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β β‘π:π΅βΆπ΄) |
20 | 6, 9 | elmapd 8782 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β (β‘π β (π΄ βm π΅) β β‘π:π΅βΆπ΄)) |
21 | 19, 20 | mpbird 257 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β β‘π β (π΄ βm π΅)) |
22 | | indistopon 22367 |
. . . . . . . 8
β’ (π΅ β V β {β
, π΅} β (TopOnβπ΅)) |
23 | 9, 22 | syl 17 |
. . . . . . 7
β’ (π:π΄β1-1-ontoβπ΅ β {β
, π΅} β (TopOnβπ΅)) |
24 | | cnindis 22659 |
. . . . . . 7
β’
(({β
, π΅}
β (TopOnβπ΅)
β§ π΄ β V) β
({β
, π΅} Cn {β
,
π΄}) = (π΄ βm π΅)) |
25 | 23, 6, 24 | syl2anc 585 |
. . . . . 6
β’ (π:π΄β1-1-ontoβπ΅ β ({β
, π΅} Cn {β
, π΄}) = (π΄ βm π΅)) |
26 | 21, 25 | eleqtrrd 2837 |
. . . . 5
β’ (π:π΄β1-1-ontoβπ΅ β β‘π β ({β
, π΅} Cn {β
, π΄})) |
27 | | ishmeo 23126 |
. . . . 5
β’ (π β ({β
, π΄}Homeo{β
, π΅}) β (π β ({β
, π΄} Cn {β
, π΅}) β§ β‘π β ({β
, π΅} Cn {β
, π΄}))) |
28 | 16, 26, 27 | sylanbrc 584 |
. . . 4
β’ (π:π΄β1-1-ontoβπ΅ β π β ({β
, π΄}Homeo{β
, π΅})) |
29 | | hmphi 23144 |
. . . 4
β’ (π β ({β
, π΄}Homeo{β
, π΅}) β {β
, π΄} β {β
, π΅}) |
30 | 28, 29 | syl 17 |
. . 3
β’ (π:π΄β1-1-ontoβπ΅ β {β
, π΄} β {β
, π΅}) |
31 | 30 | exlimiv 1934 |
. 2
β’
(βπ π:π΄β1-1-ontoβπ΅ β {β
, π΄} β {β
, π΅}) |
32 | 1, 31 | sylbi 216 |
1
β’ (π΄ β π΅ β {β
, π΄} β {β
, π΅}) |