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	⊢ ( 𝜑 → 𝐴 = 𝑋 )