Step | Hyp | Ref
| Expression |
1 | | dihglbc.h |
. . . 4
     |
2 | | dihglbc.i |
. . . 4
         |
3 | 1, 2 | dihvalrel 34893 |
. . 3
 
           |
4 | 3 | 3ad2ant1 1035 |
. 2
                     |
5 | | simp2r 1041 |
. . . . . 6
             |
6 | | n0 3753 |
. . . . . 6
    |
7 | 5, 6 | sylib 201 |
. . . . 5
           
  |
8 | | simpr 467 |
. . . . . . . 8
               |
9 | | simpl1 1017 |
. . . . . . . . 9
             
   |
10 | 1, 2 | dihvalrel 34893 |
. . . . . . . . 9
 
       |
11 | 9, 10 | syl 17 |
. . . . . . . 8
                   |
12 | 8, 11 | jca 539 |
. . . . . . 7
                     |
13 | 12 | ex 440 |
. . . . . 6
                     |
14 | 13 | eximdv 1775 |
. . . . 5
                        |
15 | 7, 14 | mpd 15 |
. . . 4
                     |
16 | | df-rex 2755 |
. . . 4
                |
17 | 15, 16 | sylibr 217 |
. . 3
           
      |
18 | | reliin 4977 |
. . 3
     

      |
19 | 17, 18 | syl 17 |
. 2
                  |
20 | | id 22 |
. 2
                       |
21 | | simp1 1014 |
. . . . 5
               |
22 | | simp1l 1038 |
. . . . . . 7
          
  |
23 | | hlclat 32970 |
. . . . . . 7
   |
24 | 22, 23 | syl 17 |
. . . . . 6
          
  |
25 | | simp2l 1040 |
. . . . . 6
             |
26 | | dihglbc.b |
. . . . . . 7
     |
27 | | dihglbc.g |
. . . . . . 7
     |
28 | 26, 27 | clatglbcl 16415 |
. . . . . 6
         |
29 | 24, 25, 28 | syl2anc 671 |
. . . . 5
                 |
30 | | simp3 1016 |
. . . . 5
                 |
31 | | dihglbc.l |
. . . . . 6
     |
32 | | dihglbcpre.j |
. . . . . 6
     |
33 | | dihglbcpre.m |
. . . . . 6
     |
34 | | dihglbcpre.a |
. . . . . 6
     |
35 | 26, 31, 32, 33, 34, 1 | lhpmcvr2 33635 |
. . . . 5
               

               |
36 | 21, 29, 30, 35 | syl12anc 1274 |
. . . 4
           

               |
37 | | simpl1 1017 |
. . . . . . . . 9
                             
   |
38 | 29 | adantr 471 |
. . . . . . . . 9
                                   |
39 | | simpl3 1019 |
. . . . . . . . 9
                                   |
40 | | simpr 467 |
. . . . . . . . 9
                                               |
41 | | dihglbcpre.p |
. . . . . . . . . 10
         |
42 | | dihglbcpre.t |
. . . . . . . . . 10
         |
43 | | dihglbcpre.r |
. . . . . . . . . 10
         |
44 | | dihglbcpre.e |
. . . . . . . . . 10
         |
45 | | dihglbcpre.f |
. . . . . . . . . 10
        |
46 | | vex 3060 |
. . . . . . . . . 10
 |
47 | | vex 3060 |
. . . . . . . . . 10
 |
48 | 26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47 | dihopelvalc 34863 |
. . . . . . . . 9
                                                                 |
49 | 37, 38, 39, 40, 48 | syl121anc 1281 |
. . . . . . . 8
                                                               |
50 | | simpl2r 1068 |
. . . . . . . . . . 11
                               |
51 | | r19.28zv 3876 |
. . . . . . . . . . 11

 
 

           
 
            
    |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
                              
              
 
            
    |
53 | | simp11 1044 |
. . . . . . . . . . . . 13
                             
   |
