| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpr 485 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β π½ β
2o) |
| 2 | | toponss 22428 |
. . . . . . . . . . . . . . . . . 18
β’ ((π½ β (TopOnβπ) β§ π₯ β π½) β π₯ β π) |
| 3 | 2 | ad2ant2rl 747 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π₯ β π) |
| 4 | | simprl 769 |
. . . . . . . . . . . . . . . . 17
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π = β
) |
| 5 | | sseq0 4399 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β π β§ π = β
) β π₯ = β
) |
| 6 | 3, 4, 5 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π₯ = β
) |
| 7 | | velsn 4644 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β {β
} β π₯ = β
) |
| 8 | 6, 7 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ (π = β
β§ π₯ β π½)) β π₯ β {β
}) |
| 9 | 8 | expr 457 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β (π₯ β π½ β π₯ β {β
})) |
| 10 | 9 | ssrdv 3988 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ β
{β
}) |
| 11 | | topontop 22414 |
. . . . . . . . . . . . . . . 16
β’ (π½ β (TopOnβπ) β π½ β Top) |
| 12 | | 0opn 22405 |
. . . . . . . . . . . . . . . 16
β’ (π½ β Top β β
β π½) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π½ β (TopOnβπ) β β
β π½) |
| 14 | 13 | ad2antrr 724 |
. . . . . . . . . . . . . 14
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β β
β π½) |
| 15 | 14 | snssd 4812 |
. . . . . . . . . . . . 13
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β {β
}
β π½) |
| 16 | 10, 15 | eqssd 3999 |
. . . . . . . . . . . 12
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ = {β
}) |
| 17 | | 0ex 5307 |
. . . . . . . . . . . . 13
β’ β
β V |
| 18 | 17 | ensn1 9016 |
. . . . . . . . . . . 12
β’ {β
}
β 1o |
| 19 | 16, 18 | eqbrtrdi 5187 |
. . . . . . . . . . 11
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ β
1o) |
| 20 | 19 | olcd 872 |
. . . . . . . . . 10
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β (π½ = β
β¨ π½ β
1o)) |
| 21 | | sdom2en01 10296 |
. . . . . . . . . 10
β’ (π½ βΊ 2o β
(π½ = β
β¨ π½ β
1o)) |
| 22 | 20, 21 | sylibr 233 |
. . . . . . . . 9
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β π½ βΊ
2o) |
| 23 | | sdomnen 8976 |
. . . . . . . . 9
β’ (π½ βΊ 2o β
Β¬ π½ β
2o) |
| 24 | 22, 23 | syl 17 |
. . . . . . . 8
β’ (((π½ β (TopOnβπ) β§ π½ β 2o) β§ π = β
) β Β¬ π½ β
2o) |
| 25 | 24 | ex 413 |
. . . . . . 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 481 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β β
β π½) |
| 30 | | toponmax 22427 |
. . . . . 6
β’ (π½ β (TopOnβπ) β π β π½) |
| 31 | 30 | adantr 481 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β π β π½) |
| 32 | | en2eqpr 10001 |
. . . . 5
β’ ((π½ β 2o β§
β
β π½ β§
π β π½) β (β
β π β π½ = {β
, π})) |
| 33 | 1, 29, 31, 32 | syl3anc 1371 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β (β
β
π β π½ = {β
, π})) |
| 34 | 28, 33 | mpd 15 |
. . 3
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β π½ = {β
, π}) |
| 35 | 34, 27 | jca 512 |
. 2
β’ ((π½ β (TopOnβπ) β§ π½ β 2o) β (π½ = {β
, π} β§ π β β
)) |
| 36 | | simprl 769 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β π½ = {β
, π}) |
| 37 | | simprr 771 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β π β β
) |
| 38 | 37 | necomd 2996 |
. . . 4
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β β
β π) |
| 39 | | enpr2 9996 |
. . . 4
β’ ((β
β V β§ π β
π½ β§ β
β π) β {β
, π} β
2o) |
| 40 | 17, 30, 38, 39 | mp3an2ani 1468 |
. . 3
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β {β
, π} β
2o) |
| 41 | 36, 40 | eqbrtrd 5170 |
. 2
β’ ((π½ β (TopOnβπ) β§ (π½ = {β
, π} β§ π β β
)) β π½ β 2o) |
| 42 | 35, 41 | impbida 799 |
1
β’ (π½ β (TopOnβπ) β (π½ β 2o β (π½ = {β
, π} β§ π β β
))) |
