Theorem tgtopon

Description: A basis generates a topology on U. B . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	tgtopon	$$⊢B\in \mathrm{TopBases}\to \mathrm{topGen}\left(B\right)\in \mathrm{TopOn}\left(\bigcup B\right)$$

Proof

Step	Hyp	Ref	Expression
1		tgcl	$$⊢B\in \mathrm{TopBases}\to \mathrm{topGen}\left(B\right)\in \mathrm{Top}$$
2		unitg	$$⊢B\in \mathrm{TopBases}\to \bigcup \mathrm{topGen}\left(B\right)=\bigcup B$$
3	2	eqcomd	$$⊢B\in \mathrm{TopBases}\to \bigcup B=\bigcup \mathrm{topGen}\left(B\right)$$
4		istopon	$$⊢\mathrm{topGen}\left(B\right)\in \mathrm{TopOn}\left(\bigcup B\right)\leftrightarrow \left(\mathrm{topGen}\left(B\right)\in \mathrm{Top}\wedge \bigcup B=\bigcup \mathrm{topGen}\left(B\right)\right)$$
5	1 3 4	sylanbrc	$$⊢B\in \mathrm{TopBases}\to \mathrm{topGen}\left(B\right)\in \mathrm{TopOn}\left(\bigcup B\right)$$