Metamath Proof Explorer

Theorem filssufilg

Description: A filter is contained in some ultrafilter. This version of filssufil contains the choice as a hypothesis (in the assumption that ~P ~P X is well-orderable). (Contributed by Mario Carneiro, 24-May-2015) (Revised by Stefan O'Rear, 2-Aug-2015)

Ref Expression
Assertion filssufilg 
|- ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> E. f e. ( UFil ` X ) F C_ f )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> ~P ~P X e. dom card )
2 rabss 
 |-  ( { g e. ( Fil ` X ) | F C_ g } C_ ~P ~P X <-> A. g e. ( Fil ` X ) ( F C_ g -> g e. ~P ~P X ) )
3 filsspw 
 |-  ( g e. ( Fil ` X ) -> g C_ ~P X )
4 velpw 
 |-  ( g e. ~P ~P X <-> g C_ ~P X )
5 3 4 sylibr 
 |-  ( g e. ( Fil ` X ) -> g e. ~P ~P X )
6 5 a1d 
 |-  ( g e. ( Fil ` X ) -> ( F C_ g -> g e. ~P ~P X ) )
7 2 6 mprgbir 
 |-  { g e. ( Fil ` X ) | F C_ g } C_ ~P ~P X
8 ssnum 
 |-  ( ( ~P ~P X e. dom card /\ { g e. ( Fil ` X ) | F C_ g } C_ ~P ~P X ) -> { g e. ( Fil ` X ) | F C_ g } e. dom card )
9 1 7 8 sylancl 
 |-  ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> { g e. ( Fil ` X ) | F C_ g } e. dom card )
10 ssid 
 |-  F C_ F
11 10 jctr 
 |-  ( F e. ( Fil ` X ) -> ( F e. ( Fil ` X ) /\ F C_ F ) )
12 sseq2 
 |-  ( g = F -> ( F C_ g <-> F C_ F ) )
13 12 elrab 
 |-  ( F e. { g e. ( Fil ` X ) | F C_ g } <-> ( F e. ( Fil ` X ) /\ F C_ F ) )
14 11 13 sylibr 
 |-  ( F e. ( Fil ` X ) -> F e. { g e. ( Fil ` X ) | F C_ g } )
15 14 ne0d 
 |-  ( F e. ( Fil ` X ) -> { g e. ( Fil ` X ) | F C_ g } =/= (/) )
16 15 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> { g e. ( Fil ` X ) | F C_ g } =/= (/) )
17 sseq2 
 |-  ( g = U. x -> ( F C_ g <-> F C_ U. x ) )
18 simpr1 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> x C_ { g e. ( Fil ` X ) | F C_ g } )
19 ssrab 
 |-  ( x C_ { g e. ( Fil ` X ) | F C_ g } <-> ( x C_ ( Fil ` X ) /\ A. g e. x F C_ g ) )
20 18 19 sylib 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> ( x C_ ( Fil ` X ) /\ A. g e. x F C_ g ) )
21 20 simpld 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> x C_ ( Fil ` X ) )
22 simpr2 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> x =/= (/) )
23 simpr3 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> [C.] Or x )
24 sorpssun 
 |-  ( ( [C.] Or x /\ ( g e. x /\ h e. x ) ) -> ( g u. h ) e. x )
25 24 ralrimivva 
 |-  ( [C.] Or x -> A. g e. x A. h e. x ( g u. h ) e. x )
26 23 25 syl 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> A. g e. x A. h e. x ( g u. h ) e. x )
27 filuni 
 |-  ( ( x C_ ( Fil ` X ) /\ x =/= (/) /\ A. g e. x A. h e. x ( g u. h ) e. x ) -> U. x e. ( Fil ` X ) )
28 21 22 26 27 syl3anc 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> U. x e. ( Fil ` X ) )
29 n0 
 |-  ( x =/= (/) <-> E. h h e. x )
30 ssel2 
 |-  ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ h e. x ) -> h e. { g e. ( Fil ` X ) | F C_ g } )
31 sseq2 
 |-  ( g = h -> ( F C_ g <-> F C_ h ) )
32 31 elrab 
 |-  ( h e. { g e. ( Fil ` X ) | F C_ g } <-> ( h e. ( Fil ` X ) /\ F C_ h ) )
33 30 32 sylib 
 |-  ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ h e. x ) -> ( h e. ( Fil ` X ) /\ F C_ h ) )
34 33 simprd 
 |-  ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ h e. x ) -> F C_ h )
35 ssuni 
 |-  ( ( F C_ h /\ h e. x ) -> F C_ U. x )
36 34 35 sylancom 
 |-  ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ h e. x ) -> F C_ U. x )
37 36 ex 
 |-  ( x C_ { g e. ( Fil ` X ) | F C_ g } -> ( h e. x -> F C_ U. x ) )
38 37 exlimdv 
 |-  ( x C_ { g e. ( Fil ` X ) | F C_ g } -> ( E. h h e. x -> F C_ U. x ) )
39 29 38 syl5bi 
 |-  ( x C_ { g e. ( Fil ` X ) | F C_ g } -> ( x =/= (/) -> F C_ U. x ) )
