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