Step | Hyp | Ref
| Expression |
1 | | simp1l 1031 |
. . . . . 6
      
    |
2 | | hllat 32923 |
. . . . . 6
   |
3 | 1, 2 | syl 17 |
. . . . 5
      
    |
4 | | simp2l 1033 |
. . . . 5
      
    |
5 | | simp3l 1035 |
. . . . 5
      
    |
6 | | dihglblem5a.b |
. . . . . 6
     |
7 | | dihglblem5a.l |
. . . . . 6
     |
8 | | dihglblem5a.m |
. . . . . 6
     |
9 | 6, 7, 8 | latmle1 16315 |
. . . . 5
 
     |
10 | 3, 4, 5, 9 | syl3anc 1267 |
. . . 4
      
   
  |
11 | | simp1 1007 |
. . . . 5
      
      |
12 | 6, 8 | latmcl 16291 |
. . . . . 6
 
     |
13 | 3, 4, 5, 12 | syl3anc 1267 |
. . . . 5
      
      |
14 | | dihglblem5a.h |
. . . . . 6
     |
15 | | dihglblem5a.i |
. . . . . 6
         |
16 | 6, 7, 14, 15 | dihord 34826 |
. . . . 5
     
     
 
   
     |
17 | 11, 13, 4, 16 | syl3anc 1267 |
. . . 4
      
             
    |
18 | 10, 17 | mpbird 236 |
. . 3
      
     
 
      |
19 | 6, 7, 8 | latmle2 16316 |
. . . . 5
 
     |
20 | 3, 4, 5, 19 | syl3anc 1267 |
. . . 4
      
   
  |
21 | 6, 7, 14, 15 | dihord 34826 |
. . . . 5
     
     
 
   
     |
22 | 11, 13, 5, 21 | syl3anc 1267 |
. . . 4
      
             
    |
23 | 20, 22 | mpbird 236 |
. . 3
      
     
 
      |
24 | 18, 23 | ssind 3655 |
. 2
      
     
 
            |
25 | 14, 15 | dihvalrel 34841 |
. . . . 5
 
       |
26 | | relin1 4950 |
. . . . 5
    
            |
27 | 25, 26 | syl 17 |
. . . 4
 
             |
28 | 27 | 3ad2ant1 1028 |
. . 3
      
 
            |
29 | | elin 3616 |
. . . 4
                                |
30 | | dihglblem5a.j |
. . . . . . 7
     |
31 | | dihglblem5a.a |
. . . . . . 7
     |
32 | 6, 7, 30, 8, 31, 14 | lhpmcvr2 33583 |
. . . . . 6
       

 
     |
33 | 32 | 3adant3 1027 |
. . . . 5
      
   
 
     |
34 | | simpl1 1010 |
. . . . . . . 8
     
     
 
     
   |
35 | | simpl2 1011 |
. . . . . . . 8
     
     
 
     
   |
36 | | simprl 763 |
. . . . . . . . 9
     
     
 
       |
37 | | simprrl 773 |
. . . . . . . . 9
     
     
 
       |
38 | 36, 37 | jca 535 |
. . . . . . . 8
     
     
 
     
   |
39 | | simprrr 774 |
. . . . . . . 8
     
     
 
     
     |
40 | | dihglblem5a.p |
. . . . . . . . 9
         |
41 | | dihglblem5a.t |
. . . . . . . . 9
         |
42 | | dihglblem5a.r |
. . . . . . . . 9
         |
43 | | dihglblem5a.e |
. . . . . . . . 9
         |
44 | | dihglblem5a.g |
. . . . . . . . 9
        |
45 | | vex 3047 |
. . . . . . . . 9
 |
46 | | vex 3047 |
. . . . . . . . 9
 |
47 | 6, 7, 30, 8, 31, 14, 40, 41, 42, 43, 15, 44, 45, 46 | dihopelvalc 34811 |
. . . . . . . 8
          
   
                          |
48 | 34, 35, 38, 39, 47 | syl112anc 1271 |
. . . . . . 7
     
     
 
                               |
49 | | simpr 463 |
. . . . . . 7
  

                         |
50 | 48, 49 | syl6bi 232 |
. . . . . 6
     
     
 
            
              |
51 | | simpl3 1012 |
. . . . . . . 8
     
     
 
     
   |
52 | | dihglblem5a.o |
. . . . . . . . 9

   |
53 | 6, 7, 14, 41, 42, 52, 15 | dihopelvalbN 34800 |
. . . . . . . 8
                         |
54 | 34, 51, 53 | syl2anc 666 |
. . . . . . 7
     
     
 
                       |
55 | 54 | biimpd 211 |
. . . . . 6
     
     
 
            
          |
56 | | simprll 771 |
. . . . . . . . . 10
                       |
57 | 56 | 3ad2ant3 1030 |
. . . . . . . . 9
     
     
 
               
           |
58 | | simp3rr 1081 |
. . . . . . . . . . . . . . . . . 18
     
     
 
               
          |
59 | 58 | fveq1d 5865 |
. . . . . . . . . . . . . . . . 17
     
     
 
               
                 |
60 | | simp11 1037 |
. . . . . . . . . . . . . . . . . . 19
     
     
 
               
             |
61 | 7, 31, 14, 40 | lhpocnel2 33578 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
     
     
 
               
             |
