This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgval

Description: The topology generated by a basis. See also tgval2 and tgval3 . (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

		Ref	Expression
	Assertion	tgval	$⊢ B \in V \to topGen (B) = \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\}$

Proof

Step	Hyp	Ref	Expression
1		df-topgen	$⊢ topGen = (y \in V ⟼ \{x \| x \subseteq ⋃ (y \cap 𝒫 x)\})$
2		ineq1	$⊢ y = B \to y \cap 𝒫 x = B \cap 𝒫 x$
3	2	unieqd	$⊢ y = B \to ⋃ (y \cap 𝒫 x) = ⋃ (B \cap 𝒫 x)$
4	3	sseq2d	$⊢ y = B \to (x \subseteq ⋃ (y \cap 𝒫 x) \leftrightarrow x \subseteq ⋃ (B \cap 𝒫 x))$
5	4	abbidv	$⊢ y = B \to \{x \| x \subseteq ⋃ (y \cap 𝒫 x)\} = \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\}$
6		elex	$⊢ B \in V \to B \in V$
7		uniexg	$⊢ B \in V \to ⋃ B \in V$
8		abssexg	$⊢ ⋃ B \in V \to \{x \| (x \subseteq ⋃ B \land x \subseteq ⋃ 𝒫 x)\} \in V$
9		uniin	$⊢ ⋃ (B \cap 𝒫 x) \subseteq ⋃ B \cap ⋃ 𝒫 x$
10		sstr	$⊢ (x \subseteq ⋃ (B \cap 𝒫 x) \land ⋃ (B \cap 𝒫 x) \subseteq ⋃ B \cap ⋃ 𝒫 x) \to x \subseteq ⋃ B \cap ⋃ 𝒫 x$
11	9 10	mpan2	$⊢ x \subseteq ⋃ (B \cap 𝒫 x) \to x \subseteq ⋃ B \cap ⋃ 𝒫 x$
12		ssin	$⊢ (x \subseteq ⋃ B \land x \subseteq ⋃ 𝒫 x) \leftrightarrow x \subseteq ⋃ B \cap ⋃ 𝒫 x$
13	11 12	sylibr	$⊢ x \subseteq ⋃ (B \cap 𝒫 x) \to (x \subseteq ⋃ B \land x \subseteq ⋃ 𝒫 x)$
14	13	ss2abi	$⊢ \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\} \subseteq \{x \| (x \subseteq ⋃ B \land x \subseteq ⋃ 𝒫 x)\}$
15		ssexg	$⊢ (\{x \| x \subseteq ⋃ (B \cap 𝒫 x)\} \subseteq \{x \| (x \subseteq ⋃ B \land x \subseteq ⋃ 𝒫 x)\} \land \{x \| (x \subseteq ⋃ B \land x \subseteq ⋃ 𝒫 x)\} \in V) \to \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\} \in V$
16	14 15	mpan	$⊢ \{x \| (x \subseteq ⋃ B \land x \subseteq ⋃ 𝒫 x)\} \in V \to \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\} \in V$
17	7 8 16	3syl	$⊢ B \in V \to \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\} \in V$
18	1 5 6 17	fvmptd3	$⊢ B \in V \to topGen (B) = \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\}$