Theorem 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 \bigcup \mathrm{topGen}\left(B\right)=\bigcup B$$

Proof

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