Metamath Proof Explorer

Theorem lpss3

Description: Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016)

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	lpss3	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to limPt (J) (T) \subseteq limPt (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2		simp1	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to J \in Top$
3		simp2	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to S \subseteq X$
4	3	ssdifssd	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to S ∖ \{x\} \subseteq X$
5		simp3	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to T \subseteq S$
6	5	ssdifd	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to T ∖ \{x\} \subseteq S ∖ \{x\}$
7	1	clsss	$⊢ (J \in Top \land S ∖ \{x\} \subseteq X \land T ∖ \{x\} \subseteq S ∖ \{x\}) \to cls (J) (T ∖ \{x\}) \subseteq cls (J) (S ∖ \{x\})$
8	2 4 6 7	syl3anc	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to cls (J) (T ∖ \{x\}) \subseteq cls (J) (S ∖ \{x\})$
9	8	sseld	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to (x \in cls (J) (T ∖ \{x\}) \to x \in cls (J) (S ∖ \{x\}))$
10	5 3	sstrd	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to T \subseteq X$
11	1	islp	$⊢ (J \in Top \land T \subseteq X) \to (x \in limPt (J) (T) \leftrightarrow x \in cls (J) (T ∖ \{x\}))$
12	2 10 11	syl2anc	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to (x \in limPt (J) (T) \leftrightarrow x \in cls (J) (T ∖ \{x\}))$
13	1	islp	$⊢ (J \in Top \land S \subseteq X) \to (x \in limPt (J) (S) \leftrightarrow x \in cls (J) (S ∖ \{x\}))$
14	2 3 13	syl2anc	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to (x \in limPt (J) (S) \leftrightarrow x \in cls (J) (S ∖ \{x\}))$
15	9 12 14	3imtr4d	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to (x \in limPt (J) (T) \to x \in limPt (J) (S))$
16	15	ssrdv	$⊢ (J \in Top \land S \subseteq X \land T \subseteq S) \to limPt (J) (T) \subseteq limPt (J) (S)$