Metamath Proof Explorer

Theorem ufldom

Description: The ultrafilter lemma property is a cardinal invariant, so since it transfers to subsets it also transfers over set dominance. (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Assertion ufldom 
|- ( ( X e. UFL /\ Y ~<_ X ) -> Y e. UFL )

Proof

Step Hyp Ref Expression
1 domeng 
 |-  ( X e. UFL -> ( Y ~<_ X <-> E. x ( Y ~~ x /\ x C_ X ) ) )
2 bren 
 |-  ( Y ~~ x <-> E. f f : Y -1-1-onto-> x )
3 2 biimpi 
 |-  ( Y ~~ x -> E. f f : Y -1-1-onto-> x )
4 ssufl 
 |-  ( ( X e. UFL /\ x C_ X ) -> x e. UFL )
5 simplr 
 |-  ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) -> x e. UFL )
6 filfbas 
 |-  ( g e. ( Fil ` Y ) -> g e. ( fBas ` Y ) )
7 6 adantl 
 |-  ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) -> g e. ( fBas ` Y ) )
8 f1of 
 |-  ( f : Y -1-1-onto-> x -> f : Y --> x )
9 8 ad2antrr 
 |-  ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) -> f : Y --> x )
10 fmfil 
 |-  ( ( x e. UFL /\ g e. ( fBas ` Y ) /\ f : Y --> x ) -> ( ( x FilMap f ) ` g ) e. ( Fil ` x ) )
11 5 7 9 10 syl3anc 
 |-  ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) -> ( ( x FilMap f ) ` g ) e. ( Fil ` x ) )
12 ufli 
 |-  ( ( x e. UFL /\ ( ( x FilMap f ) ` g ) e. ( Fil ` x ) ) -> E. y e. ( UFil ` x ) ( ( x FilMap f ) ` g ) C_ y )
13 5 11 12 syl2anc 
 |-  ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) -> E. y e. ( UFil ` x ) ( ( x FilMap f ) ` g ) C_ y )
14 f1odm 
 |-  ( f : Y -1-1-onto-> x -> dom f = Y )
15 14 adantr 
 |-  ( ( f : Y -1-1-onto-> x /\ x e. UFL ) -> dom f = Y )
16 vex 
 |-  f e. _V
17 16 dmex 
 |-  dom f e. _V
18 15 17 eqeltrrdi 
 |-  ( ( f : Y -1-1-onto-> x /\ x e. UFL ) -> Y e. _V )
19 18 ad2antrr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> Y e. _V )
20 simprl 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> y e. ( UFil ` x ) )
21 f1ocnv 
 |-  ( f : Y -1-1-onto-> x -> `' f : x -1-1-onto-> Y )
22 21 ad3antrrr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> `' f : x -1-1-onto-> Y )
23 f1of 
 |-  ( `' f : x -1-1-onto-> Y -> `' f : x --> Y )
24 22 23 syl 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> `' f : x --> Y )
25 fmufil 
 |-  ( ( Y e. _V /\ y e. ( UFil ` x ) /\ `' f : x --> Y ) -> ( ( Y FilMap `' f ) ` y ) e. ( UFil ` Y ) )
26 19 20 24 25 syl3anc 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( Y FilMap `' f ) ` y ) e. ( UFil ` Y ) )
27 f1ococnv1 
 |-  ( f : Y -1-1-onto-> x -> ( `' f o. f ) = ( _I |` Y ) )
28 27 ad3antrrr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( `' f o. f ) = ( _I |` Y ) )
29 28 oveq2d 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( Y FilMap ( `' f o. f ) ) = ( Y FilMap ( _I |` Y ) ) )
30 29 fveq1d 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( Y FilMap ( `' f o. f ) ) ` g ) = ( ( Y FilMap ( _I |` Y ) ) ` g ) )
31 5 adantr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> x e. UFL )
32 7 adantr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> g e. ( fBas ` Y ) )
33 8 ad3antrrr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> f : Y --> x )
34 fmco 
 |-  ( ( ( Y e. _V /\ x e. UFL /\ g e. ( fBas ` Y ) ) /\ ( `' f : x --> Y /\ f : Y --> x ) ) -> ( ( Y FilMap ( `' f o. f ) ) ` g ) = ( ( Y FilMap `' f ) ` ( ( x FilMap f ) ` g ) ) )
