Proof of Theorem dalawlem6
Step | Hyp | Ref
| Expression |
1 | | eqid 2451 |
. 2
         |
2 | | dalawlem.l |
. 2
     |
3 | | simp11 1018 |
. . 3
     
   
    
 
   


 
  |
4 | | hllat 33314 |
. . 3
   |
5 | 3, 4 | syl 16 |
. 2
     
   
    
 
   


 
  |
6 | | simp21 1021 |
. . . . 5
     
   
    
 
   


 
  |
7 | | simp22 1022 |
. . . . 5
     
   
    
 
   


 
  |
8 | | dalawlem.j |
. . . . . 6
     |
9 | | dalawlem.a |
. . . . . 6
     |
10 | 1, 8, 9 | hlatjcl 33317 |
. . . . 5
 
         |
11 | 3, 6, 7, 10 | syl3anc 1219 |
. . . 4
     
   
    
 
   


          |
12 | | simp32 1025 |
. . . . 5
     
   
    
 
   


 
  |
13 | 1, 9 | atbase 33240 |
. . . . 5
       |
14 | 12, 13 | syl 16 |
. . . 4
     
   
    
 
   


 
      |
15 | 1, 8 | latjcl 15323 |
. . . 4
  
    
    
          |
16 | 5, 11, 14, 15 | syl3anc 1219 |
. . 3
     
   
    
 
   


            |
17 | | simp31 1024 |
. . . 4
     
   
    
 
   


 
  |
18 | 1, 9 | atbase 33240 |
. . . 4
       |
19 | 17, 18 | syl 16 |
. . 3
     
   
    
 
   


 
      |
20 | | dalawlem.m |
. . . 4
     |
21 | 1, 20 | latmcl 15324 |
. . 3
         
    
   
        |
22 | 5, 16, 19, 21 | syl3anc 1219 |
. 2
     
   
    
 
   


      
       |
23 | | simp23 1023 |
. . . . 5
     
   
    
 
   


 
  |
24 | 1, 8, 9 | hlatjcl 33317 |
. . . . 5
 
         |
25 | 3, 7, 23, 24 | syl3anc 1219 |
. . . 4
     
   
    
 
   


          |
26 | | simp33 1026 |
. . . . 5
     
   
    
 
   


 
  |
27 | 1, 9 | atbase 33240 |
. . . . 5
       |
28 | 26, 27 | syl 16 |
. . . 4
     
   
    
 
   


 
      |
29 | 1, 20 | latmcl 15324 |
. . . 4
  
    
    
          |
30 | 5, 25, 28, 29 | syl3anc 1219 |
. . 3
     
   
    
 
   


    
       |
31 | 1, 8, 9 | hlatjcl 33317 |
. . . . 5
 
         |
32 | 3, 23, 6, 31 | syl3anc 1219 |
. . . 4
     
   
    
 
   


          |
33 | 1, 8, 9 | hlatjcl 33317 |
. . . . 5
 
         |
34 | 3, 26, 17, 33 | syl3anc 1219 |
. . . 4
     
   
    
 
   


          |
35 | 1, 20 | latmcl 15324 |
. . . 4
  
    
      
   
        |
36 | 5, 32, 34, 35 | syl3anc 1219 |
. . 3
     
   
    
 
   


    
         |
37 | 1, 8 | latjcl 15323 |
. . 3
    
    
   
                         |
38 | 5, 30, 36, 37 | syl3anc 1219 |
. 2
     
   
    
 
   


                    |
39 | 1, 8, 9 | hlatjcl 33317 |
. . . . 5
 
         |
40 | 3, 12, 26, 39 | syl3anc 1219 |
. . . 4
     
   
    
 
   


          |
41 | 1, 20 | latmcl 15324 |
. . . 4
  
    
      
   
        |
42 | 5, 25, 40, 41 | syl3anc 1219 |
. . 3
     
   
    
 
   


    
         |
43 | 1, 8 | latjcl 15323 |
. . 3
    
      
   
           
               |
44 | 5, 42, 36, 43 | syl3anc 1219 |
. 2
     
   
    
 
   


      
               |
45 | 1, 9 | atbase 33240 |
. . . . . . . 8
       |
46 | 6, 45 | syl 16 |
. . . . . . 7
     
   
    
 
   


 
      |
