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 = ⋃ J
Assertion t1connperf ⊢ J ∈ Fre ∧ J ∈ Conn ∧ ¬ X ≈ 1 𝑜 → J ∈ Perf

Proof

Step Hyp Ref Expression
1 t1connperf.1 ⊢ X = ⋃ J
2 simplr ⊢ J ∈ Fre ∧ J ∈ Conn ∧ x ∈ X ∧ x ∈ J → J ∈ Conn
3 simprr ⊢ J ∈ Fre ∧ J ∈ Conn ∧ x ∈ X ∧ x ∈ J → x ∈ J
4 vex ⊢ x ∈ V
5 4 snnz ⊢ x ≠ ∅
6 5 a1i ⊢ J ∈ Fre ∧ J ∈ Conn ∧ x ∈ X ∧ x ∈ J → x ≠ ∅
7 1 t1sncld ⊢ J ∈ Fre ∧ x ∈ X → x ∈ Clsd ⁡ J
8 7 ad2ant2r ⊢ J ∈ Fre ∧ J ∈ Conn ∧ x ∈ X ∧ x ∈ J → x ∈ Clsd ⁡ J
9 1 2 3 6 8 connclo ⊢ J ∈ Fre ∧ J ∈ Conn ∧ x ∈ X ∧ x ∈ J → x = X
10 4 ensn1 ⊢ x ≈ 1 𝑜
11 9 10 eqbrtrrdi ⊢ J ∈ Fre ∧ J ∈ Conn ∧ x ∈ X ∧ x ∈ J → X ≈ 1 𝑜
12 11 rexlimdvaa ⊢ J ∈ Fre ∧ J ∈ Conn → ∃ x ∈ X x ∈ J → X ≈ 1 𝑜
13 12 con3d ⊢ J ∈ Fre ∧ J ∈ Conn → ¬ X ≈ 1 𝑜 → ¬ ∃ x ∈ X x ∈ J
14 ralnex ⊢ ∀ x ∈ X ¬ x ∈ J ↔ ¬ ∃ x ∈ X x ∈ J
15 13 14 imbitrrdi ⊢ J ∈ Fre ∧ J ∈ Conn → ¬ X ≈ 1 𝑜 → ∀ x ∈ X ¬ x ∈ J
16 t1top ⊢ J ∈ Fre → J ∈ Top
17 16 adantr ⊢ J ∈ Fre ∧ J ∈ Conn → J ∈ Top
18 1 isperf3 ⊢ J ∈ Perf ↔ J ∈ Top ∧ ∀ x ∈ X ¬ x ∈ J
19 18 baib ⊢ J ∈ Top → J ∈ Perf ↔ ∀ x ∈ X ¬ x ∈ J
20 17 19 syl ⊢ J ∈ Fre ∧ J ∈ Conn → J ∈ Perf ↔ ∀ x ∈ X ¬ x ∈ J
21 15 20 sylibrd ⊢ J ∈ Fre ∧ J ∈ Conn → ¬ X ≈ 1 𝑜 → J ∈ Perf
22 21 3impia ⊢ J ∈ Fre ∧ J ∈ Conn ∧ ¬ X ≈ 1 𝑜 → J ∈ Perf