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 ) )