Step | Hyp | Ref
| Expression |
1 | | hllat 33000 |
. . . . . 6
   |
2 | 1 | ad2antrr 740 |
. . . . 5
      
  |
3 | | simprl 772 |
. . . . 5
      
  |
4 | | dihglblem5a.b |
. . . . . . 7
     |
5 | | dihglblem5a.h |
. . . . . . 7
     |
6 | 4, 5 | lhpbase 33634 |
. . . . . 6
   |
7 | 6 | ad2antlr 741 |
. . . . 5
      
  |
8 | | dihglblem5a.l |
. . . . . 6
     |
9 | | dihglblem5a.m |
. . . . . 6
     |
10 | 4, 8, 9 | latmle1 16400 |
. . . . 5
 
     |
11 | 2, 3, 7, 10 | syl3anc 1292 |
. . . 4
           |
12 | | simpl 464 |
. . . . 5
           |
13 | 4, 9 | latmcl 16376 |
. . . . . 6
 
     |
14 | 2, 3, 7, 13 | syl3anc 1292 |
. . . . 5
           |
15 | | dihglblem5a.i |
. . . . . 6
         |
16 | 4, 8, 5, 15 | dihord 34903 |
. . . . 5
     
     
 
   
     |
17 | 12, 14, 3, 16 | syl3anc 1292 |
. . . 4
           
 
   
     |
18 | 11, 17 | mpbird 240 |
. . 3
                   |
19 | 4, 8, 9 | latmle2 16401 |
. . . . 5
 
     |
20 | 2, 3, 7, 19 | syl3anc 1292 |
. . . 4
           |
21 | 4, 8, 5, 15 | dihord 34903 |
. . . . 5
     
     
 
   
     |
22 | 12, 14, 7, 21 | syl3anc 1292 |
. . . 4
           
 
   
     |
23 | 20, 22 | mpbird 240 |
. . 3
                   |
24 | 18, 23 | ssind 3647 |
. 2
                         |
25 | 5, 15 | dihvalrel 34918 |
. . . . 5
 
       |
26 | | relin1 4956 |
. . . . 5
    
            |
27 | 25, 26 | syl 17 |
. . . 4
 
             |
28 | 27 | adantr 472 |
. . 3
                   |
29 | | elin 3608 |
. . . 4
                                |
30 | | dihglblem5a.j |
. . . . . 6
     |
31 | | dihglblem5a.a |
. . . . . 6
     |
32 | 4, 8, 30, 9, 31, 5 | lhpmcvr2 33660 |
. . . . 5
       

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

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

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

   |
46 | 4, 8, 5, 34, 35, 45, 15 | dihopelvalbN 34877 |
. . . . . . . . . . . . 13
                         |
47 | 41, 42, 44, 46 | syl12anc 1290 |
. . . . . . . . . . . 12
 
        
          |
48 | 47 | 3ad2ant1 1051 |
. . . . . . . . . . 11
          
   
                  |
49 | 40, 48 | anbi12d 725 |
. . . . . . . . . 10
          
   
        
  
       
                        |
50 | | simprll 780 |
. . . . . . . . . . . . . 14
                       

  |
51 | 50 | adantl 473 |
. . . . . . . . . . . . 13
     
            
                        |
52 | | simprrr 783 |
. . . . . . . . . . . . . . . . . . . . . 22
     
            
                       |
53 | 52 | fveq1d 5881 |
. . . . . . . . . . . . . . . . . . . . 21
     
            
                              |
54 | | simpl1 1033 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
            
                          |
55 | 8, 31, 5, 33 | lhpocnel2 33655 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
     |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
            
                          |
57 | | simpl3l 1085 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
            
                          |
58 | 8, 31, 5, 34, 37 | ltrniotacl 34217 |
. . . . . . . . . . . . . . . . . . . . . . 23
      
 
  |
59 | 54, 56, 57, 58 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . 22
     
            
                        |
60 | 45, 4 | tendo02 34425 |
. . . . . . . . . . . . . . . . . . . . . 22
      |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
     
            
                       
   |
62 | 53, 61 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . 20
     
            
                         
   |