47 | 1, 8, 9 | hlatjcl 33317 |
. . . . . . . . 9
 
         |
48 | 3, 6, 17, 47 | syl3anc 1219 |
. . . . . . . 8
     
   
    
 
   


          |
49 | 1, 8, 9 | hlatjcl 33317 |
. . . . . . . . . 10
 
         |
50 | 3, 7, 12, 49 | syl3anc 1219 |
. . . . . . . . 9
     
   
    
 
   


          |
51 | 1, 20 | latmcl 15324 |
. . . . . . . . 9
  
    
      
   
        |
52 | 5, 25, 50, 51 | syl3anc 1219 |
. . . . . . . 8
     
   
    
 
   


    
         |
53 | 1, 20 | latmcl 15324 |
. . . . . . . 8
  
    
   
         
   
         |
54 | 5, 48, 52, 53 | syl3anc 1219 |
. . . . . . 7
     
   
    
 
   


    
   
         |
55 | 1, 8 | latjcl 15323 |
. . . . . . 7
 
      
   
       
   
   
          |
56 | 5, 46, 54, 55 | syl3anc 1219 |
. . . . . 6
     
   
    
 
   


     
   
          |
57 | 1, 9 | atbase 33240 |
. . . . . . . . 9
       |
58 | 23, 57 | syl 16 |
. . . . . . . 8
     
   
    
 
   


 
      |
59 | 1, 8 | latjcl 15323 |
. . . . . . . 8
 
      
                  |
60 | 5, 58, 30, 59 | syl3anc 1219 |
. . . . . . 7
     
   
    
 
   


     
        |
61 | 1, 8 | latjcl 15323 |
. . . . . . 7
 
              
    
         |
62 | 5, 46, 60, 61 | syl3anc 1219 |
. . . . . 6
     
   
    
 
   


                |
63 | 1, 2, 8, 20 | latmlej22 15365 |
. . . . . . . . 9
  
           
            
   |
64 | 5, 19, 16, 46, 63 | syl13anc 1221 |
. . . . . . . 8
     
   
    
 
   


      
     |
65 | 1, 20 | latmcl 15324 |
. . . . . . . . . . 11
  
    
      
   
        |
66 | 5, 50, 48, 65 | syl3anc 1219 |
. . . . . . . . . 10
     
   
    
 
   


    
         |
67 | 1, 8 | latjcl 15323 |
. . . . . . . . . 10
 
      
            
         |
68 | 5, 46, 66, 67 | syl3anc 1219 |
. . . . . . . . 9
     
   
    
 
   


     
          |
69 | 1, 8 | latjcl 15323 |
. . . . . . . . . 10
 
      
            
         |
70 | 5, 46, 52, 69 | syl3anc 1219 |
. . . . . . . . 9
     
   
    
 
   


     
          |
71 | 2, 8, 9 | hlatlej2 33326 |
. . . . . . . . . . . 12
 

    |
72 | 3, 6, 17, 71 | syl3anc 1219 |
. . . . . . . . . . 11
     
   
    
 
   


      |
73 | 1, 8 | latjcl 15323 |
. . . . . . . . . . . . 13
 
                     |
74 | 5, 46, 50, 73 | syl3anc 1219 |
. . . . . . . . . . . 12
     
   
    
 
   


            |
75 | 1, 2, 20 | latmlem2 15354 |
. . . . . . . . . . . 12
  
    
    
            
                 |
76 | 5, 19, 48, 74, 75 | syl13anc 1221 |
. . . . . . . . . . 11
     
   
    
 
   


       
 
   
 
      |
77 | 72, 76 | mpd 15 |
. . . . . . . . . 10
     
   
    
 
   


    
 
   
 
     |
78 | 8, 9 | hlatjass 33320 |
. . . . . . . . . . . 12
  
    
  
    |
79 | 3, 6, 7, 12, 78 | syl13anc 1221 |
. . . . . . . . . . 11
     
   
    
 
   


       
    |
80 | 79 | oveq1d 6205 |
. . . . . . . . . 10
     
   
    
 
   


      
         |
81 | 2, 8, 9 | hlatlej1 33325 |
. . . . . . . . . . . 12
 

    |
82 | 3, 6, 17, 81 | syl3anc 1219 |
. . . . . . . . . . 11
     
   
    
 
   


      |
