restlp

Description: The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	restcls.1	$⊢ X = ⋃ J$
	restcls.2	$⊢ K = J ↾_{𝑡} Y$
Assertion	restlp	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to limPt (K) (S) = limPt (J) (S) \cap Y$

Proof

Step	Hyp	Ref	Expression
1		restcls.1	$⊢ X = ⋃ J$
2		restcls.2	$⊢ K = J ↾_{𝑡} Y$
3		simp3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq Y$
4	3	ssdifssd	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S ∖ \{x\} \subseteq Y$
5	1 2	restcls	$⊢ (J \in Top \land Y \subseteq X \land S ∖ \{x\} \subseteq Y) \to cls (K) (S ∖ \{x\}) = cls (J) (S ∖ \{x\}) \cap Y$
6	4 5	syld3an3	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to cls (K) (S ∖ \{x\}) = cls (J) (S ∖ \{x\}) \cap Y$
7	6	eleq2d	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (x \in cls (K) (S ∖ \{x\}) \leftrightarrow x \in (cls (J) (S ∖ \{x\}) \cap Y))$
8		elin	$⊢ x \in (cls (J) (S ∖ \{x\}) \cap Y) \leftrightarrow (x \in cls (J) (S ∖ \{x\}) \land x \in Y)$
9	7 8	bitrdi	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (x \in cls (K) (S ∖ \{x\}) \leftrightarrow (x \in cls (J) (S ∖ \{x\}) \land x \in Y))$
10		simp1	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to J \in Top$
11	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
12	10 11	sylib	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to J \in TopOn (X)$
13		simp2	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to Y \subseteq X$
14		resttopon	$⊢ (J \in TopOn (X) \land Y \subseteq X) \to J ↾_{𝑡} Y \in TopOn (Y)$
15	12 13 14	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to J ↾_{𝑡} Y \in TopOn (Y)$
16	2 15	eqeltrid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to K \in TopOn (Y)$
17		topontop	$⊢ K \in TopOn (Y) \to K \in Top$
18	16 17	syl	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to K \in Top$
19		toponuni	$⊢ K \in TopOn (Y) \to Y = ⋃ K$
20	16 19	syl	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to Y = ⋃ K$
21	3 20	sseqtrd	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq ⋃ K$
22		eqid	$⊢ ⋃ K = ⋃ K$
23	22	islp	$⊢ (K \in Top \land S \subseteq ⋃ K) \to (x \in limPt (K) (S) \leftrightarrow x \in cls (K) (S ∖ \{x\}))$
24	18 21 23	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (x \in limPt (K) (S) \leftrightarrow x \in cls (K) (S ∖ \{x\}))$
25		elin	$⊢ x \in (limPt (J) (S) \cap Y) \leftrightarrow (x \in limPt (J) (S) \land x \in Y)$
26	3 13	sstrd	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to S \subseteq X$
27	1	islp	$⊢ (J \in Top \land S \subseteq X) \to (x \in limPt (J) (S) \leftrightarrow x \in cls (J) (S ∖ \{x\}))$
28	10 26 27	syl2anc	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (x \in limPt (J) (S) \leftrightarrow x \in cls (J) (S ∖ \{x\}))$
29	28	anbi1d	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to ((x \in limPt (J) (S) \land x \in Y) \leftrightarrow (x \in cls (J) (S ∖ \{x\}) \land x \in Y))$
30	25 29	bitrid	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (x \in (limPt (J) (S) \cap Y) \leftrightarrow (x \in cls (J) (S ∖ \{x\}) \land x \in Y))$
31	9 24 30	3bitr4d	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to (x \in limPt (K) (S) \leftrightarrow x \in (limPt (J) (S) \cap Y))$
32	31	eqrdv	$⊢ (J \in Top \land Y \subseteq X \land S \subseteq Y) \to limPt (K) (S) = limPt (J) (S) \cap Y$

Metamath Proof Explorer

Theorem restlp

Proof