| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. . . . . 6
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) → 𝐽 ≈
2o) |
| 2 | | toponss 22933 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽) → 𝑥 ⊆ 𝑋) |
| 3 | 2 | ad2ant2rl 749 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ (𝑋 = ∅ ∧ 𝑥 ∈ 𝐽)) → 𝑥 ⊆ 𝑋) |
| 4 | | simprl 771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ (𝑋 = ∅ ∧ 𝑥 ∈ 𝐽)) → 𝑋 = ∅) |
| 5 | | sseq0 4403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑋 = ∅) → 𝑥 = ∅) |
| 6 | 3, 4, 5 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ (𝑋 = ∅ ∧ 𝑥 ∈ 𝐽)) → 𝑥 = ∅) |
| 7 | | velsn 4642 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ {∅} ↔ 𝑥 = ∅) |
| 8 | 6, 7 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ (𝑋 = ∅ ∧ 𝑥 ∈ 𝐽)) → 𝑥 ∈ {∅}) |
| 9 | 8 | expr 456 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → (𝑥 ∈ 𝐽 → 𝑥 ∈ {∅})) |
| 10 | 9 | ssrdv 3989 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → 𝐽 ⊆
{∅}) |
| 11 | | topontop 22919 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
| 12 | | 0opn 22910 |
. . . . . . . . . . . . . . . 16
⊢ (𝐽 ∈ Top → ∅
∈ 𝐽) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐽 ∈ (TopOn‘𝑋) → ∅ ∈ 𝐽) |
| 14 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → ∅
∈ 𝐽) |
| 15 | 14 | snssd 4809 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → {∅}
⊆ 𝐽) |
| 16 | 10, 15 | eqssd 4001 |
. . . . . . . . . . . 12
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → 𝐽 = {∅}) |
| 17 | | 0ex 5307 |
. . . . . . . . . . . . 13
⊢ ∅
∈ V |
| 18 | 17 | ensn1 9061 |
. . . . . . . . . . . 12
⊢ {∅}
≈ 1o |
| 19 | 16, 18 | eqbrtrdi 5182 |
. . . . . . . . . . 11
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → 𝐽 ≈
1o) |
| 20 | 19 | olcd 875 |
. . . . . . . . . 10
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → (𝐽 = ∅ ∨ 𝐽 ≈
1o)) |
| 21 | | sdom2en01 10342 |
. . . . . . . . . 10
⊢ (𝐽 ≺ 2o ↔
(𝐽 = ∅ ∨ 𝐽 ≈
1o)) |
| 22 | 20, 21 | sylibr 234 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → 𝐽 ≺
2o) |
| 23 | | sdomnen 9021 |
. . . . . . . . 9
⊢ (𝐽 ≺ 2o →
¬ 𝐽 ≈
2o) |
| 24 | 22, 23 | syl 17 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) ∧ 𝑋 = ∅) → ¬ 𝐽 ≈
2o) |
| 25 | 24 | ex 412 |
. . . . . . 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 480 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) → ∅
∈ 𝐽) |
| 30 | | toponmax 22932 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
| 31 | 30 | adantr 480 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) → 𝑋 ∈ 𝐽) |
| 32 | | en2eqpr 10047 |
. . . . 5
⊢ ((𝐽 ≈ 2o ∧
∅ ∈ 𝐽 ∧
𝑋 ∈ 𝐽) → (∅ ≠ 𝑋 → 𝐽 = {∅, 𝑋})) |
| 33 | 1, 29, 31, 32 | syl3anc 1373 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) → (∅ ≠
𝑋 → 𝐽 = {∅, 𝑋})) |
| 34 | 28, 33 | mpd 15 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) → 𝐽 = {∅, 𝑋}) |
| 35 | 34, 27 | jca 511 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐽 ≈ 2o) → (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) |
| 36 | | simprl 771 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) → 𝐽 = {∅, 𝑋}) |
| 37 | | simprr 773 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) → 𝑋 ≠ ∅) |
| 38 | 37 | necomd 2996 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) → ∅ ≠ 𝑋) |
| 39 | | enpr2 10042 |
. . . 4
⊢ ((∅
∈ V ∧ 𝑋 ∈
𝐽 ∧ ∅ ≠ 𝑋) → {∅, 𝑋} ≈
2o) |
| 40 | 17, 30, 38, 39 | mp3an2ani 1470 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) → {∅, 𝑋} ≈
2o) |
| 41 | 36, 40 | eqbrtrd 5165 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅)) → 𝐽 ≈ 2o) |
| 42 | 35, 41 | impbida 801 |
1
⊢ (𝐽 ∈ (TopOn‘𝑋) → (𝐽 ≈ 2o ↔ (𝐽 = {∅, 𝑋} ∧ 𝑋 ≠ ∅))) |