54 | | simp12l 1127 |
. . . . . . . . . . . . . 14
                               |
55 | | simp3 1016 |
. . . . . . . . . . . . . 14
                               |
56 | 54, 55 | sseldd 3445 |
. . . . . . . . . . . . 13
                               |
57 | | simp13 1046 |
. . . . . . . . . . . . . 14
                                   |
58 | | simp11l 1125 |
. . . . . . . . . . . . . . . . 17
                               |
59 | 58, 23 | syl 17 |
. . . . . . . . . . . . . . . 16
                               |
60 | 26, 31, 27 | clatglble 16426 |
. . . . . . . . . . . . . . . 16
         |
61 | 59, 54, 55, 60 | syl3anc 1276 |
. . . . . . . . . . . . . . 15
                                   |
62 | | hllat 32975 |
. . . . . . . . . . . . . . . . 17
   |
63 | 58, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
                               |
64 | 29 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . 16
                                   |
65 | | simp11r 1126 |
. . . . . . . . . . . . . . . . 17
                               |
66 | 26, 1 | lhpbase 33609 |
. . . . . . . . . . . . . . . . 17
   |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
                               |
68 | 26, 31 | lattr 16357 |
. . . . . . . . . . . . . . . 16
      
                |
69 | 63, 64, 56, 67, 68 | syl13anc 1278 |
. . . . . . . . . . . . . . 15
                                           |
70 | 61, 69 | mpand 686 |
. . . . . . . . . . . . . 14
                                     |
71 | 57, 70 | mtod 182 |
. . . . . . . . . . . . 13
                               |
72 | | simp2l 1040 |
. . . . . . . . . . . . 13
                             
   |
73 | | simp2ll 1081 |
. . . . . . . . . . . . . . 15
                               |
74 | 26, 34 | atbase 32901 |
. . . . . . . . . . . . . . . . 17
   |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . 16
                               |
76 | 26, 33 | latmcl 16353 |
. . . . . . . . . . . . . . . . . . 19
           
   |
77 | 63, 64, 67, 76 | syl3anc 1276 |
. . . . . . . . . . . . . . . . . 18
                                 
   |
78 | 26, 31, 32 | latlej1 16361 |
. . . . . . . . . . . . . . . . . 18
 
                 |
79 | 63, 75, 77, 78 | syl3anc 1276 |
. . . . . . . . . . . . . . . . 17
                                  
    |
80 | | simp2r 1041 |
. . . . . . . . . . . . . . . . 17
                             
             |
81 | 79, 80 | breqtrd 4443 |
. . . . . . . . . . . . . . . 16
                                   |
82 | 26, 31, 63, 75, 64, 56, 81, 61 | lattrd 16359 |
. . . . . . . . . . . . . . 15
                               |
83 | 26, 31, 32, 33, 34 | atmod3i1 33475 |
. . . . . . . . . . . . . . 15
  


    
     |
84 | 58, 73, 56, 67, 82, 83 | syl131anc 1289 |
. . . . . . . . . . . . . 14
                             
    
    |
85 | | eqid 2462 |
. . . . . . . . . . . . . . . . 17
         |
86 | 31, 32, 85, 34, 1 | lhpjat2 33632 |
. . . . . . . . . . . . . . . 16
               |
87 | 53, 72, 86 | syl2anc 671 |
. . . . . . . . . . . . . . 15
                             
       |
88 | 87 | oveq2d 6336 |
. . . . . . . . . . . . . 14
                             
           |
89 | | hlol 32973 |
. . . . . . . . . . . . . . . 16
   |
90 | 58, 89 | syl 17 |
. . . . . . . . . . . . . . 15
                               |
91 | 26, 33, 85 | olm11 32839 |
. . . . . . . . . . . . . . 15
 
         |
92 | 90, 56, 91 | syl2anc 671 |
. . . . . . . . . . . . . 14
                             
       |
93 | 84, 88, 92 | 3eqtrd 2500 |
. . . . . . . . . . . . 13
                             
     |