40 18 22 39 sylc 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> F C_ U. x )
41 17 28 40 elrabd 
 |-  ( ( F e. ( Fil ` X ) /\ ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) ) -> U. x e. { g e. ( Fil ` X ) | F C_ g } )
42 41 ex 
 |-  ( F e. ( Fil ` X ) -> ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) -> U. x e. { g e. ( Fil ` X ) | F C_ g } ) )
43 42 alrimiv 
 |-  ( F e. ( Fil ` X ) -> A. x ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) -> U. x e. { g e. ( Fil ` X ) | F C_ g } ) )
44 43 adantr 
 |-  ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> A. x ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) -> U. x e. { g e. ( Fil ` X ) | F C_ g } ) )
45 zornn0g 
 |-  ( ( { g e. ( Fil ` X ) | F C_ g } e. dom card /\ { g e. ( Fil ` X ) | F C_ g } =/= (/) /\ A. x ( ( x C_ { g e. ( Fil ` X ) | F C_ g } /\ x =/= (/) /\ [C.] Or x ) -> U. x e. { g e. ( Fil ` X ) | F C_ g } ) ) -> E. f e. { g e. ( Fil ` X ) | F C_ g } A. h e. { g e. ( Fil ` X ) | F C_ g } -. f C. h )
46 9 16 44 45 syl3anc 
 |-  ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> E. f e. { g e. ( Fil ` X ) | F C_ g } A. h e. { g e. ( Fil ` X ) | F C_ g } -. f C. h )
47 sseq2 
 |-  ( g = f -> ( F C_ g <-> F C_ f ) )
48 47 elrab 
 |-  ( f e. { g e. ( Fil ` X ) | F C_ g } <-> ( f e. ( Fil ` X ) /\ F C_ f ) )
49 31 ralrab 
 |-  ( A. h e. { g e. ( Fil ` X ) | F C_ g } -. f C. h <-> A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) )
50 simpll 
 |-  ( ( ( f e. ( Fil ` X ) /\ F C_ f ) /\ A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) ) -> f e. ( Fil ` X ) )
51 sstr2 
 |-  ( F C_ f -> ( f C_ h -> F C_ h ) )
52 51 imim1d 
 |-  ( F C_ f -> ( ( F C_ h -> -. f C. h ) -> ( f C_ h -> -. f C. h ) ) )
53 df-pss 
 |-  ( f C. h <-> ( f C_ h /\ f =/= h ) )
54 53 simplbi2 
 |-  ( f C_ h -> ( f =/= h -> f C. h ) )
55 54 necon1bd 
 |-  ( f C_ h -> ( -. f C. h -> f = h ) )
56 55 a2i 
 |-  ( ( f C_ h -> -. f C. h ) -> ( f C_ h -> f = h ) )
57 52 56 syl6 
 |-  ( F C_ f -> ( ( F C_ h -> -. f C. h ) -> ( f C_ h -> f = h ) ) )
58 57 ralimdv 
 |-  ( F C_ f -> ( A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) -> A. h e. ( Fil ` X ) ( f C_ h -> f = h ) ) )
59 58 imp 
 |-  ( ( F C_ f /\ A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) ) -> A. h e. ( Fil ` X ) ( f C_ h -> f = h ) )
60 59 adantll 
 |-  ( ( ( f e. ( Fil ` X ) /\ F C_ f ) /\ A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) ) -> A. h e. ( Fil ` X ) ( f C_ h -> f = h ) )
61 isufil2 
 |-  ( f e. ( UFil ` X ) <-> ( f e. ( Fil ` X ) /\ A. h e. ( Fil ` X ) ( f C_ h -> f = h ) ) )
62 50 60 61 sylanbrc 
 |-  ( ( ( f e. ( Fil ` X ) /\ F C_ f ) /\ A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) ) -> f e. ( UFil ` X ) )
63 simplr 
 |-  ( ( ( f e. ( Fil ` X ) /\ F C_ f ) /\ A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) ) -> F C_ f )
64 62 63 jca 
 |-  ( ( ( f e. ( Fil ` X ) /\ F C_ f ) /\ A. h e. ( Fil ` X ) ( F C_ h -> -. f C. h ) ) -> ( f e. ( UFil ` X ) /\ F C_ f ) )
65 48 49 64 syl2anb 
 |-  ( ( f e. { g e. ( Fil ` X ) | F C_ g } /\ A. h e. { g e. ( Fil ` X ) | F C_ g } -. f C. h ) -> ( f e. ( UFil ` X ) /\ F C_ f ) )
66 65 reximi2 
 |-  ( E. f e. { g e. ( Fil ` X ) | F C_ g } A. h e. { g e. ( Fil ` X ) | F C_ g } -. f C. h -> E. f e. ( UFil ` X ) F C_ f )
67 46 66 syl 
 |-  ( ( F e. ( Fil ` X ) /\ ~P ~P X e. dom card ) -> E. f e. ( UFil ` X ) F C_ f )