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 XUFLYXYUFL

Proof

Step Hyp Ref Expression
1 domeng XUFLYXxYxxX
2 bren Yxff:Y1-1 ontox
3 2 biimpi Yxff:Y1-1 ontox
4 ssufl XUFLxXxUFL
5 simplr f:Y1-1 ontoxxUFLgFilYxUFL
6 filfbas gFilYgfBasY
7 6 adantl f:Y1-1 ontoxxUFLgFilYgfBasY
8 f1of f:Y1-1 ontoxf:Yx
9 8 ad2antrr f:Y1-1 ontoxxUFLgFilYf:Yx
10 fmfil xUFLgfBasYf:YxxFilMapfgFilx
11 5 7 9 10 syl3anc f:Y1-1 ontoxxUFLgFilYxFilMapfgFilx
12 ufli xUFLxFilMapfgFilxyUFilxxFilMapfgy
13 5 11 12 syl2anc f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgy
14 f1odm f:Y1-1 ontoxdomf=Y
15 14 adantr f:Y1-1 ontoxxUFLdomf=Y
16 vex fV
17 16 dmex domfV
18 15 17 eqeltrrdi f:Y1-1 ontoxxUFLYV
19 18 ad2antrr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYV
20 simprl f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyyUFilx
21 f1ocnv f:Y1-1 ontoxf-1:x1-1 ontoY
22 21 ad3antrrr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyf-1:x1-1 ontoY
23 f1of f-1:x1-1 ontoYf-1:xY
24 22 23 syl f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyf-1:xY
25 fmufil YVyUFilxf-1:xYYFilMapf-1yUFilY
26 19 20 24 25 syl3anc f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYFilMapf-1yUFilY
27 f1ococnv1 f:Y1-1 ontoxf-1f=IY
28 27 ad3antrrr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyf-1f=IY
29 28 oveq2d f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYFilMapf-1f=YFilMapIY
30 29 fveq1d f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYFilMapf-1fg=YFilMapIYg
31 5 adantr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyxUFL
32 7 adantr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgygfBasY
33 8 ad3antrrr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyf:Yx
34 fmco YVxUFLgfBasYf-1:xYf:YxYFilMapf-1fg=YFilMapf-1xFilMapfg
35 19 31 32 24 33 34 syl32anc f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYFilMapf-1fg=YFilMapf-1xFilMapfg
36 simplr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgygFilY
37 fmid gFilYYFilMapIYg=g
38 36 37 syl f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYFilMapIYg=g
39 30 35 38 3eqtr3d f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYFilMapf-1xFilMapfg=g
40 11 adantr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyxFilMapfgFilx
41 filfbas xFilMapfgFilxxFilMapfgfBasx
42 40 41 syl f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyxFilMapfgfBasx
43 ufilfil yUFilxyFilx
44 filfbas yFilxyfBasx
45 20 43 44 3syl f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyyfBasx
46 simprr f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyxFilMapfgy
47 fmss YVxFilMapfgfBasxyfBasxf-1:xYxFilMapfgyYFilMapf-1xFilMapfgYFilMapf-1y
48 19 42 45 24 46 47 syl32anc f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyYFilMapf-1xFilMapfgYFilMapf-1y
49 39 48 eqsstrrd f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgygYFilMapf-1y
50 sseq2 u=YFilMapf-1ygugYFilMapf-1y
51 50 rspcev YFilMapf-1yUFilYgYFilMapf-1yuUFilYgu
52 26 49 51 syl2anc f:Y1-1 ontoxxUFLgFilYyUFilxxFilMapfgyuUFilYgu
53 13 52 rexlimddv f:Y1-1 ontoxxUFLgFilYuUFilYgu
54 53 ralrimiva f:Y1-1 ontoxxUFLgFilYuUFilYgu
55 isufl YVYUFLgFilYuUFilYgu
56 18 55 syl f:Y1-1 ontoxxUFLYUFLgFilYuUFilYgu
57 54 56 mpbird f:Y1-1 ontoxxUFLYUFL
58 57 ex f:Y1-1 ontoxxUFLYUFL
59 58 exlimiv ff:Y1-1 ontoxxUFLYUFL
60 59 imp ff:Y1-1 ontoxxUFLYUFL
61 3 4 60 syl2an YxXUFLxXYUFL
62 61 an12s XUFLYxxXYUFL
63 62 ex XUFLYxxXYUFL
64 63 exlimdv XUFLxYxxXYUFL
65 1 64 sylbid XUFLYXYUFL
66 65 imp XUFLYXYUFL