Theorem perfcls 21662

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

Hypothesis

Ref	Expression
lpcls.1	⊢ 𝑋 = ∪ 𝐽

Assertion

Ref	Expression
perfcls	⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ (𝐽 ↾t ((cls‘𝐽)‘𝑆)) ∈ Perf))

Proof of Theorem perfcls

Step	Hyp	Ref	Expression
1		lpcls.1	. . . . 5 ⊢ 𝑋 = ∪ 𝐽
2	1	lpcls 21661	. . . 4 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((limPt‘𝐽)‘((cls‘𝐽)‘𝑆)) = ((limPt‘𝐽)‘𝑆))
3	2	sseq2d 3924	. . 3 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → (((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘((cls‘𝐽)‘𝑆)) ↔ ((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘𝑆)))
4		t1top 21627	. . . . . 6 ⊢ (𝐽 ∈ Fre → 𝐽 ∈ Top)
5	1	clslp 21445	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑆 ∪ ((limPt‘𝐽)‘𝑆)))
6	4, 5	sylan 580	. . . . 5 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) = (𝑆 ∪ ((limPt‘𝐽)‘𝑆)))
7	6	sseq1d 3923	. . . 4 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → (((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘𝑆) ↔ (𝑆 ∪ ((limPt‘𝐽)‘𝑆)) ⊆ ((limPt‘𝐽)‘𝑆)))
8		ssequn1 4081	. . . . 5 ⊢ (𝑆 ⊆ ((limPt‘𝐽)‘𝑆) ↔ (𝑆 ∪ ((limPt‘𝐽)‘𝑆)) = ((limPt‘𝐽)‘𝑆))
9		ssun2 4074	. . . . . 6 ⊢ ((limPt‘𝐽)‘𝑆) ⊆ (𝑆 ∪ ((limPt‘𝐽)‘𝑆))
10		eqss 3908	. . . . . 6 ⊢ ((𝑆 ∪ ((limPt‘𝐽)‘𝑆)) = ((limPt‘𝐽)‘𝑆) ↔ ((𝑆 ∪ ((limPt‘𝐽)‘𝑆)) ⊆ ((limPt‘𝐽)‘𝑆) ∧ ((limPt‘𝐽)‘𝑆) ⊆ (𝑆 ∪ ((limPt‘𝐽)‘𝑆))))
11	9, 10	mpbiran2 706	. . . . 5 ⊢ ((𝑆 ∪ ((limPt‘𝐽)‘𝑆)) = ((limPt‘𝐽)‘𝑆) ↔ (𝑆 ∪ ((limPt‘𝐽)‘𝑆)) ⊆ ((limPt‘𝐽)‘𝑆))
12	8, 11	bitri 276	. . . 4 ⊢ (𝑆 ⊆ ((limPt‘𝐽)‘𝑆) ↔ (𝑆 ∪ ((limPt‘𝐽)‘𝑆)) ⊆ ((limPt‘𝐽)‘𝑆))
13	7, 12	syl6bbr 290	. . 3 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → (((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘𝑆) ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆)))
14	3, 13	bitr2d 281	. 2 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → (𝑆 ⊆ ((limPt‘𝐽)‘𝑆) ↔ ((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘((cls‘𝐽)‘𝑆))))
15		eqid 2795	. . . 4 ⊢ (𝐽 ↾t 𝑆) = (𝐽 ↾t 𝑆)
16	1, 15	restperf 21481	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆)))
17	4, 16	sylan 580	. 2 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ 𝑆 ⊆ ((limPt‘𝐽)‘𝑆)))
18	1	clsss3 21356	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((cls‘𝐽)‘𝑆) ⊆ 𝑋)
19		eqid 2795	. . . . 5 ⊢ (𝐽 ↾t ((cls‘𝐽)‘𝑆)) = (𝐽 ↾t ((cls‘𝐽)‘𝑆))
20	1, 19	restperf 21481	. . . 4 ⊢ ((𝐽 ∈ Top ∧ ((cls‘𝐽)‘𝑆) ⊆ 𝑋) → ((𝐽 ↾t ((cls‘𝐽)‘𝑆)) ∈ Perf ↔ ((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘((cls‘𝐽)‘𝑆))))
21	18, 20	syldan 591	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t ((cls‘𝐽)‘𝑆)) ∈ Perf ↔ ((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘((cls‘𝐽)‘𝑆))))
22	4, 21	sylan 580	. 2 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t ((cls‘𝐽)‘𝑆)) ∈ Perf ↔ ((cls‘𝐽)‘𝑆) ⊆ ((limPt‘𝐽)‘((cls‘𝐽)‘𝑆))))
23	14, 17, 22	3bitr4d 312	1 ⊢ ((𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋) → ((𝐽 ↾t 𝑆) ∈ Perf ↔ (𝐽 ↾t ((cls‘𝐽)‘𝑆)) ∈ Perf))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1522   ∈ wcel 2081   ∪ cun 3861   ⊆ wss 3863  ∪ cuni 4749  ‘cfv 6230  (class class class)co 7021   ↾_t crest 16528  Topctop 21190  clsccl 21315  limPtclp 21431  Perfcperf 21432  Frect1 21604

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-rep 5086  ax-sep 5099  ax-nul 5106  ax-pow 5162  ax-pr 5226  ax-un 7324

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-ral 3110  df-rex 3111  df-reu 3112  df-rab 3114  df-v 3439  df-sbc 3710  df-csb 3816  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-pss 3880  df-nul 4216  df-if 4386  df-pw 4459  df-sn 4477  df-pr 4479  df-tp 4481  df-op 4483  df-uni 4750  df-int 4787  df-iun 4831  df-iin 4832  df-br 4967  df-opab 5029  df-mpt 5046  df-tr 5069  df-id 5353  df-eprel 5358  df-po 5367  df-so 5368  df-fr 5407  df-we 5409  df-xp 5454  df-rel 5455  df-cnv 5456  df-co 5457  df-dm 5458  df-rn 5459  df-res 5460  df-ima 5461  df-pred 6028  df-ord 6074  df-on 6075  df-lim 6076  df-suc 6077  df-iota 6194  df-fun 6232  df-fn 6233  df-f 6234  df-f1 6235  df-fo 6236  df-f1o 6237  df-fv 6238  df-ov 7024  df-oprab 7025  df-mpo 7026  df-om 7442  df-1st 7550  df-2nd 7551  df-wrecs 7803  df-recs 7865  df-rdg 7903  df-oadd 7962  df-er 8144  df-en 8363  df-fin 8366  df-fi 8726  df-rest 16530  df-topgen 16551  df-top 21191  df-topon 21208  df-bases 21243  df-cld 21316  df-ntr 21317  df-cls 21318  df-nei 21395  df-lp 21433  df-perf 21434  df-t1 21611

This theorem is referenced by: (None)