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 B V topGen B = x | x B 𝒫 x

Proof

Step Hyp Ref Expression
1 df-topgen topGen = y V x | x y 𝒫 x
2 ineq1 y = B y 𝒫 x = B 𝒫 x
3 2 unieqd y = B y 𝒫 x = B 𝒫 x
4 3 sseq2d y = B x y 𝒫 x x B 𝒫 x
5 4 abbidv y = B x | x y 𝒫 x = x | x B 𝒫 x
6 elex B V B V
7 uniexg B V B V
8 abssexg B V x | x B x 𝒫 x V
9 uniin B 𝒫 x B 𝒫 x
10 sstr x B 𝒫 x B 𝒫 x B 𝒫 x x B 𝒫 x
11 9 10 mpan2 x B 𝒫 x x B 𝒫 x
12 ssin x B x 𝒫 x x B 𝒫 x
13 11 12 sylibr x B 𝒫 x x B x 𝒫 x
14 13 ss2abi x | x B 𝒫 x x | x B x 𝒫 x
15 ssexg x | x B 𝒫 x x | x B x 𝒫 x x | x B x 𝒫 x V x | x B 𝒫 x V
16 14 15 mpan x | x B x 𝒫 x V x | x B 𝒫 x V
17 7 8 16 3syl B V x | x B 𝒫 x V
18 1 5 6 17 fvmptd3 B V topGen B = x | x B 𝒫 x