Step | Hyp | Ref
| Expression |
1 | | simprl 529 |
. . . . 5
         
             |
2 | | suplocexprlemell 7703 |
. . . . 5
     

      |
3 | 1, 2 | sylib 122 |
. . . 4
         
      
      |
4 | | simprr 531 |
. . . . . 6
   
             
            |
5 | | simplrr 536 |
. . . . . . . . 9
   
             
            |
6 | | suplocexpr.m |
. . . . . . . . . . . . 13
    |
7 | | suplocexpr.ub |
. . . . . . . . . . . . 13
     |
8 | | suplocexpr.loc |
. . . . . . . . . . . . 13
     

    |
9 | 6, 7, 8 | suplocexprlemss 7705 |
. . . . . . . . . . . 12

  |
10 | 9 | ad3antrrr 492 |
. . . . . . . . . . 11
   
             
        |
11 | | suplocexpr.b |
. . . . . . . . . . . . 13
                  |
12 | 11 | suplocexprlem2b 7704 |
. . . . . . . . . . . 12

     
         |
13 | 12 | eleq2d 2247 |
. . . . . . . . . . 11

      
          |
14 | 10, 13 | syl 14 |
. . . . . . . . . 10
   
             
            
          |
15 | | breq2 4004 |
. . . . . . . . . . . 12
 
   |
16 | 15 | rexbidv 2478 |
. . . . . . . . . . 11
  
     
      
   |
17 | 16 | elrab 2893 |
. . . . . . . . . 10
                 
   |
18 | 14, 17 | bitrdi 196 |
. . . . . . . . 9
   
             
           
           |
19 | 5, 18 | mpbid 147 |
. . . . . . . 8
   
             
      
          |
20 | 19 | simprd 114 |
. . . . . . 7
   
             
            
  |
21 | | simprr 531 |
. . . . . . . 8
                  
           
    |
22 | 10 | adantr 276 |
. . . . . . . . . . 11
                  
           
    |
23 | | simplrl 535 |
. . . . . . . . . . 11
                  
           
    |
24 | 22, 23 | sseldd 3156 |
. . . . . . . . . 10
                  
           
    |
25 | | prop 7465 |
. . . . . . . . . 10
              |
26 | 24, 25 | syl 14 |
. . . . . . . . 9
                  
           
               |
27 | | eleq2 2241 |
. . . . . . . . . 10
    

       |
28 | | simprl 529 |
. . . . . . . . . . 11
                  
           
         |
29 | | vex 2740 |
. . . . . . . . . . . 12
 |
30 | 29 | elint2 3849 |
. . . . . . . . . . 11
              |
31 | 28, 30 | sylib 122 |
. . . . . . . . . 10
                  
           
          |
32 | | fo2nd 6153 |
. . . . . . . . . . . . . 14
     |
33 | | fofun 5435 |
. . . . . . . . . . . . . 14
       |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . 13
 |
35 | | vex 2740 |
. . . . . . . . . . . . . 14
 |
36 | | fof 5434 |
. . . . . . . . . . . . . . . 16
           |
37 | 32, 36 | ax-mp 5 |
. . . . . . . . . . . . . . 15
     |
38 | 37 | fdmi 5369 |
. . . . . . . . . . . . . 14
 |
39 | 35, 38 | eleqtrri 2253 |
. . . . . . . . . . . . 13
 |
40 | | funfvima 5743 |
. . . . . . . . . . . . 13
 
             |
41 | 34, 39, 40 | mp2an 426 |
. . . . . . . . . . . 12
           |
42 | 41 | ad2antrl 490 |
. . . . . . . . . . 11
   
             
                |
43 | 42 | adantr 276 |
. . . . . . . . . 10
                  
           
            |
44 | 27, 31, 43 | rspcdva 2846 |
. . . . . . . . 9
                  
           
        |
45 | | prcunqu 7475 |
. . . . . . . . 9
                          |
46 | 26, 44, 45 | syl2anc 411 |
. . . . . . . 8
                  
           
          |
47 | 21, 46 | mpd 13 |
. . . . . . 7
                  
           
        |
48 | 20, 47 | rexlimddv 2599 |
. . . . . 6
   
             
            |
49 | 4, 48 | jca 306 |
. . . . 5
   
             
          
       |
50 | | simprl 529 |
. . . . . . . 8
   
             
        |
51 | 10, 50 | sseldd 3156 |
. . . . . . 7
   
             
        |
52 | 51, 25 | syl 14 |
. . . . . 6
   
             
                   |
53 | | simpllr 534 |
. . . . . 6
   
             
        |
54 | | prdisj 7482 |
. . . . . 6
                  
       |
55 | 52, 53, 54 | syl2anc 411 |
. . . . 5
   
             
     
    
       |
56 | 49, 55 | pm2.21fal 1373 |
. . . 4
   
             
       |
57 | 3, 56 | rexlimddv 2599 |
. . 3
         
       |
58 | 57 | inegd 1372 |
. 2
 

     
       |
59 | 58 | ralrimiva 2550 |
1
               |