Metamath Proof Explorer

Theorem tgdif0

Description: A generated topology is not affected by the addition or removal of the empty set from the base. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Assertion tgdif0 
|- ( topGen ` ( B \ { (/) } ) ) = ( topGen ` B )

Proof

Step Hyp Ref Expression
1 indif1 
 |-  ( ( B \ { (/) } ) i^i ~P x ) = ( ( B i^i ~P x ) \ { (/) } )
2 1 unieqi 
 |-  U. ( ( B \ { (/) } ) i^i ~P x ) = U. ( ( B i^i ~P x ) \ { (/) } )
3 unidif0 
 |-  U. ( ( B i^i ~P x ) \ { (/) } ) = U. ( B i^i ~P x )
4 2 3 eqtri 
 |-  U. ( ( B \ { (/) } ) i^i ~P x ) = U. ( B i^i ~P x )
5 4 sseq2i 
 |-  ( x C_ U. ( ( B \ { (/) } ) i^i ~P x ) <-> x C_ U. ( B i^i ~P x ) )
6 5 abbii 
 |-  { x | x C_ U. ( ( B \ { (/) } ) i^i ~P x ) } = { x | x C_ U. ( B i^i ~P x ) }
7 difexg 
 |-  ( B e. _V -> ( B \ { (/) } ) e. _V )
8 tgval 
 |-  ( ( B \ { (/) } ) e. _V -> ( topGen ` ( B \ { (/) } ) ) = { x | x C_ U. ( ( B \ { (/) } ) i^i ~P x ) } )
9 7 8 syl 
 |-  ( B e. _V -> ( topGen ` ( B \ { (/) } ) ) = { x | x C_ U. ( ( B \ { (/) } ) i^i ~P x ) } )
10 tgval 
 |-  ( B e. _V -> ( topGen ` B ) = { x | x C_ U. ( B i^i ~P x ) } )
11 6 9 10 3eqtr4a 
 |-  ( B e. _V -> ( topGen ` ( B \ { (/) } ) ) = ( topGen ` B ) )
12 difsnexi 
 |-  ( ( B \ { (/) } ) e. _V -> B e. _V )
13 fvprc 
 |-  ( -. ( B \ { (/) } ) e. _V -> ( topGen ` ( B \ { (/) } ) ) = (/) )
14 12 13 nsyl5 
 |-  ( -. B e. _V -> ( topGen ` ( B \ { (/) } ) ) = (/) )
15 fvprc 
 |-  ( -. B e. _V -> ( topGen ` B ) = (/) )
16 14 15 eqtr4d 
 |-  ( -. B e. _V -> ( topGen ` ( B \ { (/) } ) ) = ( topGen ` B ) )
17 11 16 pm2.61i 
 |-  ( topGen ` ( B \ { (/) } ) ) = ( topGen ` B )