Proof of Theorem dalem25
Step | Hyp | Ref
| Expression |
1 | | dalem.ph |
. . . 4
         
 
  
    
 
   
 
 
               |
2 | | dalem.l |
. . . 4
     |
3 | | dalem.j |
. . . 4
     |
4 | | dalem.a |
. . . 4
     |
5 | 1, 2, 3, 4 | dalemcnes 33603 |
. . 3
   |
6 | 5 | 3ad2ant1 1009 |
. 2
 
   |
7 | | dalem.ps |
. . . . . . . . . . 11
  

       |
8 | 7 | dalemclccjdd 33641 |
. . . . . . . . . 10

    |
9 | 8 | 3ad2ant3 1011 |
. . . . . . . . 9
 
     |
10 | 9 | adantr 465 |
. . . . . . . 8
  


    |
11 | | simpr 461 |
. . . . . . . . . 10
  


  |
12 | | dalem23.g |
. . . . . . . . . . . . 13
  
    |
13 | 1 | dalemkelat 33577 |
. . . . . . . . . . . . . . 15
   |
14 | 13 | 3ad2ant1 1009 |
. . . . . . . . . . . . . 14
 

  |
15 | 1 | dalemkehl 33576 |
. . . . . . . . . . . . . . . 16
   |
16 | 15 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . 15
 

  |
17 | 7 | dalemccea 33636 |
. . . . . . . . . . . . . . . 16

  |
18 | 17 | 3ad2ant3 1011 |
. . . . . . . . . . . . . . 15
 
   |
19 | 1 | dalempea 33579 |
. . . . . . . . . . . . . . . 16
   |
20 | 19 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . 15
 

  |
21 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
         |
22 | 21, 3, 4 | hlatjcl 33320 |
. . . . . . . . . . . . . . 15
 
         |
23 | 16, 18, 20, 22 | syl3anc 1219 |
. . . . . . . . . . . . . 14
 
         |
24 | 7 | dalemddea 33637 |
. . . . . . . . . . . . . . . 16

  |
25 | 24 | 3ad2ant3 1011 |
. . . . . . . . . . . . . . 15
 
   |
26 | 1 | dalemsea 33582 |
. . . . . . . . . . . . . . . 16
   |
27 | 26 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . 15
 

  |
28 | 21, 3, 4 | hlatjcl 33320 |
. . . . . . . . . . . . . . 15
 
         |
29 | 16, 25, 27, 28 | syl3anc 1219 |
. . . . . . . . . . . . . 14
 
         |
30 | | dalem23.m |
. . . . . . . . . . . . . . 15
     |
31 | 21, 2, 30 | latmle2 15358 |
. . . . . . . . . . . . . 14
        
        
       |
32 | 14, 23, 29, 31 | syl3anc 1219 |
. . . . . . . . . . . . 13
 
   
       |
33 | 12, 32 | syl5eqbr 4426 |
. . . . . . . . . . . 12
 
     |
34 | 3, 4 | hlatjcom 33321 |
. . . . . . . . . . . . 13
 
       |
35 | 16, 25, 27, 34 | syl3anc 1219 |
. . . . . . . . . . . 12
 
       |
36 | 33, 35 | breqtrd 4417 |
. . . . . . . . . . 11
 
     |
37 | 36 | adantr 465 |
. . . . . . . . . 10
  


    |
38 | 11, 37 | eqbrtrd 4413 |
. . . . . . . . 9
  


    |
39 | 2, 3, 4 | hlatlej2 33329 |
. . . . . . . . . . 11
 

    |
40 | 16, 27, 25, 39 | syl3anc 1219 |
. . . . . . . . . 10
 
     |
41 | 40 | adantr 465 |
. . . . . . . . 9
  


    |
42 | 7, 4 | dalemcceb 33642 |
. . . . . . . . . . . 12

      |
43 | 42 | 3ad2ant3 1011 |
. . . . . . . . . . 11
 
       |
44 | 21, 4 | atbase 33243 |
. . . . . . . . . . . . 13
       |
45 | 24, 44 | syl 16 |
. . . . . . . . . . . 12

      |
46 | 45 | 3ad2ant3 1011 |
. . . . . . . . . . 11
 
       |
47 | 21, 3, 4 | hlatjcl 33320 |
. . . . . . . . . . . 12
 
         |
