Metamath Proof Explorer


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 syl5bb
 |-  ( 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 ) ) )