Proof of Theorem cdlemeg46req
Step | Hyp | Ref
| Expression |
1 | | simp11l 1120 |
. 2
     
    
     
 
   
  |
2 | | simp12l 1122 |
. . 3
     
    
     
 
   
  |
3 | | simp13l 1124 |
. . 3
     
    
     
 
   
  |
4 | | simp21 1042 |
. . 3
     
    
     
 
   
  |
5 | | cdlemef46g.j |
. . . 4
     |
6 | | cdlemef46g.a |
. . . 4
     |
7 | | eqid 2453 |
. . . 4
         |
8 | 5, 6, 7 | llni2 33089 |
. . 3
  


        |
9 | 1, 2, 3, 4, 8 | syl31anc 1272 |
. 2
     
    
     
 
   
        |
10 | | simp1 1009 |
. . . . 5
     
    
     
 
   
 
 
      |
11 | | simp23 1044 |
. . . . 5
     
    
     
 
   

   |
12 | | cdlemef46g.b |
. . . . . 6
     |
13 | | cdlemef46g.l |
. . . . . 6
     |
14 | | cdlemef46g.m |
. . . . . 6
     |
15 | | cdlemef46g.h |
. . . . . 6
     |
16 | | cdlemef46g.u |
. . . . . 6
  
  |
17 | | cdlemef46g.d |
. . . . . 6
  
        |
18 | | cdlemefs46g.e |
. . . . . 6
  
        |
19 | | cdlemef46g.f |
. . . . . 6
        
      
   
      
        ![]_ ]_](_urbrack.gif) 
         |
20 | | cdlemef46.v |
. . . . . 6
  
  |
21 | | cdlemef46.n |
. . . . . 6
  
        |
22 | | cdlemefs46.o |
. . . . . 6
  
        |
23 | | cdlemef46.g |
. . . . . 6
        
      
          
        ![]_ ]_](_urbrack.gif) 
         |
24 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23 | cdlemeg46fvaw 34095 |
. . . . 5
     
    
 
    
       |
25 | 10, 11, 4, 24 | syl3anc 1269 |
. . . 4
     
    
     
 
   
    
       |
26 | 25 | simpld 461 |
. . 3
     
    
     
 
   
      |
27 | | simp11 1039 |
. . . 4
     
    
     
 
   
    |
28 | | simp22 1043 |
. . . . 5
     
    
     
 
   

   |
29 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19 | cdleme46fvaw 34080 |
. . . . 5
     
    
 
    
       |
30 | 10, 28, 29 | syl2anc 667 |
. . . 4
     
    
     
 
   
    
       |
31 | | simp23l 1130 |
. . . 4
     
    
     
 
   
  |
32 | | simp3l 1037 |
. . . . . 6
     
    
     
 
   
    |
33 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19 | cdleme46fsvlpq 34084 |
. . . . . 6
     
    
     
        |
34 | 10, 4, 28, 32, 33 | syl121anc 1274 |
. . . . 5
     
    
     
 
   
        |
35 | | simp3r 1038 |
. . . . 5
     
    
     
 
   
    |
36 | | nbrne2 4424 |
. . . . 5
                 |
37 | 34, 35, 36 | syl2anc 667 |
. . . 4
     
    
     
 
   
      |
38 | | cdlemeg46.x |
. . . . 5
      
  |
39 | 13, 5, 14, 6, 15, 38 | lhpat2 33622 |
. . . 4
              
        |
40 | 27, 30, 31, 37, 39 | syl112anc 1273 |
. . 3
     
    
     
 
   
  |
41 | | hllat 32941 |
. . . . . . . 8
   |
42 | 1, 41 | syl 17 |
. . . . . . 7
     
    
     
 
   
  |
43 | 30 | simpld 461 |
. . . . . . . 8
     
    
     
 
   
      |
44 | 12, 5, 6 | hlatjcl 32944 |
. . . . . . . 8
           
   |
45 | 1, 43, 31, 44 | syl3anc 1269 |
. . . . . . 7
     
    
     
 
   
        |
46 | | simp11r 1121 |
. . . . . . . 8
     
    
     
 
   
  |
47 | 12, 15 | lhpbase 33575 |
. . . . . . . 8
   |
48 | 46, 47 | syl 17 |
. . . . . . 7
     
    
     
 
   
  |
49 | 12, 13, 14 | latmle2 16335 |
. . . . . . 7
       
       
   |
50 | 42, 45, 48, 49 | syl3anc 1269 |
. . . . . 6
     
    
     
 
   
     
    |
51 | 38, 50 | syl5eqbr 4439 |
. . . . 5
     
    
     
 
   
  |
52 | 25 | simprd 465 |
. . . . 5
     
    
     
 
   
      |
53 | | nbrne2 4424 |
. . . . 5
 
           |
54 | 51, 52, 53 | syl2anc 667 |
. . . 4
     
    
     
 
   
      |
55 | 54 | necomd 2681 |
. . 3
     
    
     
 
   
      |
56 | 5, 6, 7 | llni2 33089 |
. . 3
      
                  |
57 | 1, 26, 40, 55, 56 | syl31anc 1272 |
. 2
     
    
     
 
   
            |
58 | | simp22l 1128 |
. 2
     
    
     
 
   
  |
59 | 13, 5, 6 | hlatlej1 32952 |
. . . . 5
                   |
60 | 1, 26, 40, 59 | syl3anc 1269 |
. . . 4
     
    
     
 
   
            |
61 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23 | cdlemeg46nlpq 34096 |
. . . . 5
     
    
              |
62 | 10, 4, 11, 35, 61 | syl121anc 1274 |
. . . 4
     
    
     
 
   
        |
63 | | nbrne1 4423 |
. . . 4
                       
     |
64 | 60, 62, 63 | syl2anc 667 |
. . 3
     
    
     
 
   
          |
65 | 64 | necomd 2681 |
. 2
     
    
     
 
   
      
   |
66 | | cdlemeg46.y |
. . . 4
      
  |
67 | 12, 13, 5, 14, 6, 15, 16, 17, 18, 19, 20, 21, 22, 23, 66, 38 | cdlemeg46rgv 34107 |
. . 3
     
    
     
 
   
    
   |
68 | 12, 6 | atbase 32867 |
. . . . 5
   |
69 | 58, 68 | syl 17 |
. . . 4
     
    
     
 
   
  |
70 | 12, 5, 6 | hlatjcl 32944 |
. . . . 5
 
     |
71 | 1, 2, 3, 70 | syl3anc 1269 |
. . . 4
     
    
     
 
   
    |
72 | 12, 5, 6 | hlatjcl 32944 |
. . . . 5
           
   |
73 | 1, 26, 40, 72 | syl3anc 1269 |
. . . 4
     
    
     
 
   
        |
74 | 12, 13, 14 | latlem12 16336 |
. . . 4
  
         
        
 
             |
75 | 42, 69, 71, 73, 74 | syl13anc 1271 |
. . 3
     
    
     
 
   
        
 
             |
76 | 32, 67, 75 | mpbi2and 933 |
. 2
     
    
     
 
   
  
         |
77 | 13, 14, 6, 7 | 2llnmeqat 33148 |
. 2
             
    

        
  
        
  
         |
78 | 1, 9, 57, 58, 65, 76, 77 | syl132anc 1287 |
1
     
    
     
 
   
  
         |