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∈Xx∈J→X≈1𝑜
13 12 con3d ⊢J∈Fre∧J∈Conn→¬X≈1𝑜→¬∃x∈Xx∈J
14 ralnex ⊢∀x∈X¬x∈J↔¬∃x∈Xx∈J
15 13 14 syl6ibr ⊢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