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		pr2nelem	⊢ ( ( ∅ ∈ V ∧ 𝑋 ∈ 𝐽 ∧ ∅ ≠ 𝑋 ) → { ∅ , 𝑋 } ≈ 2o )
40	17 30 38 39	mp3an2ani	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) → { ∅ , 𝑋 } ≈ 2o )
41	36 40	eqbrtrd	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) → 𝐽 ≈ 2o )
42	35 41	impbida	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ≈ 2o ↔ ( 𝐽 = { ∅ , 𝑋 } ∧ 𝑋 ≠ ∅ ) ) )