isneip

Description: The predicate "the class N is a neighborhood of point P ". (Contributed by NM, 26-Feb-2007)

		Ref	Expression
	Hypothesis	neifval.1	$⊢ X = ⋃ J$
	Assertion	isneip	$⊢ (J \in Top \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists g \in J (P \in g \land g \subseteq N)))$

Step	Hyp	Ref	Expression
1		neifval.1	$⊢ X = ⋃ J$
2		snssi	$⊢ P \in X \to \{P\} \subseteq X$
3	1	isnei	$⊢ (J \in Top \land \{P\} \subseteq X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists g \in J (\{P\} \subseteq g \land g \subseteq N)))$
4	2 3	sylan2	$⊢ (J \in Top \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists g \in J (\{P\} \subseteq g \land g \subseteq N)))$
5		snssg	$⊢ P \in X \to (P \in g \leftrightarrow \{P\} \subseteq g)$
6	5	anbi1d	$⊢ P \in X \to ((P \in g \land g \subseteq N) \leftrightarrow (\{P\} \subseteq g \land g \subseteq N))$
7	6	rexbidv	$⊢ P \in X \to (\exists g \in J (P \in g \land g \subseteq N) \leftrightarrow \exists g \in J (\{P\} \subseteq g \land g \subseteq N))$
8	7	anbi2d	$⊢ P \in X \to ((N \subseteq X \land \exists g \in J (P \in g \land g \subseteq N)) \leftrightarrow (N \subseteq X \land \exists g \in J (\{P\} \subseteq g \land g \subseteq N)))$
9	8	adantl	$⊢ (J \in Top \land P \in X) \to ((N \subseteq X \land \exists g \in J (P \in g \land g \subseteq N)) \leftrightarrow (N \subseteq X \land \exists g \in J (\{P\} \subseteq g \land g \subseteq N)))$
10	4 9	bitr4d	$⊢ (J \in Top \land P \in X) \to (N \in nei (J) (\{P\}) \leftrightarrow (N \subseteq X \land \exists g \in J (P \in g \land g \subseteq N)))$

Metamath Proof Explorer