neifg

Description: The neighborhood filter of a nonempty set is generated by its open supersets. See comments for opnfbas . (Contributed by Jeff Hankins, 3-Sep-2009)

		Ref	Expression
	Hypothesis	neifg.1	$⊢ X = ⋃ J$
	Assertion	neifg	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to X filGen \{x \in J \| S \subseteq x\} = nei (J) (S)$

Proof

Step	Hyp	Ref	Expression
1		neifg.1	$⊢ X = ⋃ J$
2	1	opnfbas	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \{x \in J \| S \subseteq x\} \in fBas (X)$
3		fgval	$⊢ \{x \in J \| S \subseteq x\} \in fBas (X) \to X filGen \{x \in J \| S \subseteq x\} = \{t \in 𝒫 X \| \{x \in J \| S \subseteq x\} \cap 𝒫 t \neq \emptyset\}$
4	2 3	syl	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to X filGen \{x \in J \| S \subseteq x\} = \{t \in 𝒫 X \| \{x \in J \| S \subseteq x\} \cap 𝒫 t \neq \emptyset\}$
5		pweq	$⊢ t = u \to 𝒫 t = 𝒫 u$
6	5	ineq2d	$⊢ t = u \to \{x \in J \| S \subseteq x\} \cap 𝒫 t = \{x \in J \| S \subseteq x\} \cap 𝒫 u$
7	6	neeq1d	$⊢ t = u \to (\{x \in J \| S \subseteq x\} \cap 𝒫 t \neq \emptyset \leftrightarrow \{x \in J \| S \subseteq x\} \cap 𝒫 u \neq \emptyset)$
8	7	elrab	$⊢ u \in \{t \in 𝒫 X \| \{x \in J \| S \subseteq x\} \cap 𝒫 t \neq \emptyset\} \leftrightarrow (u \in 𝒫 X \land \{x \in J \| S \subseteq x\} \cap 𝒫 u \neq \emptyset)$
9		velpw	$⊢ u \in 𝒫 X \leftrightarrow u \subseteq X$
10	9	a1i	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (u \in 𝒫 X \leftrightarrow u \subseteq X)$
11		n0	$⊢ \{x \in J \| S \subseteq x\} \cap 𝒫 u \neq \emptyset \leftrightarrow \exists z z \in (\{x \in J \| S \subseteq x\} \cap 𝒫 u)$
12		elin	$⊢ z \in (\{x \in J \| S \subseteq x\} \cap 𝒫 u) \leftrightarrow (z \in \{x \in J \| S \subseteq x\} \land z \in 𝒫 u)$
13		sseq2	$⊢ x = z \to (S \subseteq x \leftrightarrow S \subseteq z)$
14	13	elrab	$⊢ z \in \{x \in J \| S \subseteq x\} \leftrightarrow (z \in J \land S \subseteq z)$
15		velpw	$⊢ z \in 𝒫 u \leftrightarrow z \subseteq u$
16	14 15	anbi12i	$⊢ (z \in \{x \in J \| S \subseteq x\} \land z \in 𝒫 u) \leftrightarrow ((z \in J \land S \subseteq z) \land z \subseteq u)$
17	12 16	bitri	$⊢ z \in (\{x \in J \| S \subseteq x\} \cap 𝒫 u) \leftrightarrow ((z \in J \land S \subseteq z) \land z \subseteq u)$
18	17	exbii	$⊢ \exists z z \in (\{x \in J \| S \subseteq x\} \cap 𝒫 u) \leftrightarrow \exists z ((z \in J \land S \subseteq z) \land z \subseteq u)$
19	11 18	bitri	$⊢ \{x \in J \| S \subseteq x\} \cap 𝒫 u \neq \emptyset \leftrightarrow \exists z ((z \in J \land S \subseteq z) \land z \subseteq u)$
20	19	a1i	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (\{x \in J \| S \subseteq x\} \cap 𝒫 u \neq \emptyset \leftrightarrow \exists z ((z \in J \land S \subseteq z) \land z \subseteq u))$
21	10 20	anbi12d	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to ((u \in 𝒫 X \land \{x \in J \| S \subseteq x\} \cap 𝒫 u \neq \emptyset) \leftrightarrow (u \subseteq X \land \exists z ((z \in J \land S \subseteq z) \land z \subseteq u)))$
22		anass	$⊢ ((z \in J \land S \subseteq z) \land z \subseteq u) \leftrightarrow (z \in J \land (S \subseteq z \land z \subseteq u))$
23	22	exbii	$⊢ \exists z ((z \in J \land S \subseteq z) \land z \subseteq u) \leftrightarrow \exists z (z \in J \land (S \subseteq z \land z \subseteq u))$
24		df-rex	$⊢ \exists z \in J (S \subseteq z \land z \subseteq u) \leftrightarrow \exists z (z \in J \land (S \subseteq z \land z \subseteq u))$
25	23 24	bitr4i	$⊢ \exists z ((z \in J \land S \subseteq z) \land z \subseteq u) \leftrightarrow \exists z \in J (S \subseteq z \land z \subseteq u)$
26	25	anbi2i	$⊢ (u \subseteq X \land \exists z ((z \in J \land S \subseteq z) \land z \subseteq u)) \leftrightarrow (u \subseteq X \land \exists z \in J (S \subseteq z \land z \subseteq u))$
27	1	isnei	$⊢ (J \in Top \land S \subseteq X) \to (u \in nei (J) (S) \leftrightarrow (u \subseteq X \land \exists z \in J (S \subseteq z \land z \subseteq u)))$
28	27	3adant3	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (u \in nei (J) (S) \leftrightarrow (u \subseteq X \land \exists z \in J (S \subseteq z \land z \subseteq u)))$
29	26 28	bitr4id	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to ((u \subseteq X \land \exists z ((z \in J \land S \subseteq z) \land z \subseteq u)) \leftrightarrow u \in nei (J) (S))$
30	21 29	bitrd	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to ((u \in 𝒫 X \land \{x \in J \| S \subseteq x\} \cap 𝒫 u \neq \emptyset) \leftrightarrow u \in nei (J) (S))$
31	8 30	bitrid	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to (u \in \{t \in 𝒫 X \| \{x \in J \| S \subseteq x\} \cap 𝒫 t \neq \emptyset\} \leftrightarrow u \in nei (J) (S))$
32	31	eqrdv	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to \{t \in 𝒫 X \| \{x \in J \| S \subseteq x\} \cap 𝒫 t \neq \emptyset\} = nei (J) (S)$
33	4 32	eqtrd	$⊢ (J \in Top \land S \subseteq X \land S \neq \emptyset) \to X filGen \{x \in J \| S \subseteq x\} = nei (J) (S)$

Metamath Proof Explorer

Theorem neifg

Proof