Metamath Proof Explorer

Theorem gchpwdom

Description: A relationship between dominance over the powerset and strict dominance when the sets involved are infinite GCH-sets. Proposition 3.1 of KanamoriPincus p. 421. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchpwdom 
|- ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) -> ( A ~< B <-> ~P A ~<_ B ) )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> A e. GCH )
2 1 pwexd 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ~P A e. _V )
3 simpl3 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> B e. GCH )
4 djudoml 
 |-  ( ( ~P A e. _V /\ B e. GCH ) -> ~P A ~<_ ( ~P A |_| B ) )
5 2 3 4 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ~P A ~<_ ( ~P A |_| B ) )
6 domen2 
 |-  ( B ~~ ( ~P A |_| B ) -> ( ~P A ~<_ B <-> ~P A ~<_ ( ~P A |_| B ) ) )
7 5 6 syl5ibrcom 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( B ~~ ( ~P A |_| B ) -> ~P A ~<_ B ) )
8 djucomen 
 |-  ( ( B e. GCH /\ ~P A e. _V ) -> ( B |_| ~P A ) ~~ ( ~P A |_| B ) )
9 3 2 8 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( B |_| ~P A ) ~~ ( ~P A |_| B ) )
10 entr 
 |-  ( ( ( B |_| ~P A ) ~~ ( ~P A |_| B ) /\ ( ~P A |_| B ) ~~ ~P B ) -> ( B |_| ~P A ) ~~ ~P B )
11 10 ex 
 |-  ( ( B |_| ~P A ) ~~ ( ~P A |_| B ) -> ( ( ~P A |_| B ) ~~ ~P B -> ( B |_| ~P A ) ~~ ~P B ) )
12 9 11 syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ( ~P A |_| B ) ~~ ~P B -> ( B |_| ~P A ) ~~ ~P B ) )
13 ensym 
 |-  ( ( B |_| ~P A ) ~~ ~P B -> ~P B ~~ ( B |_| ~P A ) )
14 endom 
 |-  ( ~P B ~~ ( B |_| ~P A ) -> ~P B ~<_ ( B |_| ~P A ) )
15 13 14 syl 
 |-  ( ( B |_| ~P A ) ~~ ~P B -> ~P B ~<_ ( B |_| ~P A ) )
16 12 15 syl6 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ( ~P A |_| B ) ~~ ~P B -> ~P B ~<_ ( B |_| ~P A ) ) )
17 domsdomtr 
 |-  ( ( _om ~<_ A /\ A ~< B ) -> _om ~< B )
18 17 3ad2antl1 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> _om ~< B )
19 sdomnsym 
 |-  ( _om ~< B -> -. B ~< _om )
20 18 19 syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> -. B ~< _om )
21 isfinite 
 |-  ( B e. Fin <-> B ~< _om )
22 20 21 sylnibr 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> -. B e. Fin )
23 gchdjuidm 
 |-  ( ( B e. GCH /\ -. B e. Fin ) -> ( B |_| B ) ~~ B )
24 3 22 23 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( B |_| B ) ~~ B )
25 pwen 
 |-  ( ( B |_| B ) ~~ B -> ~P ( B |_| B ) ~~ ~P B )
26 domen1 
 |-  ( ~P ( B |_| B ) ~~ ~P B -> ( ~P ( B |_| B ) ~<_ ( B |_| ~P A ) <-> ~P B ~<_ ( B |_| ~P A ) ) )
27 24 25 26 3syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P ( B |_| B ) ~<_ ( B |_| ~P A ) <-> ~P B ~<_ ( B |_| ~P A ) ) )
28 pwdjudom 
 |-  ( ~P ( B |_| B ) ~<_ ( B |_| ~P A ) -> ~P B ~<_ ~P A )
29 canth2g 
 |-  ( B e. GCH -> B ~< ~P B )
30 sdomdomtr 
 |-  ( ( B ~< ~P B /\ ~P B ~<_ ~P A ) -> B ~< ~P A )
31 30 ex 
 |-  ( B ~< ~P B -> ( ~P B ~<_ ~P A -> B ~< ~P A ) )
32 3 29 31 3syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P B ~<_ ~P A -> B ~< ~P A ) )
33 gchi 
 |-  ( ( A e. GCH /\ A ~< B /\ B ~< ~P A ) -> A e. Fin )
34 33 3expia 
 |-  ( ( A e. GCH /\ A ~< B ) -> ( B ~< ~P A -> A e. Fin ) )
35 34 3ad2antl2 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( B ~< ~P A -> A e. Fin ) )
36 isfinite 
 |-  ( A e. Fin <-> A ~< _om )
37 simpl1 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> _om ~<_ A )
38 domnsym 
 |-  ( _om ~<_ A -> -. A ~< _om )
