Proof of Theorem gchhar
Step | Hyp | Ref
| Expression |
1 | | harcl 8081 |
. . . 4
har   |
2 | | simp3 1011 |
. . . 4
  GCH  GCH
 GCH |
3 | | cdadom3 8623 |
. . . 4
  har   GCH
har   har      |
4 | 1, 2, 3 | sylancr 670 |
. . 3
  GCH  GCH
har   har      |
5 | | domnsym 7703 |
. . . . . . . . 9

  |
6 | 5 | 3ad2ant1 1030 |
. . . . . . . 8
  GCH  GCH
  |
7 | | isfinite 8162 |
. . . . . . . 8

  |
8 | 6, 7 | sylnibr 307 |
. . . . . . 7
  GCH  GCH
  |
9 | | pwfi 7874 |
. . . . . . 7

   |
10 | 8, 9 | sylnib 306 |
. . . . . 6
  GCH  GCH
   |
11 | | cdadom3 8623 |
. . . . . . 7
   GCH har      har     |
12 | 2, 1, 11 | sylancl 669 |
. . . . . 6
  GCH  GCH
   har     |
13 | | ovex 6323 |
. . . . . . . 8
  har    |
14 | 13 | canth2 7730 |
. . . . . . 7
  har      har    |
15 | | pwcdaen 8620 |
. . . . . . . . 9
   GCH har      har       har     |
16 | 2, 1, 15 | sylancl 669 |
. . . . . . . 8
  GCH  GCH
  
har       har     |
17 | | pwexg 4590 |
. . . . . . . . . . 11
  GCH  
  |
18 | 2, 17 | syl 17 |
. . . . . . . . . 10
  GCH  GCH
 
  |
19 | | simp2 1010 |
. . . . . . . . . . 11
  GCH  GCH
GCH |
20 | | harwdom 8110 |
. . . . . . . . . . 11
 GCH har  *      |
21 | | wdompwdom 8098 |
. . . . . . . . . . 11
 har  *     har        |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . 10
  GCH  GCH
 har    
   |
23 | | xpdom2g 7673 |
. . . . . . . . . 10
   
 har    
      har             |
24 | 18, 22, 23 | syl2anc 667 |
. . . . . . . . 9
  GCH  GCH
  
 har             |
25 | | xpexg 6598 |
. . . . . . . . . . . . . 14
  GCH GCH
    |
26 | 19, 19, 25 | syl2anc 667 |
. . . . . . . . . . . . 13
  GCH  GCH
    |
27 | | pwexg 4590 |
. . . . . . . . . . . . 13
    
   |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
  GCH  GCH
     |
29 | | pwcdaen 8620 |
. . . . . . . . . . . 12
   GCH                      |
30 | 2, 28, 29 | syl2anc 667 |
. . . . . . . . . . 11
  GCH  GCH
  
              |
31 | 30 | ensymd 7625 |
. . . . . . . . . 10
  GCH  GCH
  
  
      
    |
32 | | enrefg 7606 |
. . . . . . . . . . . . . 14
  GCH     |
33 | 2, 32 | syl 17 |
. . . . . . . . . . . . 13
  GCH  GCH
    |
34 | | gchxpidm 9099 |
. . . . . . . . . . . . . . 15
  GCH
  
  |
35 | 19, 8, 34 | syl2anc 667 |
. . . . . . . . . . . . . 14
  GCH  GCH
    |
36 | | pwen 7750 |
. . . . . . . . . . . . . 14
    

   |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
  GCH  GCH
      |
38 | | cdaen 8608 |
. . . . . . . . . . . . 13
          
          |
39 | 33, 37, 38 | syl2anc 667 |
. . . . . . . . . . . 12
  GCH  GCH
            |
40 | | gchcdaidm 9098 |
. . . . . . . . . . . . 13
   GCH          |
41 | 2, 10, 40 | syl2anc 667 |
. . . . . . . . . . . 12
  GCH  GCH
       |
42 | | entr 7626 |
. . . . . . . . . . . 12
         
 
               |
43 | 39, 41, 42 | syl2anc 667 |
. . . . . . . . . . 11
  GCH  GCH
         |
44 | | pwen 7750 |
. . . . . . . . . . 11
    
              |
45 | 43, 44 | syl 17 |
. . . . . . . . . 10
  GCH  GCH
  
        |
46 | | entr 7626 |
. . . . . . . . . 10
                                       |
47 | 31, 45, 46 | syl2anc 667 |
. . . . . . . . 9
  GCH  GCH
  
  
      |
48 | | domentr 7633 |
. . . . . . . . 9
      har                          har       |
49 | 24, 47, 48 | syl2anc 667 |
. . . . . . . 8
  GCH  GCH
  
 har       |
