Metamath Proof Explorer

Theorem isufil2

Description: The maximal property of an ultrafilter. (Contributed by Jeff Hankins, 30-Nov-2009) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion isufil2 
|- ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) )

Proof

Step Hyp Ref Expression
1 ufilfil 
 |-  ( F e. ( UFil ` X ) -> F e. ( Fil ` X ) )
2 ufilmax 
 |-  ( ( F e. ( UFil ` X ) /\ f e. ( Fil ` X ) /\ F C_ f ) -> F = f )
3 2 3expia 
 |-  ( ( F e. ( UFil ` X ) /\ f e. ( Fil ` X ) ) -> ( F C_ f -> F = f ) )
4 3 ralrimiva 
 |-  ( F e. ( UFil ` X ) -> A. f e. ( Fil ` X ) ( F C_ f -> F = f ) )
5 1 4 jca 
 |-  ( F e. ( UFil ` X ) -> ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) )
6 simpl 
 |-  ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) -> F e. ( Fil ` X ) )
7 velpw 
 |-  ( x e. ~P X <-> x C_ X )
8 simpll 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> F e. ( Fil ` X ) )
9 snex 
 |-  { x } e. _V
10 unexg 
 |-  ( ( F e. ( Fil ` X ) /\ { x } e. _V ) -> ( F u. { x } ) e. _V )
11 8 9 10 sylancl 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( F u. { x } ) e. _V )
12 ssfii 
 |-  ( ( F u. { x } ) e. _V -> ( F u. { x } ) C_ ( fi ` ( F u. { x } ) ) )
13 11 12 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( F u. { x } ) C_ ( fi ` ( F u. { x } ) ) )
14 filsspw 
 |-  ( F e. ( Fil ` X ) -> F C_ ~P X )
15 14 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> F C_ ~P X )
16 7 biimpri 
 |-  ( x C_ X -> x e. ~P X )
17 16 ad2antlr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> x e. ~P X )
18 17 snssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> { x } C_ ~P X )
19 15 18 unssd 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( F u. { x } ) C_ ~P X )
20 ssun2 
 |-  { x } C_ ( F u. { x } )
21 vex 
 |-  x e. _V
22 21 snnz 
 |-  { x } =/= (/)
23 ssn0 
 |-  ( ( { x } C_ ( F u. { x } ) /\ { x } =/= (/) ) -> ( F u. { x } ) =/= (/) )
24 20 22 23 mp2an 
 |-  ( F u. { x } ) =/= (/)
25 24 a1i 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( F u. { x } ) =/= (/) )
26 simpr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> A. y e. F ( y i^i x ) =/= (/) )
27 ineq2 
 |-  ( f = x -> ( y i^i f ) = ( y i^i x ) )
28 27 neeq1d 
 |-  ( f = x -> ( ( y i^i f ) =/= (/) <-> ( y i^i x ) =/= (/) ) )
29 21 28 ralsn 
 |-  ( A. f e. { x } ( y i^i f ) =/= (/) <-> ( y i^i x ) =/= (/) )
30 29 ralbii 
 |-  ( A. y e. F A. f e. { x } ( y i^i f ) =/= (/) <-> A. y e. F ( y i^i x ) =/= (/) )
31 26 30 sylibr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> A. y e. F A. f e. { x } ( y i^i f ) =/= (/) )
32 filfbas 
 |-  ( F e. ( Fil ` X ) -> F e. ( fBas ` X ) )
33 32 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> F e. ( fBas ` X ) )
34 simplr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> x C_ X )
35 inss2 
 |-  ( X i^i x ) C_ x
36 filtop 
 |-  ( F e. ( Fil ` X ) -> X e. F )
37 36 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ x C_ X ) -> X e. F )
38 ineq1 
 |-  ( y = X -> ( y i^i x ) = ( X i^i x ) )
39 38 neeq1d 
 |-  ( y = X -> ( ( y i^i x ) =/= (/) <-> ( X i^i x ) =/= (/) ) )
40 39 rspcva 
 |-  ( ( X e. F /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( X i^i x ) =/= (/) )
41 37 40 sylan 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( X i^i x ) =/= (/) )
42 ssn0 
 |-  ( ( ( X i^i x ) C_ x /\ ( X i^i x ) =/= (/) ) -> x =/= (/) )
43 35 41 42 sylancr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> x =/= (/) )
44 36 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> X e. F )
45 snfbas 
 |-  ( ( x C_ X /\ x =/= (/) /\ X e. F ) -> { x } e. ( fBas ` X ) )
