Metamath Proof Explorer


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 ) )