Metamath Proof Explorer

Theorem gchhar

Description: A "local" form of gchac . If A and ~P A are GCH-sets, then the Hartogs number of A is ~P A (so ~P A and a fortiori A are well-orderable). The proof is due to Specker. Theorem 2.1 of KanamoriPincus p. 419. (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Assertion gchhar 
|- ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( har ` A ) ~~ ~P A )

Proof

Step Hyp Ref Expression
1 harcl 
 |-  ( har ` A ) e. On
2 simp3 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P A e. GCH )
3 djudoml 
 |-  ( ( ( har ` A ) e. On /\ ~P A e. GCH ) -> ( har ` A ) ~<_ ( ( har ` A ) |_| ~P A ) )
4 1 2 3 sylancr 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( har ` A ) ~<_ ( ( har ` A ) |_| ~P A ) )
5 domnsym 
 |-  ( _om ~<_ A -> -. A ~< _om )
6 5 3ad2ant1 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> -. A ~< _om )
7 isfinite 
 |-  ( A e. Fin <-> A ~< _om )
8 6 7 sylnibr 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> -. A e. Fin )
9 pwfi 
 |-  ( A e. Fin <-> ~P A e. Fin )
10 8 9 sylnib 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> -. ~P A e. Fin )
11 djudoml 
 |-  ( ( ~P A e. GCH /\ ( har ` A ) e. On ) -> ~P A ~<_ ( ~P A |_| ( har ` A ) ) )
12 2 1 11 sylancl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P A ~<_ ( ~P A |_| ( har ` A ) ) )
13 fvexd 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( har ` A ) e. _V )
14 djuex 
 |-  ( ( ~P A e. GCH /\ ( har ` A ) e. _V ) -> ( ~P A |_| ( har ` A ) ) e. _V )
15 2 13 14 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ( har ` A ) ) e. _V )
16 canth2g 
 |-  ( ( ~P A |_| ( har ` A ) ) e. _V -> ( ~P A |_| ( har ` A ) ) ~< ~P ( ~P A |_| ( har ` A ) ) )
17 15 16 syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ( har ` A ) ) ~< ~P ( ~P A |_| ( har ` A ) ) )
18 pwdjuen 
 |-  ( ( ~P A e. GCH /\ ( har ` A ) e. On ) -> ~P ( ~P A |_| ( har ` A ) ) ~~ ( ~P ~P A X. ~P ( har ` A ) ) )
19 2 1 18 sylancl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( ~P A |_| ( har ` A ) ) ~~ ( ~P ~P A X. ~P ( har ` A ) ) )
20 2 pwexd 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ~P A e. _V )
21 simp2 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> A e. GCH )
22 harwdom 
 |-  ( A e. GCH -> ( har ` A ) ~<_* ~P ( A X. A ) )
23 wdompwdom 
 |-  ( ( har ` A ) ~<_* ~P ( A X. A ) -> ~P ( har ` A ) ~<_ ~P ~P ( A X. A ) )
24 21 22 23 3syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( har ` A ) ~<_ ~P ~P ( A X. A ) )
25 xpdom2g 
 |-  ( ( ~P ~P A e. _V /\ ~P ( har ` A ) ~<_ ~P ~P ( A X. A ) ) -> ( ~P ~P A X. ~P ( har ` A ) ) ~<_ ( ~P ~P A X. ~P ~P ( A X. A ) ) )
