Step | Hyp | Ref
| Expression |
1 | | restsspw 15330 |
. . . 4
 ↾t   
    |
2 | 1 | a1i 11 |
. . 3
  UnifOn    ↾t 
   
   |
3 | | inxp 4967 |
. . . . . 6
             |
4 | | dfss1 3637 |
. . . . . . . 8

    |
5 | 4 | biimpi 198 |
. . . . . . 7
     |
6 | 5 | sqxpeqd 4860 |
. . . . . 6
           |
7 | 3, 6 | syl5eq 2497 |
. . . . 5
   
       |
8 | 7 | adantl 468 |
. . . 4
  UnifOn     
       |
9 | | simpl 459 |
. . . . 5
  UnifOn   UnifOn    |
10 | | elfvex 5892 |
. . . . . . . 8
 UnifOn 
  |
11 | 10 | adantr 467 |
. . . . . . 7
  UnifOn     |
12 | | simpr 463 |
. . . . . . 7
  UnifOn     |
13 | 11, 12 | ssexd 4550 |
. . . . . 6
  UnifOn     |
14 | | xpexg 6593 |
. . . . . 6
 
     |
15 | 13, 13, 14 | syl2anc 667 |
. . . . 5
  UnifOn       |
16 | | ustbasel 21221 |
. . . . . 6
 UnifOn 
    |
17 | 16 | adantr 467 |
. . . . 5
  UnifOn       |
18 | | elrestr 15327 |
. . . . 5
  UnifOn   
  
       ↾t      |
19 | 9, 15, 17, 18 | syl3anc 1268 |
. . . 4
  UnifOn     
   
↾t      |
20 | 8, 19 | eqeltrrd 2530 |
. . 3
  UnifOn     
↾t      |
21 | 9 | ad5antr 740 |
. . . . . . . . 9
       UnifOn   
↾t      
        
UnifOn    |
22 | 15 | ad5antr 740 |
. . . . . . . . 9
       UnifOn   
↾t      
             |
23 | | simplr 762 |
. . . . . . . . . . 11
       UnifOn   
↾t      
        
  |
24 | | simp-4r 777 |
. . . . . . . . . . . . . 14
       UnifOn   
↾t      
        
     |
25 | 24 | elpwid 3961 |
. . . . . . . . . . . . 13
       UnifOn   
↾t      
             |
26 | 12 | ad5antr 740 |
. . . . . . . . . . . . . 14
       UnifOn   
↾t      
           |
27 | | xpss12 4940 |
. . . . . . . . . . . . . 14
 
  
    |
28 | 26, 26, 27 | syl2anc 667 |
. . . . . . . . . . . . 13
       UnifOn   
↾t      
          
    |
29 | 25, 28 | sstrd 3442 |
. . . . . . . . . . . 12
       UnifOn   
↾t      
             |
30 | | ustssxp 21219 |
. . . . . . . . . . . . 13
  UnifOn       |
31 | 21, 23, 30 | syl2anc 667 |
. . . . . . . . . . . 12
       UnifOn   
↾t      
             |
32 | 29, 31 | unssd 3610 |
. . . . . . . . . . 11
       UnifOn   
↾t      
          
    |
33 | | ssun2 3598 |
. . . . . . . . . . . 12

  |
34 | | ustssel 21220 |
. . . . . . . . . . . 12
  UnifOn 
             |
35 | 33, 34 | mpi 20 |
. . . . . . . . . . 11
  UnifOn 
         |
36 | 21, 23, 32, 35 | syl3anc 1268 |
. . . . . . . . . 10
       UnifOn   
↾t      
             |
37 | | df-ss 3418 |
. . . . . . . . . . . . . 14
  
      |
38 | 25, 37 | sylib 200 |
. . . . . . . . . . . . 13
       UnifOn   
↾t      
               |
39 | 38 | uneq1d 3587 |
. . . . . . . . . . . 12
       UnifOn   
↾t      
              
            |
40 | | simpr 463 |
. . . . . . . . . . . . . 14
       UnifOn   
↾t      
               |
