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

Metamath Proof Explorer

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 → ( ∪ 𝐽 = ∅ ↔ 𝐽 = { ∅ } ) )