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

Metamath Proof Explorer

Theorem tgval

Description: The topology generated by a basis. See also tgval2 and tgval3 . (Contributed by NM, 16-Jul-2006) (Revised by Mario Carneiro, 10-Jan-2015)

Ref Expression
Assertion tgval 
|- ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )

Proof

Step Hyp Ref Expression
1 df-topgen 
 |-  topGen = ( y e. _V |-> { x | x C_ U. ( y i^i ~P x ) } )
2 ineq1 
 |-  ( y = B -> ( y i^i ~P x ) = ( B i^i ~P x ) )
3 2 unieqd 
 |-  ( y = B -> U. ( y i^i ~P x ) = U. ( B i^i ~P x ) )
4 3 sseq2d 
 |-  ( y = B -> ( x C_ U. ( y i^i ~P x ) <-> x C_ U. ( B i^i ~P x ) ) )
5 4 abbidv 
 |-  ( y = B -> { x | x C_ U. ( y i^i ~P x ) } = { x | x C_ U. ( B i^i ~P x ) } )
6 elex 
 |-  ( B e. V -> B e. _V )
7 uniexg 
 |-  ( B e. V -> U. B e. _V )
8 abssexg 
 |-  ( U. B e. _V -> { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V )
9 uniin 
 |-  U. ( B i^i ~P x ) C_ ( U. B i^i U. ~P x )
10 sstr 
 |-  ( ( x C_ U. ( B i^i ~P x ) /\ U. ( B i^i ~P x ) C_ ( U. B i^i U. ~P x ) ) -> x C_ ( U. B i^i U. ~P x ) )
11 9 10 mpan2 
 |-  ( x C_ U. ( B i^i ~P x ) -> x C_ ( U. B i^i U. ~P x ) )
12 ssin 
 |-  ( ( x C_ U. B /\ x C_ U. ~P x ) <-> x C_ ( U. B i^i U. ~P x ) )
13 11 12 sylibr 
 |-  ( x C_ U. ( B i^i ~P x ) -> ( x C_ U. B /\ x C_ U. ~P x ) )
14 13 ss2abi 
 |-  { x | x C_ U. ( B i^i ~P x ) } C_ { x | ( x C_ U. B /\ x C_ U. ~P x ) }
15 ssexg 
 |-  ( ( { x | x C_ U. ( B i^i ~P x ) } C_ { x | ( x C_ U. B /\ x C_ U. ~P x ) } /\ { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V ) -> { x | x C_ U. ( B i^i ~P x ) } e. _V )
16 14 15 mpan 
 |-  ( { x | ( x C_ U. B /\ x C_ U. ~P x ) } e. _V -> { x | x C_ U. ( B i^i ~P x ) } e. _V )
17 7 8 16 3syl 
 |-  ( B e. V -> { x | x C_ U. ( B i^i ~P x ) } e. _V )
18 1 5 6 17 fvmptd3 
 |-  ( B e. V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )