This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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