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 e. V -> U. ( topGen ` B ) = U. B )

Proof

Step	Hyp	Ref	Expression
1		tg1	|- ( x e. ( topGen ` B ) -> x C_ U. B )
2		velpw	|- ( x e. ~P U. B <-> x C_ U. B )
3	1 2	sylibr	|- ( x e. ( topGen ` B ) -> x e. ~P U. B )
4	3	ssriv	|- ( topGen ` B ) C_ ~P U. B
5		sspwuni	|- ( ( topGen ` B ) C_ ~P U. B <-> U. ( topGen ` B ) C_ U. B )
6	4 5	mpbi	|- U. ( topGen ` B ) C_ U. B
7	6	a1i	|- ( B e. V -> U. ( topGen ` B ) C_ U. B )
8		bastg	|- ( B e. V -> B C_ ( topGen ` B ) )
9	8	unissd	|- ( B e. V -> U. B C_ U. ( topGen ` B ) )
10	7 9	eqssd	|- ( B e. V -> U. ( topGen ` B ) = U. B )