Metamath Proof Explorer

Theorem isfil2

Description: Derive the standard axioms of a filter. (Contributed by Mario Carneiro, 27-Nov-2013) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion isfil2 
|- ( F e. ( Fil ` X ) <-> ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) )

Proof

Step Hyp Ref Expression
1 filsspw 
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )
2 0nelfil 
 |-  ( F e. ( Fil ` X ) -> -. (/) e. F )
3 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
4 1 2 3 3jca 
 |-  ( F e. ( Fil ` X ) -> ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) )
5 elpwi 
 |-  ( x e. ~P X -> x C_ X )
6 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( y e. F /\ x C_ X /\ y C_ x ) ) -> x e. F )
7 6 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( y e. F -> ( x C_ X -> ( y C_ x -> x e. F ) ) ) )
8 7 com23 
 |-  ( F e. ( Fil ` X ) -> ( x C_ X -> ( y e. F -> ( y C_ x -> x e. F ) ) ) )
9 8 imp 
 |-  ( ( F e. ( Fil ` X ) /\ x C_ X ) -> ( y e. F -> ( y C_ x -> x e. F ) ) )
10 9 rexlimdv 
 |-  ( ( F e. ( Fil ` X ) /\ x C_ X ) -> ( E. y e. F y C_ x -> x e. F ) )
11 5 10 sylan2 
 |-  ( ( F e. ( Fil ` X ) /\ x e. ~P X ) -> ( E. y e. F y C_ x -> x e. F ) )
12 11 ralrimiva 
 |-  ( F e. ( Fil ` X ) -> A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) )
13 filin 
 |-  ( ( F e. ( Fil ` X ) /\ x e. F /\ y e. F ) -> ( x i^i y ) e. F )
14 13 3expb 
 |-  ( ( F e. ( Fil ` X ) /\ ( x e. F /\ y e. F ) ) -> ( x i^i y ) e. F )
15 14 ralrimivva 
 |-  ( F e. ( Fil ` X ) -> A. x e. F A. y e. F ( x i^i y ) e. F )
16 4 12 15 3jca 
 |-  ( F e. ( Fil ` X ) -> ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) )
17 simp11 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> F C_ ~P X )
18 simp13 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> X e. F )
19 18 ne0d 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> F =/= (/) )
20 simp12 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> -. (/) e. F )
21 df-nel 
 |-  ( (/) e/ F <-> -. (/) e. F )
22 20 21 sylibr 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> (/) e/ F )
23 ssid 
 |-  ( x i^i y ) C_ ( x i^i y )
24 sseq1 
 |-  ( z = ( x i^i y ) -> ( z C_ ( x i^i y ) <-> ( x i^i y ) C_ ( x i^i y ) ) )
25 24 rspcev 
 |-  ( ( ( x i^i y ) e. F /\ ( x i^i y ) C_ ( x i^i y ) ) -> E. z e. F z C_ ( x i^i y ) )
26 23 25 mpan2 
 |-  ( ( x i^i y ) e. F -> E. z e. F z C_ ( x i^i y ) )
27 26 ralimi 
 |-  ( A. y e. F ( x i^i y ) e. F -> A. y e. F E. z e. F z C_ ( x i^i y ) )
28 27 ralimi 
 |-  ( A. x e. F A. y e. F ( x i^i y ) e. F -> A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) )
29 28 3ad2ant3 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) )
30 19 22 29 3jca 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) )
31 isfbas2 
 |-  ( X e. F -> ( F e. ( fBas ` X ) <-> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) )
32 18 31 syl 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> ( F e. ( fBas ` X ) <-> ( F C_ ~P X /\ ( F =/= (/) /\ (/) e/ F /\ A. x e. F A. y e. F E. z e. F z C_ ( x i^i y ) ) ) ) )
33 17 30 32 mpbir2and 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> F e. ( fBas ` X ) )
34 n0 
 |-  ( ( F i^i ~P x ) =/= (/) <-> E. y y e. ( F i^i ~P x ) )
35 elin 
 |-  ( y e. ( F i^i ~P x ) <-> ( y e. F /\ y e. ~P x ) )
36 elpwi 
 |-  ( y e. ~P x -> y C_ x )
37 36 anim2i 
 |-  ( ( y e. F /\ y e. ~P x ) -> ( y e. F /\ y C_ x ) )
38 35 37 sylbi 
 |-  ( y e. ( F i^i ~P x ) -> ( y e. F /\ y C_ x ) )
39 38 eximi 
 |-  ( E. y y e. ( F i^i ~P x ) -> E. y ( y e. F /\ y C_ x ) )
40 34 39 sylbi 
 |-  ( ( F i^i ~P x ) =/= (/) -> E. y ( y e. F /\ y C_ x ) )
41 df-rex 
 |-  ( E. y e. F y C_ x <-> E. y ( y e. F /\ y C_ x ) )
42 40 41 sylibr 
 |-  ( ( F i^i ~P x ) =/= (/) -> E. y e. F y C_ x )
43 42 imim1i 
 |-  ( ( E. y e. F y C_ x -> x e. F ) -> ( ( F i^i ~P x ) =/= (/) -> x e. F ) )
44 43 ralimi 
 |-  ( A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) -> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) )
45 44 3ad2ant2 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) )
46 isfil 
 |-  ( F e. ( Fil ` X ) <-> ( F e. ( fBas ` X ) /\ A. x e. ~P X ( ( F i^i ~P x ) =/= (/) -> x e. F ) ) )
47 33 45 46 sylanbrc 
 |-  ( ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) -> F e. ( Fil ` X ) )
48 16 47 impbii 
 |-  ( F e. ( Fil ` X ) <-> ( ( F C_ ~P X /\ -. (/) e. F /\ X e. F ) /\ A. x e. ~P X ( E. y e. F y C_ x -> x e. F ) /\ A. x e. F A. y e. F ( x i^i y ) e. F ) )