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 )