26 20 24 25 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P ~P A X. ~P ( har ` A ) ) ~<_ ( ~P ~P A X. ~P ~P ( A X. A ) ) )
27 21 21 xpexd 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A X. A ) e. _V )
28 27 pwexd 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( A X. A ) e. _V )
29 pwdjuen 
 |-  ( ( ~P A e. GCH /\ ~P ( A X. A ) e. _V ) -> ~P ( ~P A |_| ~P ( A X. A ) ) ~~ ( ~P ~P A X. ~P ~P ( A X. A ) ) )
30 2 28 29 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( ~P A |_| ~P ( A X. A ) ) ~~ ( ~P ~P A X. ~P ~P ( A X. A ) ) )
31 30 ensymd 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P ~P A X. ~P ~P ( A X. A ) ) ~~ ~P ( ~P A |_| ~P ( A X. A ) ) )
32 enrefg 
 |-  ( ~P A e. GCH -> ~P A ~~ ~P A )
33 2 32 syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P A ~~ ~P A )
34 gchxpidm 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A X. A ) ~~ A )
35 21 8 34 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A X. A ) ~~ A )
36 pwen 
 |-  ( ( A X. A ) ~~ A -> ~P ( A X. A ) ~~ ~P A )
37 35 36 syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( A X. A ) ~~ ~P A )
38 djuen 
 |-  ( ( ~P A ~~ ~P A /\ ~P ( A X. A ) ~~ ~P A ) -> ( ~P A |_| ~P ( A X. A ) ) ~~ ( ~P A |_| ~P A ) )
39 33 37 38 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ~P ( A X. A ) ) ~~ ( ~P A |_| ~P A ) )
40 gchdjuidm 
 |-  ( ( ~P A e. GCH /\ -. ~P A e. Fin ) -> ( ~P A |_| ~P A ) ~~ ~P A )
41 2 10 40 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ~P A ) ~~ ~P A )
42 entr 
 |-  ( ( ( ~P A |_| ~P ( A X. A ) ) ~~ ( ~P A |_| ~P A ) /\ ( ~P A |_| ~P A ) ~~ ~P A ) -> ( ~P A |_| ~P ( A X. A ) ) ~~ ~P A )
43 39 41 42 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ~P ( A X. A ) ) ~~ ~P A )
44 pwen 
 |-  ( ( ~P A |_| ~P ( A X. A ) ) ~~ ~P A -> ~P ( ~P A |_| ~P ( A X. A ) ) ~~ ~P ~P A )
45 43 44 syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( ~P A |_| ~P ( A X. A ) ) ~~ ~P ~P A )
46 entr 
 |-  ( ( ( ~P ~P A X. ~P ~P ( A X. A ) ) ~~ ~P ( ~P A |_| ~P ( A X. A ) ) /\ ~P ( ~P A |_| ~P ( A X. A ) ) ~~ ~P ~P A ) -> ( ~P ~P A X. ~P ~P ( A X. A ) ) ~~ ~P ~P A )
47 31 45 46 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P ~P A X. ~P ~P ( A X. A ) ) ~~ ~P ~P A )
48 domentr 
 |-  ( ( ( ~P ~P A X. ~P ( har ` A ) ) ~<_ ( ~P ~P A X. ~P ~P ( A X. A ) ) /\ ( ~P ~P A X. ~P ~P ( A X. A ) ) ~~ ~P ~P A ) -> ( ~P ~P A X. ~P ( har ` A ) ) ~<_ ~P ~P A )
49 26 47 48 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P ~P A X. ~P ( har ` A ) ) ~<_ ~P ~P A )
50 endomtr 
 |-  ( ( ~P ( ~P A |_| ( har ` A ) ) ~~ ( ~P ~P A X. ~P ( har ` A ) ) /\ ( ~P ~P A X. ~P ( har ` A ) ) ~<_ ~P ~P A ) -> ~P ( ~P A |_| ( har ` A ) ) ~<_ ~P ~P A )
51 19 49 50 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( ~P A |_| ( har ` A ) ) ~<_ ~P ~P A )
52 sdomdomtr 
 |-  ( ( ( ~P A |_| ( har ` A ) ) ~< ~P ( ~P A |_| ( har ` A ) ) /\ ~P ( ~P A |_| ( har ` A ) ) ~<_ ~P ~P A ) -> ( ~P A |_| ( har ` A ) ) ~< ~P ~P A )
53 17 51 52 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ( har ` A ) ) ~< ~P ~P A )
54 gchen1 
 |-  ( ( ( ~P A e. GCH /\ -. ~P A e. Fin ) /\ ( ~P A ~<_ ( ~P A |_| ( har ` A ) ) /\ ( ~P A |_| ( har ` A ) ) ~< ~P ~P A ) ) -> ~P A ~~ ( ~P A |_| ( har ` A ) ) )
55 2 10 12 53 54 syl22anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P A ~~ ( ~P A |_| ( har ` A ) ) )
56 djucomen 
 |-  ( ( ~P A e. GCH /\ ( har ` A ) e. _V ) -> ( ~P A |_| ( har ` A ) ) ~~ ( ( har ` A ) |_| ~P A ) )
57 2 13 56 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ( har ` A ) ) ~~ ( ( har ` A ) |_| ~P A ) )
58 entr 
 |-  ( ( ~P A ~~ ( ~P A |_| ( har ` A ) ) /\ ( ~P A |_| ( har ` A ) ) ~~ ( ( har ` A ) |_| ~P A ) ) -> ~P A ~~ ( ( har ` A ) |_| ~P A ) )
59 55 57 58 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P A ~~ ( ( har ` A ) |_| ~P A ) )
60 59 ensymd 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ( har ` A ) |_| ~P A ) ~~ ~P A )
61 domentr 
 |-  ( ( ( har ` A ) ~<_ ( ( har ` A ) |_| ~P A ) /\ ( ( har ` A ) |_| ~P A ) ~~ ~P A ) -> ( har ` A ) ~<_ ~P A )
62 4 60 61 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( har ` A ) ~<_ ~P A )
63 gchdjuidm 
 |-  ( ( A e. GCH /\ -. A e. Fin ) -> ( A |_| A ) ~~ A )
64 21 8 63 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A |_| A ) ~~ A )
65 pwen 
 |-  ( ( A |_| A ) ~~ A -> ~P ( A |_| A ) ~~ ~P A )
66 64 65 syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( A |_| A ) ~~ ~P A )
67 djudoml 
 |-  ( ( A e. GCH /\ ( har ` A ) e. On ) -> A ~<_ ( A |_| ( har ` A ) ) )
