Step | Hyp | Ref
| Expression |
1 | | dibintcl.h |
. . . . . . . 8
     |
2 | | dibintcl.i |
. . . . . . . 8
         |
3 | 1, 2 | dibf11N 34800 |
. . . . . . 7
 
       |
4 | 3 | adantr 472 |
. . . . . 6
             |
5 | | f1ofn 5829 |
. . . . . 6
       |
6 | 4, 5 | syl 17 |
. . . . 5
         |
7 | | cnvimass 5194 |
. . . . 5
    
 |
8 | | fnssres 5699 |
. . . . 5
                      |
9 | 6, 7, 8 | sylancl 675 |
. . . 4
                     |
10 | | fniinfv 5939 |
. . . 4
 
                   
         
         |
11 | 9, 10 | syl 17 |
. . 3
               
         
         |
12 | | df-ima 4852 |
. . . . 5
                 |
13 | | f1ofo 5835 |
. . . . . . . 8
           |
14 | 3, 13 | syl 17 |
. . . . . . 7
 
       |
15 | 14 | adantr 472 |
. . . . . 6
             |
16 | | simprl 772 |
. . . . . 6
         |
17 | | foimacnv 5845 |
. . . . . 6
                  |
18 | 15, 16, 17 | syl2anc 673 |
. . . . 5
                  |
19 | 12, 18 | syl5eqr 2519 |
. . . 4
       
        |
20 | 19 | inteqd 4231 |
. . 3
        
         |
21 | 11, 20 | eqtrd 2505 |
. 2
               
            |
22 | | simpl 464 |
. . . . 5
       
   |
23 | 7 | a1i 11 |
. . . . 5
           
  |
24 | | simprr 774 |
. . . . . . 7
         |
25 | | n0 3732 |
. . . . . . 7
    |
26 | 24, 25 | sylib 201 |
. . . . . 6
          |
27 | 16 | sselda 3418 |
. . . . . . . 8
       
   |
28 | 3 | ad2antrr 740 |
. . . . . . . . . 10
       
       |
29 | 28, 5 | syl 17 |
. . . . . . . . 9
       
   |
30 | | fvelrnb 5926 |
. . . . . . . . 9
           |
31 | 29, 30 | syl 17 |
. . . . . . . 8
       
           |
32 | 27, 31 | mpbid 215 |
. . . . . . 7
       
         |
33 | | f1ofun 5830 |
. . . . . . . . . . . . . . . 16
       |
34 | 3, 33 | syl 17 |
. . . . . . . . . . . . . . 15
 
   |
35 | 34 | adantr 472 |
. . . . . . . . . . . . . 14
         |
36 | | fvimacnv 6012 |
. . . . . . . . . . . . . 14
                |
37 | 35, 36 | sylan 479 |
. . . . . . . . . . . . 13
       
     
        |
38 | | ne0i 3728 |
. . . . . . . . . . . . 13
             |
39 | 37, 38 | syl6bi 236 |
. . . . . . . . . . . 12
       
     
        |
40 | 39 | ex 441 |
. . . . . . . . . . 11
                      |
41 | | eleq1 2537 |
. . . . . . . . . . . . 13
         
   |
42 | 41 | biimprd 231 |
. . . . . . . . . . . 12
             |
43 | 42 | imim1d 77 |
. . . . . . . . . . 11
                           |
44 | 40, 43 | syl9 72 |
. . . . . . . . . 10
             
          |
45 | 44 | com24 89 |
. . . . . . . . 9
             
          |
46 | 45 | imp 436 |
. . . . . . . 8
       
      
         |
47 | 46 | rexlimdv 2870 |
. . . . . . 7
       
       
        |
48 | 32, 47 | mpd 15 |
. . . . . 6
       
        |
49 | 26, 48 | exlimddv 1789 |
. . . . 5
              |
50 | | eqid 2471 |
. . . . . 6
         |
