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

Metamath Proof Explorer

Theorem t1connperf

Description: A connected T_1 space is perfect, unless it is the topology of a singleton. (Contributed by Mario Carneiro, 26-Dec-2016)

Ref Expression
Hypothesis t1connperf.1 
|- X = U. J
Assertion t1connperf 
|- ( ( J e. Fre /\ J e. Conn /\ -. X ~~ 1o ) -> J e. Perf )

Proof

Step Hyp Ref Expression
1 t1connperf.1 
 |-  X = U. J
2 simplr 
 |-  ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> J e. Conn )
3 simprr 
 |-  ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } e. J )
4 vex 
 |-  x e. _V
5 4 snnz 
 |-  { x } =/= (/)
6 5 a1i 
 |-  ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } =/= (/) )
7 1 t1sncld 
 |-  ( ( J e. Fre /\ x e. X ) -> { x } e. ( Clsd ` J ) )
8 7 ad2ant2r 
 |-  ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } e. ( Clsd ` J ) )
9 1 2 3 6 8 connclo 
 |-  ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> { x } = X )
10 4 ensn1 
 |-  { x } ~~ 1o
11 9 10 eqbrtrrdi 
 |-  ( ( ( J e. Fre /\ J e. Conn ) /\ ( x e. X /\ { x } e. J ) ) -> X ~~ 1o )
12 11 rexlimdvaa 
 |-  ( ( J e. Fre /\ J e. Conn ) -> ( E. x e. X { x } e. J -> X ~~ 1o ) )
13 12 con3d 
 |-  ( ( J e. Fre /\ J e. Conn ) -> ( -. X ~~ 1o -> -. E. x e. X { x } e. J ) )
14 ralnex 
 |-  ( A. x e. X -. { x } e. J <-> -. E. x e. X { x } e. J )
15 13 14 imbitrrdi 
 |-  ( ( J e. Fre /\ J e. Conn ) -> ( -. X ~~ 1o -> A. x e. X -. { x } e. J ) )
16 t1top 
 |-  ( J e. Fre -> J e. Top )
17 16 adantr 
 |-  ( ( J e. Fre /\ J e. Conn ) -> J e. Top )
18 1 isperf3 
 |-  ( J e. Perf <-> ( J e. Top /\ A. x e. X -. { x } e. J ) )
19 18 baib 
 |-  ( J e. Top -> ( J e. Perf <-> A. x e. X -. { x } e. J ) )
20 17 19 syl 
 |-  ( ( J e. Fre /\ J e. Conn ) -> ( J e. Perf <-> A. x e. X -. { x } e. J ) )
21 15 20 sylibrd 
 |-  ( ( J e. Fre /\ J e. Conn ) -> ( -. X ~~ 1o -> J e. Perf ) )
22 21 3impia 
 |-  ( ( J e. Fre /\ J e. Conn /\ -. X ~~ 1o ) -> J e. Perf )