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	⊢ 𝑋 = ∪ 𝐽
Assertion	t1connperf	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ∧ ¬ 𝑋 ≈ 1o ) → 𝐽 ∈ Perf )

Proof

Step	Hyp	Ref	Expression
1		t1connperf.1	⊢ 𝑋 = ∪ 𝐽
2		simplr	⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝑋 ∧ { 𝑥 } ∈ 𝐽 ) ) → 𝐽 ∈ Conn )
3		simprr	⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝑋 ∧ { 𝑥 } ∈ 𝐽 ) ) → { 𝑥 } ∈ 𝐽 )
4		vex	⊢ 𝑥 ∈ V
5	4	snnz	⊢ { 𝑥 } ≠ ∅
6	5	a1i	⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝑋 ∧ { 𝑥 } ∈ 𝐽 ) ) → { 𝑥 } ≠ ∅ )
7	1	t1sncld	⊢ ( ( 𝐽 ∈ Fre ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
8	7	ad2ant2r	⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝑋 ∧ { 𝑥 } ∈ 𝐽 ) ) → { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
9	1 2 3 6 8	connclo	⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝑋 ∧ { 𝑥 } ∈ 𝐽 ) ) → { 𝑥 } = 𝑋 )
10	4	ensn1	⊢ { 𝑥 } ≈ 1o
11	9 10	eqbrtrrdi	⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝑋 ∧ { 𝑥 } ∈ 𝐽 ) ) → 𝑋 ≈ 1o )
12	11	rexlimdvaa	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) → ( ∃ 𝑥 ∈ 𝑋 { 𝑥 } ∈ 𝐽 → 𝑋 ≈ 1o ) )
13	12	con3d	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) → ( ¬ 𝑋 ≈ 1o → ¬ ∃ 𝑥 ∈ 𝑋 { 𝑥 } ∈ 𝐽 ) )
14		ralnex	⊢ ( ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ↔ ¬ ∃ 𝑥 ∈ 𝑋 { 𝑥 } ∈ 𝐽 )
15	13 14	syl6ibr	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) → ( ¬ 𝑋 ≈ 1o → ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
16		t1top	⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
17	16	adantr	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) → 𝐽 ∈ Top )
18	1	isperf3	⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
19	18	baib	⊢ ( 𝐽 ∈ Top → ( 𝐽 ∈ Perf ↔ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
20	17 19	syl	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) → ( 𝐽 ∈ Perf ↔ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
21	15 20	sylibrd	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ) → ( ¬ 𝑋 ≈ 1o → 𝐽 ∈ Perf ) )
22	21	3impia	⊢ ( ( 𝐽 ∈ Fre ∧ 𝐽 ∈ Conn ∧ ¬ 𝑋 ≈ 1o ) → 𝐽 ∈ Perf )