Proof of Theorem gchhar
Step | Hyp | Ref
| Expression |
1 | | harcl 8466 |
. . . 4
har |
2 | | simp3 1063 |
. . . 4
GCH GCH
GCH |
3 | | cdadom3 9010 |
. . . 4
har GCH
har har |
4 | 1, 2, 3 | sylancr 695 |
. . 3
GCH GCH
har har |
5 | | domnsym 8086 |
. . . . . . . . 9
|
6 | 5 | 3ad2ant1 1082 |
. . . . . . . 8
GCH GCH
|
7 | | isfinite 8549 |
. . . . . . . 8
|
8 | 6, 7 | sylnibr 319 |
. . . . . . 7
GCH GCH
|
9 | | pwfi 8261 |
. . . . . . 7
|
10 | 8, 9 | sylnib 318 |
. . . . . 6
GCH GCH
|
11 | | cdadom3 9010 |
. . . . . . 7
GCH har har |
12 | 2, 1, 11 | sylancl 694 |
. . . . . 6
GCH GCH
har |
13 | | ovex 6678 |
. . . . . . . 8
har |
14 | 13 | canth2 8113 |
. . . . . . 7
har har |
15 | | pwcdaen 9007 |
. . . . . . . . 9
GCH har har har |
16 | 2, 1, 15 | sylancl 694 |
. . . . . . . 8
GCH GCH
har har |
17 | | pwexg 4850 |
. . . . . . . . . . 11
GCH
|
18 | 2, 17 | syl 17 |
. . . . . . . . . 10
GCH GCH
|
19 | | simp2 1062 |
. . . . . . . . . . 11
GCH GCH
GCH |
20 | | harwdom 8495 |
. . . . . . . . . . 11
GCH har * |
21 | | wdompwdom 8483 |
. . . . . . . . . . 11
har * har |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . 10
GCH GCH
har
|
23 | | xpdom2g 8056 |
. . . . . . . . . 10
har
har |
24 | 18, 22, 23 | syl2anc 693 |
. . . . . . . . 9
GCH GCH
har |
25 | | xpexg 6960 |
. . . . . . . . . . . . . 14
GCH GCH
|
26 | 19, 19, 25 | syl2anc 693 |
. . . . . . . . . . . . 13
GCH GCH
|
27 | | pwexg 4850 |
. . . . . . . . . . . . 13
|
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
GCH GCH
|
29 | | pwcdaen 9007 |
. . . . . . . . . . . 12
GCH |
30 | 2, 28, 29 | syl2anc 693 |
. . . . . . . . . . 11
GCH GCH
|
31 | 30 | ensymd 8007 |
. . . . . . . . . 10
GCH GCH
|
32 | | enrefg 7987 |
. . . . . . . . . . . . . 14
GCH |
33 | 2, 32 | syl 17 |
. . . . . . . . . . . . 13
GCH GCH
|
34 | | gchxpidm 9491 |
. . . . . . . . . . . . . . 15
GCH
|
35 | 19, 8, 34 | syl2anc 693 |
. . . . . . . . . . . . . 14
GCH GCH
|
36 | | pwen 8133 |
. . . . . . . . . . . . . 14
|
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
GCH GCH
|
38 | | cdaen 8995 |
. . . . . . . . . . . . 13
|
39 | 33, 37, 38 | syl2anc 693 |
. . . . . . . . . . . 12
GCH GCH
|
40 | | gchcdaidm 9490 |
. . . . . . . . . . . . 13
GCH |
41 | 2, 10, 40 | syl2anc 693 |
. . . . . . . . . . . 12
GCH GCH
|
42 | | entr 8008 |
. . . . . . . . . . . 12
|
43 | 39, 41, 42 | syl2anc 693 |
. . . . . . . . . . 11
GCH GCH
|
44 | | pwen 8133 |
. . . . . . . . . . 11
|
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
GCH GCH
|
46 | | entr 8008 |
. . . . . . . . . 10
|
47 | 31, 45, 46 | syl2anc 693 |
. . . . . . . . 9
GCH GCH
|
48 | | domentr 8015 |
. . . . . . . . 9
har har |
49 | 24, 47, 48 | syl2anc 693 |
. . . . . . . 8
GCH GCH
har |
50 | | endomtr 8014 |
. . . . . . . 8
har
har har har |
51 | 16, 49, 50 | syl2anc 693 |
. . . . . . 7
GCH GCH
har |
52 | | sdomdomtr 8093 |
. . . . . . 7
har har
har har |
53 | 14, 51, 52 | sylancr 695 |
. . . . . 6
GCH GCH
har |
54 | | gchen1 9447 |
. . . . . 6
GCH
har
har har |
55 | 2, 10, 12, 53, 54 | syl22anc 1327 |
. . . . 5
GCH GCH
har |
56 | | cdacomen 9003 |
. . . . 5
har har |
57 | | entr 8008 |
. . . . 5
har har har har |
58 | 55, 56, 57 | sylancl 694 |
. . . 4
GCH GCH
har |
59 | 58 | ensymd 8007 |
. . 3
GCH GCH
har |
60 | | domentr 8015 |
. . 3
har har har har |
61 | 4, 59, 60 | syl2anc 693 |
. 2
GCH GCH
har |
62 | | gchcdaidm 9490 |
. . . . . 6
GCH
|
63 | 19, 8, 62 | syl2anc 693 |
. . . . 5
GCH GCH
|
64 | | pwen 8133 |
. . . . 5
|
65 | 63, 64 | syl 17 |
. . . 4
GCH GCH
|
66 | | cdadom3 9010 |
. . . . . . . 8
GCH har har |
67 | 19, 1, 66 | sylancl 694 |
. . . . . . 7
GCH GCH
har |
68 | | harndom 8469 |
. . . . . . . 8
har |
69 | | cdadom3 9010 |
. . . . . . . . . . 11
har GCH
har har |
70 | 1, 19, 69 | sylancr 695 |
. . . . . . . . . 10
GCH GCH
har har |
71 | | cdacomen 9003 |
. . . . . . . . . 10
har har |
72 | | domentr 8015 |
. . . . . . . . . 10
har har har har har
har |
73 | 70, 71, 72 | sylancl 694 |
. . . . . . . . 9
GCH GCH
har har |
74 | | domen2 8103 |
. . . . . . . . 9
har har
har har |
75 | 73, 74 | syl5ibrcom 237 |
. . . . . . . 8
GCH GCH
har har |
76 | 68, 75 | mtoi 190 |
. . . . . . 7
GCH GCH
har |
77 | | brsdom 7978 |
. . . . . . 7
har
har
har |
78 | 67, 76, 77 | sylanbrc 698 |
. . . . . 6
GCH GCH
har |
79 | | canth2g 8114 |
. . . . . . . . 9
GCH |
80 | | sdomdom 7983 |
. . . . . . . . 9
|
81 | | cdadom1 9008 |
. . . . . . . . 9
har har |
82 | 19, 79, 80, 81 | 4syl 19 |
. . . . . . . 8
GCH GCH
har har |
83 | | cdadom2 9009 |
. . . . . . . . 9
har
har |
84 | 61, 83 | syl 17 |
. . . . . . . 8
GCH GCH
har |
85 | | domtr 8009 |
. . . . . . . 8
har har har har |
86 | 82, 84, 85 | syl2anc 693 |
. . . . . . 7
GCH GCH
har |
87 | | domentr 8015 |
. . . . . . 7
har
har |
88 | 86, 41, 87 | syl2anc 693 |
. . . . . 6
GCH GCH
har |
89 | | gchen2 9448 |
. . . . . 6
GCH
har
har har |
90 | 19, 8, 78, 88, 89 | syl22anc 1327 |
. . . . 5
GCH GCH
har
|
91 | 90 | ensymd 8007 |
. . . 4
GCH GCH
har |
92 | | entr 8008 |
. . . 4
har
har |
93 | 65, 91, 92 | syl2anc 693 |
. . 3
GCH GCH
har |
94 | | endom 7982 |
. . 3
har
har |
95 | | pwcdadom 9038 |
. . 3
har har |
96 | 93, 94, 95 | 3syl 18 |
. 2
GCH GCH
har |
97 | | sbth 8080 |
. 2
har
har har
|
98 | 61, 96, 97 | syl2anc 693 |
1
GCH GCH
har
|