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

Metamath Proof Explorer

Theorem eltg4i

Description: An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion eltg4i 
|- ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) )

Proof

Step Hyp Ref Expression
1 elfvdm 
 |-  ( A e. ( topGen ` B ) -> B e. dom topGen )
2 eltg 
 |-  ( B e. dom topGen -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )
3 1 2 syl 
 |-  ( A e. ( topGen ` B ) -> ( A e. ( topGen ` B ) <-> A C_ U. ( B i^i ~P A ) ) )
4 3 ibi 
 |-  ( A e. ( topGen ` B ) -> A C_ U. ( B i^i ~P A ) )
5 inss2 
 |-  ( B i^i ~P A ) C_ ~P A
6 5 unissi 
 |-  U. ( B i^i ~P A ) C_ U. ~P A
7 unipw 
 |-  U. ~P A = A
8 6 7 sseqtri 
 |-  U. ( B i^i ~P A ) C_ A
9 8 a1i 
 |-  ( A e. ( topGen ` B ) -> U. ( B i^i ~P A ) C_ A )
10 4 9 eqssd 
 |-  ( A e. ( topGen ` B ) -> A = U. ( B i^i ~P A ) )