Step | Hyp | Ref
| Expression |
1 | | ovex 6336 |
. . . . . 6
 ↾t   |
2 | | elfi2 7946 |
. . . . . 6
  ↾t       ↾t  
     ↾t           |
3 | 1, 2 | ax-mp 5 |
. . . . 5
    
↾t  
     ↾t          |
4 | | eldifi 3544 |
. . . . . . . . . . 11
    
↾t         ↾t     |
5 | 4 | adantl 473 |
. . . . . . . . . 10
   
    ↾t          ↾t     |
6 | | elfpw 7894 |
. . . . . . . . . . 11
    ↾t     ↾t     |
7 | 6 | simprbi 471 |
. . . . . . . . . 10
    ↾t     |
8 | 5, 7 | syl 17 |
. . . . . . . . 9
   
    ↾t         |
9 | 6 | simplbi 467 |
. . . . . . . . . . . . 13
    ↾t    ↾t    |
10 | 5, 9 | syl 17 |
. . . . . . . . . . . 12
   
    ↾t        ↾t    |
11 | 10 | sseld 3417 |
. . . . . . . . . . 11
   
    ↾t       

↾t     |
12 | | elrest 15404 |
. . . . . . . . . . . 12
 
   ↾t 

     |
13 | 12 | adantr 472 |
. . . . . . . . . . 11
   
    ↾t        
↾t 

     |
14 | 11, 13 | sylibd 222 |
. . . . . . . . . 10
   
    ↾t       

     |
15 | 14 | ralrimiv 2808 |
. . . . . . . . 9
   
    ↾t        
    |
16 | | ineq1 3618 |
. . . . . . . . . . 11
     
         |
17 | 16 | eqeq2d 2481 |
. . . . . . . . . 10
       
         |
18 | 17 | ac6sfi 7833 |
. . . . . . . . 9
   
          
         |
19 | 8, 15, 18 | syl2anc 673 |
. . . . . . . 8
   
    ↾t                        |
20 | | eldifsni 4089 |
. . . . . . . . . . . . . 14
    
↾t        |
21 | 20 | ad2antlr 741 |
. . . . . . . . . . . . 13
   

    ↾t              |
22 | | iinin1 4340 |
. . . . . . . . . . . . 13

            
   |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . 12
   

    ↾t                 
  
       |
24 | | fvex 5889 |
. . . . . . . . . . . . . 14
     |
25 | 24 | a1i 11 |
. . . . . . . . . . . . 13
   

    ↾t                  |
26 | | simpllr 777 |
. . . . . . . . . . . . 13
   

    ↾t           
  |
27 | | ffn 5739 |
. . . . . . . . . . . . . . . 16
       |
28 | 27 | adantl 473 |
. . . . . . . . . . . . . . 15
   

    ↾t              |
29 | | fniinfv 5939 |
. . . . . . . . . . . . . . 15
 
       |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . . 14
   

    ↾t                    |
31 | | simplll 776 |
. . . . . . . . . . . . . . 15
   

    ↾t           
  |
32 | | simpr 468 |
. . . . . . . . . . . . . . 15
   

    ↾t                  |
33 | 8 | adantr 472 |
. . . . . . . . . . . . . . 15
   

    ↾t              |
34 | | intrnfi 7948 |
. . . . . . . . . . . . . . 15
         
      |
35 | 31, 32, 21, 33, 34 | syl13anc 1294 |
. . . . . . . . . . . . . 14
   

    ↾t                   |
36 | 30, 35 | eqeltrd 2549 |
. . . . . . . . . . . . 13
   

    ↾t                       |
37 | | elrestr 15405 |
. . . . . . . . . . . . 13
     

                    
↾t    |
38 | 25, 26, 36, 37 | syl3anc 1292 |
. . . . . . . . . . . 12
   

    ↾t                 
     
↾t    |
39 | 23, 38 | eqeltrd 2549 |
. . . . . . . . . . 11
   

    ↾t                 
     
↾t    |
40 | | intiin 4323 |
. . . . . . . . . . . . 13
   |
41 | | iineq2 4287 |
. . . . . . . . . . . . 13
 
      
     
   |
42 | 40, 41 | syl5eq 2517 |
. . . . . . . . . . . 12
 
                |
43 | 42 | eleq1d 2533 |
. . . . . . . . . . 11
 
       
     ↾t 
            ↾t     |
44 | 39, 43 | syl5ibrcom 230 |
. . . . . . . . . 10
   

    ↾t                  
       ↾t     |
45 | 44 | expimpd 614 |
. . . . . . . . 9
   
    ↾t                     
     ↾t     |
46 | 45 | exlimdv 1787 |
. . . . . . . 8
   
    ↾t               
            
↾t     |
47 | 19, 46 | mpd 15 |
. . . . . . 7
   
    ↾t             ↾t    |
48 | | eleq1 2537 |
. . . . . . 7
        ↾t 
     
↾t     |
49 | 47, 48 | syl5ibrcom 230 |
. . . . . 6
   
    ↾t             
↾t     |
50 | 49 | rexlimdva 2871 |
. . . . 5
 
       ↾t             ↾t     |
51 | 3, 50 | syl5bi 225 |
. . . 4
 
      ↾t       
↾t     |
52 | | simpr 468 |
. . . . . 6
 
   |