41 | | simpllr 769 |
. . . . . . . . . . . . . 14
       UnifOn   
↾t      
        
  |
42 | 40, 41 | eqsstr3d 3467 |
. . . . . . . . . . . . 13
       UnifOn   
↾t      
               |
43 | | ssequn2 3607 |
. . . . . . . . . . . . 13
    
        |
44 | 42, 43 | sylib 200 |
. . . . . . . . . . . 12
       UnifOn   
↾t      
          
      |
45 | 39, 44 | eqtr2d 2486 |
. . . . . . . . . . 11
       UnifOn   
↾t      
        
 
          |
46 | | indir 3691 |
. . . . . . . . . . 11
           
     |
47 | 45, 46 | syl6eqr 2503 |
. . . . . . . . . 10
       UnifOn   
↾t      
        
        |
48 | | ineq1 3627 |
. . . . . . . . . . . 12
   
           |
49 | 48 | eqeq2d 2461 |
. . . . . . . . . . 11
       
         |
50 | 49 | rspcev 3150 |
. . . . . . . . . 10
   
       
      |
51 | 36, 47, 50 | syl2anc 667 |
. . . . . . . . 9
       UnifOn   
↾t      
         
      |
52 | | elrest 15326 |
. . . . . . . . . 10
  UnifOn       ↾t    
       |
53 | 52 | biimpar 488 |
. . . . . . . . 9
   UnifOn     
    
 ↾t      |
54 | 21, 22, 51, 53 | syl21anc 1267 |
. . . . . . . 8
       UnifOn   
↾t      
        
 ↾t      |
55 | | simp1 1008 |
. . . . . . . . . . 11
  UnifOn  
↾t     UnifOn    |
56 | 15 | 3adant3 1028 |
. . . . . . . . . . 11
  UnifOn  
↾t         |
57 | | simp3 1010 |
. . . . . . . . . . 11
  UnifOn  
↾t      ↾t      |
58 | | elrest 15326 |
. . . . . . . . . . . 12
  UnifOn       ↾t    
       |
59 | 58 | biimpa 487 |
. . . . . . . . . . 11
   UnifOn     
↾t     
      |
60 | 55, 56, 57, 59 | syl21anc 1267 |
. . . . . . . . . 10
  UnifOn  
↾t     
      |
61 | 60 | 3expa 1208 |
. . . . . . . . 9
   UnifOn   
↾t     
      |
62 | 61 | ad2antrr 732 |
. . . . . . . 8
     UnifOn 


↾t      
   

     |
63 | 54, 62 | r19.29a 2932 |
. . . . . . 7
     UnifOn 


↾t      
   
↾t      |
64 | 63 | ex 436 |
. . . . . 6
    UnifOn 
  ↾t    
      ↾t       |
65 | 64 | ralrimiva 2802 |
. . . . 5
   UnifOn   
↾t      
    ↾t       |
66 | 9 | ad5antr 740 |
. . . . . . . 8
       UnifOn   
↾t      ↾t    


           UnifOn    |
67 | 15 | ad5antr 740 |
. . . . . . . 8
       UnifOn   
↾t      ↾t    


               |
68 | | simpllr 769 |
. . . . . . . . . 10
       UnifOn   
↾t      ↾t    


             |
69 | | simplr 762 |
. . . . . . . . . 10
       UnifOn   
↾t      ↾t    


             |
70 | | ustincl 21222 |
. . . . . . . . . 10
  UnifOn 
 
   |
71 | 66, 68, 69, 70 | syl3anc 1268 |
. . . . . . . . 9
       UnifOn   
↾t      ↾t    


               |
72 | | simprl 764 |
. . . . . . . . . . 11
       UnifOn   
↾t      ↾t    


                 |
73 | | simprr 766 |
. . . . . . . . . . 11
       UnifOn   
↾t      ↾t    


                 |
74 | 72, 73 | ineq12d 3635 |
. . . . . . . . . 10
       UnifOn   
↾t      ↾t    


                         |
75 | | inindir 3650 |
. . . . . . . . . 10
           
     |
