Theorem tgiun

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

	Ref	Expression
Assertion	tgiun	|- ( ( B e. V /\ A. x e. A C e. B ) -> U_ x e. A C e. ( topGen ` B ) )

Proof

Step	Hyp	Ref	Expression
1		dfiun3g	|- ( A. x e. A C e. B -> U_ x e. A C = U. ran ( x e. A |-> C ) )
2	1	adantl	|- ( ( B e. V /\ A. x e. A C e. B ) -> U_ x e. A C = U. ran ( x e. A |-> C ) )
3		eqid	|- ( x e. A |-> C ) = ( x e. A |-> C )
4	3	rnmptss	|- ( A. x e. A C e. B -> ran ( x e. A |-> C ) C_ B )
5		eltg3i	|- ( ( B e. V /\ ran ( x e. A |-> C ) C_ B ) -> U. ran ( x e. A |-> C ) e. ( topGen ` B ) )
6	4 5	sylan2	|- ( ( B e. V /\ A. x e. A C e. B ) -> U. ran ( x e. A |-> C ) e. ( topGen ` B ) )
7	2 6	eqeltrd	|- ( ( B e. V /\ A. x e. A C e. B ) -> U_ x e. A C e. ( topGen ` B ) )