Theorem eltg3i

Description: The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015)

	Ref	Expression
Assertion	eltg3i	|- ( ( B e. V /\ A C_ B ) -> U. A e. ( topGen ` B ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( B e. V /\ A C_ B ) -> A C_ B )
2		pwuni	|- A C_ ~P U. A
3		ssin	|- ( ( A C_ B /\ A C_ ~P U. A ) <-> A C_ ( B i^i ~P U. A ) )
4	1 2 3	sylanblc	|- ( ( B e. V /\ A C_ B ) -> A C_ ( B i^i ~P U. A ) )
5	4	unissd	|- ( ( B e. V /\ A C_ B ) -> U. A C_ U. ( B i^i ~P U. A ) )
6		eltg	|- ( B e. V -> ( U. A e. ( topGen ` B ) <-> U. A C_ U. ( B i^i ~P U. A ) ) )
7	6	adantr	|- ( ( B e. V /\ A C_ B ) -> ( U. A e. ( topGen ` B ) <-> U. A C_ U. ( B i^i ~P U. A ) ) )
8	5 7	mpbird	|- ( ( B e. V /\ A C_ B ) -> U. A e. ( topGen ` B ) )