35 19 31 32 24 33 34 syl32anc 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( Y FilMap ( `' f o. f ) ) ` g ) = ( ( Y FilMap `' f ) ` ( ( x FilMap f ) ` g ) ) )
36 simplr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> g e. ( Fil ` Y ) )
37 fmid 
 |-  ( g e. ( Fil ` Y ) -> ( ( Y FilMap ( _I |` Y ) ) ` g ) = g )
38 36 37 syl 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( Y FilMap ( _I |` Y ) ) ` g ) = g )
39 30 35 38 3eqtr3d 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( Y FilMap `' f ) ` ( ( x FilMap f ) ` g ) ) = g )
40 11 adantr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( x FilMap f ) ` g ) e. ( Fil ` x ) )
41 filfbas 
 |-  ( ( ( x FilMap f ) ` g ) e. ( Fil ` x ) -> ( ( x FilMap f ) ` g ) e. ( fBas ` x ) )
42 40 41 syl 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( x FilMap f ) ` g ) e. ( fBas ` x ) )
43 ufilfil 
 |-  ( y e. ( UFil ` x ) -> y e. ( Fil ` x ) )
44 filfbas 
 |-  ( y e. ( Fil ` x ) -> y e. ( fBas ` x ) )
45 20 43 44 3syl 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> y e. ( fBas ` x ) )
46 simprr 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( x FilMap f ) ` g ) C_ y )
47 fmss 
 |-  ( ( ( Y e. _V /\ ( ( x FilMap f ) ` g ) e. ( fBas ` x ) /\ y e. ( fBas ` x ) ) /\ ( `' f : x --> Y /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( Y FilMap `' f ) ` ( ( x FilMap f ) ` g ) ) C_ ( ( Y FilMap `' f ) ` y ) )
48 19 42 45 24 46 47 syl32anc 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> ( ( Y FilMap `' f ) ` ( ( x FilMap f ) ` g ) ) C_ ( ( Y FilMap `' f ) ` y ) )
49 39 48 eqsstrrd 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> g C_ ( ( Y FilMap `' f ) ` y ) )
50 sseq2 
 |-  ( u = ( ( Y FilMap `' f ) ` y ) -> ( g C_ u <-> g C_ ( ( Y FilMap `' f ) ` y ) ) )
51 50 rspcev 
 |-  ( ( ( ( Y FilMap `' f ) ` y ) e. ( UFil ` Y ) /\ g C_ ( ( Y FilMap `' f ) ` y ) ) -> E. u e. ( UFil ` Y ) g C_ u )
52 26 49 51 syl2anc 
 |-  ( ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) /\ ( y e. ( UFil ` x ) /\ ( ( x FilMap f ) ` g ) C_ y ) ) -> E. u e. ( UFil ` Y ) g C_ u )
53 13 52 rexlimddv 
 |-  ( ( ( f : Y -1-1-onto-> x /\ x e. UFL ) /\ g e. ( Fil ` Y ) ) -> E. u e. ( UFil ` Y ) g C_ u )
54 53 ralrimiva 
 |-  ( ( f : Y -1-1-onto-> x /\ x e. UFL ) -> A. g e. ( Fil ` Y ) E. u e. ( UFil ` Y ) g C_ u )
55 isufl 
 |-  ( Y e. _V -> ( Y e. UFL <-> A. g e. ( Fil ` Y ) E. u e. ( UFil ` Y ) g C_ u ) )
56 18 55 syl 
 |-  ( ( f : Y -1-1-onto-> x /\ x e. UFL ) -> ( Y e. UFL <-> A. g e. ( Fil ` Y ) E. u e. ( UFil ` Y ) g C_ u ) )
57 54 56 mpbird 
 |-  ( ( f : Y -1-1-onto-> x /\ x e. UFL ) -> Y e. UFL )
58 57 ex 
 |-  ( f : Y -1-1-onto-> x -> ( x e. UFL -> Y e. UFL ) )
59 58 exlimiv 
 |-  ( E. f f : Y -1-1-onto-> x -> ( x e. UFL -> Y e. UFL ) )
60 59 imp 
 |-  ( ( E. f f : Y -1-1-onto-> x /\ x e. UFL ) -> Y e. UFL )
61 3 4 60 syl2an 
 |-  ( ( Y ~~ x /\ ( X e. UFL /\ x C_ X ) ) -> Y e. UFL )
62 61 an12s 
 |-  ( ( X e. UFL /\ ( Y ~~ x /\ x C_ X ) ) -> Y e. UFL )
63 62 ex 
 |-  ( X e. UFL -> ( ( Y ~~ x /\ x C_ X ) -> Y e. UFL ) )
64 63 exlimdv 
 |-  ( X e. UFL -> ( E. x ( Y ~~ x /\ x C_ X ) -> Y e. UFL ) )
65 1 64 sylbid 
 |-  ( X e. UFL -> ( Y ~<_ X -> Y e. UFL ) )
66 65 imp 
 |-  ( ( X e. UFL /\ Y ~<_ X ) -> Y e. UFL )