Metamath Proof Explorer

Theorem restperf

Description: Perfection of a subspace. Note that the term "perfect set" is reserved forclosed sets which are perfect in the subspace topology. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses restcls.1 ⊢ 𝑋 = ∪ 𝐽
restcls.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
Assertion restperf ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐾 ∈ Perf ↔ 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 restcls.1 ⊢ 𝑋 = ∪ 𝐽
2 restcls.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
3 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
4 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
5 3 4 sylanb ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
6 2 5 eqeltrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
7 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
8 6 7 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝐾 ∈ Top )
9 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
10 9 isperf ⊢ ( 𝐾 ∈ Perf ↔ ( 𝐾 ∈ Top ∧ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
11 10 baib ⊢ ( 𝐾 ∈ Top → ( 𝐾 ∈ Perf ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
12 8 11 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐾 ∈ Perf ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
13 sseqin2 ⊢ ( 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ↔ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) = 𝑌 )
14 ssid ⊢ 𝑌 ⊆ 𝑌
15 1 2 restlp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑌 ⊆ 𝑌 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑌 ) = ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) )
16 14 15 mp3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑌 ) = ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) )
17 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
18 6 17 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → 𝑌 = ∪ 𝐾 )
19 18 fveq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑌 ) = ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) )
20 16 19 eqtr3d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) = ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) )
21 20 18 eqeq12d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( ( ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ∩ 𝑌 ) = 𝑌 ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
22 13 21 bitrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ↔ ( ( limPt ‘ 𝐾 ) ‘ ∪ 𝐾 ) = ∪ 𝐾 ) )
23 12 22 bitr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐾 ∈ Perf ↔ 𝑌 ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑌 ) ) )