Step | Hyp | Ref
| Expression |
1 | | diaintcl.h |
. . . . . . . 8
     |
2 | | diaintcl.i |
. . . . . . . 8
         |
3 | 1, 2 | diaf11N 34611 |
. . . . . . 7
 
       |
4 | 3 | adantr 467 |
. . . . . 6
             |
5 | | f1ofn 5813 |
. . . . . 6
       |
6 | 4, 5 | syl 17 |
. . . . 5
         |
7 | | cnvimass 5187 |
. . . . 5
    
 |
8 | | fnssres 5687 |
. . . . 5
                      |
9 | 6, 7, 8 | sylancl 667 |
. . . 4
                     |
10 | | fniinfv 5922 |
. . . 4
 
                   
         
         |
11 | 9, 10 | syl 17 |
. . 3
               
         
         |
12 | | df-ima 4846 |
. . . . 5
                 |
13 | | f1ofo 5819 |
. . . . . . . 8
           |
14 | 3, 13 | syl 17 |
. . . . . . 7
 
       |
15 | 14 | adantr 467 |
. . . . . 6
             |
16 | | simprl 763 |
. . . . . 6
         |
17 | | foimacnv 5829 |
. . . . . 6
                  |
18 | 15, 16, 17 | syl2anc 666 |
. . . . 5
                  |
19 | 12, 18 | syl5eqr 2498 |
. . . 4
       
        |
20 | 19 | inteqd 4238 |
. . 3
        
         |
21 | 11, 20 | eqtrd 2484 |
. 2
               
            |
22 | | simpl 459 |
. . . . 5
       
   |
23 | 7 | a1i 11 |
. . . . 5
           
  |
24 | | simprr 765 |
. . . . . . 7
         |
25 | | n0 3740 |
. . . . . . 7
    |
26 | 24, 25 | sylib 200 |
. . . . . 6
          |
27 | 16 | sselda 3431 |
. . . . . . . 8
       
   |
28 | 3 | ad2antrr 731 |
. . . . . . . . . 10
       
       |
29 | 28, 5 | syl 17 |
. . . . . . . . 9
       
   |
30 | | fvelrnb 5910 |
. . . . . . . . 9
           |
31 | 29, 30 | syl 17 |
. . . . . . . 8
       
           |
32 | 27, 31 | mpbid 214 |
. . . . . . 7
       
         |
33 | | f1ofun 5814 |
. . . . . . . . . . . . . . . 16
       |
34 | 3, 33 | syl 17 |
. . . . . . . . . . . . . . 15
 
   |
35 | 34 | adantr 467 |
. . . . . . . . . . . . . 14
         |
36 | | fvimacnv 5995 |
. . . . . . . . . . . . . 14
                |
37 | 35, 36 | sylan 474 |
. . . . . . . . . . . . 13
       
     
        |
38 | | ne0i 3736 |
. . . . . . . . . . . . 13
             |
39 | 37, 38 | syl6bi 232 |
. . . . . . . . . . . 12
       
     
        |
40 | 39 | ex 436 |
. . . . . . . . . . 11
                      |
41 | | eleq1 2516 |
. . . . . . . . . . . . 13
         
   |
42 | 41 | biimprd 227 |
. . . . . . . . . . . 12
             |
43 | 42 | imim1d 78 |
. . . . . . . . . . 11
                           |
44 | 40, 43 | syl9 73 |
. . . . . . . . . 10
             
          |
45 | 44 | com24 90 |
. . . . . . . . 9
             
          |
46 | 45 | imp 431 |
. . . . . . . 8
       
      
         |
47 | 46 | rexlimdv 2876 |
. . . . . . 7
       
       
        |
48 | 32, 47 | mpd 15 |
. . . . . 6
       
        |
49 | 26, 48 | exlimddv 1780 |
. . . . 5
              |
50 | | eqid 2450 |
. . . . . 6
         |
