This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem en2top

Description: If a topology has two elements, it is the indiscrete topology. (Contributed by FL, 11-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion en2top ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ≈ 2o ↔ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → 𝐽 ≈ 2o )
2 toponss ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 )
3 2 ad2ant2rl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ ( 𝑋 = ∅ ∧ 𝑥 ∈ 𝐽 ) ) → 𝑥 ⊆ 𝑋 )
4 simprl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ ( 𝑋 = ∅ ∧ 𝑥 ∈ 𝐽 ) ) → 𝑋 = ∅ )
5 sseq0 ⊢ ( ( 𝑥 ⊆ 𝑋 ∧ 𝑋 = ∅ ) → 𝑥 = ∅ )
6 3 4 5 syl2anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ ( 𝑋 = ∅ ∧ 𝑥 ∈ 𝐽 ) ) → 𝑥 = ∅ )
7 velsn ⊢ ( 𝑥 ∈ { ∅ } ↔ 𝑥 = ∅ )
8 6 7 sylibr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ ( 𝑋 = ∅ ∧ 𝑥 ∈ 𝐽 ) ) → 𝑥 ∈ { ∅ } )
9 8 expr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → ( 𝑥 ∈ 𝐽 → 𝑥 ∈ { ∅ } ) )
10 9 ssrdv ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → 𝐽 ⊆ { ∅ } )
11 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
12 0opn ⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
13 11 12 syl ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ∅ ∈ 𝐽 )
14 13 ad2antrr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → ∅ ∈ 𝐽 )
15 14 snssd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → { ∅ } ⊆ 𝐽 )
16 10 15 eqssd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → 𝐽 = { ∅ } )
17 0ex ⊢ ∅ ∈ V
18 17 ensn1 ⊢ { ∅ } ≈ 1o
19 16 18 eqbrtrdi ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → 𝐽 ≈ 1o )
20 19 olcd ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → ( 𝐽 = ∅ ∨ 𝐽 ≈ 1o ) )
21 sdom2en01 ⊢ ( 𝐽 ≺ 2o ↔ ( 𝐽 = ∅ ∨ 𝐽 ≈ 1o ) )
22 20 21 sylibr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → 𝐽 ≺ 2o )
23 sdomnen ⊢ ( 𝐽 ≺ 2o → ¬ 𝐽 ≈ 2o )
24 22 23 syl ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) ∧ 𝑋 = ∅ ) → ¬ 𝐽 ≈ 2o )
25 24 ex ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → ( 𝑋 = ∅ → ¬ 𝐽 ≈ 2o ) )
26 25 necon2ad ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → ( 𝐽 ≈ 2o → 𝑋 ≠ ∅ ) )
27 1 26 mpd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → 𝑋 ≠ ∅ )
28 27 necomd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → ∅ ≠ 𝑋 )
29 13 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → ∅ ∈ 𝐽 )
30 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
31 30 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → 𝑋 ∈ 𝐽 )
32 en2eqpr ⊢ ( ( 𝐽 ≈ 2o ∧ ∅ ∈ 𝐽 ∧ 𝑋 ∈ 𝐽 ) → ( ∅ ≠ 𝑋 → 𝐽 = { ∅ , 𝑋 } ) )
33 1 29 31 32 syl3anc ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → ( ∅ ≠ 𝑋 → 𝐽 = { ∅ , 𝑋 } ) )
34 28 33 mpd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → 𝐽 = { ∅ , 𝑋 } )
35 34 27 jca ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐽 ≈ 2o ) → ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) )
36 simprl ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) → 𝐽 = { ∅ , 𝑋 } )
37 simprr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) → 𝑋 ≠ ∅ )
38 37 necomd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) → ∅ ≠ 𝑋 )
39 enpr2 ⊢ ( ( ∅ ∈ V ∧ 𝑋 ∈ 𝐽 ∧ ∅ ≠ 𝑋 ) → { ∅ , 𝑋 } ≈ 2o )
40 17 30 38 39 mp3an2ani ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) → { ∅ , 𝑋 } ≈ 2o )
41 36 40 eqbrtrd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) → 𝐽 ≈ 2o )
42 35 41 impbida ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ≈ 2o ↔ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) )