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 UFL Y X Y UFL

Proof

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