unitg

Description: The topology generated by a basis B is a topology on U. B . Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class TopBases completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006) (Proof shortened by OpenAI, 30-Mar-2020)

		Ref	Expression
	Assertion	unitg	$⊢ B \in V \to ⋃ topGen (B) = ⋃ B$

Proof

Step	Hyp	Ref	Expression
1		tg1	$⊢ x \in topGen (B) \to x \subseteq ⋃ B$
2		velpw	$⊢ x \in 𝒫 ⋃ B \leftrightarrow x \subseteq ⋃ B$
3	1 2	sylibr	$⊢ x \in topGen (B) \to x \in 𝒫 ⋃ B$
4	3	ssriv	$⊢ topGen (B) \subseteq 𝒫 ⋃ B$
5		sspwuni	$⊢ topGen (B) \subseteq 𝒫 ⋃ B \leftrightarrow ⋃ topGen (B) \subseteq ⋃ B$
6	4 5	mpbi	$⊢ ⋃ topGen (B) \subseteq ⋃ B$
7	6	a1i	$⊢ B \in V \to ⋃ topGen (B) \subseteq ⋃ B$
8		bastg	$⊢ B \in V \to B \subseteq topGen (B)$
9	8	unissd	$⊢ B \in V \to ⋃ B \subseteq ⋃ topGen (B)$
10	7 9	eqssd	$⊢ B \in V \to ⋃ topGen (B) = ⋃ B$

Metamath Proof Explorer

Theorem unitg

Proof