39 37 38 syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> -. A ~< _om )
40 39 pm2.21d 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( A ~< _om -> ~P A ~<_ B ) )
41 36 40 syl5bi 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( A e. Fin -> ~P A ~<_ B ) )
42 32 35 41 3syld 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P B ~<_ ~P A -> ~P A ~<_ B ) )
43 28 42 syl5 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P ( B |_| B ) ~<_ ( B |_| ~P A ) -> ~P A ~<_ B ) )
44 27 43 sylbird 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P B ~<_ ( B |_| ~P A ) -> ~P A ~<_ B ) )
45 16 44 syld 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ( ~P A |_| B ) ~~ ~P B -> ~P A ~<_ B ) )
46 djudoml 
 |-  ( ( B e. GCH /\ ~P A e. _V ) -> B ~<_ ( B |_| ~P A ) )
47 3 2 46 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> B ~<_ ( B |_| ~P A ) )
48 domentr 
 |-  ( ( B ~<_ ( B |_| ~P A ) /\ ( B |_| ~P A ) ~~ ( ~P A |_| B ) ) -> B ~<_ ( ~P A |_| B ) )
49 47 9 48 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> B ~<_ ( ~P A |_| B ) )
50 sdomdom 
 |-  ( A ~< B -> A ~<_ B )
51 50 adantl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> A ~<_ B )
52 pwdom 
 |-  ( A ~<_ B -> ~P A ~<_ ~P B )
53 51 52 syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ~P A ~<_ ~P B )
54 djudom1 
 |-  ( ( ~P A ~<_ ~P B /\ B e. GCH ) -> ( ~P A |_| B ) ~<_ ( ~P B |_| B ) )
55 53 3 54 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P A |_| B ) ~<_ ( ~P B |_| B ) )
56 sdomdom 
 |-  ( B ~< ~P B -> B ~<_ ~P B )
57 3 29 56 3syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> B ~<_ ~P B )
58 3 pwexd 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ~P B e. _V )
59 djudom2 
 |-  ( ( B ~<_ ~P B /\ ~P B e. _V ) -> ( ~P B |_| B ) ~<_ ( ~P B |_| ~P B ) )
60 57 58 59 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P B |_| B ) ~<_ ( ~P B |_| ~P B ) )
61 domtr 
 |-  ( ( ( ~P A |_| B ) ~<_ ( ~P B |_| B ) /\ ( ~P B |_| B ) ~<_ ( ~P B |_| ~P B ) ) -> ( ~P A |_| B ) ~<_ ( ~P B |_| ~P B ) )
62 55 60 61 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P A |_| B ) ~<_ ( ~P B |_| ~P B ) )
63 pwdju1 
 |-  ( B e. GCH -> ( ~P B |_| ~P B ) ~~ ~P ( B |_| 1o ) )
64 3 63 syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P B |_| ~P B ) ~~ ~P ( B |_| 1o ) )
65 gchdju1 
 |-  ( ( B e. GCH /\ -. B e. Fin ) -> ( B |_| 1o ) ~~ B )
66 3 22 65 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( B |_| 1o ) ~~ B )
67 pwen 
 |-  ( ( B |_| 1o ) ~~ B -> ~P ( B |_| 1o ) ~~ ~P B )
68 66 67 syl 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ~P ( B |_| 1o ) ~~ ~P B )
69 entr 
 |-  ( ( ( ~P B |_| ~P B ) ~~ ~P ( B |_| 1o ) /\ ~P ( B |_| 1o ) ~~ ~P B ) -> ( ~P B |_| ~P B ) ~~ ~P B )
70 64 68 69 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P B |_| ~P B ) ~~ ~P B )
71 domentr 
 |-  ( ( ( ~P A |_| B ) ~<_ ( ~P B |_| ~P B ) /\ ( ~P B |_| ~P B ) ~~ ~P B ) -> ( ~P A |_| B ) ~<_ ~P B )
72 62 70 71 syl2anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( ~P A |_| B ) ~<_ ~P B )
73 gchor 
 |-  ( ( ( B e. GCH /\ -. B e. Fin ) /\ ( B ~<_ ( ~P A |_| B ) /\ ( ~P A |_| B ) ~<_ ~P B ) ) -> ( B ~~ ( ~P A |_| B ) \/ ( ~P A |_| B ) ~~ ~P B ) )
74 3 22 49 72 73 syl22anc 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ( B ~~ ( ~P A |_| B ) \/ ( ~P A |_| B ) ~~ ~P B ) )
75 7 45 74 mpjaod 
 |-  ( ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) /\ A ~< B ) -> ~P A ~<_ B )
76 75 ex 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) -> ( A ~< B -> ~P A ~<_ B ) )
77 reldom 
 |-  Rel ~<_
78 77 brrelex1i 
 |-  ( ~P A ~<_ B -> ~P A e. _V )
79 pwexb 
 |-  ( A e. _V <-> ~P A e. _V )
80 canth2g 
 |-  ( A e. _V -> A ~< ~P A )
81 79 80 sylbir 
 |-  ( ~P A e. _V -> A ~< ~P A )
82 78 81 syl 
 |-  ( ~P A ~<_ B -> A ~< ~P A )
83 sdomdomtr 
 |-  ( ( A ~< ~P A /\ ~P A ~<_ B ) -> A ~< B )
84 82 83 mpancom 
 |-  ( ~P A ~<_ B -> A ~< B )
85 76 84 impbid1 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ B e. GCH ) -> ( A ~< B <-> ~P A ~<_ B ) )