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	$⊢ X = ⋃ J$
	Assertion	perfcls	$⊢ (J \in Fre \land S \subseteq X) \to (J ↾_{𝑡} S \in Perf \leftrightarrow J ↾_{𝑡} cls (J) (S) \in Perf)$

Proof

Step	Hyp	Ref	Expression
1		lpcls.1	$⊢ X = ⋃ J$
2	1	lpcls	$⊢ (J \in Fre \land S \subseteq X) \to limPt (J) (cls (J) (S)) = limPt (J) (S)$
3	2	sseq2d	$⊢ (J \in Fre \land S \subseteq X) \to (cls (J) (S) \subseteq limPt (J) (cls (J) (S)) \leftrightarrow cls (J) (S) \subseteq limPt (J) (S))$
4		t1top	$⊢ J \in Fre \to J \in Top$
5	1	clslp	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) = S \cup limPt (J) (S)$
6	4 5	sylan	$⊢ (J \in Fre \land S \subseteq X) \to cls (J) (S) = S \cup limPt (J) (S)$
7	6	sseq1d	$⊢ (J \in Fre \land S \subseteq X) \to (cls (J) (S) \subseteq limPt (J) (S) \leftrightarrow S \cup limPt (J) (S) \subseteq limPt (J) (S))$
8		ssequn1	$⊢ S \subseteq limPt (J) (S) \leftrightarrow S \cup limPt (J) (S) = limPt (J) (S)$
9		ssun2	$⊢ limPt (J) (S) \subseteq S \cup limPt (J) (S)$
10		eqss	$⊢ S \cup limPt (J) (S) = limPt (J) (S) \leftrightarrow (S \cup limPt (J) (S) \subseteq limPt (J) (S) \land limPt (J) (S) \subseteq S \cup limPt (J) (S))$
11	9 10	mpbiran2	$⊢ S \cup limPt (J) (S) = limPt (J) (S) \leftrightarrow S \cup limPt (J) (S) \subseteq limPt (J) (S)$
12	8 11	bitri	$⊢ S \subseteq limPt (J) (S) \leftrightarrow S \cup limPt (J) (S) \subseteq limPt (J) (S)$
13	7 12	bitr4di	$⊢ (J \in Fre \land S \subseteq X) \to (cls (J) (S) \subseteq limPt (J) (S) \leftrightarrow S \subseteq limPt (J) (S))$
14	3 13	bitr2d	$⊢ (J \in Fre \land S \subseteq X) \to (S \subseteq limPt (J) (S) \leftrightarrow cls (J) (S) \subseteq limPt (J) (cls (J) (S)))$
15		eqid	$⊢ J ↾_{𝑡} S = J ↾_{𝑡} S$
16	1 15	restperf	$⊢ (J \in Top \land S \subseteq X) \to (J ↾_{𝑡} S \in Perf \leftrightarrow S \subseteq limPt (J) (S))$
17	4 16	sylan	$⊢ (J \in Fre \land S \subseteq X) \to (J ↾_{𝑡} S \in Perf \leftrightarrow S \subseteq limPt (J) (S))$
18	1	clsss3	$⊢ (J \in Top \land S \subseteq X) \to cls (J) (S) \subseteq X$
19		eqid	$⊢ J ↾_{𝑡} cls (J) (S) = J ↾_{𝑡} cls (J) (S)$
20	1 19	restperf	$⊢ (J \in Top \land cls (J) (S) \subseteq X) \to (J ↾_{𝑡} cls (J) (S) \in Perf \leftrightarrow cls (J) (S) \subseteq limPt (J) (cls (J) (S)))$
21	18 20	syldan	$⊢ (J \in Top \land S \subseteq X) \to (J ↾_{𝑡} cls (J) (S) \in Perf \leftrightarrow cls (J) (S) \subseteq limPt (J) (cls (J) (S)))$
22	4 21	sylan	$⊢ (J \in Fre \land S \subseteq X) \to (J ↾_{𝑡} cls (J) (S) \in Perf \leftrightarrow cls (J) (S) \subseteq limPt (J) (cls (J) (S)))$
23	14 17 22	3bitr4d	$⊢ (J \in Fre \land S \subseteq X) \to (J ↾_{𝑡} S \in Perf \leftrightarrow J ↾_{𝑡} cls (J) (S) \in Perf)$

Metamath Proof Explorer

Theorem perfcls

Proof