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 ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } )

Proof

Step Hyp Ref Expression
1 df-fg filGen = ( 𝑣 ∈ V , 𝑓 ∈ ( fBas ‘ 𝑣 ) ↦ { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } )
2 1 a1i ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → filGen = ( 𝑣 ∈ V , 𝑓 ∈ ( fBas ‘ 𝑣 ) ↦ { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } ) )
3 pweq ( 𝑣 = 𝑋 → 𝒫 𝑣 = 𝒫 𝑋 )
4 3 adantr ( ( 𝑣 = 𝑋𝑓 = 𝐹 ) → 𝒫 𝑣 = 𝒫 𝑋 )
5 ineq1 ( 𝑓 = 𝐹 → ( 𝑓 ∩ 𝒫 𝑥 ) = ( 𝐹 ∩ 𝒫 𝑥 ) )
6 5 neeq1d ( 𝑓 = 𝐹 → ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ ) )
7 6 adantl ( ( 𝑣 = 𝑋𝑓 = 𝐹 ) → ( ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ ) )
8 4 7 rabeqbidv ( ( 𝑣 = 𝑋𝑓 = 𝐹 ) → { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } )
9 8 adantl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ( 𝑣 = 𝑋𝑓 = 𝐹 ) ) → { 𝑥 ∈ 𝒫 𝑣 ∣ ( 𝑓 ∩ 𝒫 𝑥 ) ≠ ∅ } = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } )
10 fveq2 ( 𝑣 = 𝑋 → ( fBas ‘ 𝑣 ) = ( fBas ‘ 𝑋 ) )
11 10 adantl ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ 𝑣 = 𝑋 ) → ( fBas ‘ 𝑣 ) = ( fBas ‘ 𝑋 ) )
12 elfvex ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ V )
13 id ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝐹 ∈ ( fBas ‘ 𝑋 ) )
14 elfvdm ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas )
15 pwexg ( 𝑋 ∈ dom fBas → 𝒫 𝑋 ∈ V )
16 rabexg ( 𝒫 𝑋 ∈ V → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } ∈ V )
17 14 15 16 3syl ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } ∈ V )
18 2 9 11 12 13 17 ovmpodx ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = { 𝑥 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑥 ) ≠ ∅ } )