Step | Hyp | Ref
| Expression |
1 | | dihglblem.b |
. 2
     |
2 | | dihglblem.l |
. 2
     |
3 | | dihglblem.g |
. 2
     |
4 | | simpl1l 1058 |
. . . 4
             |
5 | | hllat 32923 |
. . . 4
   |
6 | 4, 5 | syl 17 |
. . 3
             |
7 | | simp1l 1031 |
. . . . . 6
        
  |
8 | | hlclat 32918 |
. . . . . 6
   |
9 | 7, 8 | syl 17 |
. . . . 5
        
  |
10 | | dihglblem.t |
. . . . . 6
 
    |
11 | | ssrab2 3513 |
. . . . . 6


    |
12 | 10, 11 | eqsstri 3461 |
. . . . 5
 |
13 | 1, 3 | clatglbcl 16353 |
. . . . 5
         |
14 | 9, 12, 13 | sylancl 667 |
. . . 4
               |
15 | 14 | adantr 467 |
. . 3
                 |
16 | | simpl2 1011 |
. . . . 5
             |
17 | | simpr 463 |
. . . . 5
             |
18 | 16, 17 | sseldd 3432 |
. . . 4
             |
19 | | simpl1r 1059 |
. . . . 5
             |
20 | | dihglblem.h |
. . . . . 6
     |
21 | 1, 20 | lhpbase 33557 |
. . . . 5
   |
22 | 19, 21 | syl 17 |
. . . 4
             |
23 | | dihglblem.m |
. . . . 5
     |
24 | 1, 23 | latmcl 16291 |
. . . 4
 
     |
25 | 6, 18, 22, 24 | syl3anc 1267 |
. . 3
           
   |
26 | 4, 8 | syl 17 |
. . . 4
             |
27 | | eqidd 2451 |
. . . . . . 7
           
     |
28 | | oveq1 6295 |
. . . . . . . . 9
 
     |
29 | 28 | eqeq2d 2460 |
. . . . . . . 8
     
  
    |
30 | 29 | rspcev 3149 |
. . . . . . 7
  
    
  
   |
31 | 17, 27, 30 | syl2anc 666 |
. . . . . 6
           
  
   |
32 | | eqeq1 2454 |
. . . . . . . 8
  
          |
33 | 32 | rexbidv 2900 |
. . . . . . 7
  
 
   
      |
34 | 33 | elrab 3195 |
. . . . . 6
 
  
  
 


  
    |
35 | 25, 31, 34 | sylanbrc 669 |
. . . . 5
           
  
     |
36 | 35, 10 | syl6eleqr 2539 |
. . . 4
           
   |
37 | 1, 2, 3 | clatglble 16364 |
. . . . 5
             |
38 | 12, 37 | mp3an2 1351 |
. . . 4
  
          |
39 | 26, 36, 38 | syl2anc 666 |
. . 3
                   |
40 | 1, 2, 23 | latmle1 16315 |
. . . 4
 
     |
41 | 6, 18, 22, 40 | syl3anc 1267 |
. . 3
           
   |
42 | 1, 2, 6, 15, 25, 18, 39, 41 | lattrd 16297 |
. 2
                 |
43 | | eqeq1 2454 |
. . . . . . . 8
   
     |
44 | 43 | rexbidv 2900 |
. . . . . . 7
  
 

     |
45 | | oveq1 6295 |
. . . . . . . . 9
 
     |
46 | 45 | eqeq2d 2460 |
. . . . . . . 8
   
     |
47 | 46 | cbvrexv 3019 |
. . . . . . 7
    
    |
48 | 44, 47 | syl6bb 265 |
. . . . . 6
  
 

     |
49 | 48, 10 | elrab2 3197 |
. . . . 5



     |
50 | | simp3 1009 |
. . . . . . . . . . 11
          

    |
51 | | simp13 1039 |
. . . . . . . . . . 11
          

  
  |
52 | | breq2 4405 |
. . . . . . . . . . . 12
 
   |
53 | 52 | rspcva 3147 |
. . . . . . . . . . 11
      |
54 | 50, 51, 53 | syl2anc 666 |
. . . . . . . . . 10
          

    |
55 | | simp11l 1118 |
. . . . . . . . . . . . 13
         


  |
56 | 55 | 3ad2ant1 1028 |
. . . . . . . . . . . 12
          

    |
57 | 56, 5 | syl 17 |
. . . . . . . . . . 11
          

    |
58 | | simp12 1038 |
. . . . . . . . . . 11
          

    |
59 | 56, 8 | syl 17 |
. . . . . . . . . . . 12
          

    |
60 | | simp112 1137 |
. . . . . . . . . . . 12
          

    |
61 | 1, 3 | clatglbcl 16353 |
. . . . . . . . . . . 12
         |
62 | 59, 60, 61 | syl2anc 666 |
. . . . . . . . . . 11
          

        |
63 | | simp11r 1119 |
. . . . . . . . . . . . 13
         


  |
64 | 63 | 3ad2ant1 1028 |
. . . . . . . . . . . 12
          

    |
65 | 64, 21 | syl 17 |
. . . . . . . . . . 11
          

    |
66 | 1, 2, 3 | clatleglb 16365 |
. . . . . . . . . . . . 13
 
     

   |
67 | 59, 58, 60, 66 | syl3anc 1267 |
. . . . . . . . . . . 12
          

      

   |
68 | 51, 67 | mpbird 236 |
. . . . . . . . . . 11
          

        |
69 | | simp113 1138 |
. . . . . . . . . . 11
          

        |
70 | 1, 2, 57, 58, 62, 65, 68, 69 | lattrd 16297 |
. . . . . . . . . 10
          

    |
71 | 60, 50 | sseldd 3432 |
. . . . . . . . . . 11
          

    |
72 | 1, 2, 23 | latlem12 16317 |
. . . . . . . . . . 11
  
    

    |
73 | 57, 58, 71, 65, 72 | syl13anc 1269 |
. . . . . . . . . 10
          

    

    |
74 | 54, 70, 73 | mpbi2and 931 |
. . . . . . . . 9
          

      |
75 | 74 | 3expia 1209 |
. . . . . . . 8
          

        |
76 | | breq2 4405 |
. . . . . . . . 9
  
      |
77 | 76 | biimprcd 229 |
. . . . . . . 8
  
  
   |
78 | 75, 77 | syl6 34 |
. . . . . . 7
          

    

    |
79 | 78 | rexlimdv 2876 |
. . . . . 6
          

   
     |
80 | 79 | expimpd 607 |
. . . . 5
         


         |
81 | 49, 80 | syl5bi 221 |
. . . 4
         



   |
82 | 81 | ralrimiv 2799 |
. . 3
         



  |
83 | 55, 8 | syl 17 |
. . . 4
         


  |
84 | | simp2 1008 |
. . . 4
         


  |
85 | 1, 2, 3 | clatleglb 16365 |
. . . . 5
 
     

   |
86 | 12, 85 | mp3an3 1352 |
. . . 4
       

   |
87 | 83, 84, 86 | syl2anc 666 |
. . 3
         


         |
88 | 82, 87 | mpbird 236 |
. 2
         


      |
89 | | simp2 1008 |
. 2
           |
90 | 1, 2, 3, 42, 88, 9, 89, 14 | isglbd 16356 |
1
                   |