46 34 43 44 45 syl3anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> { x } e. ( fBas ` X ) )
47 fbunfip 
 |-  ( ( F e. ( fBas ` X ) /\ { x } e. ( fBas ` X ) ) -> ( -. (/) e. ( fi ` ( F u. { x } ) ) <-> A. y e. F A. f e. { x } ( y i^i f ) =/= (/) ) )
48 33 46 47 syl2anc 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( -. (/) e. ( fi ` ( F u. { x } ) ) <-> A. y e. F A. f e. { x } ( y i^i f ) =/= (/) ) )
49 31 48 mpbird 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> -. (/) e. ( fi ` ( F u. { x } ) ) )
50 fsubbas 
 |-  ( X e. F -> ( ( fi ` ( F u. { x } ) ) e. ( fBas ` X ) <-> ( ( F u. { x } ) C_ ~P X /\ ( F u. { x } ) =/= (/) /\ -. (/) e. ( fi ` ( F u. { x } ) ) ) ) )
51 44 50 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( ( fi ` ( F u. { x } ) ) e. ( fBas ` X ) <-> ( ( F u. { x } ) C_ ~P X /\ ( F u. { x } ) =/= (/) /\ -. (/) e. ( fi ` ( F u. { x } ) ) ) ) )
52 19 25 49 51 mpbir3and 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( fi ` ( F u. { x } ) ) e. ( fBas ` X ) )
53 ssfg 
 |-  ( ( fi ` ( F u. { x } ) ) e. ( fBas ` X ) -> ( fi ` ( F u. { x } ) ) C_ ( X filGen ( fi ` ( F u. { x } ) ) ) )
54 52 53 syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( fi ` ( F u. { x } ) ) C_ ( X filGen ( fi ` ( F u. { x } ) ) ) )
55 13 54 sstrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( F u. { x } ) C_ ( X filGen ( fi ` ( F u. { x } ) ) ) )
56 55 unssad 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> F C_ ( X filGen ( fi ` ( F u. { x } ) ) ) )
57 fgcl 
 |-  ( ( fi ` ( F u. { x } ) ) e. ( fBas ` X ) -> ( X filGen ( fi ` ( F u. { x } ) ) ) e. ( Fil ` X ) )
58 sseq2 
 |-  ( f = ( X filGen ( fi ` ( F u. { x } ) ) ) -> ( F C_ f <-> F C_ ( X filGen ( fi ` ( F u. { x } ) ) ) ) )
59 eqeq2 
 |-  ( f = ( X filGen ( fi ` ( F u. { x } ) ) ) -> ( F = f <-> F = ( X filGen ( fi ` ( F u. { x } ) ) ) ) )
60 58 59 imbi12d 
 |-  ( f = ( X filGen ( fi ` ( F u. { x } ) ) ) -> ( ( F C_ f -> F = f ) <-> ( F C_ ( X filGen ( fi ` ( F u. { x } ) ) ) -> F = ( X filGen ( fi ` ( F u. { x } ) ) ) ) ) )
61 60 rspcv 
 |-  ( ( X filGen ( fi ` ( F u. { x } ) ) ) e. ( Fil ` X ) -> ( A. f e. ( Fil ` X ) ( F C_ f -> F = f ) -> ( F C_ ( X filGen ( fi ` ( F u. { x } ) ) ) -> F = ( X filGen ( fi ` ( F u. { x } ) ) ) ) ) )
62 52 57 61 3syl 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( A. f e. ( Fil ` X ) ( F C_ f -> F = f ) -> ( F C_ ( X filGen ( fi ` ( F u. { x } ) ) ) -> F = ( X filGen ( fi ` ( F u. { x } ) ) ) ) ) )
63 56 62 mpid 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( A. f e. ( Fil ` X ) ( F C_ f -> F = f ) -> F = ( X filGen ( fi ` ( F u. { x } ) ) ) ) )
64 vsnid 
 |-  x e. { x }
65 20 64 sselii 
 |-  x e. ( F u. { x } )
66 65 a1i 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> x e. ( F u. { x } ) )
67 55 66 sseldd 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> x e. ( X filGen ( fi ` ( F u. { x } ) ) ) )
68 eleq2 
 |-  ( F = ( X filGen ( fi ` ( F u. { x } ) ) ) -> ( x e. F <-> x e. ( X filGen ( fi ` ( F u. { x } ) ) ) ) )
