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 ⊢ J ∈ Top → ⋃ J = ∅ ↔ J = ∅

Proof

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