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

Metamath Proof Explorer

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