94 | 26, 31, 32, 33, 34, 1, 41, 42, 43, 44, 2, 45, 46, 47 | dihopelvalc 34863 |
. . . . . . . . . . . . 13
          
   
                          |
95 | 53, 56, 71, 72, 93, 94 | syl122anc 1285 |
. . . . . . . . . . . 12
                                                       |
96 | 95 | 3expa 1215 |
. . . . . . . . . . 11
                                                         |
97 | 96 | ralbidva 2836 |
. . . . . . . . . 10
                              
                          |
98 | | simp11l 1125 |
. . . . . . . . . . . . . 14
                              
  |
99 | 98, 23 | syl 17 |
. . . . . . . . . . . . 13
                              
  |
100 | | simp11 1044 |
. . . . . . . . . . . . . 14
                                   |
101 | | simp3l 1042 |
. . . . . . . . . . . . . . 15
                                 |
102 | | simp3r 1043 |
. . . . . . . . . . . . . . . . 17
                                 |
103 | 31, 34, 1, 41 | lhpocnel2 33630 |
. . . . . . . . . . . . . . . . . . 19
 
     |
104 | 100, 103 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                                   |
105 | | simp2l 1040 |
. . . . . . . . . . . . . . . . . 18
                                   |
106 | 31, 34, 1, 42, 45 | ltrniotacl 34192 |
. . . . . . . . . . . . . . . . . 18
      
 
  |
107 | 100, 104,
105, 106 | syl3anc 1276 |
. . . . . . . . . . . . . . . . 17
                              
  |
108 | 1, 42, 44 | tendocl 34380 |
. . . . . . . . . . . . . . . . 17
   

      |
109 | 100, 102,
107, 108 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
                                     |
110 | 1, 42 | ltrncnv 33757 |
. . . . . . . . . . . . . . . 16
        
       |
111 | 100, 109,
110 | syl2anc 671 |
. . . . . . . . . . . . . . 15
                                      |
112 | 1, 42 | ltrnco 34332 |
. . . . . . . . . . . . . . 15
         
         |
113 | 100, 101,
111, 112 | syl3anc 1276 |
. . . . . . . . . . . . . 14
                                        |
114 | 26, 1, 42, 43 | trlcl 33776 |
. . . . . . . . . . . . . 14
                         |
115 | 100, 113,
114 | syl2anc 671 |
. . . . . . . . . . . . 13
                                            |
116 | | simp12l 1127 |
. . . . . . . . . . . . 13
                                 |
117 | 26, 31, 27 | clatleglb 16427 |
. . . . . . . . . . . . 13
                             

              |
118 | 99, 115, 116, 117 | syl3anc 1276 |
. . . . . . . . . . . 12
                                               
          
   |
119 | 118 | 3expa 1215 |
. . . . . . . . . . 11
                              
 
                           
   |
120 | 119 | pm5.32da 651 |
. . . . . . . . . 10
                                                
 
            
    |
121 | 52, 97, 120 | 3bitr4rd 294 |
. . . . . . . . 9
                                                

  
       |
122 | | opex 4681 |
. . . . . . . . . 10
    |
123 | | eliin 4298 |
. . . . . . . . . 10
   
        

  
       |
124 | 122, 123 | ax-mp 5 |
. . . . . . . . 9
                   |
125 | 121, 124 | syl6bbr 271 |
. . . . . . . 8
                                                
  

       |
126 | 49, 125 | bitrd 261 |
. . . . . . 7
                                                    |
127 | 126 | exp44 622 |
. . . . . 6
                                                    |
128 | 127 | imp4a 598 |
. . . . 5
                          
                         |
129 | 128 | rexlimdv 2889 |
. . . 4
                          
                        |
130 | 36, 129 | mpd 15 |
. . 3
                                  |
131 | 130 | eqrelrdv2 4956 |
. 2
                                    
      |
132 | 4, 19, 20, 131 | syl21anc 1275 |
1
                   
      |