48 | 16, 27, 25, 47 | syl3anc 1219 |
. . . . . . . . . . 11
 
         |
49 | 21, 2, 3 | latjle12 15343 |
. . . . . . . . . . 11
      
    
         
           |
50 | 14, 43, 46, 48, 49 | syl13anc 1221 |
. . . . . . . . . 10
 
   
           |
51 | 50 | adantr 465 |
. . . . . . . . 9
  


      
       |
52 | 38, 41, 51 | mpbi2and 912 |
. . . . . . . 8
  


      |
53 | 1, 4 | dalemceb 33591 |
. . . . . . . . . . 11
       |
54 | 53 | 3ad2ant1 1009 |
. . . . . . . . . 10
 

      |
55 | 21, 3, 4 | hlatjcl 33320 |
. . . . . . . . . . 11
 
         |
56 | 16, 18, 25, 55 | syl3anc 1219 |
. . . . . . . . . 10
 
         |
57 | 21, 2 | lattr 15337 |
. . . . . . . . . 10
  
                                |
58 | 14, 54, 56, 48, 57 | syl13anc 1221 |
. . . . . . . . 9
 
               |
59 | 58 | adantr 465 |
. . . . . . . 8
  


    
         |
60 | 10, 52, 59 | mp2and 679 |
. . . . . . 7
  


    |
61 | | dalem23.o |
. . . . . . . . . . 11
     |
62 | 1, 61 | dalemyeb 33602 |
. . . . . . . . . 10
       |
63 | 62 | 3ad2ant1 1009 |
. . . . . . . . 9
 

      |
64 | 21, 2, 30 | latmlem1 15362 |
. . . . . . . . 9
  
    
    
                  |
65 | 14, 54, 48, 63, 64 | syl13anc 1221 |
. . . . . . . 8
 
             |
66 | 65 | adantr 465 |
. . . . . . 7
  


  
         |
67 | 60, 66 | mpd 15 |
. . . . . 6
  


        |
68 | | dalem23.y |
. . . . . . . . . 10
     |
69 | | dalem23.z |
. . . . . . . . . 10
     |
70 | 1, 2, 3, 4, 61, 68, 69 | dalem17 33633 |
. . . . . . . . 9
 
   |
71 | 70 | 3adant3 1008 |
. . . . . . . 8
 
   |
72 | 21, 2, 30 | latleeqm1 15360 |
. . . . . . . . 9
 
         
     |
73 | 14, 54, 63, 72 | syl3anc 1219 |
. . . . . . . 8
 
 
     |
74 | 71, 73 | mpbid 210 |
. . . . . . 7
 
     |
75 | 74 | adantr 465 |
. . . . . 6
  


    |
76 | 1, 2, 3, 4, 69 | dalemsly 33608 |
. . . . . . . . 9
 
   |
77 | 76 | 3adant3 1008 |
. . . . . . . 8
 
   |
78 | 7 | dalem-ddly 33639 |
. . . . . . . . 9
   |
79 | 78 | 3ad2ant3 1011 |
. . . . . . . 8
 

  |
80 | 21, 2, 3, 30, 4 | 2atjm 33398 |
. . . . . . . 8
  
              |
81 | 16, 27, 25, 63, 77, 79, 80 | syl132anc 1237 |
. . . . . . 7
 
       |
82 | 81 | adantr 465 |
. . . . . 6
  


      |
83 | 67, 75, 82 | 3brtr3d 4422 |
. . . . 5
  


  |
84 | | hlatl 33314 |
. . . . . . . . 9
   |
85 | 15, 84 | syl 16 |
. . . . . . . 8
   |
86 | 1, 2, 3, 4, 61, 68 | dalemcea 33613 |
. . . . . . . 8
   |
87 | 2, 4 | atcmp 33265 |
. . . . . . . 8
 
 
   |
88 | 85, 86, 26, 87 | syl3anc 1219 |
. . . . . . 7
 
   |
89 | 88 | 3ad2ant1 1009 |
. . . . . 6
 
 
   |
90 | 89 | adantr 465 |
. . . . 5
  



   |
91 | 83, 90 | mpbid 210 |
. . . 4
  


  |
92 | 91 | ex 434 |
. . 3
 
     |
93 | 92 | necon3d 2672 |
. 2
 
     |
94 | 6, 93 | mpd 15 |
1
 
   |