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

Metamath Proof Explorer

Theorem isperf3

Description: A perfect space is a topology which has no open singletons. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis lpfval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion isperf3 ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 isperf2 ⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
3 dfss3 ⊢ ( 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) )
4 1 maxlp ⊢ ( 𝐽 ∈ Top → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ¬ { 𝑥 } ∈ 𝐽 ) ) )
5 4 baibd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ¬ { 𝑥 } ∈ 𝐽 ) )
6 5 ralbidva ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑥 ∈ 𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
7 3 6 bitrid ⊢ ( 𝐽 ∈ Top → ( 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ↔ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
8 7 pm5.32i ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )
9 2 8 bitri ⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝑋 ¬ { 𝑥 } ∈ 𝐽 ) )