Metamath Proof Explorer

Theorem ufilen

Description: Any infinite set has an ultrafilter on it whose elements are of the same cardinality as the set. Any such ultrafilter is necessarily free. (Contributed by Jeff Hankins, 7-Dec-2009) (Revised by Stefan O'Rear, 3-Aug-2015)

Ref Expression
Assertion ufilen 
|- ( _om ~<_ X -> E. f e. ( UFil ` X ) A. x e. f x ~~ X )

Proof

Step Hyp Ref Expression
1 reldom 
 |-  Rel ~<_
2 1 brrelex2i 
 |-  ( _om ~<_ X -> X e. _V )
3 numth3 
 |-  ( X e. _V -> X e. dom card )
4 2 3 syl 
 |-  ( _om ~<_ X -> X e. dom card )
5 csdfil 
 |-  ( ( X e. dom card /\ _om ~<_ X ) -> { y e. ~P X | ( X \ y ) ~< X } e. ( Fil ` X ) )
6 4 5 mpancom 
 |-  ( _om ~<_ X -> { y e. ~P X | ( X \ y ) ~< X } e. ( Fil ` X ) )
7 filssufil 
 |-  ( { y e. ~P X | ( X \ y ) ~< X } e. ( Fil ` X ) -> E. f e. ( UFil ` X ) { y e. ~P X | ( X \ y ) ~< X } C_ f )
8 6 7 syl 
 |-  ( _om ~<_ X -> E. f e. ( UFil ` X ) { y e. ~P X | ( X \ y ) ~< X } C_ f )
9 elfvex 
 |-  ( f e. ( UFil ` X ) -> X e. _V )
10 9 ad2antlr 
 |-  ( ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) /\ x e. f ) -> X e. _V )
11 ufilfil 
 |-  ( f e. ( UFil ` X ) -> f e. ( Fil ` X ) )
12 filelss 
 |-  ( ( f e. ( Fil ` X ) /\ x e. f ) -> x C_ X )
13 11 12 sylan 
 |-  ( ( f e. ( UFil ` X ) /\ x e. f ) -> x C_ X )
14 13 adantll 
 |-  ( ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) /\ x e. f ) -> x C_ X )
15 ssdomg 
 |-  ( X e. _V -> ( x C_ X -> x ~<_ X ) )
16 10 14 15 sylc 
 |-  ( ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) /\ x e. f ) -> x ~<_ X )
17 filfbas 
 |-  ( f e. ( Fil ` X ) -> f e. ( fBas ` X ) )
18 11 17 syl 
 |-  ( f e. ( UFil ` X ) -> f e. ( fBas ` X ) )
19 18 adantl 
 |-  ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) -> f e. ( fBas ` X ) )
20 fbncp 
 |-  ( ( f e. ( fBas ` X ) /\ x e. f ) -> -. ( X \ x ) e. f )
21 19 20 sylan 
 |-  ( ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) /\ x e. f ) -> -. ( X \ x ) e. f )
22 difeq2 
 |-  ( y = ( X \ x ) -> ( X \ y ) = ( X \ ( X \ x ) ) )
23 22 breq1d 
 |-  ( y = ( X \ x ) -> ( ( X \ y ) ~< X <-> ( X \ ( X \ x ) ) ~< X ) )
24 difss 
 |-  ( X \ x ) C_ X
25 elpw2g 
 |-  ( X e. _V -> ( ( X \ x ) e. ~P X <-> ( X \ x ) C_ X ) )
26 24 25 mpbiri 
 |-  ( X e. _V -> ( X \ x ) e. ~P X )
27 26 3ad2ant1 
 |-  ( ( X e. _V /\ x C_ X /\ x ~< X ) -> ( X \ x ) e. ~P X )
28 simp2 
 |-  ( ( X e. _V /\ x C_ X /\ x ~< X ) -> x C_ X )
29 dfss4 
 |-  ( x C_ X <-> ( X \ ( X \ x ) ) = x )
30 28 29 sylib 
 |-  ( ( X e. _V /\ x C_ X /\ x ~< X ) -> ( X \ ( X \ x ) ) = x )
31 simp3 
 |-  ( ( X e. _V /\ x C_ X /\ x ~< X ) -> x ~< X )
32 30 31 eqbrtrd 
 |-  ( ( X e. _V /\ x C_ X /\ x ~< X ) -> ( X \ ( X \ x ) ) ~< X )
33 23 27 32 elrabd 
 |-  ( ( X e. _V /\ x C_ X /\ x ~< X ) -> ( X \ x ) e. { y e. ~P X | ( X \ y ) ~< X } )
34 ssel 
 |-  ( { y e. ~P X | ( X \ y ) ~< X } C_ f -> ( ( X \ x ) e. { y e. ~P X | ( X \ y ) ~< X } -> ( X \ x ) e. f ) )
35 33 34 syl5com 
 |-  ( ( X e. _V /\ x C_ X /\ x ~< X ) -> ( { y e. ~P X | ( X \ y ) ~< X } C_ f -> ( X \ x ) e. f ) )
36 35 3expa 
 |-  ( ( ( X e. _V /\ x C_ X ) /\ x ~< X ) -> ( { y e. ~P X | ( X \ y ) ~< X } C_ f -> ( X \ x ) e. f ) )
37 36 impancom 
 |-  ( ( ( X e. _V /\ x C_ X ) /\ { y e. ~P X | ( X \ y ) ~< X } C_ f ) -> ( x ~< X -> ( X \ x ) e. f ) )
38 37 con3d 
 |-  ( ( ( X e. _V /\ x C_ X ) /\ { y e. ~P X | ( X \ y ) ~< X } C_ f ) -> ( -. ( X \ x ) e. f -> -. x ~< X ) )
39 38 impancom 
 |-  ( ( ( X e. _V /\ x C_ X ) /\ -. ( X \ x ) e. f ) -> ( { y e. ~P X | ( X \ y ) ~< X } C_ f -> -. x ~< X ) )
40 10 14 21 39 syl21anc 
 |-  ( ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) /\ x e. f ) -> ( { y e. ~P X | ( X \ y ) ~< X } C_ f -> -. x ~< X ) )
41 bren2 
 |-  ( x ~~ X <-> ( x ~<_ X /\ -. x ~< X ) )
42 41 simplbi2 
 |-  ( x ~<_ X -> ( -. x ~< X -> x ~~ X ) )
43 16 40 42 sylsyld 
 |-  ( ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) /\ x e. f ) -> ( { y e. ~P X | ( X \ y ) ~< X } C_ f -> x ~~ X ) )
44 43 ralrimdva 
 |-  ( ( _om ~<_ X /\ f e. ( UFil ` X ) ) -> ( { y e. ~P X | ( X \ y ) ~< X } C_ f -> A. x e. f x ~~ X ) )
45 44 reximdva 
 |-  ( _om ~<_ X -> ( E. f e. ( UFil ` X ) { y e. ~P X | ( X \ y ) ~< X } C_ f -> E. f e. ( UFil ` X ) A. x e. f x ~~ X ) )
46 8 45 mpd 
 |-  ( _om ~<_ X -> E. f e. ( UFil ` X ) A. x e. f x ~~ X )