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

Metamath Proof Explorer

Theorem perfcls

Description: A subset of a perfect space is perfect iff its closure is perfect (and the closure is an actual perfect set, since it is both closed and perfect in the subspace topology). (Contributed by Mario Carneiro, 26-Dec-2016)

Ref Expression
Hypothesis lpcls.1 ⊢ 𝑋 = ∪ 𝐽
Assertion perfcls ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Perf ↔ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Perf ) )

Proof

Step Hyp Ref Expression
1 lpcls.1 ⊢ 𝑋 = ∪ 𝐽
2 1 lpcls ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )
3 2 sseq2d ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
4 t1top ⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
5 1 clslp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
6 4 5 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) = ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
7 6 sseq1d ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
8 ssequn1 ⊢ ( 𝑆 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )
9 ssun2 ⊢ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )
10 eqss ⊢ ( ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∧ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
11 9 10 mpbiran2 ⊢ ( ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )
12 8 11 bitri ⊢ ( 𝑆 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑆 ∪ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )
13 7 12 bitr4di ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑆 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
14 3 13 bitr2d ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
15 eqid ⊢ ( 𝐽 ↾t 𝑆 ) = ( 𝐽 ↾t 𝑆 )
16 1 15 restperf ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Perf ↔ 𝑆 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
17 4 16 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Perf ↔ 𝑆 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
18 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
19 eqid ⊢ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
20 1 19 restperf ⊢ ( ( 𝐽 ∈ Top ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Perf ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
21 18 20 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Perf ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
22 4 21 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Perf ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
23 14 17 22 3bitr4d ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( 𝐽 ↾t 𝑆 ) ∈ Perf ↔ ( 𝐽 ↾t ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ Perf ) )