Theorem eltg4i

Description: An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Assertion	eltg4i	|- ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	|- ( A e. ( topGen ` B ) -> B e. dom topGen )
2		eltg	|- ( B e. dom topGen -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )
3	1 2	syl	|- ( A e. ( topGen ` B ) -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )
4	3	ibi	|- ( A e. ( topGen ` B ) -> A C_ U. ( B i^i ~P A ) )
5		inss2	|- ( B i^i ~P A ) C_ ~P A
6	5	unissi	|- U. ( B i^i ~P A ) C_ U. ~P A
7		unipw	|- U. ~P A = A
8	6 7	sseqtri	|- U. ( B i^i ~P A ) C_ A
9	8	a1i	|- ( A e. ( topGen ` B ) -> U. ( B i^i ~P A ) C_ A )
10	4 9	eqssd	|- ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) )