83 | 1, 2, 8, 20, 9 | atmod1i1 33807 |
. . . . . . . . . . 11
  
                    
             |
84 | 3, 6, 50, 48, 82, 83 | syl131anc 1232 |
. . . . . . . . . 10
     
   
    
 
   


     
              |
85 | 77, 80, 84 | 3brtr4d 4420 |
. . . . . . . . 9
     
   
    
 
   


      
    
      |
86 | 1, 20 | latmcom 15347 |
. . . . . . . . . . . . 13
  
    
      
   
          |
87 | 5, 50, 48, 86 | syl3anc 1219 |
. . . . . . . . . . . 12
     
   
    
 
   


    
     
     |
88 | | simp12 1019 |
. . . . . . . . . . . 12
     
   
    
 
   


    
   
   |
89 | 87, 88 | eqbrtrd 4410 |
. . . . . . . . . . 11
     
   
    
 
   


    
   
   |
90 | 1, 2, 20 | latmle1 15348 |
. . . . . . . . . . . 12
  
    
      
   
 
    |
91 | 5, 50, 48, 90 | syl3anc 1219 |
. . . . . . . . . . 11
     
   
    
 
   


    
   
   |
92 | 1, 2, 20 | latlem12 15350 |
. . . . . . . . . . . 12
      
           
             
 
    
   
     
 
   
     |
93 | 5, 66, 25, 50, 92 | syl13anc 1221 |
. . . . . . . . . . 11
     
   
    
 
   


              
   
     
 
   
     |
94 | 89, 91, 93 | mpbi2and 912 |
. . . . . . . . . 10
     
   
    
 
   


    
     
     |
95 | 1, 2, 8 | latjlej2 15338 |
. . . . . . . . . . 11
      
        
      
         
     
      
       
       |
96 | 5, 66, 52, 46, 95 | syl13anc 1221 |
. . . . . . . . . 10
     
   
    
 
   


      
 
   
 
   
       
       |
97 | 94, 96 | mpd 15 |
. . . . . . . . 9
     
   
    
 
   


     
       
      |
98 | 1, 2, 5, 22, 68, 70, 85, 97 | lattrd 15330 |
. . . . . . . 8
     
   
    
 
   


      
    
      |
99 | 1, 2, 20 | latlem12 15350 |
. . . . . . . . 9
                  
   
               
        
    
          
   
           |
100 | 5, 22, 48, 70, 99 | syl13anc 1221 |
. . . . . . . 8
     
   
    
 
   


       
        
    
          
   
           |
101 | 64, 98, 100 | mpbi2and 912 |
. . . . . . 7
     
   
    
 
   


      
   
   
       |
102 | 1, 2, 8, 20, 9 | atmod3i1 33814 |
. . . . . . . 8
  
        
                 
           
       |
103 | 3, 6, 48, 52, 82, 102 | syl131anc 1232 |
. . . . . . 7
     
   
    
 
   


     
   
      
   
       |
104 | 101, 103 | breqtrrd 4416 |
. . . . . 6
     
   
    
 
   


      
    
   
      |
105 | | simp13 1020 |
. . . . . . . . 9
     
   
    
 
   


    
   
   |
106 | 1, 20 | latmcl 15324 |
. . . . . . . . . . 11
  
    
      
   
        |
107 | 5, 48, 50, 106 | syl3anc 1219 |
. . . . . . . . . 10
     
   
    
 
   


    
         |
108 | 1, 8, 9 | hlatjcl 33317 |
. . . . . . . . . . 11
 
         |
109 | 3, 23, 26, 108 | syl3anc 1219 |
. . . . . . . . . 10
     
   
    
 
   


          |
110 | 1, 2, 20 | latmlem2 15354 |
. . . . . . . . . 10
      
           
           
   
      
      
      |
111 | 5, 107, 109, 25, 110 | syl13anc 1221 |
. . . . . . . . 9
     
   
    
 
   


      
 
    
   
            |
112 | 105, 111 | mpd 15 |
. . . . . . . 8
     
   
    
 
   


    
   
           |
113 | | hlol 33312 |
. . . . . . . . . 10
   |
114 | 3, 113 | syl 16 |
. . . . . . . . 9
     
   
    
 
   


 
  |