76 | 74, 75 | syl6eqr 2503 |
. . . . . . . . 9
       UnifOn   
↾t      ↾t    


               
     |
77 | | ineq1 3627 |
. . . . . . . . . . 11
   
           |
78 | 77 | eqeq2d 2461 |
. . . . . . . . . 10
         
    
      |
79 | 78 | rspcev 3150 |
. . . . . . . . 9
                      |
80 | 71, 76, 79 | syl2anc 667 |
. . . . . . . 8
       UnifOn   
↾t      ↾t    


                    |
81 | | elrest 15326 |
. . . . . . . . 9
  UnifOn         ↾t              |
82 | 81 | biimpar 488 |
. . . . . . . 8
   UnifOn     

         ↾t      |
83 | 66, 67, 80, 82 | syl21anc 1267 |
. . . . . . 7
       UnifOn   
↾t      ↾t    


              ↾t      |
84 | 61 | adantr 467 |
. . . . . . . 8
    UnifOn 
  ↾t    
 ↾t    


     |
85 | 9 | ad2antrr 732 |
. . . . . . . . 9
    UnifOn 
  ↾t    
 ↾t    
UnifOn    |
86 | 15 | ad2antrr 732 |
. . . . . . . . 9
    UnifOn 
  ↾t    
 ↾t    
    |
87 | | simpr 463 |
. . . . . . . . 9
    UnifOn 
  ↾t    
 ↾t    

↾t      |
88 | 52 | biimpa 487 |
. . . . . . . . 9
   UnifOn     
↾t     
      |
89 | 85, 86, 87, 88 | syl21anc 1267 |
. . . . . . . 8
    UnifOn 
  ↾t    
 ↾t    


     |
90 | | reeanv 2958 |
. . . . . . . 8
  
    
    
 
    
       |
91 | 84, 89, 90 | sylanbrc 670 |
. . . . . . 7
    UnifOn 
  ↾t    
 ↾t    


            |
92 | 83, 91 | r19.29vva 2934 |
. . . . . 6
    UnifOn 
  ↾t    
 ↾t    
   ↾t      |
93 | 92 | ralrimiva 2802 |
. . . . 5
   UnifOn   
↾t       ↾t       
↾t      |
94 | | simp-4l 776 |
. . . . . . . . . 10
     UnifOn 


↾t     

   
UnifOn    |
95 | | simplr 762 |
. . . . . . . . . 10
     UnifOn 


↾t     

   
  |
96 | | ustdiag 21223 |
. . . . . . . . . 10
  UnifOn      |
97 | 94, 95, 96 | syl2anc 667 |
. . . . . . . . 9
     UnifOn 


↾t     

   
   |
98 | | simp-4r 777 |
. . . . . . . . 9
     UnifOn 


↾t     

   
  |
99 | | inss1 3652 |
. . . . . . . . . . . . . 14

      |
100 | | resss 5128 |
. . . . . . . . . . . . . 14
  |
101 | 99, 100 | sstri 3441 |
. . . . . . . . . . . . 13

     |
102 | | iss 5152 |
. . . . . . . . . . . . 13
                   |
103 | 101, 102 | mpbi 212 |
. . . . . . . . . . . 12

   

      |
104 | | simpr 463 |
. . . . . . . . . . . . . . . 16
 
   |
105 | | ssel2 3427 |
. . . . . . . . . . . . . . . . 17
 
   |
106 | | equid 1855 |
. . . . . . . . . . . . . . . . . 18
 |
107 | | resieq 5115 |
. . . . . . . . . . . . . . . . . 18
 
    
   |
108 | 106, 107 | mpbiri 237 |
. . . . . . . . . . . . . . . . 17
 
      |
109 | 105, 105,
108 | syl2anc 667 |
. . . . . . . . . . . . . . . 16
 
      |
110 | | breq2 4406 |
. . . . . . . . . . . . . . . . 17
           |
111 | 110 | rspcev 3150 |
. . . . . . . . . . . . . . . 16
      
     |
112 | 104, 109,
111 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
       |
