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 syl6ibr
 |-  ( ( 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 )