115 | 1, 20 | latm12 33181 |
. . . . . . . . 9
              
          
   
     
   
     |
116 | 114, 48, 25, 50, 115 | syl13anc 1221 |
. . . . . . . 8
     
   
    
 
   


    
   
     
   
     |
117 | 2, 8, 9 | hlatlej2 33326 |
. . . . . . . . . 10
 

    |
118 | 3, 7, 23, 117 | syl3anc 1219 |
. . . . . . . . 9
     
   
    
 
   


      |
119 | 1, 2, 8, 20, 9 | atmod3i1 33814 |
. . . . . . . . 9
  
                      
     |
120 | 3, 23, 25, 28, 118, 119 | syl131anc 1232 |
. . . . . . . 8
     
   
    
 
   


     
          |
121 | 112, 116,
120 | 3brtr4d 4420 |
. . . . . . 7
     
   
    
 
   


    
   
           |
122 | 1, 2, 8 | latjlej2 15338 |
. . . . . . . 8
        
       
   
                  
       
 
   
   
    
          |
123 | 5, 54, 60, 46, 122 | syl13anc 1221 |
. . . . . . 7
     
   
    
 
   


        
       
 
   
   
    
          |
124 | 121, 123 | mpd 15 |
. . . . . 6
     
   
    
 
   


     
   
    
         |
125 | 1, 2, 5, 22, 56, 62, 104, 124 | lattrd 15330 |
. . . . 5
     
   
    
 
   


      
           |
126 | 1, 8 | latj13 15370 |
. . . . . 6
  
   
      
                         |
127 | 5, 46, 58, 30, 126 | syl13anc 1221 |
. . . . 5
     
   
    
 
   


                    |
128 | 125, 127 | breqtrd 4414 |
. . . 4
     
   
    
 
   


      
           |
129 | 1, 2, 8, 20 | latmlej22 15365 |
. . . . 5
  
           
            
   |
130 | 5, 19, 16, 28, 129 | syl13anc 1221 |
. . . 4
     
   
    
 
   


      
     |
131 | 1, 8 | latjcl 15323 |
. . . . . 6
    
    
      
   
          |
132 | 5, 30, 32, 131 | syl3anc 1219 |
. . . . 5
     
   
    
 
   


                |
133 | 1, 2, 20 | latlem12 15350 |
. . . . 5
                
                                     
  
   
      
          |
134 | 5, 22, 132, 34, 133 | syl13anc 1221 |
. . . 4
     
   
    
 
   


       
     
          
       
    
          |
135 | 128, 130,
134 | mpbi2and 912 |
. . 3
     
   
    
 
   


      
       
 
     |
136 | 1, 2, 8, 20 | latmlej21 15364 |
. . . . 5
  
    
    
        
     |
137 | 5, 28, 25, 19, 136 | syl13anc 1221 |
. . . 4
     
   
    
 
   


    
     |
138 | 1, 2, 8, 20, 9 | atmod1i1m 33808 |
. . . 4
          
               
       
   
        
         |
139 | 3, 26, 25, 32, 34, 137, 138 | syl231anc 1239 |
. . 3
     
   
    
 
   


                    
 
     |
140 | 135, 139 | breqtrrd 4416 |
. 2
     
   
    
 
   


      
               |
141 | 2, 8, 9 | hlatlej2 33326 |
. . . . 5
 

    |
142 | 3, 12, 26, 141 | syl3anc 1219 |
. . . 4
     
   
    
 
   


      |
143 | 1, 2, 20 | latmlem2 15354 |
. . . . 5
  
    
    
          
   
   
     |
144 | 5, 28, 40, 25, 143 | syl13anc 1221 |
. . . 4
     
   
    
 
   


       
   
      |
145 | 142, 144 | mpd 15 |
. . 3
     
   
    
 
   


    
   
     |
146 | 1, 2, 8 | latjlej1 15337 |
. . . 4
             
      
   
               
                   
            |
147 | 5, 30, 42, 36, 146 | syl13anc 1221 |
. . 3
     
   
    
 
   


      
   
 
   
   
        
            |
148 | 145, 147 | mpd 15 |
. 2
     
   
    
 
   


                  
           |
149 | 1, 2, 5, 22, 38, 44, 140, 148 | lattrd 15330 |
1
     
   
    
 
   


      
     
           |