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 ⊢ 𝑋 = ∪ 𝐽
connclo.1 ⊢ ( 𝜑 → 𝐽 ∈ Conn )
connclo.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
connclo.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
connclo.4 ⊢ ( 𝜑 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )
Assertion connclo ( 𝜑 → 𝐴 = 𝑋 )

Proof

Step Hyp Ref Expression
1 isconn.1 ⊢ 𝑋 = ∪ 𝐽
2 connclo.1 ⊢ ( 𝜑 → 𝐽 ∈ Conn )
3 connclo.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝐽 )
4 connclo.3 ⊢ ( 𝜑 → 𝐴 ≠ ∅ )
5 connclo.4 ⊢ ( 𝜑 → 𝐴 ∈ ( Clsd ‘ 𝐽 ) )
6 4 neneqd ⊢ ( 𝜑 → ¬ 𝐴 = ∅ )
7 3 5 elind ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) )
8 1 isconn ⊢ ( 𝐽 ∈ Conn ↔ ( 𝐽 ∈ Top ∧ ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } ) )
9 8 simprbi ⊢ ( 𝐽 ∈ Conn → ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } )
10 2 9 syl ⊢ ( 𝜑 → ( 𝐽 ∩ ( Clsd ‘ 𝐽 ) ) = { ∅ , 𝑋 } )
11 7 10 eleqtrd ⊢ ( 𝜑 → 𝐴 ∈ { ∅ , 𝑋 } )
12 elpri ⊢ ( 𝐴 ∈ { ∅ , 𝑋 } → ( 𝐴 = ∅ ∨ 𝐴 = 𝑋 ) )
13 11 12 syl ⊢ ( 𝜑 → ( 𝐴 = ∅ ∨ 𝐴 = 𝑋 ) )
14 13 ord ⊢ ( 𝜑 → ( ¬ 𝐴 = ∅ → 𝐴 = 𝑋 ) )
15 6 14 mpd ⊢ ( 𝜑 → 𝐴 = 𝑋 )