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 = 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 )