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 ⊢ X = ⋃ J
restcls.2 ⊢ K = J ↾ 𝑡 Y
Assertion restperf ⊢ J ∈ Top ∧ Y ⊆ X → K ∈ Perf ↔ Y ⊆ limPt ⁡ J ⁡ Y

Proof

Step Hyp Ref Expression
1 restcls.1 ⊢ X = ⋃ J
2 restcls.2 ⊢ K = J ↾ 𝑡 Y
3 1 toptopon ⊢ J ∈ Top ↔ J ∈ TopOn ⁡ X
4 resttopon ⊢ J ∈ TopOn ⁡ X ∧ Y ⊆ X → J ↾ 𝑡 Y ∈ TopOn ⁡ Y
5 3 4 sylanb ⊢ J ∈ Top ∧ Y ⊆ X → J ↾ 𝑡 Y ∈ TopOn ⁡ Y
6 2 5 eqeltrid ⊢ J ∈ Top ∧ Y ⊆ X → K ∈ TopOn ⁡ Y
7 topontop ⊢ K ∈ TopOn ⁡ Y → K ∈ Top
8 6 7 syl ⊢ J ∈ Top ∧ Y ⊆ X → K ∈ Top
9 eqid ⊢ ⋃ K = ⋃ K
10 9 isperf ⊢ K ∈ Perf ↔ K ∈ Top ∧ limPt ⁡ K ⁡ ⋃ K = ⋃ K
11 10 baib ⊢ K ∈ Top → K ∈ Perf ↔ limPt ⁡ K ⁡ ⋃ K = ⋃ K
12 8 11 syl ⊢ J ∈ Top ∧ Y ⊆ X → K ∈ Perf ↔ limPt ⁡ K ⁡ ⋃ K = ⋃ K
13 sseqin2 ⊢ Y ⊆ limPt ⁡ J ⁡ Y ↔ limPt ⁡ J ⁡ Y ∩ Y = Y
14 ssid ⊢ Y ⊆ Y
15 1 2 restlp ⊢ J ∈ Top ∧ Y ⊆ X ∧ Y ⊆ Y → limPt ⁡ K ⁡ Y = limPt ⁡ J ⁡ Y ∩ Y
16 14 15 mp3an3 ⊢ J ∈ Top ∧ Y ⊆ X → limPt ⁡ K ⁡ Y = limPt ⁡ J ⁡ Y ∩ Y
17 toponuni ⊢ K ∈ TopOn ⁡ Y → Y = ⋃ K
18 6 17 syl ⊢ J ∈ Top ∧ Y ⊆ X → Y = ⋃ K
19 18 fveq2d ⊢ J ∈ Top ∧ Y ⊆ X → limPt ⁡ K ⁡ Y = limPt ⁡ K ⁡ ⋃ K
20 16 19 eqtr3d ⊢ J ∈ Top ∧ Y ⊆ X → limPt ⁡ J ⁡ Y ∩ Y = limPt ⁡ K ⁡ ⋃ K
21 20 18 eqeq12d ⊢ J ∈ Top ∧ Y ⊆ X → limPt ⁡ J ⁡ Y ∩ Y = Y ↔ limPt ⁡ K ⁡ ⋃ K = ⋃ K
22 13 21 bitrid ⊢ J ∈ Top ∧ Y ⊆ X → Y ⊆ limPt ⁡ J ⁡ Y ↔ limPt ⁡ K ⁡ ⋃ K = ⋃ K
23 12 22 bitr4d ⊢ J ∈ Top ∧ Y ⊆ X → K ∈ Perf ↔ Y ⊆ limPt ⁡ J ⁡ Y