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