51 | 50, 1, 2 | dibglbN 34805 |
. . . . 5
         
                                     |
52 | 22, 23, 49, 51 | syl12anc 1290 |
. . . 4
                        
            |
53 | | fvres 5893 |
. . . . 5
                       |
54 | 53 | iineq2i 4289 |
. . . 4
        
                     |
55 | 52, 54 | syl6eqr 2523 |
. . 3
                        
                   |
56 | | hlclat 32995 |
. . . . . . 7
   |
57 | 56 | ad2antrr 740 |
. . . . . 6
         |
58 | | eqid 2471 |
. . . . . . . . . 10
         |
59 | | eqid 2471 |
. . . . . . . . . 10
         |
60 | 58, 59, 1, 2 | dibdmN 34796 |
. . . . . . . . 9
 
               |
61 | | ssrab2 3500 |
. . . . . . . . 9
                 |
62 | 60, 61 | syl6eqss 3468 |
. . . . . . . 8
 
       |
63 | 62 | adantr 472 |
. . . . . . 7
             |
64 | 7, 63 | syl5ss 3429 |
. . . . . 6
                  |
65 | 58, 50 | clatglbcl 16438 |
. . . . . 6
                               |
66 | 57, 64, 65 | syl2anc 673 |
. . . . 5
                          |
67 | | n0 3732 |
. . . . . . 7
              |
68 | 49, 67 | sylib 201 |
. . . . . 6
               |
69 | | hllat 33000 |
. . . . . . . 8
   |
70 | 69 | ad3antrrr 744 |
. . . . . . 7
       
        |
71 | 66 | adantr 472 |
. . . . . . 7
       
                         |
72 | 64 | sselda 3418 |
. . . . . . 7
       
            |
73 | 58, 1 | lhpbase 33634 |
. . . . . . . 8
       |
74 | 73 | ad3antlr 745 |
. . . . . . 7
       
            |
75 | 56 | ad3antrrr 744 |
. . . . . . . 8
       
        |
76 | 60 | adantr 472 |
. . . . . . . . . . 11
      
              |
77 | 7, 76 | syl5sseq 3466 |
. . . . . . . . . 10
                          |
78 | 77, 61 | syl6ss 3430 |
. . . . . . . . 9
                  |
79 | 78 | adantr 472 |
. . . . . . . 8
       
                 |
80 | | simpr 468 |
. . . . . . . 8
       
             |
81 | 58, 59, 50 | clatglble 16449 |
. . . . . . . 8
          
     
                     |
82 | 75, 79, 80, 81 | syl3anc 1292 |
. . . . . . 7
       
                           |
83 | 7 | sseli 3414 |
. . . . . . . . . 10
        |
84 | 83 | adantl 473 |
. . . . . . . . 9
       
        |
85 | 58, 59, 1, 2 | dibeldmN 34797 |
. . . . . . . . . 10
 
                 |
86 | 85 | ad2antrr 740 |
. . . . . . . . 9
       
      
    
          |
87 | 84, 86 | mpbid 215 |
. . . . . . . 8
       
          
         |
88 | 87 | simprd 470 |
. . . . . . 7
       
              |
89 | 58, 59, 70, 71, 72, 74, 82, 88 | lattrd 16382 |
. . . . . 6
       
                           |
90 | 68, 89 | exlimddv 1789 |
. . . . 5
                            |
91 | 58, 59, 1, 2 | dibeldmN 34797 |
. . . . . 6
 
                                
                       |
92 | 91 | adantr 472 |
. . . . 5
                    
                 
                       |
93 | 66, 90, 92 | mpbir2and 936 |
. . . 4
                      |
94 | 1, 2 | dibclN 34801 |
. . . 4
                 
                   |
95 | 93, 94 | syldan 478 |
. . 3
                          |
96 | 55, 95 | eqeltrrd 2550 |
. 2
               
           |
97 | 21, 96 | eqeltrrd 2550 |
1
          |