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 = U. J
	connclo.1	|- ( ph -> J e. Conn )
	connclo.2	|- ( ph -> A e. J )
	connclo.3	|- ( ph -> A =/= (/) )
	connclo.4	|- ( ph -> A e. ( Clsd ` J ) )
Assertion	connclo	|- ( ph -> A = X )

Proof

Step	Hyp	Ref	Expression
1		isconn.1	|- X = U. J
2		connclo.1	|- ( ph -> J e. Conn )
3		connclo.2	|- ( ph -> A e. J )
4		connclo.3	|- ( ph -> A =/= (/) )
5		connclo.4	|- ( ph -> A e. ( Clsd ` J ) )
6	4	neneqd	|- ( ph -> -. A = (/) )
7	3 5	elind	|- ( ph -> A e. ( J i^i ( Clsd ` J ) ) )
8	1	isconn	|- ( J e. Conn <-> ( J e. Top /\ ( J i^i ( Clsd ` J ) ) = { (/) , X } ) )
9	8	simprbi	|- ( J e. Conn -> ( J i^i ( Clsd ` J ) ) = { (/) , X } )
10	2 9	syl	|- ( ph -> ( J i^i ( Clsd ` J ) ) = { (/) , X } )
11	7 10	eleqtrd	|- ( ph -> A e. { (/) , X } )
12		elpri	|- ( A e. { (/) , X } -> ( A = (/) \/ A = X ) )
13	11 12	syl	|- ( ph -> ( A = (/) \/ A = X ) )
14	13	ord	|- ( ph -> ( -. A = (/) -> A = X ) )
15	6 14	mpd	|- ( ph -> A = X )