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 ‘ 𝐵 ) = { 𝑥𝑥 ( 𝐵 ∩ 𝒫 𝑥 ) } )