Step | Hyp | Ref
| Expression |
1 | | ovex 6316 |
. . . . . 6
 ↾t   |
2 | | elfi2 7925 |
. . . . . 6
  ↾t       ↾t  
     ↾t           |
3 | 1, 2 | ax-mp 5 |
. . . . 5
    
↾t  
     ↾t          |
4 | | eldifi 3554 |
. . . . . . . . . . 11
    
↾t         ↾t     |
5 | 4 | adantl 468 |
. . . . . . . . . 10
   
    ↾t          ↾t     |
6 | | elfpw 7873 |
. . . . . . . . . . 11
    ↾t     ↾t     |
7 | 6 | simprbi 466 |
. . . . . . . . . 10
    ↾t     |
8 | 5, 7 | syl 17 |
. . . . . . . . 9
   
    ↾t         |
9 | 6 | simplbi 462 |
. . . . . . . . . . . . 13
    ↾t    ↾t    |
10 | 5, 9 | syl 17 |
. . . . . . . . . . . 12
   
    ↾t        ↾t    |
11 | 10 | sseld 3430 |
. . . . . . . . . . 11
   
    ↾t       

↾t     |
12 | | elrest 15319 |
. . . . . . . . . . . 12
 
   ↾t 

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

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

     |
15 | 14 | ralrimiv 2799 |
. . . . . . . . 9
   
    ↾t        
    |
16 | | ineq1 3626 |
. . . . . . . . . . 11
     
         |
17 | 16 | eqeq2d 2460 |
. . . . . . . . . 10
       
         |
18 | 17 | ac6sfi 7812 |
. . . . . . . . 9
   
          
         |
19 | 8, 15, 18 | syl2anc 666 |
. . . . . . . 8
   
    ↾t                        |
20 | | eldifsni 4097 |
. . . . . . . . . . . . . 14
    
↾t        |
21 | 20 | ad2antlr 732 |
. . . . . . . . . . . . 13
   

    ↾t              |
22 | | iinin1 4348 |
. . . . . . . . . . . . 13

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

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

    ↾t                  |
26 | | simpllr 768 |
. . . . . . . . . . . . 13
   

    ↾t           
  |
27 | | ffn 5726 |
. . . . . . . . . . . . . . . 16
       |
28 | 27 | adantl 468 |
. . . . . . . . . . . . . . 15
   

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

    ↾t                    |
31 | | simplll 767 |
. . . . . . . . . . . . . . 15
   

    ↾t           
  |
32 | | simpr 463 |
. . . . . . . . . . . . . . 15
   

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

    ↾t              |
34 | | intrnfi 7927 |
. . . . . . . . . . . . . . 15
         
      |
35 | 31, 32, 21, 33, 34 | syl13anc 1269 |
. . . . . . . . . . . . . 14
   

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

    ↾t                       |
37 | | elrestr 15320 |
. . . . . . . . . . . . 13
     

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

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

    ↾t                 
     
↾t    |
40 | | intiin 4331 |
. . . . . . . . . . . . 13
   |
41 | | iineq2 4295 |
. . . . . . . . . . . . 13
 
      
     
   |
42 | 40, 41 | syl5eq 2496 |
. . . . . . . . . . . 12
 
                |
43 | 42 | eleq1d 2512 |
. . . . . . . . . . 11
 
       
     ↾t 
            ↾t     |
44 | 39, 43 | syl5ibrcom 226 |
. . . . . . . . . 10
   

    ↾t                  
       ↾t     |
45 | 44 | expimpd 607 |
. . . . . . . . 9
   
    ↾t                     
     ↾t     |
46 | 45 | exlimdv 1778 |
. . . . . . . 8
   
    ↾t               
            
↾t     |
47 | 19, 46 | mpd 15 |
. . . . . . 7
   
    ↾t             ↾t    |
48 | | eleq1 2516 |
. . . . . . 7
        ↾t 
     
↾t     |
49 | 47, 48 | syl5ibrcom 226 |
. . . . . 6
   
    ↾t             
↾t     |
50 | 49 | rexlimdva 2878 |
. . . . 5
 
       ↾t             ↾t     |
51 | 3, 50 | syl5bi 221 |
. . . 4
 
      ↾t       
↾t     |
52 | | simpr 463 |
. . . . . 6
 
   |
53 | | elrest 15319 |
. . . . . 6
     
       ↾t 
           |
54 | 24, 52, 53 | sylancr 668 |
. . . . 5
 
       ↾t 
           |
55 | | elfi2 7925 |
. . . . . . . 8
     
             |
56 | 55 | adantr 467 |
. . . . . . 7
 
      
            |
57 | | eldifsni 4097 |
. . . . . . . . . . . . . 14
          |
58 | 57 | adantl 468 |
. . . . . . . . . . . . 13
   
          |
