Metamath Proof Explorer


Theorem fgval

Description: The filter generating class gives a filter for every filter base. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion fgval F fBas X X filGen F = x 𝒫 X | F 𝒫 x

Proof

Step Hyp Ref Expression
1 df-fg filGen = v V , f fBas v x 𝒫 v | f 𝒫 x
2 1 a1i F fBas X filGen = v V , f fBas v x 𝒫 v | f 𝒫 x
3 pweq v = X 𝒫 v = 𝒫 X
4 3 adantr v = X f = F 𝒫 v = 𝒫 X
5 ineq1 f = F f 𝒫 x = F 𝒫 x
6 5 neeq1d f = F f 𝒫 x F 𝒫 x
7 6 adantl v = X f = F f 𝒫 x F 𝒫 x
8 4 7 rabeqbidv v = X f = F x 𝒫 v | f 𝒫 x = x 𝒫 X | F 𝒫 x
9 8 adantl F fBas X v = X f = F x 𝒫 v | f 𝒫 x = x 𝒫 X | F 𝒫 x
10 fveq2 v = X fBas v = fBas X
11 10 adantl F fBas X v = X fBas v = fBas X
12 elfvex F fBas X X V
13 id F fBas X F fBas X
14 elfvdm F fBas X X dom fBas
15 pwexg X dom fBas 𝒫 X V
16 rabexg 𝒫 X V x 𝒫 X | F 𝒫 x V
17 14 15 16 3syl F fBas X x 𝒫 X | F 𝒫 x V
18 2 9 11 12 13 17 ovmpodx F fBas X X filGen F = x 𝒫 X | F 𝒫 x