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 )