50 | | endomtr 7632 |
. . . . . . . 8
     har  
  
 har       har         har       |
51 | 16, 49, 50 | syl2anc 667 |
. . . . . . 7
  GCH  GCH
  
har       |
52 | | sdomdomtr 7710 |
. . . . . . 7
    har      har  
  
har        har       |
53 | 14, 51, 52 | sylancr 670 |
. . . . . 6
  GCH  GCH
  har       |
54 | | gchen1 9055 |
. . . . . 6
    GCH    
  har    
har          har     |
55 | 2, 10, 12, 53, 54 | syl22anc 1270 |
. . . . 5
  GCH  GCH
   har     |
56 | | cdacomen 8616 |
. . . . 5
  har    har     |
57 | | entr 7626 |
. . . . 5
    
har     har    har       har      |
58 | 55, 56, 57 | sylancl 669 |
. . . 4
  GCH  GCH
  har      |
59 | 58 | ensymd 7625 |
. . 3
  GCH  GCH
 har       |
60 | | domentr 7633 |
. . 3
  har   har     har      har     |
61 | 4, 59, 60 | syl2anc 667 |
. 2
  GCH  GCH
har     |
62 | | gchcdaidm 9098 |
. . . . . 6
  GCH
  
  |
63 | 19, 8, 62 | syl2anc 667 |
. . . . 5
  GCH  GCH
    |
64 | | pwen 7750 |
. . . . 5
    

   |
65 | 63, 64 | syl 17 |
. . . 4
  GCH  GCH
      |
66 | | cdadom3 8623 |
. . . . . . . 8
  GCH har    har     |
67 | 19, 1, 66 | sylancl 669 |
. . . . . . 7
  GCH  GCH
 har     |
68 | | harndom 8084 |
. . . . . . . 8
har   |
69 | | cdadom3 8623 |
. . . . . . . . . . 11
  har  GCH
har   har     |
70 | 1, 19, 69 | sylancr 670 |
. . . . . . . . . 10
  GCH  GCH
har   har     |
71 | | cdacomen 8616 |
. . . . . . . . . 10
 har    har    |
72 | | domentr 7633 |
. . . . . . . . . 10
  har   har    har    har    har  
har     |
73 | 70, 71, 72 | sylancl 669 |
. . . . . . . . 9
  GCH  GCH
har   har     |
74 | | domen2 7720 |
. . . . . . . . 9
  har    har 
har   har      |
75 | 73, 74 | syl5ibrcom 226 |
. . . . . . . 8
  GCH  GCH
  har   har     |
76 | 68, 75 | mtoi 182 |
. . . . . . 7
  GCH  GCH
 har     |
77 | | brsdom 7597 |
. . . . . . 7
  har  
 
har  
 har      |
78 | 67, 76, 77 | sylanbrc 671 |
. . . . . 6
  GCH  GCH
 har     |
79 | | canth2g 7731 |
. . . . . . . . 9
 GCH    |
80 | | sdomdom 7602 |
. . . . . . . . 9
     |
81 | | cdadom1 8621 |
. . . . . . . . 9
   har     har     |
82 | 19, 79, 80, 81 | 4syl 19 |
. . . . . . . 8
  GCH  GCH
 har     har     |
83 | | cdadom2 8622 |
. . . . . . . . 9
 har  
  har         |
84 | 61, 83 | syl 17 |
. . . . . . . 8
  GCH  GCH
  har         |
85 | | domtr 7627 |
. . . . . . . 8
   har     har     har         har         |
86 | 82, 84, 85 | syl2anc 667 |
. . . . . . 7
  GCH  GCH
 har         |
87 | | domentr 7633 |
. . . . . . 7
   har        
 
 
 har      |
88 | 86, 41, 87 | syl2anc 667 |
. . . . . 6
  GCH  GCH
 har      |
89 | | gchen2 9056 |
. . . . . 6
   GCH
   har   
har       har      |
90 | 19, 8, 78, 88, 89 | syl22anc 1270 |
. . . . 5
  GCH  GCH
 har  
   |
91 | 90 | ensymd 7625 |
. . . 4
  GCH  GCH
  har     |
92 | | entr 7626 |
. . . 4
       
har       
har     |
93 | 65, 91, 92 | syl2anc 667 |
. . 3
  GCH  GCH
   
har     |
94 | | endom 7601 |
. . 3
   
 har  
    har     |
95 | | pwcdadom 8651 |
. . 3
     har    har    |
96 | 93, 94, 95 | 3syl 18 |
. 2
  GCH  GCH
 har    |
97 | | sbth 7697 |
. 2
  har  
 har   har 
   |
98 | 61, 96, 97 | syl2anc 667 |
1
  GCH  GCH
har 
   |