neiint

Description: An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		neifval.1	$⊢ X = ⋃ J$
2	1	isnei	$⊢ (J \in Top \land S \subseteq X) \to (N \in nei (J) (S) \leftrightarrow (N \subseteq X \land \exists v \in J (S \subseteq v \land v \subseteq N)))$
3	2	3adant3	$⊢ (J \in Top \land S \subseteq X \land N \subseteq X) \to (N \in nei (J) (S) \leftrightarrow (N \subseteq X \land \exists v \in J (S \subseteq v \land v \subseteq N)))$
4	3	3anibar	$⊢ (J \in Top \land S \subseteq X \land N \subseteq X) \to (N \in nei (J) (S) \leftrightarrow \exists v \in J (S \subseteq v \land v \subseteq N))$
5		simprrl	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land (v \in J \land (S \subseteq v \land v \subseteq N))) \to S \subseteq v$
6	1	ssntr	$⊢ ((J \in Top \land N \subseteq X) \land (v \in J \land v \subseteq N)) \to v \subseteq int (J) (N)$
7	6	3adantl2	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land (v \in J \land v \subseteq N)) \to v \subseteq int (J) (N)$
8	7	adantrrl	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land (v \in J \land (S \subseteq v \land v \subseteq N))) \to v \subseteq int (J) (N)$
9	5 8	sstrd	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land (v \in J \land (S \subseteq v \land v \subseteq N))) \to S \subseteq int (J) (N)$
10	9	rexlimdvaa	$⊢ (J \in Top \land S \subseteq X \land N \subseteq X) \to (\exists v \in J (S \subseteq v \land v \subseteq N) \to S \subseteq int (J) (N))$
11		simpl1	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land S \subseteq int (J) (N)) \to J \in Top$
12		simpl3	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land S \subseteq int (J) (N)) \to N \subseteq X$
13	1	ntropn	$⊢ (J \in Top \land N \subseteq X) \to int (J) (N) \in J$
14	11 12 13	syl2anc	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land S \subseteq int (J) (N)) \to int (J) (N) \in J$
15		simpr	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land S \subseteq int (J) (N)) \to S \subseteq int (J) (N)$
16	1	ntrss2	$⊢ (J \in Top \land N \subseteq X) \to int (J) (N) \subseteq N$
17	11 12 16	syl2anc	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land S \subseteq int (J) (N)) \to int (J) (N) \subseteq N$
18		sseq2	$⊢ v = int (J) (N) \to (S \subseteq v \leftrightarrow S \subseteq int (J) (N))$
19		sseq1	$⊢ v = int (J) (N) \to (v \subseteq N \leftrightarrow int (J) (N) \subseteq N)$
20	18 19	anbi12d	$⊢ v = int (J) (N) \to ((S \subseteq v \land v \subseteq N) \leftrightarrow (S \subseteq int (J) (N) \land int (J) (N) \subseteq N))$
21	20	rspcev	$⊢ (int (J) (N) \in J \land (S \subseteq int (J) (N) \land int (J) (N) \subseteq N)) \to \exists v \in J (S \subseteq v \land v \subseteq N)$
22	14 15 17 21	syl12anc	$⊢ ((J \in Top \land S \subseteq X \land N \subseteq X) \land S \subseteq int (J) (N)) \to \exists v \in J (S \subseteq v \land v \subseteq N)$
23	22	ex	$⊢ (J \in Top \land S \subseteq X \land N \subseteq X) \to (S \subseteq int (J) (N) \to \exists v \in J (S \subseteq v \land v \subseteq N))$
24	10 23	impbid	$⊢ (J \in Top \land S \subseteq X \land N \subseteq X) \to (\exists v \in J (S \subseteq v \land v \subseteq N) \leftrightarrow S \subseteq int (J) (N))$
25	4 24	bitrd	$⊢ (J \in Top \land S \subseteq X \land N \subseteq X) \to (N \in nei (J) (S) \leftrightarrow S \subseteq int (J) (N))$

Metamath Proof Explorer

Theorem neiint

Proof