Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β π½ β
2o) |
2 | | toponss 22292 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β (TopOnβπ) β§ π₯ β π½) β π₯ β π) |
3 | 2 | ad2ant2rl 748 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π₯ β π) |
4 | | simprl 770 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π = β
) |
5 | | sseq0 4360 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β§ π = β
) β π₯ = β
) |
6 | 3, 4, 5 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π₯ = β
) |
7 | | velsn 4603 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β {β
} β π₯ = β
) |
8 | 6, 7 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π₯ β {β
}) |
9 | 8 | expr 458 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β (π₯ β π½ β π₯ β {β
})) |
10 | 9 | ssrdv 3951 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ β
{β
}) |
11 | | topontop 22278 |
. . . . . . . . . . . . . . . 16
β’ (π½ β (TopOnβπ) β π½ β Top) |
12 | | 0opn 22269 |
. . . . . . . . . . . . . . . 16
β’ (π½ β Top β β
β π½) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π½ β (TopOnβπ) β β
β π½) |
14 | 13 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β β
β π½) |
15 | 14 | snssd 4770 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β {β
}
β π½) |
16 | 10, 15 | eqssd 3962 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ = {β
}) |
17 | | 0ex 5265 |
. . . . . . . . . . . . 13
β’ β
β V |
18 | 17 | ensn1 8964 |
. . . . . . . . . . . 12
β’ {β
}
β 1o |
19 | 16, 18 | eqbrtrdi 5145 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ β
1o) |
20 | 19 | olcd 873 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β (π½ = β
β¨ π½ β
1o)) |
21 | | sdom2en01 10243 |
. . . . . . . . . 10
β’ (π½ βΊ 2o β
(π½ = β
β¨ π½ β
1o)) |
22 | 20, 21 | sylibr 233 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ βΊ
2o) |
23 | | sdomnen 8924 |
. . . . . . . . 9
β’ (π½ βΊ 2o β
Β¬ π½ β
2o) |
24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β Β¬ π½ β
2o) |
25 | 24 | ex 414 |
. . . . . . 7
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β (π = β
β Β¬ π½ β
2o)) |
26 | 25 | necon2ad 2955 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β (π½ β 2o β
π β
β
)) |
27 | 1, 26 | mpd 15 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β π β β
) |
28 | 27 | necomd 2996 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β β
β
π) |
29 | 13 | adantr 482 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β β
β π½) |
30 | | toponmax 22291 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π β π½) |
31 | 30 | adantr 482 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β π β π½) |
32 | | en2eqpr 9948 |
. . . . 5
β’ ((π½ β 2o β§
β
β π½ β§
π β π½) β (β
β π β π½ = {β
, π})) |
33 | 1, 29, 31, 32 | syl3anc 1372 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β (β
β
π β π½ = {β
, π})) |
34 | 28, 33 | mpd 15 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β π½ = {β
, π}) |
35 | 34, 27 | jca 513 |
. 2
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β (π½ = {β
, π} β§ π β β
)) |
36 | | simprl 770 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β π½ = {β
, π}) |
37 | | simprr 772 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β π β β
) |
38 | 37 | necomd 2996 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β β
β π) |
39 | | enpr2 9943 |
. . . 4
β’ ((β
β V β§ π β
π½ β§ β
β π) β {β
, π} β
2o) |
40 | 17, 30, 38, 39 | mp3an2ani 1469 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β {β
, π} β
2o) |
41 | 36, 40 | eqbrtrd 5128 |
. 2
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β π½ β 2o) |
42 | 35, 41 | impbida 800 |
1
β’ (π½ β (TopOnβπ) β (π½ β 2o β (π½ = {β
, π} β§ π β β
))) |