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

Metamath Proof Explorer

Theorem connclo

Description: The only nonempty clopen set of a connected topology is the whole space. (Contributed by Mario Carneiro, 10-Mar-2015)

Ref Expression
Hypotheses isconn.1 ⊢ X = ⋃ J
connclo.1 ⊢ φ → J ∈ Conn
connclo.2 ⊢ φ → A ∈ J
connclo.3 ⊢ φ → A ≠ ∅
connclo.4 ⊢ φ → A ∈ Clsd ⁡ J
Assertion connclo ⊢ φ → A = X

Proof

Step Hyp Ref Expression
1 isconn.1 ⊢ X = ⋃ J
2 connclo.1 ⊢ φ → J ∈ Conn
3 connclo.2 ⊢ φ → A ∈ J
4 connclo.3 ⊢ φ → A ≠ ∅
5 connclo.4 ⊢ φ → A ∈ Clsd ⁡ J
6 4 neneqd ⊢ φ → ¬ A = ∅
7 3 5 elind ⊢ φ → A ∈ J ∩ Clsd ⁡ J
8 1 isconn ⊢ J ∈ Conn ↔ J ∈ Top ∧ J ∩ Clsd ⁡ J = ∅ X
9 8 simprbi ⊢ J ∈ Conn → J ∩ Clsd ⁡ J = ∅ X
10 2 9 syl ⊢ φ → J ∩ Clsd ⁡ J = ∅ X
11 7 10 eleqtrd ⊢ φ → A ∈ ∅ X
12 elpri ⊢ A ∈ ∅ X → A = ∅ ∨ A = X
13 11 12 syl ⊢ φ → A = ∅ ∨ A = X
14 13 ord ⊢ φ → ¬ A = ∅ → A = X
15 6 14 mpd ⊢ φ → A = X