islp2

Description: The predicate " P is a limit point of S " in terms of neighborhoods. Definition of limit point in Munkres p. 97. Although Munkres uses open neighborhoods, it also works for our more general neighborhoods. (Contributed by NM, 26-Feb-2007) (Proof shortened by Mario Carneiro, 25-Dec-2016)

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

Proof

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		ssdifss	$⊢ S \subseteq X \to S ∖ \{P\} \subseteq X$
5	1	neindisj2	$⊢ (J \in Top \land S ∖ \{P\} \subseteq X \land P \in X) \to (P \in cls (J) (S ∖ \{P\}) \leftrightarrow \forall n \in nei (J) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset)$
6	4 5	syl3an2	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in cls (J) (S ∖ \{P\}) \leftrightarrow \forall n \in nei (J) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset)$
7	3 6	bitrd	$⊢ (J \in Top \land S \subseteq X \land P \in X) \to (P \in limPt (J) (S) \leftrightarrow \forall n \in nei (J) (\{P\}) n \cap (S ∖ \{P\}) \neq \emptyset)$

Metamath Proof Explorer

Theorem islp2

Proof