islp

Description: The predicate "the class P is a limit point of S ". (Contributed by NM, 10-Feb-2007)

		Ref	Expression
	Hypothesis	lpfval.1	$⊢ X = ⋃ J$
	Assertion	islp	$⊢ (J \in Top \land S \subseteq X) \to (P \in limPt (J) (S) \leftrightarrow P \in cls (J) (S ∖ \{P\}))$

Step	Hyp	Ref	Expression
1		lpfval.1	$⊢ X = ⋃ J$
2	1	lpval	$⊢ (J \in Top \land S \subseteq X) \to limPt (J) (S) = \{x \| x \in cls (J) (S ∖ \{x\})\}$
3	2	eleq2d	$⊢ (J \in Top \land S \subseteq X) \to (P \in limPt (J) (S) \leftrightarrow P \in \{x \| x \in cls (J) (S ∖ \{x\})\})$
4		id	$⊢ P \in cls (J) (S ∖ \{P\}) \to P \in cls (J) (S ∖ \{P\})$
5		id	$⊢ x = P \to x = P$
6		sneq	$⊢ x = P \to \{x\} = \{P\}$
7	6	difeq2d	$⊢ x = P \to S ∖ \{x\} = S ∖ \{P\}$
8	7	fveq2d	$⊢ x = P \to cls (J) (S ∖ \{x\}) = cls (J) (S ∖ \{P\})$
9	5 8	eleq12d	$⊢ x = P \to (x \in cls (J) (S ∖ \{x\}) \leftrightarrow P \in cls (J) (S ∖ \{P\}))$
10	4 9	elab3	$⊢ P \in \{x \| x \in cls (J) (S ∖ \{x\})\} \leftrightarrow P \in cls (J) (S ∖ \{P\})$
11	3 10	bitrdi	$⊢ (J \in Top \land S \subseteq X) \to (P \in limPt (J) (S) \leftrightarrow P \in cls (J) (S ∖ \{P\}))$

Metamath Proof Explorer