68 21 1 67 sylancl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> A ~<_ ( A |_| ( har ` A ) ) )
69 harndom 
 |-  -. ( har ` A ) ~<_ A
70 djudoml 
 |-  ( ( ( har ` A ) e. On /\ A e. GCH ) -> ( har ` A ) ~<_ ( ( har ` A ) |_| A ) )
71 1 21 70 sylancr 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( har ` A ) ~<_ ( ( har ` A ) |_| A ) )
72 djucomen 
 |-  ( ( ( har ` A ) e. On /\ A e. GCH ) -> ( ( har ` A ) |_| A ) ~~ ( A |_| ( har ` A ) ) )
73 1 21 72 sylancr 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ( har ` A ) |_| A ) ~~ ( A |_| ( har ` A ) ) )
74 domentr 
 |-  ( ( ( har ` A ) ~<_ ( ( har ` A ) |_| A ) /\ ( ( har ` A ) |_| A ) ~~ ( A |_| ( har ` A ) ) ) -> ( har ` A ) ~<_ ( A |_| ( har ` A ) ) )
75 71 73 74 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( har ` A ) ~<_ ( A |_| ( har ` A ) ) )
76 domen2 
 |-  ( A ~~ ( A |_| ( har ` A ) ) -> ( ( har ` A ) ~<_ A <-> ( har ` A ) ~<_ ( A |_| ( har ` A ) ) ) )
77 75 76 syl5ibrcom 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A ~~ ( A |_| ( har ` A ) ) -> ( har ` A ) ~<_ A ) )
78 69 77 mtoi 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> -. A ~~ ( A |_| ( har ` A ) ) )
79 brsdom 
 |-  ( A ~< ( A |_| ( har ` A ) ) <-> ( A ~<_ ( A |_| ( har ` A ) ) /\ -. A ~~ ( A |_| ( har ` A ) ) ) )
80 68 78 79 sylanbrc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> A ~< ( A |_| ( har ` A ) ) )
81 canth2g 
 |-  ( A e. GCH -> A ~< ~P A )
82 sdomdom 
 |-  ( A ~< ~P A -> A ~<_ ~P A )
83 21 81 82 3syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> A ~<_ ~P A )
84 djudom1 
 |-  ( ( A ~<_ ~P A /\ ( har ` A ) e. On ) -> ( A |_| ( har ` A ) ) ~<_ ( ~P A |_| ( har ` A ) ) )
85 83 1 84 sylancl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A |_| ( har ` A ) ) ~<_ ( ~P A |_| ( har ` A ) ) )
86 djudom2 
 |-  ( ( ( har ` A ) ~<_ ~P A /\ ~P A e. GCH ) -> ( ~P A |_| ( har ` A ) ) ~<_ ( ~P A |_| ~P A ) )
87 62 2 86 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( ~P A |_| ( har ` A ) ) ~<_ ( ~P A |_| ~P A ) )
88 domtr 
 |-  ( ( ( A |_| ( har ` A ) ) ~<_ ( ~P A |_| ( har ` A ) ) /\ ( ~P A |_| ( har ` A ) ) ~<_ ( ~P A |_| ~P A ) ) -> ( A |_| ( har ` A ) ) ~<_ ( ~P A |_| ~P A ) )
89 85 87 88 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A |_| ( har ` A ) ) ~<_ ( ~P A |_| ~P A ) )
90 domentr 
 |-  ( ( ( A |_| ( har ` A ) ) ~<_ ( ~P A |_| ~P A ) /\ ( ~P A |_| ~P A ) ~~ ~P A ) -> ( A |_| ( har ` A ) ) ~<_ ~P A )
91 89 41 90 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A |_| ( har ` A ) ) ~<_ ~P A )
92 gchen2 
 |-  ( ( ( A e. GCH /\ -. A e. Fin ) /\ ( A ~< ( A |_| ( har ` A ) ) /\ ( A |_| ( har ` A ) ) ~<_ ~P A ) ) -> ( A |_| ( har ` A ) ) ~~ ~P A )
93 21 8 80 91 92 syl22anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( A |_| ( har ` A ) ) ~~ ~P A )
94 93 ensymd 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P A ~~ ( A |_| ( har ` A ) ) )
95 entr 
 |-  ( ( ~P ( A |_| A ) ~~ ~P A /\ ~P A ~~ ( A |_| ( har ` A ) ) ) -> ~P ( A |_| A ) ~~ ( A |_| ( har ` A ) ) )
96 66 94 95 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P ( A |_| A ) ~~ ( A |_| ( har ` A ) ) )
97 endom 
 |-  ( ~P ( A |_| A ) ~~ ( A |_| ( har ` A ) ) -> ~P ( A |_| A ) ~<_ ( A |_| ( har ` A ) ) )
98 pwdjudom 
 |-  ( ~P ( A |_| A ) ~<_ ( A |_| ( har ` A ) ) -> ~P A ~<_ ( har ` A ) )
99 96 97 98 3syl 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ~P A ~<_ ( har ` A ) )
100 sbth 
 |-  ( ( ( har ` A ) ~<_ ~P A /\ ~P A ~<_ ( har ` A ) ) -> ( har ` A ) ~~ ~P A )
101 62 99 100 syl2anc 
 |-  ( ( _om ~<_ A /\ A e. GCH /\ ~P A e. GCH ) -> ( har ` A ) ~~ ~P A )