This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑋 = ∪ 𝐽
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 imbitrrdi ⊢ ( ( 𝐽 ∈ 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 )