Metamath Proof Explorer

Theorem isfil

Description: The predicate "is a filter." (Contributed by FL, 20-Jul-2007) (Revised by Mario Carneiro, 28-Jul-2015)

Ref Expression
Assertion isfil 
|- ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )

Proof

Step Hyp Ref Expression
1 df-fil 
 |-  Fil = ( z e. _V |-> { f e. ( fBas ` z ) | A. x e. ~P z ( ( f i^i ~P x ) =/= (/) -> x e. f ) } )
2 pweq 
 |-  ( z = X -> ~P z = ~P X )
3 2 adantr 
 |-  ( ( z = X /\ f = F ) -> ~P z = ~P X )
4 ineq1 
 |-  ( f = F -> ( f i^i ~P x ) = ( F i^i ~P x ) )
5 4 neeq1d 
 |-  ( f = F -> ( ( f i^i ~P x ) =/= (/) <-> ( F i^i ~P x ) =/= (/) ) )
6 eleq2 
 |-  ( f = F -> ( x e. f <-> x e. F ) )
7 5 6 imbi12d 
 |-  ( f = F -> ( ( ( f i^i ~P x ) =/= (/) -> x e. f ) <-> ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )
8 7 adantl 
 |-  ( ( z = X /\ f = F ) -> ( ( ( f i^i ~P x ) =/= (/) -> x e. f ) <-> ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )
9 3 8 raleqbidv 
 |-  ( ( z = X /\ f = F ) -> ( A. x e. ~P z ( ( f i^i ~P x ) =/= (/) -> x e. f ) <-> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )
10 fveq2 
 |-  ( z = X -> ( fBas ` z ) = ( fBas ` X ) )
11 fvex 
 |-  ( fBas ` z ) e. _V
12 elfvdm 
 |-  ( F e. ( fBas ` X ) -> X e. dom fBas )
13 1 9 10 11 12 elmptrab2 
 |-  ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )