Theorem elfg

Description: A condition for elements of a generated filter. (Contributed by Jeff Hankins, 3-Sep-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

	Ref	Expression
Assertion	elfg	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fgval	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝑋 filGen 𝐹 ) = { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } )
2	1	eleq2d	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ 𝐴 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } ) )
3		pweq	⊢ ( 𝑦 = 𝐴 → 𝒫 𝑦 = 𝒫 𝐴 )
4	3	ineq2d	⊢ ( 𝑦 = 𝐴 → ( 𝐹 ∩ 𝒫 𝑦 ) = ( 𝐹 ∩ 𝒫 𝐴 ) )
5	4	neeq1d	⊢ ( 𝑦 = 𝐴 → ( ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ ↔ ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ) )
6	5	elrab	⊢ ( 𝐴 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } ↔ ( 𝐴 ∈ 𝒫 𝑋 ∧ ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ) )
7		elfvdm	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → 𝑋 ∈ dom fBas )
8		elpw2g	⊢ ( 𝑋 ∈ dom fBas → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
9	7 8	syl	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ 𝒫 𝑋 ↔ 𝐴 ⊆ 𝑋 ) )
10		elin	⊢ ( 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ∈ 𝒫 𝐴 ) )
11		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
12	11	anbi2i	⊢ ( ( 𝑥 ∈ 𝐹 ∧ 𝑥 ∈ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
13	10 12	bitri	⊢ ( 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) ↔ ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
14	13	exbii	⊢ ( ∃ 𝑥 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
15		n0	⊢ ( ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ ( 𝐹 ∩ 𝒫 𝐴 ) )
16		df-rex	⊢ ( ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐹 ∧ 𝑥 ⊆ 𝐴 ) )
17	14 15 16	3bitr4i	⊢ ( ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 )
18	17	a1i	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) )
19	9 18	anbi12d	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( ( 𝐴 ∈ 𝒫 𝑋 ∧ ( 𝐹 ∩ 𝒫 𝐴 ) ≠ ∅ ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )
20	6 19	bitrid	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ { 𝑦 ∈ 𝒫 𝑋 ∣ ( 𝐹 ∩ 𝒫 𝑦 ) ≠ ∅ } ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )
21	2 20	bitrd	⊢ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) → ( 𝐴 ∈ ( 𝑋 filGen 𝐹 ) ↔ ( 𝐴 ⊆ 𝑋 ∧ ∃ 𝑥 ∈ 𝐹 𝑥 ⊆ 𝐴 ) ) )