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

Metamath Proof Explorer

Theorem isperf2

Description: Definition of a perfect space. (Contributed by Mario Carneiro, 24-Dec-2016)

Ref Expression
Hypothesis lpfval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion isperf2 ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 isperf ⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) )
3 ssid ⊢ 𝑋 ⊆ 𝑋
4 1 lpss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑋 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
5 3 4 mpan2 ⊢ ( 𝐽 ∈ Top → ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 )
6 eqss ⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
7 6 baib ⊢ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ⊆ 𝑋 → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
8 5 7 syl ⊢ ( 𝐽 ∈ Top → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ↔ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
9 8 pm5.32i ⊢ ( ( 𝐽 ∈ Top ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 ) ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )
10 2 9 bitri ⊢ ( 𝐽 ∈ Perf ↔ ( 𝐽 ∈ Top ∧ 𝑋 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑋 ) ) )