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	|- ( F e. ( fBas ` X ) -> ( A e. ( X filGen F ) <-> ( A C_ X /\ E. x e. F x C_ A ) ) )

Proof

Step	Hyp	Ref	Expression
1		fgval	|- ( F e. ( fBas ` X ) -> ( X filGen F ) = { y e. ~P X | ( F i^i ~P y ) =/= (/) } )
2	1	eleq2d	|- ( F e. ( fBas ` X ) -> ( A e. ( X filGen F ) <-> A e. { y e. ~P X | ( F i^i ~P y ) =/= (/) } ) )
3		pweq	|- ( y = A -> ~P y = ~P A )
4	3	ineq2d	|- ( y = A -> ( F i^i ~P y ) = ( F i^i ~P A ) )
5	4	neeq1d	|- ( y = A -> ( ( F i^i ~P y ) =/= (/) <-> ( F i^i ~P A ) =/= (/) ) )
6	5	elrab	|- ( A e. { y e. ~P X | ( F i^i ~P y ) =/= (/) } <-> ( A e. ~P X /\ ( F i^i ~P A ) =/= (/) ) )
7		elfvdm	|- ( F e. ( fBas ` X ) -> X e. dom fBas )
8		elpw2g	|- ( X e. dom fBas -> ( A e. ~P X <-> A C_ X ) )
9	7 8	syl	|- ( F e. ( fBas ` X ) -> ( A e. ~P X <-> A C_ X ) )
10		elin	|- ( x e. ( F i^i ~P A ) <-> ( x e. F /\ x e. ~P A ) )
11		velpw	|- ( x e. ~P A <-> x C_ A )
12	11	anbi2i	|- ( ( x e. F /\ x e. ~P A ) <-> ( x e. F /\ x C_ A ) )
13	10 12	bitri	|- ( x e. ( F i^i ~P A ) <-> ( x e. F /\ x C_ A ) )
14	13	exbii	|- ( E. x x e. ( F i^i ~P A ) <-> E. x ( x e. F /\ x C_ A ) )
15		n0	|- ( ( F i^i ~P A ) =/= (/) <-> E. x x e. ( F i^i ~P A ) )
16		df-rex	|- ( E. x e. F x C_ A <-> E. x ( x e. F /\ x C_ A ) )
17	14 15 16	3bitr4i	|- ( ( F i^i ~P A ) =/= (/) <-> E. x e. F x C_ A )
18	17	a1i	|- ( F e. ( fBas ` X ) -> ( ( F i^i ~P A ) =/= (/) <-> E. x e. F x C_ A ) )
19	9 18	anbi12d	|- ( F e. ( fBas ` X ) -> ( ( A e. ~P X /\ ( F i^i ~P A ) =/= (/) ) <-> ( A C_ X /\ E. x e. F x C_ A ) ) )
20	6 19	bitrid	|- ( F e. ( fBas ` X ) -> ( A e. { y e. ~P X | ( F i^i ~P y ) =/= (/) } <-> ( A C_ X /\ E. x e. F x C_ A ) ) )
21	2 20	bitrd	|- ( F e. ( fBas ` X ) -> ( A e. ( X filGen F ) <-> ( A C_ X /\ E. x e. F x C_ A ) ) )