Metamath Proof Explorer

Theorem opnneissb

Description: An open set is a neighborhood of any of its subsets. (Contributed by FL, 2-Oct-2006)

		Ref	Expression
	Hypothesis	neips.1	$⊢ X = ⋃ J$
	Assertion	opnneissb	$⊢ (J \in Top \land N \in J \land S \subseteq X) \to (S \subseteq N \leftrightarrow N \in nei (J) (S))$

Proof

Step	Hyp	Ref	Expression
1		neips.1	$⊢ X = ⋃ J$
2	1	eltopss	$⊢ (J \in Top \land N \in J) \to N \subseteq X$
3	2	adantr	$⊢ ((J \in Top \land N \in J) \land (S \subseteq X \land S \subseteq N)) \to N \subseteq X$
4		ssid	$⊢ N \subseteq N$
5		sseq2	$⊢ g = N \to (S \subseteq g \leftrightarrow S \subseteq N)$
6		sseq1	$⊢ g = N \to (g \subseteq N \leftrightarrow N \subseteq N)$
7	5 6	anbi12d	$⊢ g = N \to ((S \subseteq g \land g \subseteq N) \leftrightarrow (S \subseteq N \land N \subseteq N))$
8	7	rspcev	$⊢ (N \in J \land (S \subseteq N \land N \subseteq N)) \to \exists g \in J (S \subseteq g \land g \subseteq N)$
9	4 8	mpanr2	$⊢ (N \in J \land S \subseteq N) \to \exists g \in J (S \subseteq g \land g \subseteq N)$
10	9	ad2ant2l	$⊢ ((J \in Top \land N \in J) \land (S \subseteq X \land S \subseteq N)) \to \exists g \in J (S \subseteq g \land g \subseteq N)$
11	1	isnei	$⊢ (J \in Top \land S \subseteq X) \to (N \in nei (J) (S) \leftrightarrow (N \subseteq X \land \exists g \in J (S \subseteq g \land g \subseteq N)))$
12	11	ad2ant2r	$⊢ ((J \in Top \land N \in J) \land (S \subseteq X \land S \subseteq N)) \to (N \in nei (J) (S) \leftrightarrow (N \subseteq X \land \exists g \in J (S \subseteq g \land g \subseteq N)))$
13	3 10 12	mpbir2and	$⊢ ((J \in Top \land N \in J) \land (S \subseteq X \land S \subseteq N)) \to N \in nei (J) (S)$
14	13	exp43	$⊢ J \in Top \to (N \in J \to (S \subseteq X \to (S \subseteq N \to N \in nei (J) (S))))$
15	14	3imp	$⊢ (J \in Top \land N \in J \land S \subseteq X) \to (S \subseteq N \to N \in nei (J) (S))$
16		ssnei	$⊢ (J \in Top \land N \in nei (J) (S)) \to S \subseteq N$
17	16	ex	$⊢ J \in Top \to (N \in nei (J) (S) \to S \subseteq N)$
18	17	3ad2ant1	$⊢ (J \in Top \land N \in J \land S \subseteq X) \to (N \in nei (J) (S) \to S \subseteq N)$
19	15 18	impbid	$⊢ (J \in Top \land N \in J \land S \subseteq X) \to (S \subseteq N \leftrightarrow N \in nei (J) (S))$