59 | | iinin1 4348 |
. . . . . . . . . . . . 13

        |
60 | 58, 59 | syl 17 |
. . . . . . . . . . . 12
   
        
       |
61 | 40 | ineq1i 3629 |
. . . . . . . . . . . 12
       |
62 | 60, 61 | syl6eqr 2502 |
. . . . . . . . . . 11
   
        
       |
63 | 1 | a1i 11 |
. . . . . . . . . . . 12
   
         ↾t    |
64 | | eldifi 3554 |
. . . . . . . . . . . . . . 15
             |
65 | 64 | adantl 468 |
. . . . . . . . . . . . . 14
   
             |
66 | | elfpw 7873 |
. . . . . . . . . . . . . . 15
   
    |
67 | 66 | simplbi 462 |
. . . . . . . . . . . . . 14
      |
68 | 65, 67 | syl 17 |
. . . . . . . . . . . . 13
   
          |
69 | | elrestr 15320 |
. . . . . . . . . . . . . . . 16
 
 
 
↾t    |
70 | 69 | 3expa 1207 |
. . . . . . . . . . . . . . 15
   

   ↾t    |
71 | 70 | ralrimiva 2801 |
. . . . . . . . . . . . . 14
 
     ↾t    |
72 | 71 | adantr 467 |
. . . . . . . . . . . . 13
   
        
   ↾t    |
73 | | ssralv 3492 |
. . . . . . . . . . . . 13
  
   ↾t 

   ↾t     |
74 | 68, 72, 73 | sylc 62 |
. . . . . . . . . . . 12
   
        
   ↾t    |
75 | 66 | simprbi 466 |
. . . . . . . . . . . . 13
      |
76 | 65, 75 | syl 17 |
. . . . . . . . . . . 12
   
          |
77 | | iinfi 7928 |
. . . . . . . . . . . 12
  
↾t       ↾t          
↾t     |
78 | 63, 74, 58, 76, 77 | syl13anc 1269 |
. . . . . . . . . . 11
   
        
      ↾t     |
79 | 62, 78 | eqeltrrd 2529 |
. . . . . . . . . 10
   
         
    
↾t     |
80 | | eleq1 2516 |
. . . . . . . . . 10
         ↾t          ↾t      |
81 | 79, 80 | syl5ibrcom 226 |
. . . . . . . . 9
   
           
   
↾t      |
82 | | ineq1 3626 |
. . . . . . . . . . 11
         |
83 | 82 | eqeq2d 2460 |
. . . . . . . . . 10
           |
84 | 83 | imbi1d 319 |
. . . . . . . . 9
     
    ↾t   
        ↾t       |
85 | 81, 84 | syl5ibrcom 226 |
. . . . . . . 8
   
                 ↾t       |
86 | 85 | rexlimdva 2878 |
. . . . . . 7
 
              
   
↾t       |
87 | 56, 86 | sylbid 219 |
. . . . . 6
 
        
    ↾t       |
88 | 87 | rexlimdv 2876 |
. . . . 5
 
              ↾t      |
89 | 54, 88 | sylbid 219 |
. . . 4
 
       ↾t      ↾t      |
90 | 51, 89 | impbid 194 |
. . 3
 
      ↾t  
    
↾t     |
91 | 90 | eqrdv 2448 |
. 2
 
     ↾t       
↾t    |
92 | | fi0 7931 |
. . 3
     |
93 | | relxp 4941 |
. . . . . 6
   |
94 | | restfn 15316 |
. . . . . . . 8
↾t
   |
95 | | fndm 5673 |
. . . . . . . 8
↾t   ↾t     |
96 | 94, 95 | ax-mp 5 |
. . . . . . 7
↾t
   |
97 | 96 | releqi 4917 |
. . . . . 6
 ↾t     |
98 | 93, 97 | mpbir 213 |
. . . . 5
↾t |
99 | 98 | ovprc 6318 |
. . . 4
   
↾t    |
100 | 99 | fveq2d 5867 |
. . 3
       ↾t         |
101 | | ianor 491 |
. . . 4
       |
102 | | fvprc 5857 |
. . . . . . 7
       |
103 | 102 | oveq1d 6303 |
. . . . . 6
      ↾t   ↾t    |
104 | | 0rest 15321 |
. . . . . 6
 ↾t   |
105 | 103, 104 | syl6eq 2500 |
. . . . 5
      ↾t    |
106 | 98 | ovprc2 6320 |
. . . . 5
      ↾t    |
107 | 105, 106 | jaoi 381 |
. . . 4
        ↾t    |
108 | 101, 107 | sylbi 199 |
. . 3
       
↾t    |
109 | 92, 100, 108 | 3eqtr4a 2510 |
. 2
       ↾t       
↾t    |
110 | 91, 109 | pm2.61i 168 |
1
    ↾t        ↾t   |