Step | Hyp | Ref
| Expression |
1 | | cmphaushmeo.1 |
. . 3
β’ π = βͺ
π½ |
2 | | cmphaushmeo.2 |
. . 3
β’ π = βͺ
πΎ |
3 | 1, 2 | hmeof1o 23268 |
. 2
β’ (πΉ β (π½HomeoπΎ) β πΉ:πβ1-1-ontoβπ) |
4 | | f1ocnv 6846 |
. . . . . . . 8
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
5 | | f1of 6834 |
. . . . . . . 8
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
6 | 4, 5 | syl 17 |
. . . . . . 7
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
7 | 6 | a1i 11 |
. . . . . 6
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ)) |
8 | | f1orel 6837 |
. . . . . . . . . . . 12
β’ (πΉ:πβ1-1-ontoβπ β Rel πΉ) |
9 | 8 | ad2antll 728 |
. . . . . . . . . . 11
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β Rel πΉ) |
10 | | dfrel2 6189 |
. . . . . . . . . . 11
β’ (Rel
πΉ β β‘β‘πΉ = πΉ) |
11 | 9, 10 | sylib 217 |
. . . . . . . . . 10
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β β‘β‘πΉ = πΉ) |
12 | 11 | imaeq1d 6059 |
. . . . . . . . 9
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β (β‘β‘πΉ β π₯) = (πΉ β π₯)) |
13 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΎ β Haus) |
14 | 13 | adantr 482 |
. . . . . . . . . 10
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β πΎ β Haus) |
15 | | imassrn 6071 |
. . . . . . . . . . 11
β’ (πΉ β π₯) β ran πΉ |
16 | | f1ofo 6841 |
. . . . . . . . . . . . 13
β’ (πΉ:πβ1-1-ontoβπ β πΉ:πβontoβπ) |
17 | 16 | ad2antll 728 |
. . . . . . . . . . . 12
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β πΉ:πβontoβπ) |
18 | | forn 6809 |
. . . . . . . . . . . 12
β’ (πΉ:πβontoβπ β ran πΉ = π) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β ran πΉ = π) |
20 | 15, 19 | sseqtrid 4035 |
. . . . . . . . . 10
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β (πΉ β π₯) β π) |
21 | | simpl3 1194 |
. . . . . . . . . . 11
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β πΉ β (π½ Cn πΎ)) |
22 | | simp1 1137 |
. . . . . . . . . . . . 13
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β π½ β Comp) |
23 | 22 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β π½ β Comp) |
24 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β π₯ β (Clsdβπ½)) |
25 | | cmpcld 22906 |
. . . . . . . . . . . 12
β’ ((π½ β Comp β§ π₯ β (Clsdβπ½)) β (π½ βΎt π₯) β Comp) |
26 | 23, 24, 25 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β (π½ βΎt π₯) β Comp) |
27 | | imacmp 22901 |
. . . . . . . . . . 11
β’ ((πΉ β (π½ Cn πΎ) β§ (π½ βΎt π₯) β Comp) β (πΎ βΎt (πΉ β π₯)) β Comp) |
28 | 21, 26, 27 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β (πΎ βΎt (πΉ β π₯)) β Comp) |
29 | 2 | hauscmp 22911 |
. . . . . . . . . 10
β’ ((πΎ β Haus β§ (πΉ β π₯) β π β§ (πΎ βΎt (πΉ β π₯)) β Comp) β (πΉ β π₯) β (ClsdβπΎ)) |
30 | 14, 20, 28, 29 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β (πΉ β π₯) β (ClsdβπΎ)) |
31 | 12, 30 | eqeltrd 2834 |
. . . . . . . 8
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ (π₯ β (Clsdβπ½) β§ πΉ:πβ1-1-ontoβπ)) β (β‘β‘πΉ β π₯) β (ClsdβπΎ)) |
32 | 31 | expr 458 |
. . . . . . 7
β’ (((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β§ π₯ β (Clsdβπ½)) β (πΉ:πβ1-1-ontoβπ β (β‘β‘πΉ β π₯) β (ClsdβπΎ))) |
33 | 32 | ralrimdva 3155 |
. . . . . 6
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβ1-1-ontoβπ β βπ₯ β (Clsdβπ½)(β‘β‘πΉ β π₯) β (ClsdβπΎ))) |
34 | 7, 33 | jcad 514 |
. . . . 5
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβ1-1-ontoβπ β (β‘πΉ:πβΆπ β§ βπ₯ β (Clsdβπ½)(β‘β‘πΉ β π₯) β (ClsdβπΎ)))) |
35 | | haustop 22835 |
. . . . . . . 8
β’ (πΎ β Haus β πΎ β Top) |
36 | 13, 35 | syl 17 |
. . . . . . 7
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΎ β Top) |
37 | 2 | toptopon 22419 |
. . . . . . 7
β’ (πΎ β Top β πΎ β (TopOnβπ)) |
38 | 36, 37 | sylib 217 |
. . . . . 6
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΎ β (TopOnβπ)) |
39 | | cmptop 22899 |
. . . . . . . 8
β’ (π½ β Comp β π½ β Top) |
40 | 22, 39 | syl 17 |
. . . . . . 7
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β π½ β Top) |
41 | 1 | toptopon 22419 |
. . . . . . 7
β’ (π½ β Top β π½ β (TopOnβπ)) |
42 | 40, 41 | sylib 217 |
. . . . . 6
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β π½ β (TopOnβπ)) |
43 | | iscncl 22773 |
. . . . . 6
β’ ((πΎ β (TopOnβπ) β§ π½ β (TopOnβπ)) β (β‘πΉ β (πΎ Cn π½) β (β‘πΉ:πβΆπ β§ βπ₯ β (Clsdβπ½)(β‘β‘πΉ β π₯) β (ClsdβπΎ)))) |
44 | 38, 42, 43 | syl2anc 585 |
. . . . 5
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (β‘πΉ β (πΎ Cn π½) β (β‘πΉ:πβΆπ β§ βπ₯ β (Clsdβπ½)(β‘β‘πΉ β π₯) β (ClsdβπΎ)))) |
45 | 34, 44 | sylibrd 259 |
. . . 4
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβ1-1-ontoβπ β β‘πΉ β (πΎ Cn π½))) |
46 | | simp3 1139 |
. . . 4
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β πΉ β (π½ Cn πΎ)) |
47 | 45, 46 | jctild 527 |
. . 3
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβ1-1-ontoβπ β (πΉ β (π½ Cn πΎ) β§ β‘πΉ β (πΎ Cn π½)))) |
48 | | ishmeo 23263 |
. . 3
β’ (πΉ β (π½HomeoπΎ) β (πΉ β (π½ Cn πΎ) β§ β‘πΉ β (πΎ Cn π½))) |
49 | 47, 48 | syl6ibr 252 |
. 2
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ:πβ1-1-ontoβπ β πΉ β (π½HomeoπΎ))) |
50 | 3, 49 | impbid2 225 |
1
β’ ((π½ β Comp β§ πΎ β Haus β§ πΉ β (π½ Cn πΎ)) β (πΉ β (π½HomeoπΎ) β πΉ:πβ1-1-ontoβπ)) |