63 | | simp2l 1033 |
. . . . . . . . . . . . . . . . . . 19
     
     
 
               
           |
64 | | simp2rl 1076 |
. . . . . . . . . . . . . . . . . . 19
     
     
 
               
        
  |
65 | 7, 31, 14, 41, 44 | ltrniotacl 34140 |
. . . . . . . . . . . . . . . . . . 19
      
 
  |
66 | 60, 62, 63, 64, 65 | syl112anc 1271 |
. . . . . . . . . . . . . . . . . 18
     
     
 
               
           |
67 | 52, 6 | tendo02 34348 |
. . . . . . . . . . . . . . . . . 18
      |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . 17
     
     
 
               
          
   |
69 | 59, 68 | eqtrd 2484 |
. . . . . . . . . . . . . . . 16
     
     
 
               
            
   |
70 | 69 | cnveqd 5009 |
. . . . . . . . . . . . . . 15
     
     
 
               
              
   |
71 | | cnvresid 5651 |
. . . . . . . . . . . . . . 15


  |
72 | 70, 71 | syl6eq 2500 |
. . . . . . . . . . . . . 14
     
     
 
               
                 |
73 | 72 | coeq2d 4996 |
. . . . . . . . . . . . 13
     
     
 
               
                     |
74 | 6, 14, 41 | ltrn1o 33683 |
. . . . . . . . . . . . . . 15
    
      |
75 | 60, 57, 74 | syl2anc 666 |
. . . . . . . . . . . . . 14
     
     
 
               
               |
76 | | f1of 5812 |
. . . . . . . . . . . . . 14
    
      |
77 | | fcoi1 5755 |
. . . . . . . . . . . . . 14
          |
78 | 75, 76, 77 | 3syl 18 |
. . . . . . . . . . . . 13
     
     
 
               
              |
79 | 73, 78 | eqtrd 2484 |
. . . . . . . . . . . 12
     
     
 
               
                  |
80 | 79 | fveq2d 5867 |
. . . . . . . . . . 11
     
     
 
               
                          |
81 | | simp3l 1035 |
. . . . . . . . . . 11
     
     
 
               
                      |
82 | 80, 81 | eqbrtrrd 4424 |
. . . . . . . . . 10
     
     
 
               
               |
83 | | simprlr 772 |
. . . . . . . . . . 11
                           |
84 | 83 | 3ad2ant3 1030 |
. . . . . . . . . 10
     
     
 
               
               |
85 | | simp11l 1118 |
. . . . . . . . . . . 12
     
     
 
               
           |
86 | 85, 2 | syl 17 |
. . . . . . . . . . 11
     
     
 
               
           |
87 | 6, 14, 41, 42 | trlcl 33724 |
. . . . . . . . . . . 12
    
      |
88 | 60, 57, 87 | syl2anc 666 |
. . . . . . . . . . 11
     
     
 
               
               |
89 | | simp12l 1120 |
. . . . . . . . . . 11
     
     
 
               
           |
90 | | simp13l 1122 |
. . . . . . . . . . 11
     
     
 
               
           |
91 | 6, 7, 8 | latlem12 16317 |
. . . . . . . . . . 11
      
            
         |
92 | 86, 88, 89, 90, 91 | syl13anc 1269 |
. . . . . . . . . 10
     
     
 
               
                   
         |
93 | 82, 84, 92 | mpbi2and 931 |
. . . . . . . . 9
     
     
 
               
                 |
94 | 57, 93 | jca 535 |
. . . . . . . 8
     
     
 
               
              
    |
95 | 86, 89, 90, 12 | syl3anc 1267 |
. . . . . . . . 9
     
     
 
               
             |
96 | | simp11r 1119 |
. . . . . . . . . . 11
     
     
 
               
           |
97 | 6, 14 | lhpbase 33557 |
. . . . . . . . . . 11
   |
98 | 96, 97 | syl 17 |
. . . . . . . . . 10
     
     
 
               
           |
99 | 86, 89, 90, 19 | syl3anc 1267 |
. . . . . . . . . 10
     
     
 
               
          
  |
100 | | simp13r 1123 |
. . . . . . . . . 10
     
     
 
               
           |
101 | 6, 7, 86, 95, 90, 98, 99, 100 | lattrd 16297 |
. . . . . . . . 9
     
     
 
               
          
  |
102 | 6, 7, 14, 41, 42, 52, 15 | dihopelvalbN 34800 |
. . . . . . . . 9
                  
              |
103 | 60, 95, 101, 102 | syl12anc 1265 |
. . . . . . . 8
     
     
 
               
                         
     |
104 | 94, 58, 103 | mpbir2and 932 |
. . . . . . 7
     
     
 
               
               
    |
105 | 104 | 3expia 1209 |
. . . . . 6
     
     
 
                                      |
106 | 50, 55, 105 | syl2and 486 |
. . . . 5
     
     
 
                     
  
         |
107 | 33, 106 | rexlimddv 2882 |
. . . 4
      
          
  
    
  
         |
108 | 29, 107 | syl5bi 221 |
. . 3
      
          
                 |
109 | 28, 108 | relssdv 4926 |
. 2
      
                    |
110 | 24, 109 | eqssd 3448 |
1
      
     
              |