tgval2

Description: Definition of a topology generated by a basis in Munkres p. 78. Later we show (in tgcl ) that ( topGenB ) is indeed a topology (on U. B , see unitg ). See also tgval and tgval3 . (Contributed by NM, 15-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

		Ref	Expression
	Assertion	tgval2	$⊢ B \in V \to topGen (B) = \{x \| (x \subseteq ⋃ B \land \forall y \in x \exists z \in B (y \in z \land z \subseteq x))\}$

Proof

Step	Hyp	Ref	Expression
1		tgval	$⊢ B \in V \to topGen (B) = \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\}$
2		inss1	$⊢ B \cap 𝒫 x \subseteq B$
3	2	unissi	$⊢ ⋃ (B \cap 𝒫 x) \subseteq ⋃ B$
4	3	sseli	$⊢ y \in ⋃ (B \cap 𝒫 x) \to y \in ⋃ B$
5	4	pm4.71ri	$⊢ y \in ⋃ (B \cap 𝒫 x) \leftrightarrow (y \in ⋃ B \land y \in ⋃ (B \cap 𝒫 x))$
6	5	ralbii	$⊢ \forall y \in x y \in ⋃ (B \cap 𝒫 x) \leftrightarrow \forall y \in x (y \in ⋃ B \land y \in ⋃ (B \cap 𝒫 x))$
7		r19.26	$⊢ \forall y \in x (y \in ⋃ B \land y \in ⋃ (B \cap 𝒫 x)) \leftrightarrow (\forall y \in x y \in ⋃ B \land \forall y \in x y \in ⋃ (B \cap 𝒫 x))$
8	6 7	bitri	$⊢ \forall y \in x y \in ⋃ (B \cap 𝒫 x) \leftrightarrow (\forall y \in x y \in ⋃ B \land \forall y \in x y \in ⋃ (B \cap 𝒫 x))$
9		dfss3	$⊢ x \subseteq ⋃ (B \cap 𝒫 x) \leftrightarrow \forall y \in x y \in ⋃ (B \cap 𝒫 x)$
10		dfss3	$⊢ x \subseteq ⋃ B \leftrightarrow \forall y \in x y \in ⋃ B$
11		elin	$⊢ z \in (B \cap 𝒫 x) \leftrightarrow (z \in B \land z \in 𝒫 x)$
12	11	anbi2i	$⊢ (y \in z \land z \in (B \cap 𝒫 x)) \leftrightarrow (y \in z \land (z \in B \land z \in 𝒫 x))$
13		an12	$⊢ (y \in z \land (z \in B \land z \in 𝒫 x)) \leftrightarrow (z \in B \land (y \in z \land z \in 𝒫 x))$
14	12 13	bitri	$⊢ (y \in z \land z \in (B \cap 𝒫 x)) \leftrightarrow (z \in B \land (y \in z \land z \in 𝒫 x))$
15	14	exbii	$⊢ \exists z (y \in z \land z \in (B \cap 𝒫 x)) \leftrightarrow \exists z (z \in B \land (y \in z \land z \in 𝒫 x))$
16		eluni	$⊢ y \in ⋃ (B \cap 𝒫 x) \leftrightarrow \exists z (y \in z \land z \in (B \cap 𝒫 x))$
17		df-rex	$⊢ \exists z \in B (y \in z \land z \in 𝒫 x) \leftrightarrow \exists z (z \in B \land (y \in z \land z \in 𝒫 x))$
18	15 16 17	3bitr4i	$⊢ y \in ⋃ (B \cap 𝒫 x) \leftrightarrow \exists z \in B (y \in z \land z \in 𝒫 x)$
19		velpw	$⊢ z \in 𝒫 x \leftrightarrow z \subseteq x$
20	19	anbi2i	$⊢ (y \in z \land z \in 𝒫 x) \leftrightarrow (y \in z \land z \subseteq x)$
21	20	rexbii	$⊢ \exists z \in B (y \in z \land z \in 𝒫 x) \leftrightarrow \exists z \in B (y \in z \land z \subseteq x)$
22	18 21	bitr2i	$⊢ \exists z \in B (y \in z \land z \subseteq x) \leftrightarrow y \in ⋃ (B \cap 𝒫 x)$
23	22	ralbii	$⊢ \forall y \in x \exists z \in B (y \in z \land z \subseteq x) \leftrightarrow \forall y \in x y \in ⋃ (B \cap 𝒫 x)$
24	10 23	anbi12i	$⊢ (x \subseteq ⋃ B \land \forall y \in x \exists z \in B (y \in z \land z \subseteq x)) \leftrightarrow (\forall y \in x y \in ⋃ B \land \forall y \in x y \in ⋃ (B \cap 𝒫 x))$
25	8 9 24	3bitr4i	$⊢ x \subseteq ⋃ (B \cap 𝒫 x) \leftrightarrow (x \subseteq ⋃ B \land \forall y \in x \exists z \in B (y \in z \land z \subseteq x))$
26	25	abbii	$⊢ \{x \| x \subseteq ⋃ (B \cap 𝒫 x)\} = \{x \| (x \subseteq ⋃ B \land \forall y \in x \exists z \in B (y \in z \land z \subseteq x))\}$
27	1 26	eqtrdi	$⊢ B \in V \to topGen (B) = \{x \| (x \subseteq ⋃ B \land \forall y \in x \exists z \in B (y \in z \land z \subseteq x))\}$

Metamath Proof Explorer

Theorem tgval2

Proof