Step | Hyp | Ref
| Expression |
1 | | pwuni 4950 |
. . . 4
β’ π½ β π« βͺ π½ |
2 | | hmphdis.1 |
. . . . 5
β’ π = βͺ
π½ |
3 | 2 | pweqi 4619 |
. . . 4
β’ π«
π = π« βͺ π½ |
4 | 1, 3 | sseqtrri 4020 |
. . 3
β’ π½ β π« π |
5 | 4 | a1i 11 |
. 2
β’ (π½ β π« π΄ β π½ β π« π) |
6 | | hmph 23280 |
. . 3
β’ (π½ β π« π΄ β (π½Homeoπ« π΄) β β
) |
7 | | n0 4347 |
. . . 4
β’ ((π½Homeoπ« π΄) β β
β βπ π β (π½Homeoπ« π΄)) |
8 | | elpwi 4610 |
. . . . . . 7
β’ (π₯ β π« π β π₯ β π) |
9 | | imassrn 6071 |
. . . . . . . . . . 11
β’ (π β π₯) β ran π |
10 | | unipw 5451 |
. . . . . . . . . . . . . . 15
β’ βͺ π« π΄ = π΄ |
11 | 10 | eqcomi 2742 |
. . . . . . . . . . . . . 14
β’ π΄ = βͺ
π« π΄ |
12 | 2, 11 | hmeof1o 23268 |
. . . . . . . . . . . . 13
β’ (π β (π½Homeoπ« π΄) β π:πβ1-1-ontoβπ΄) |
13 | | f1of 6834 |
. . . . . . . . . . . . 13
β’ (π:πβ1-1-ontoβπ΄ β π:πβΆπ΄) |
14 | | frn 6725 |
. . . . . . . . . . . . 13
β’ (π:πβΆπ΄ β ran π β π΄) |
15 | 12, 13, 14 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β (π½Homeoπ« π΄) β ran π β π΄) |
16 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β (π½Homeoπ« π΄) β§ π₯ β π) β ran π β π΄) |
17 | 9, 16 | sstrid 3994 |
. . . . . . . . . 10
β’ ((π β (π½Homeoπ« π΄) β§ π₯ β π) β (π β π₯) β π΄) |
18 | | vex 3479 |
. . . . . . . . . . . 12
β’ π β V |
19 | 18 | imaex 7907 |
. . . . . . . . . . 11
β’ (π β π₯) β V |
20 | 19 | elpw 4607 |
. . . . . . . . . 10
β’ ((π β π₯) β π« π΄ β (π β π₯) β π΄) |
21 | 17, 20 | sylibr 233 |
. . . . . . . . 9
β’ ((π β (π½Homeoπ« π΄) β§ π₯ β π) β (π β π₯) β π« π΄) |
22 | 2 | hmeoopn 23270 |
. . . . . . . . 9
β’ ((π β (π½Homeoπ« π΄) β§ π₯ β π) β (π₯ β π½ β (π β π₯) β π« π΄)) |
23 | 21, 22 | mpbird 257 |
. . . . . . . 8
β’ ((π β (π½Homeoπ« π΄) β§ π₯ β π) β π₯ β π½) |
24 | 23 | ex 414 |
. . . . . . 7
β’ (π β (π½Homeoπ« π΄) β (π₯ β π β π₯ β π½)) |
25 | 8, 24 | syl5 34 |
. . . . . 6
β’ (π β (π½Homeoπ« π΄) β (π₯ β π« π β π₯ β π½)) |
26 | 25 | ssrdv 3989 |
. . . . 5
β’ (π β (π½Homeoπ« π΄) β π« π β π½) |
27 | 26 | exlimiv 1934 |
. . . 4
β’
(βπ π β (π½Homeoπ« π΄) β π« π β π½) |
28 | 7, 27 | sylbi 216 |
. . 3
β’ ((π½Homeoπ« π΄) β β
β π« π β π½) |
29 | 6, 28 | sylbi 216 |
. 2
β’ (π½ β π« π΄ β π« π β π½) |
30 | 5, 29 | eqssd 4000 |
1
β’ (π½ β π« π΄ β π½ = π« π) |