51 | 50, 1, 2 | diaglbN 34617 |
. . . . 5
         
                                     |
52 | 22, 23, 49, 51 | syl12anc 1265 |
. . . 4
                        
            |
53 | | fvres 5877 |
. . . . 5
                       |
54 | 53 | iineq2i 4297 |
. . . 4
        
                     |
55 | 52, 54 | syl6eqr 2502 |
. . 3
                        
                   |
56 | | hlclat 32918 |
. . . . . . 7
   |
57 | 56 | ad2antrr 731 |
. . . . . 6
         |
58 | | eqid 2450 |
. . . . . . . . . 10
         |
59 | | eqid 2450 |
. . . . . . . . . 10
         |
60 | 58, 59, 1, 2 | diadm 34597 |
. . . . . . . . 9
 
               |
61 | | ssrab2 3513 |
. . . . . . . . 9
                 |
62 | 60, 61 | syl6eqss 3481 |
. . . . . . . 8
 
       |
63 | 62 | adantr 467 |
. . . . . . 7
             |
64 | 7, 63 | syl5ss 3442 |
. . . . . 6
                  |
65 | 58, 50 | clatglbcl 16353 |
. . . . . 6
                               |
66 | 57, 64, 65 | syl2anc 666 |
. . . . 5
                          |
67 | | n0 3740 |
. . . . . . 7
              |
68 | 49, 67 | sylib 200 |
. . . . . 6
               |
69 | | hllat 32923 |
. . . . . . . 8
   |
70 | 69 | ad3antrrr 735 |
. . . . . . 7
       
        |
71 | 66 | adantr 467 |
. . . . . . 7
       
                         |
72 | 64 | sselda 3431 |
. . . . . . 7
       
            |
73 | 58, 1 | lhpbase 33557 |
. . . . . . . 8
       |
74 | 73 | ad3antlr 736 |
. . . . . . 7
       
            |
75 | 56 | ad3antrrr 735 |
. . . . . . . 8
       
        |
76 | 60 | adantr 467 |
. . . . . . . . . . 11
      
              |
77 | 7, 76 | syl5sseq 3479 |
. . . . . . . . . 10
                          |
78 | 77, 61 | syl6ss 3443 |
. . . . . . . . 9
                  |
79 | 78 | adantr 467 |
. . . . . . . 8
       
                 |
80 | | simpr 463 |
. . . . . . . 8
       
             |
81 | 58, 59, 50 | clatglble 16364 |
. . . . . . . 8
          
     
                     |
82 | 75, 79, 80, 81 | syl3anc 1267 |
. . . . . . 7
       
                           |
83 | 7 | sseli 3427 |
. . . . . . . . . 10
        |
84 | 83 | adantl 468 |
. . . . . . . . 9
       
        |
85 | 58, 59, 1, 2 | diaeldm 34598 |
. . . . . . . . . 10
 
                 |
86 | 85 | ad2antrr 731 |
. . . . . . . . 9
       
      
    
          |
87 | 84, 86 | mpbid 214 |
. . . . . . . 8
       
          
         |
88 | 87 | simprd 465 |
. . . . . . 7
       
              |
89 | 58, 59, 70, 71, 72, 74, 82, 88 | lattrd 16297 |
. . . . . 6
       
                           |
90 | 68, 89 | exlimddv 1780 |
. . . . 5
                            |
91 | 58, 59, 1, 2 | diaeldm 34598 |
. . . . . 6
 
                                
                       |
92 | 91 | adantr 467 |
. . . . 5
                    
                 
                       |
93 | 66, 90, 92 | mpbir2and 932 |
. . . 4
                      |
94 | 1, 2 | diaclN 34612 |
. . . 4
                 
                   |
95 | 93, 94 | syldan 473 |
. . 3
                          |
96 | 55, 95 | eqeltrrd 2529 |
. 2
               
           |
97 | 21, 96 | eqeltrrd 2529 |
1
          |