63 | 62 | cnveqd 5015 |
. . . . . . . . . . . . . . . . . . 19
     
            
                           
   |
64 | | cnvresid 5663 |
. . . . . . . . . . . . . . . . . . 19


  |
65 | 63, 64 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . 18
     
            
                              |
66 | 65 | coeq2d 5002 |
. . . . . . . . . . . . . . . . 17
     
            
                                  |
67 | 4, 5, 34 | ltrn1o 33760 |
. . . . . . . . . . . . . . . . . . 19
    
      |
68 | 54, 51, 67 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
     
            
                            |
69 | | f1of 5828 |
. . . . . . . . . . . . . . . . . 18
    
      |
70 | | fcoi1 5769 |
. . . . . . . . . . . . . . . . . 18
          |
71 | 68, 69, 70 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
     
            
                           |
72 | 66, 71 | eqtrd 2505 |
. . . . . . . . . . . . . . . 16
     
            
                               |
73 | 72 | fveq2d 5883 |
. . . . . . . . . . . . . . 15
     
            
                                       |
74 | | simprlr 781 |
. . . . . . . . . . . . . . 15
     
            
                                   |
75 | 73, 74 | eqbrtrrd 4418 |
. . . . . . . . . . . . . 14
     
            
                            |
76 | 8, 5, 34, 35 | trlle 33821 |
. . . . . . . . . . . . . . 15
    
      |
77 | 54, 51, 76 | syl2anc 673 |
. . . . . . . . . . . . . 14
     
            
                            |
78 | | simpl1l 1081 |
. . . . . . . . . . . . . . . 16
     
            
                        |
79 | 78, 1 | syl 17 |
. . . . . . . . . . . . . . 15
     
            
                        |
80 | 4, 5, 34, 35 | trlcl 33801 |
. . . . . . . . . . . . . . . 16
    
      |
81 | 54, 51, 80 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     
            
                            |
82 | | simpl2l 1083 |
. . . . . . . . . . . . . . 15
     
            
                        |
83 | | simpl1r 1082 |
. . . . . . . . . . . . . . . 16
     
            
                        |
84 | 83, 6 | syl 17 |
. . . . . . . . . . . . . . 15
     
            
                        |
85 | 4, 8, 9 | latlem12 16402 |
. . . . . . . . . . . . . . 15
      
            
         |
86 | 79, 81, 82, 84, 85 | syl13anc 1294 |
. . . . . . . . . . . . . 14
     
            
                                
         |
87 | 75, 77, 86 | mpbi2and 935 |
. . . . . . . . . . . . 13
     
            
                              |
88 | 51, 87 | jca 541 |
. . . . . . . . . . . 12
     
            
                           
    |
89 | 79, 82, 84, 13 | syl3anc 1292 |
. . . . . . . . . . . . 13
     
            
                          |
90 | 79, 82, 84, 19 | syl3anc 1292 |
. . . . . . . . . . . . 13
     
            
                       
  |
91 | 4, 8, 5, 34, 35, 45, 15 | dihopelvalbN 34877 |
. . . . . . . . . . . . 13
                  
              |
92 | 54, 89, 90, 91 | syl12anc 1290 |
. . . . . . . . . . . 12
     
            
                                      
     |
93 | 88, 52, 92 | mpbir2and 936 |
. . . . . . . . . . 11
     
            
                            
    |
94 | 93 | ex 441 |
. . . . . . . . . 10
          
   
                       

  
         |
95 | 49, 94 | sylbid 223 |
. . . . . . . . 9
          
   
        
  
    
  
         |
96 | 95 | 3expia 1233 |
. . . . . . . 8
                                              |
97 | 96 | exp4c 619 |
. . . . . . 7
                      
  
    
  
            |
98 | 97 | imp4a 600 |
. . . . . 6
              
        
  
    
  
           |
99 | 98 | rexlimdv 2870 |
. . . . 5
              
        
  
    
  
          |
100 | 32, 99 | mpd 15 |
. . . 4
                                    |
101 | 29, 100 | syl5bi 225 |
. . 3
                                 |
102 | 28, 101 | relssdv 4932 |
. 2
                
        |
103 | 24, 102 | eqssd 3435 |
1
                         |