Step | Hyp | Ref
| Expression |
1 | | hllat 32929 |
. . . . . 6
   |
2 | 1 | ad2antrr 732 |
. . . . 5
      
  |
3 | | simprl 764 |
. . . . 5
      
  |
4 | | dihglblem5a.b |
. . . . . . 7
     |
5 | | dihglblem5a.h |
. . . . . . 7
     |
6 | 4, 5 | lhpbase 33563 |
. . . . . 6
   |
7 | 6 | ad2antlr 733 |
. . . . 5
      
  |
8 | | dihglblem5a.l |
. . . . . 6
     |
9 | | dihglblem5a.m |
. . . . . 6
     |
10 | 4, 8, 9 | latmle1 16322 |
. . . . 5
 
     |
11 | 2, 3, 7, 10 | syl3anc 1268 |
. . . 4
           |
12 | | simpl 459 |
. . . . 5
           |
13 | 4, 9 | latmcl 16298 |
. . . . . 6
 
     |
14 | 2, 3, 7, 13 | syl3anc 1268 |
. . . . 5
           |
15 | | dihglblem5a.i |
. . . . . 6
         |
16 | 4, 8, 5, 15 | dihord 34832 |
. . . . 5
     
     
 
   
     |
17 | 12, 14, 3, 16 | syl3anc 1268 |
. . . 4
           
 
   
     |
18 | 11, 17 | mpbird 236 |
. . 3
                   |
19 | 4, 8, 9 | latmle2 16323 |
. . . . 5
 
     |
20 | 2, 3, 7, 19 | syl3anc 1268 |
. . . 4
           |
21 | 4, 8, 5, 15 | dihord 34832 |
. . . . 5
     
     
 
   
     |
22 | 12, 14, 7, 21 | syl3anc 1268 |
. . . 4
           
 
   
     |
23 | 20, 22 | mpbird 236 |
. . 3
                   |
24 | 18, 23 | ssind 3656 |
. 2
                         |
25 | 5, 15 | dihvalrel 34847 |
. . . . 5
 
       |
26 | | relin1 4951 |
. . . . 5
    
            |
27 | 25, 26 | syl 17 |
. . . 4
 
             |
28 | 27 | adantr 467 |
. . 3
                   |
29 | | elin 3617 |
. . . 4
                                |
30 | | dihglblem5a.j |
. . . . . 6
     |
31 | | dihglblem5a.a |
. . . . . 6
     |
32 | 4, 8, 30, 9, 31, 5 | lhpmcvr2 33589 |
. . . . 5
       

 
     |
33 | | dihglblem5a.p |
. . . . . . . . . . . 12
         |
34 | | dihglblem5a.t |
. . . . . . . . . . . 12
         |
35 | | dihglblem5a.r |
. . . . . . . . . . . 12
         |
36 | | dihglblem5a.e |
. . . . . . . . . . . 12
         |
37 | | dihglblem5a.g |
. . . . . . . . . . . 12
        |
38 | | vex 3048 |
. . . . . . . . . . . 12
 |
39 | | vex 3048 |
. . . . . . . . . . . 12
 |
40 | 4, 8, 30, 9, 31, 5, 33, 34, 35, 36, 15, 37, 38, 39 | dihopelvalc 34817 |
. . . . . . . . . . 11
          
   
                          |
41 | | id 22 |
. . . . . . . . . . . . 13
 
     |
42 | 6 | adantl 468 |
. . . . . . . . . . . . 13
 
   |
43 | 4, 8 | latref 16299 |
. . . . . . . . . . . . . 14
 

  |
44 | 1, 6, 43 | syl2an 480 |
. . . . . . . . . . . . 13
 

  |
45 | | dihglblem5a.o |
. . . . . . . . . . . . . 14

   |
46 | 4, 8, 5, 34, 35, 45, 15 | dihopelvalbN 34806 |
. . . . . . . . . . . . 13
                         |
47 | 41, 42, 44, 46 | syl12anc 1266 |
. . . . . . . . . . . 12
 
        
          |
48 | 47 | 3ad2ant1 1029 |
. . . . . . . . . . 11
          
   
                  |
49 | 40, 48 | anbi12d 717 |
. . . . . . . . . 10
          
   
        
  
       
                        |
50 | | simprll 772 |
. . . . . . . . . . . . . 14
                       

  |
51 | 50 | adantl 468 |
. . . . . . . . . . . . 13
     
            
                        |
52 | | simprrr 775 |
. . . . . . . . . . . . . . . . . . . . . 22
     
            
                       |
53 | 52 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . . 21
     
            
                              |
54 | | simpl1 1011 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
            
                          |
55 | 8, 31, 5, 33 | lhpocnel2 33584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
            
                          |
