Step | Hyp | Ref
| Expression |
1 | | simp-6l 785 |
. . . . . . . 8
        UnifOn 

                         
 UnifOn 
   |
2 | | simp-7l 787 |
. . . . . . . . . 10
        UnifOn 

                         
UnifOn    |
3 | | simp-4r 782 |
. . . . . . . . . 10
        UnifOn 

                         
  |
4 | | simplr 767 |
. . . . . . . . . 10
        UnifOn 

                         
  |
5 | | ustincl 21270 |
. . . . . . . . . 10
  UnifOn 
 
   |
6 | 2, 3, 4, 5 | syl3anc 1276 |
. . . . . . . . 9
        UnifOn 

                         
    |
7 | | simpllr 774 |
. . . . . . . . . 10
        UnifOn 

                         
        |
8 | | ineq12 3640 |
. . . . . . . . . . 11
       
                         |
9 | | vex 3059 |
. . . . . . . . . . . 12
 |
10 | | inimasn 5271 |
. . . . . . . . . . . 12
                         |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . . 11
                       |
12 | 8, 11 | syl6eqr 2513 |
. . . . . . . . . 10
       
                   |
13 | 7, 12 | sylancom 678 |
. . . . . . . . 9
        UnifOn 

                         
            |
14 | | imaeq1 5181 |
. . . . . . . . . . 11
                   |
15 | 14 | eqeq2d 2471 |
. . . . . . . . . 10
                         |
16 | 15 | rspcev 3161 |
. . . . . . . . 9
               
          |
17 | 6, 13, 16 | syl2anc 671 |
. . . . . . . 8
        UnifOn 

                         

          |
18 | | vex 3059 |
. . . . . . . . . . 11
 |
19 | 18 | inex1 4557 |
. . . . . . . . . 10
   |
20 | | utopustuq.1 |
. . . . . . . . . . 11
           |
21 | 20 | ustuqtoplem 21302 |
. . . . . . . . . 10
   UnifOn   
        

           |
22 | 19, 21 | mpan2 682 |
. . . . . . . . 9
  UnifOn         

           |
23 | 22 | biimpar 492 |
. . . . . . . 8
   UnifOn   

       
        |
24 | 1, 17, 23 | syl2anc 671 |
. . . . . . 7
        UnifOn 

                         
        |
25 | | simp-4l 781 |
. . . . . . . 8
      UnifOn                    
 UnifOn 
   |
26 | | simpllr 774 |
. . . . . . . 8
      UnifOn                    
      |
27 | | vex 3059 |
. . . . . . . . . 10
 |
28 | 20 | ustuqtoplem 21302 |
. . . . . . . . . 10
   UnifOn        

         |
29 | 27, 28 | mpan2 682 |
. . . . . . . . 9
  UnifOn       

         |
30 | 29 | biimpa 491 |
. . . . . . . 8
   UnifOn        
        |
31 | 25, 26, 30 | syl2anc 671 |
. . . . . . 7
      UnifOn                    

        |
32 | 24, 31 | r19.29a 2943 |
. . . . . 6
      UnifOn                    
        |
33 | 20 | ustuqtoplem 21302 |
. . . . . . . . 9
   UnifOn        

         |
34 | 18, 33 | mpan2 682 |
. . . . . . . 8
  UnifOn       

         |
35 | 34 | biimpa 491 |
. . . . . . 7
   UnifOn        
        |
36 | 35 | adantr 471 |
. . . . . 6
    UnifOn 

          
        |
37 | 32, 36 | r19.29a 2943 |
. . . . 5
    UnifOn 

          
       |
38 | 37 | ralrimiva 2813 |
. . . 4
   UnifOn                      |
39 | 38 | ralrimiva 2813 |
. . 3
  UnifOn                       |
40 | | fvex 5897 |
. . . 4
     |
41 | | inficl 7964 |
. . . 4
      
     
          
               |
42 | 40, 41 | ax-mp 5 |
. . 3
 
                               |
43 | 39, 42 | sylib 201 |
. 2
  UnifOn                 |
44 | | eqimss 3495 |
. 2
                           |
45 | 43, 44 | syl 17 |
1
  UnifOn                 |