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 \in Top \land Y \subseteq X) \to (K \in Perf \leftrightarrow Y \subseteq limPt (J) (Y))$

Proof

Step	Hyp	Ref	Expression
1		restcls.1	$⊢ X = ⋃ J$
2		restcls.2	$⊢ K = J ↾_{𝑡} Y$
3	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
4		resttopon	$⊢ (J \in TopOn (X) \land Y \subseteq X) \to J ↾_{𝑡} Y \in TopOn (Y)$
5	3 4	sylanb	$⊢ (J \in Top \land Y \subseteq X) \to J ↾_{𝑡} Y \in TopOn (Y)$
6	2 5	eqeltrid	$⊢ (J \in Top \land Y \subseteq X) \to K \in TopOn (Y)$
7		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
8	6 7	syl	$⊢ (J \in Top \land Y \subseteq X) \to K \in Top$
9		eqid	$⊢ ⋃ K = ⋃ K$
10	9	isperf	$⊢ K \in Perf \leftrightarrow (K \in Top \land limPt (K) (⋃ K) = ⋃ K)$
11	10	baib	$⊢ K \in Top \to (K \in Perf \leftrightarrow limPt (K) (⋃ K) = ⋃ K)$
12	8 11	syl	$⊢ (J \in Top \land Y \subseteq X) \to (K \in Perf \leftrightarrow limPt (K) (⋃ K) = ⋃ K)$
13		sseqin2	$⊢ Y \subseteq limPt (J) (Y) \leftrightarrow limPt (J) (Y) \cap Y = Y$
14		ssid	$⊢ Y \subseteq Y$
15	1 2	restlp	$⊢ (J \in Top \land Y \subseteq X \land Y \subseteq Y) \to limPt (K) (Y) = limPt (J) (Y) \cap Y$
16	14 15	mp3an3	$⊢ (J \in Top \land Y \subseteq X) \to limPt (K) (Y) = limPt (J) (Y) \cap Y$
17		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
18	6 17	syl	$⊢ (J \in Top \land Y \subseteq X) \to Y = ⋃ K$
19	18	fveq2d	$⊢ (J \in Top \land Y \subseteq X) \to limPt (K) (Y) = limPt (K) (⋃ K)$
20	16 19	eqtr3d	$⊢ (J \in Top \land Y \subseteq X) \to limPt (J) (Y) \cap Y = limPt (K) (⋃ K)$
21	20 18	eqeq12d	$⊢ (J \in Top \land Y \subseteq X) \to (limPt (J) (Y) \cap Y = Y \leftrightarrow limPt (K) (⋃ K) = ⋃ K)$
22	13 21	bitrid	$⊢ (J \in Top \land Y \subseteq X) \to (Y \subseteq limPt (J) (Y) \leftrightarrow limPt (K) (⋃ K) = ⋃ K)$
23	12 22	bitr4d	$⊢ (J \in Top \land Y \subseteq X) \to (K \in Perf \leftrightarrow Y \subseteq limPt (J) (Y))$

Metamath Proof Explorer

Theorem restperf

Proof