113 | 112 | ralrimiva 2802 |
. . . . . . . . . . . . . 14
 

     |
114 | | dminxp 5277 |
. . . . . . . . . . . . . 14
       
     |
115 | 113, 114 | sylibr 216 |
. . . . . . . . . . . . 13
        |
116 | 115 | reseq2d 5105 |
. . . . . . . . . . . 12
 
        |
117 | 103, 116 | syl5req 2498 |
. . . . . . . . . . 11
         |
118 | 117 | adantl 468 |
. . . . . . . . . 10
            |
119 | | ssrin 3657 |
. . . . . . . . . . 11


     
     |
120 | 119 | adantr 467 |
. . . . . . . . . 10
         
     |
121 | 118, 120 | eqsstrd 3466 |
. . . . . . . . 9
     
     |
122 | 97, 98, 121 | syl2anc 667 |
. . . . . . . 8
     UnifOn 


↾t     

   
 
     |
123 | | simpr 463 |
. . . . . . . 8
     UnifOn 


↾t     

   

     |
124 | 122, 123 | sseqtr4d 3469 |
. . . . . . 7
     UnifOn 


↾t     

   
   |
125 | 124, 61 | r19.29a 2932 |
. . . . . 6
   UnifOn   
↾t        |
126 | 15 | ad3antrrr 736 |
. . . . . . . 8
     UnifOn 


↾t     

   
    |
127 | | ustinvel 21224 |
. . . . . . . . . 10
  UnifOn   
  |
128 | 94, 95, 127 | syl2anc 667 |
. . . . . . . . 9
     UnifOn 


↾t     

   
   |
129 | 123 | cnveqd 5010 |
. . . . . . . . . 10
     UnifOn 


↾t     

   
        |
130 | | cnvin 5243 |
. . . . . . . . . . 11
            |
131 | | cnvxp 5254 |
. . . . . . . . . . . 12
      |
132 | 131 | ineq2i 3631 |
. . . . . . . . . . 11
            |
133 | 130, 132 | eqtri 2473 |
. . . . . . . . . 10
           |
134 | 129, 133 | syl6eq 2501 |
. . . . . . . . 9
     UnifOn 


↾t     

   
        |
135 | | ineq1 3627 |
. . . . . . . . . . 11
             |
136 | 135 | eqeq2d 2461 |
. . . . . . . . . 10
        
 
      |
137 | 136 | rspcev 3150 |
. . . . . . . . 9
  

 
   

       |
138 | 128, 134,
137 | syl2anc 667 |
. . . . . . . 8
     UnifOn 


↾t     

   

       |
139 | | elrest 15326 |
. . . . . . . . 9
  UnifOn      
 ↾t 
 

        |
140 | 139 | biimpar 488 |
. . . . . . . 8
   UnifOn     

     
 ↾t 
    |
141 | 94, 126, 138, 140 | syl21anc 1267 |
. . . . . . 7
     UnifOn 


↾t     

   
 
↾t      |
142 | 141, 61 | r19.29a 2932 |
. . . . . 6
   UnifOn   
↾t      
↾t      |
143 | | simp-4l 776 |
. . . . . . . . . . . 12
     UnifOn 

    
UnifOn    |
144 | 15 | ad3antrrr 736 |
. . . . . . . . . . . 12
     UnifOn 

         |
145 | | simplr 762 |
. . . . . . . . . . . 12
     UnifOn 

    
  |
146 | | elrestr 15327 |
. . . . . . . . . . . 12
  UnifOn   
 
   
↾t      |
147 | 143, 144,
145, 146 | syl3anc 1268 |
. . . . . . . . . . 11
     UnifOn 

          ↾t      |
148 | | inss1 3652 |
. . . . . . . . . . . . . . 15
     |
149 | | coss1 4990 |
. . . . . . . . . . . . . . . 16
               

      |
150 | | coss2 4991 |
. . . . . . . . . . . . . . . 16
               |
151 | 149, 150 | sstrd 3442 |
. . . . . . . . . . . . . . 15
               
   |
152 | 148, 151 | ax-mp 5 |
. . . . . . . . . . . . . 14
          
  |
