islp3

Description: The predicate " P is a limit point of S " in terms of open sets. see islp2 , elcls , islp . (Contributed by FL, 31-Jul-2009)

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	islp3	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in limPt (J) (S) \leftrightarrow \forall x \in J (P \in x \to x \cap (S ∖ \{P\}) \neq \emptyset))$

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	islp	$⊢ (J \in Top \land S \subseteq X) \to (P \in limPt (J) (S) \leftrightarrow P \in cls (J) (S ∖ \{P\}))$
3	2	3adant3	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in limPt (J) (S) \leftrightarrow P \in cls (J) (S ∖ \{P\}))$
4		simp2	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to S \subseteq X$
5	4	ssdifssd	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to S ∖ \{P\} \subseteq X$
6	1	elcls	$⊢ (J \in Top \land S ∖ \{P\} \subseteq X \land P \in X) \to (P \in cls (J) (S ∖ \{P\}) \leftrightarrow \forall x \in J (P \in x \to x \cap (S ∖ \{P\}) \neq \emptyset))$
7	5 6	syld3an2	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in cls (J) (S ∖ \{P\}) \leftrightarrow \forall x \in J (P \in x \to x \cap (S ∖ \{P\}) \neq \emptyset))$
8	3 7	bitrd	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in limPt (J) (S) \leftrightarrow \forall x \in J (P \in x \to x \cap (S ∖ \{P\}) \neq \emptyset))$

Metamath Proof Explorer