69 67 68 syl5ibrcom 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( F = ( X filGen ( fi ` ( F u. { x } ) ) ) -> x e. F ) )
70 63 69 syld 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. y e. F ( y i^i x ) =/= (/) ) -> ( A. f e. ( Fil ` X ) ( F C_ f -> F = f ) -> x e. F ) )
71 70 impancom 
 |-  ( ( ( F e. ( Fil ` X ) /\ x C_ X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) -> ( A. y e. F ( y i^i x ) =/= (/) -> x e. F ) )
72 71 an32s 
 |-  ( ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) /\ x C_ X ) -> ( A. y e. F ( y i^i x ) =/= (/) -> x e. F ) )
73 72 con3d 
 |-  ( ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) /\ x C_ X ) -> ( -. x e. F -> -. A. y e. F ( y i^i x ) =/= (/) ) )
74 rexnal 
 |-  ( E. y e. F -. ( y i^i x ) =/= (/) <-> -. A. y e. F ( y i^i x ) =/= (/) )
75 nne 
 |-  ( -. ( y i^i x ) =/= (/) <-> ( y i^i x ) = (/) )
76 filelss 
 |-  ( ( F e. ( Fil ` X ) /\ y e. F ) -> y C_ X )
77 reldisj 
 |-  ( y C_ X -> ( ( y i^i x ) = (/) <-> y C_ ( X \ x ) ) )
78 76 77 syl 
 |-  ( ( F e. ( Fil ` X ) /\ y e. F ) -> ( ( y i^i x ) = (/) <-> y C_ ( X \ x ) ) )
79 difss 
 |-  ( X \ x ) C_ X
80 filss 
 |-  ( ( F e. ( Fil ` X ) /\ ( y e. F /\ ( X \ x ) C_ X /\ y C_ ( X \ x ) ) ) -> ( X \ x ) e. F )
81 80 3exp2 
 |-  ( F e. ( Fil ` X ) -> ( y e. F -> ( ( X \ x ) C_ X -> ( y C_ ( X \ x ) -> ( X \ x ) e. F ) ) ) )
82 79 81 mpii 
 |-  ( F e. ( Fil ` X ) -> ( y e. F -> ( y C_ ( X \ x ) -> ( X \ x ) e. F ) ) )
83 82 imp 
 |-  ( ( F e. ( Fil ` X ) /\ y e. F ) -> ( y C_ ( X \ x ) -> ( X \ x ) e. F ) )
84 78 83 sylbid 
 |-  ( ( F e. ( Fil ` X ) /\ y e. F ) -> ( ( y i^i x ) = (/) -> ( X \ x ) e. F ) )
85 75 84 syl5bi 
 |-  ( ( F e. ( Fil ` X ) /\ y e. F ) -> ( -. ( y i^i x ) =/= (/) -> ( X \ x ) e. F ) )
86 85 rexlimdva 
 |-  ( F e. ( Fil ` X ) -> ( E. y e. F -. ( y i^i x ) =/= (/) -> ( X \ x ) e. F ) )
87 74 86 syl5bir 
 |-  ( F e. ( Fil ` X ) -> ( -. A. y e. F ( y i^i x ) =/= (/) -> ( X \ x ) e. F ) )
88 87 ad2antrr 
 |-  ( ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) /\ x C_ X ) -> ( -. A. y e. F ( y i^i x ) =/= (/) -> ( X \ x ) e. F ) )
89 73 88 syld 
 |-  ( ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) /\ x C_ X ) -> ( -. x e. F -> ( X \ x ) e. F ) )
90 89 orrd 
 |-  ( ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) /\ x C_ X ) -> ( x e. F \/ ( X \ x ) e. F ) )
91 7 90 sylan2b 
 |-  ( ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) /\ x e. ~P X ) -> ( x e. F \/ ( X \ x ) e. F ) )
92 91 ralrimiva 
 |-  ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) -> A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) )
93 isufil 
 |-  ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. x e. ~P X ( x e. F \/ ( X \ x ) e. F ) ) )
94 6 92 93 sylanbrc 
 |-  ( ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) -> F e. ( UFil ` X ) )
95 5 94 impbii 
 |-  ( F e. ( UFil ` X ) <-> ( F e. ( Fil ` X ) /\ A. f e. ( Fil ` X ) ( F C_ f -> F = f ) ) )