Theorem 0top

Description: The singleton of the empty set is the only topology possible for an empty underlying set. (Contributed by NM, 9-Sep-2006)

	Ref	Expression
Assertion	0top	⊢ ( 𝐽 ∈ Top → ( ∪ 𝐽 = ∅ ↔ 𝐽 = { ∅ } ) )

Proof

Step	Hyp	Ref	Expression
1		olc	⊢ ( 𝐽 = { ∅ } → ( 𝐽 = ∅ ∨ 𝐽 = { ∅ } ) )
2		0opn	⊢ ( 𝐽 ∈ Top → ∅ ∈ 𝐽 )
3		n0i	⊢ ( ∅ ∈ 𝐽 → ¬ 𝐽 = ∅ )
4	2 3	syl	⊢ ( 𝐽 ∈ Top → ¬ 𝐽 = ∅ )
5	4	pm2.21d	⊢ ( 𝐽 ∈ Top → ( 𝐽 = ∅ → 𝐽 = { ∅ } ) )
6		idd	⊢ ( 𝐽 ∈ Top → ( 𝐽 = { ∅ } → 𝐽 = { ∅ } ) )
7	5 6	jaod	⊢ ( 𝐽 ∈ Top → ( ( 𝐽 = ∅ ∨ 𝐽 = { ∅ } ) → 𝐽 = { ∅ } ) )
8	1 7	impbid2	⊢ ( 𝐽 ∈ Top → ( 𝐽 = { ∅ } ↔ ( 𝐽 = ∅ ∨ 𝐽 = { ∅ } ) ) )
9		uni0b	⊢ ( ∪ 𝐽 = ∅ ↔ 𝐽 ⊆ { ∅ } )
10		sssn	⊢ ( 𝐽 ⊆ { ∅ } ↔ ( 𝐽 = ∅ ∨ 𝐽 = { ∅ } ) )
11	9 10	bitr2i	⊢ ( ( 𝐽 = ∅ ∨ 𝐽 = { ∅ } ) ↔ ∪ 𝐽 = ∅ )
12	8 11	bitr2di	⊢ ( 𝐽 ∈ Top → ( ∪ 𝐽 = ∅ ↔ 𝐽 = { ∅ } ) )