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

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 ‘ ( 𝐵 ∖ { ∅ } ) ) = ( topGen ‘ 𝐵 )

Proof

Step Hyp Ref Expression
1 indif1 ⊢ ( ( 𝐵 ∖ { ∅ } ) ∩ 𝒫 𝑥 ) = ( ( 𝐵 ∩ 𝒫 𝑥 ) ∖ { ∅ } )
2 1 unieqi ⊢ ∪ ( ( 𝐵 ∖ { ∅ } ) ∩ 𝒫 𝑥 ) = ∪ ( ( 𝐵 ∩ 𝒫 𝑥 ) ∖ { ∅ } )
3 unidif0 ⊢ ∪ ( ( 𝐵 ∩ 𝒫 𝑥 ) ∖ { ∅ } ) = ∪ ( 𝐵 ∩ 𝒫 𝑥 )
4 2 3 eqtri ⊢ ∪ ( ( 𝐵 ∖ { ∅ } ) ∩ 𝒫 𝑥 ) = ∪ ( 𝐵 ∩ 𝒫 𝑥 )
5 4 sseq2i ⊢ ( 𝑥 ⊆ ∪ ( ( 𝐵 ∖ { ∅ } ) ∩ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
6 5 abbii ⊢ { 𝑥 ∣ 𝑥 ⊆ ∪ ( ( 𝐵 ∖ { ∅ } ) ∩ 𝒫 𝑥 ) } = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) }
7 difexg ⊢ ( 𝐵 ∈ V → ( 𝐵 ∖ { ∅ } ) ∈ V )
8 tgval ⊢ ( ( 𝐵 ∖ { ∅ } ) ∈ V → ( topGen ‘ ( 𝐵 ∖ { ∅ } ) ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( ( 𝐵 ∖ { ∅ } ) ∩ 𝒫 𝑥 ) } )
9 7 8 syl ⊢ ( 𝐵 ∈ V → ( topGen ‘ ( 𝐵 ∖ { ∅ } ) ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( ( 𝐵 ∖ { ∅ } ) ∩ 𝒫 𝑥 ) } )
10 tgval ⊢ ( 𝐵 ∈ V → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )
11 6 9 10 3eqtr4a ⊢ ( 𝐵 ∈ V → ( topGen ‘ ( 𝐵 ∖ { ∅ } ) ) = ( topGen ‘ 𝐵 ) )
12 difsnexi ⊢ ( ( 𝐵 ∖ { ∅ } ) ∈ V → 𝐵 ∈ V )
13 fvprc ⊢ ( ¬ ( 𝐵 ∖ { ∅ } ) ∈ V → ( topGen ‘ ( 𝐵 ∖ { ∅ } ) ) = ∅ )
14 12 13 nsyl5 ⊢ ( ¬ 𝐵 ∈ V → ( topGen ‘ ( 𝐵 ∖ { ∅ } ) ) = ∅ )
15 fvprc ⊢ ( ¬ 𝐵 ∈ V → ( topGen ‘ 𝐵 ) = ∅ )
16 14 15 eqtr4d ⊢ ( ¬ 𝐵 ∈ V → ( topGen ‘ ( 𝐵 ∖ { ∅ } ) ) = ( topGen ‘ 𝐵 ) )
17 11 16 pm2.61i ⊢ ( topGen ‘ ( 𝐵 ∖ { ∅ } ) ) = ( topGen ‘ 𝐵 )