153 | | sstr 3440 |
. . . . . . . . . . . . . 14
       
              
      |
154 | 152, 153 | mpan 676 |
. . . . . . . . . . . . 13
               |
155 | 154 | adantl 468 |
. . . . . . . . . . . 12
     UnifOn 

          
      |
156 | | inss2 3653 |
. . . . . . . . . . . . . . 15
    
  |
157 | | coss1 4990 |
. . . . . . . . . . . . . . . 16
                    
      |
158 | | coss2 4991 |
. . . . . . . . . . . . . . . 16
                       |
159 | 157, 158 | sstrd 3442 |
. . . . . . . . . . . . . . 15
                         |
160 | 156, 159 | ax-mp 5 |
. . . . . . . . . . . . . 14
                 |
161 | | xpidtr 5222 |
. . . . . . . . . . . . . 14
      
  |
162 | 160, 161 | sstri 3441 |
. . . . . . . . . . . . 13
          
  |
163 | 162 | a1i 11 |
. . . . . . . . . . . 12
     UnifOn 

          
        |
164 | 155, 163 | ssind 3656 |
. . . . . . . . . . 11
     UnifOn 

          
          |
165 | | id 22 |
. . . . . . . . . . . . . 14
           |
166 | 165, 165 | coeq12d 4999 |
. . . . . . . . . . . . 13
                   |
167 | 166 | sseq1d 3459 |
. . . . . . . . . . . 12
       
   
 
       
       |
168 | 167 | rspcev 3150 |
. . . . . . . . . . 11
       ↾t             
     
 ↾t 
     
     |
169 | 147, 164,
168 | syl2anc 667 |
. . . . . . . . . 10
     UnifOn 

     
 ↾t 
     
     |
170 | | ustexhalf 21225 |
. . . . . . . . . . 11
  UnifOn   
    |
171 | 170 | adantlr 721 |
. . . . . . . . . 10
   UnifOn    
    |
172 | 169, 171 | r19.29a 2932 |
. . . . . . . . 9
   UnifOn     
↾t             |
173 | 94, 98, 95, 172 | syl21anc 1267 |
. . . . . . . 8
     UnifOn 


↾t     

   
 
↾t             |
174 | 123 | sseq2d 3460 |
. . . . . . . . 9
     UnifOn 


↾t     

   
  
  
      |
175 | 174 | rexbidv 2901 |
. . . . . . . 8
     UnifOn 


↾t     

   
 
 ↾t      
 
↾t              |
176 | 173, 175 | mpbird 236 |
. . . . . . 7
     UnifOn 


↾t     

   
 
↾t         |
177 | 176, 61 | r19.29a 2932 |
. . . . . 6
   UnifOn   
↾t       ↾t         |
178 | 125, 142,
177 | 3jca 1188 |
. . . . 5
   UnifOn   
↾t       
 ↾t 
  
 ↾t      
   |
179 | 65, 93, 178 | 3jca 1188 |
. . . 4
   UnifOn   
↾t           
↾t      
↾t        ↾t      
 ↾t 
  
 ↾t      
    |
180 | 179 | ralrimiva 2802 |
. . 3
  UnifOn    
↾t       
    ↾t       ↾t        ↾t      
 ↾t     
↾t           |
181 | 2, 20, 180 | 3jca 1188 |
. 2
  UnifOn    
↾t      
   ↾t    
 ↾t           
↾t      
↾t        ↾t      
 ↾t 
  
 ↾t      
     |
182 | | isust 21218 |
. . 3
  
↾t    UnifOn   
↾t      
   ↾t    
 ↾t           
↾t      
↾t        ↾t      
 ↾t 
  
 ↾t      
      |
183 | 13, 182 | syl 17 |
. 2
  UnifOn    
↾t    UnifOn   
↾t      
   ↾t    
 ↾t           
↾t      
↾t        ↾t      
 ↾t 
  
 ↾t      
      |
184 | 181, 183 | mpbird 236 |
1
  UnifOn    ↾t 
  UnifOn    |