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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | domeng | |
|
2 | bren | |
|
3 | 2 | biimpi | |
4 | ssufl | |
|
5 | simplr | |
|
6 | filfbas | |
|
7 | 6 | adantl | |
8 | f1of | |
|
9 | 8 | ad2antrr | |
10 | fmfil | |
|
11 | 5 7 9 10 | syl3anc | |
12 | ufli | |
|
13 | 5 11 12 | syl2anc | |
14 | f1odm | |
|
15 | 14 | adantr | |
16 | vex | |
|
17 | 16 | dmex | |
18 | 15 17 | eqeltrrdi | |
19 | 18 | ad2antrr | |
20 | simprl | |
|
21 | f1ocnv | |
|
22 | 21 | ad3antrrr | |
23 | f1of | |
|
24 | 22 23 | syl | |
25 | fmufil | |
|
26 | 19 20 24 25 | syl3anc | |
27 | f1ococnv1 | |
|
28 | 27 | ad3antrrr | |
29 | 28 | oveq2d | |
30 | 29 | fveq1d | |
31 | 5 | adantr | |
32 | 7 | adantr | |
33 | 8 | ad3antrrr | |
34 | fmco | |
|
35 | 19 31 32 24 33 34 | syl32anc | |
36 | simplr | |
|
37 | fmid | |
|
38 | 36 37 | syl | |
39 | 30 35 38 | 3eqtr3d | |
40 | 11 | adantr | |
41 | filfbas | |
|
42 | 40 41 | syl | |
43 | ufilfil | |
|
44 | filfbas | |
|
45 | 20 43 44 | 3syl | |
46 | simprr | |
|
47 | fmss | |
|
48 | 19 42 45 24 46 47 | syl32anc | |
49 | 39 48 | eqsstrrd | |
50 | sseq2 | |
|
51 | 50 | rspcev | |
52 | 26 49 51 | syl2anc | |
53 | 13 52 | rexlimddv | |
54 | 53 | ralrimiva | |
55 | isufl | |
|
56 | 18 55 | syl | |
57 | 54 56 | mpbird | |
58 | 57 | ex | |
59 | 58 | exlimiv | |
60 | 59 | imp | |
61 | 3 4 60 | syl2an | |
62 | 61 | an12s | |
63 | 62 | ex | |
64 | 63 | exlimdv | |
65 | 1 64 | sylbid | |
66 | 65 | imp | |