53 | | elrest 15404 |
. . . . . 6
     
       ↾t 
           |
54 | 24, 52, 53 | sylancr 676 |
. . . . 5
 
       ↾t 
           |
55 | | elfi2 7946 |
. . . . . . . 8
     
             |
56 | 55 | adantr 472 |
. . . . . . 7
 
      
            |
57 | | eldifsni 4089 |
. . . . . . . . . . . . . 14
          |
58 | 57 | adantl 473 |
. . . . . . . . . . . . 13
   
          |
59 | | iinin1 4340 |
. . . . . . . . . . . . 13

        |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
   
        
       |
61 | 40 | ineq1i 3621 |
. . . . . . . . . . . 12
       |
62 | 60, 61 | syl6eqr 2523 |
. . . . . . . . . . 11
   
        
       |
63 | 1 | a1i 11 |
. . . . . . . . . . . 12
   
         ↾t    |
64 | | eldifi 3544 |
. . . . . . . . . . . . . . 15
             |
65 | 64 | adantl 473 |
. . . . . . . . . . . . . 14
   
             |
66 | | elfpw 7894 |
. . . . . . . . . . . . . . 15
   
    |
67 | 66 | simplbi 467 |
. . . . . . . . . . . . . 14
      |
68 | 65, 67 | syl 17 |
. . . . . . . . . . . . 13
   
          |
69 | | elrestr 15405 |
. . . . . . . . . . . . . . . 16
 
 
 
↾t    |
70 | 69 | 3expa 1231 |
. . . . . . . . . . . . . . 15
   

   ↾t    |
71 | 70 | ralrimiva 2809 |
. . . . . . . . . . . . . 14
 
     ↾t    |
72 | 71 | adantr 472 |
. . . . . . . . . . . . 13
   
        
   ↾t    |
73 | | ssralv 3479 |
. . . . . . . . . . . . 13
  
   ↾t 

   ↾t     |
74 | 68, 72, 73 | sylc 61 |
. . . . . . . . . . . 12
   
        
   ↾t    |
75 | 66 | simprbi 471 |
. . . . . . . . . . . . 13
      |
76 | 65, 75 | syl 17 |
. . . . . . . . . . . 12
   
          |
77 | | iinfi 7949 |
. . . . . . . . . . . 12
  
↾t       ↾t          
↾t     |
78 | 63, 74, 58, 76, 77 | syl13anc 1294 |
. . . . . . . . . . 11
   
        
      ↾t     |
79 | 62, 78 | eqeltrrd 2550 |
. . . . . . . . . 10
   
         
    
↾t     |
80 | | eleq1 2537 |
. . . . . . . . . 10
         ↾t          ↾t      |
81 | 79, 80 | syl5ibrcom 230 |
. . . . . . . . 9
   
           
   
↾t      |
82 | | ineq1 3618 |
. . . . . . . . . . 11
         |
83 | 82 | eqeq2d 2481 |
. . . . . . . . . 10
           |
84 | 83 | imbi1d 324 |
. . . . . . . . 9
     
    ↾t   
        ↾t       |
85 | 81, 84 | syl5ibrcom 230 |
. . . . . . . 8
   
                 ↾t       |
86 | 85 | rexlimdva 2871 |
. . . . . . 7
 
              
   
↾t       |
87 | 56, 86 | sylbid 223 |
. . . . . 6
 
        
    ↾t       |
88 | 87 | rexlimdv 2870 |
. . . . 5
 
              ↾t      |
89 | 54, 88 | sylbid 223 |
. . . 4
 
       ↾t      ↾t      |
90 | 51, 89 | impbid 195 |
. . 3
 
      ↾t  
    
↾t     |
91 | 90 | eqrdv 2469 |
. 2
 
     ↾t       
↾t    |
92 | | fi0 7952 |
. . 3
     |
93 | | relxp 4947 |
. . . . . 6
   |
94 | | restfn 15401 |
. . . . . . . 8
↾t
   |
95 | | fndm 5685 |
. . . . . . . 8
↾t   ↾t     |
96 | 94, 95 | ax-mp 5 |
. . . . . . 7
↾t
   |
97 | 96 | releqi 4923 |
. . . . . 6
 ↾t     |
98 | 93, 97 | mpbir 214 |
. . . . 5
↾t |
99 | 98 | ovprc 6338 |
. . . 4
   
↾t    |
100 | 99 | fveq2d 5883 |
. . 3
       ↾t         |
101 | | ianor 496 |
. . . 4
       |
102 | | fvprc 5873 |
. . . . . . 7
       |
103 | 102 | oveq1d 6323 |
. . . . . 6
      ↾t   ↾t    |
104 | | 0rest 15406 |
. . . . . 6
 ↾t   |
105 | 103, 104 | syl6eq 2521 |
. . . . 5
      ↾t    |
106 | 98 | ovprc2 6340 |
. . . . 5
      ↾t    |
107 | 105, 106 | jaoi 386 |
. . . 4
        ↾t    |
108 | 101, 107 | sylbi 200 |
. . 3
       
↾t    |
109 | 92, 100, 108 | 3eqtr4a 2531 |
. 2
       ↾t       
↾t    |
110 | 91, 109 | pm2.61i 169 |
1
    ↾t        ↾t   |