This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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