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 ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 df-topgen ⊢ topGen = ( 𝑦 ∈ V ↦ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) } )
2 ineq1 ⊢ ( 𝑦 = 𝐵 → ( 𝑦 ∩ 𝒫 𝑥 ) = ( 𝐵 ∩ 𝒫 𝑥 ) )
3 2 unieqd ⊢ ( 𝑦 = 𝐵 → ∪ ( 𝑦 ∩ 𝒫 𝑥 ) = ∪ ( 𝐵 ∩ 𝒫 𝑥 ) )
4 3 sseq2d ⊢ ( 𝑦 = 𝐵 → ( 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ) )
5 4 abbidv ⊢ ( 𝑦 = 𝐵 → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝑦 ∩ 𝒫 𝑥 ) } = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )
6 elex ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
7 uniexg ⊢ ( 𝐵 ∈ 𝑉 → ∪ 𝐵 ∈ V )
8 abssexg ⊢ ( ∪ 𝐵 ∈ V → { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V )
9 uniin ⊢ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 )
10 sstr ⊢ ( ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ∧ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) ) → 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) )
11 9 10 mpan2 ⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) )
12 ssin ⊢ ( ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) ↔ 𝑥 ⊆ ( ∪ 𝐵 ∩ ∪ 𝒫 𝑥 ) )
13 11 12 sylibr ⊢ ( 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) → ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) )
14 13 ss2abi ⊢ { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) }
15 ssexg ⊢ ( ( { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ⊆ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∧ { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V ) → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V )
16 14 15 mpan ⊢ ( { 𝑥 ∣ ( 𝑥 ⊆ ∪ 𝐵 ∧ 𝑥 ⊆ ∪ 𝒫 𝑥 ) } ∈ V → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V )
17 7 8 16 3syl ⊢ ( 𝐵 ∈ 𝑉 → { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } ∈ V )
18 1 5 6 17 fvmptd3 ⊢ ( 𝐵 ∈ 𝑉 → ( topGen ‘ 𝐵 ) = { 𝑥 ∣ 𝑥 ⊆ ∪ ( 𝐵 ∩ 𝒫 𝑥 ) } )