57 | | simpl3l 1063 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
            
                          |
58 | 8, 31, 5, 34, 37 | ltrniotacl 34146 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
 
  |
59 | 54, 56, 57, 58 | syl3anc 1268 |
. . . . . . . . . . . . . . . . . . . . . 22
     
            
                        |
60 | 45, 4 | tendo02 34354 |
. . . . . . . . . . . . . . . . . . . . . 22
      |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
     
            
                       
   |
62 | 53, 61 | eqtrd 2485 |
. . . . . . . . . . . . . . . . . . . 20
     
            
                         
   |
63 | 62 | cnveqd 5010 |
. . . . . . . . . . . . . . . . . . 19
     
            
                           
   |
64 | | cnvresid 5653 |
. . . . . . . . . . . . . . . . . . 19


  |
65 | 63, 64 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . 18
     
            
                              |
66 | 65 | coeq2d 4997 |
. . . . . . . . . . . . . . . . 17
     
            
                                  |
67 | 4, 5, 34 | ltrn1o 33689 |
. . . . . . . . . . . . . . . . . . 19
    
      |
68 | 54, 51, 67 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
     
            
                            |
69 | | f1of 5814 |
. . . . . . . . . . . . . . . . . 18
    
      |
70 | | fcoi1 5757 |
. . . . . . . . . . . . . . . . . 18
          |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
     
            
                           |
72 | 66, 71 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
     
            
                               |
73 | 72 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
     
            
                                       |
74 | | simprlr 773 |
. . . . . . . . . . . . . . 15
     
            
                                   |
75 | 73, 74 | eqbrtrrd 4425 |
. . . . . . . . . . . . . 14
     
            
                            |
76 | 8, 5, 34, 35 | trlle 33750 |
. . . . . . . . . . . . . . 15
    
      |
77 | 54, 51, 76 | syl2anc 667 |
. . . . . . . . . . . . . 14
     
            
                            |
78 | | simpl1l 1059 |
. . . . . . . . . . . . . . . 16
     
            
                        |
79 | 78, 1 | syl 17 |
. . . . . . . . . . . . . . 15
     
            
                        |
80 | 4, 5, 34, 35 | trlcl 33730 |
. . . . . . . . . . . . . . . 16
    
      |
81 | 54, 51, 80 | syl2anc 667 |
. . . . . . . . . . . . . . 15
     
            
                            |
82 | | simpl2l 1061 |
. . . . . . . . . . . . . . 15
     
            
                        |
83 | | simpl1r 1060 |
. . . . . . . . . . . . . . . 16
     
            
                        |
84 | 83, 6 | syl 17 |
. . . . . . . . . . . . . . 15
     
            
                        |
85 | 4, 8, 9 | latlem12 16324 |
. . . . . . . . . . . . . . 15
      
            
         |
86 | 79, 81, 82, 84, 85 | syl13anc 1270 |
. . . . . . . . . . . . . 14
     
            
                                
         |
87 | 75, 77, 86 | mpbi2and 932 |
. . . . . . . . . . . . 13
     
            
                              |
88 | 51, 87 | jca 535 |
. . . . . . . . . . . 12
     
            
                           
    |
89 | 79, 82, 84, 13 | syl3anc 1268 |
. . . . . . . . . . . . 13
     
            
                          |
90 | 79, 82, 84, 19 | syl3anc 1268 |
. . . . . . . . . . . . 13
     
            
                       
  |
91 | 4, 8, 5, 34, 35, 45, 15 | dihopelvalbN 34806 |
. . . . . . . . . . . . 13
                  
              |
92 | 54, 89, 90, 91 | syl12anc 1266 |
. . . . . . . . . . . 12
     
            
                                      
     |
93 | 88, 52, 92 | mpbir2and 933 |
. . . . . . . . . . 11
     
            
                            
    |
94 | 93 | ex 436 |
. . . . . . . . . 10
          
   
                       

  
         |
95 | 49, 94 | sylbid 219 |
. . . . . . . . 9
          
   
        
  
    
  
         |
96 | 95 | 3expia 1210 |
. . . . . . . 8
                                              |
97 | 96 | exp4c 613 |
. . . . . . 7
                      
  
    
  
            |
98 | 97 | imp4a 594 |
. . . . . 6
              
        
  
    
  
           |
99 | 98 | rexlimdv 2877 |
. . . . 5
              
        
  
    
  
          |
100 | 32, 99 | mpd 15 |
. . . 4
                                    |
101 | 29, 100 | syl5bi 221 |
. . 3
                                 |
102 | 28, 101 | relssdv 4927 |
. 2
                
        |
103 | 24, 102 | eqssd 3449 |
1
                         |