Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . . 5
   
 

  |
2 | | ltbtwnnqq 7416 |
. . . . 5

 
   |
3 | 1, 2 | sylib 122 |
. . . 4
   
 

 
   |
4 | | simplll 533 |
. . . . . . 7
      
        |
5 | | simprl 529 |
. . . . . . . 8
 
     |
6 | 5 | ad2antrr 488 |
. . . . . . 7
      
        |
7 | | simprl 529 |
. . . . . . 7
      
        |
8 | 4, 6, 7 | jca32 310 |
. . . . . 6
      
            |
9 | | simprrl 539 |
. . . . . 6
      
        |
10 | | ltnqpri 7595 |
. . . . . . . . 9

   

   
       |
11 | 10 | adantl 277 |
. . . . . . . 8
   
 

   

   
       |
12 | | breq2 4009 |
. . . . . . . . . 10
  
            
   

   
        |
13 | | breq2 4009 |
. . . . . . . . . . . 12
  
     
          |
14 | 13 | ralbidv 2477 |
. . . . . . . . . . 11
  
      

          |
15 | 14 | orbi2d 790 |
. . . . . . . . . 10
  
         
      
 
      
  
         |
16 | 12, 15 | imbi12d 234 |
. . . . . . . . 9
  
        
        
          
        

   
   

  
            |
17 | | breq1 4008 |
. . . . . . . . . . . 12
  
     
   

     |
18 | | breq1 4008 |
. . . . . . . . . . . . . 14
  
     
   

     |
19 | 18 | rexbidv 2478 |
. . . . . . . . . . . . 13
  
      

   

     |
20 | 19 | orbi1d 791 |
. . . . . . . . . . . 12
  
         
 
      
     |
21 | 17, 20 | imbi12d 234 |
. . . . . . . . . . 11
  
              
        
           |
22 | 21 | ralbidv 2477 |
. . . . . . . . . 10
  
      

     
  
        
           |
23 | | suplocexpr.loc |
. . . . . . . . . . 11
     

    |
24 | 23 | ad2antrr 488 |
. . . . . . . . . 10
   
 

    
     |
25 | | simplrl 535 |
. . . . . . . . . . 11
   
 

  |
26 | | nqprlu 7548 |
. . . . . . . . . . 11
    

    |
27 | 25, 26 | syl 14 |
. . . . . . . . . 10
   
 

   

    |
28 | 22, 24, 27 | rspcdva 2848 |
. . . . . . . . 9
   
 

     

   
      
     |
29 | | simplrr 536 |
. . . . . . . . . 10
   
 

  |
30 | | nqprlu 7548 |
. . . . . . . . . 10
    

    |
31 | 29, 30 | syl 14 |
. . . . . . . . 9
   
 

   

    |
32 | 16, 28, 31 | rspcdva 2848 |
. . . . . . . 8
   
 

       
   

   
   

  
           |
33 | 11, 32 | mpd 13 |
. . . . . . 7
   
 

 
      
  
        |
34 | | simpr 110 |
. . . . . . . . . . . 12
       
        
  
       |
35 | 27 | ad2antrr 488 |
. . . . . . . . . . . . 13
       
        
  
       |
36 | | suplocexpr.m |
. . . . . . . . . . . . . . . 16
    |
37 | | suplocexpr.ub |
. . . . . . . . . . . . . . . 16
     |
38 | 36, 37, 23 | suplocexprlemss 7716 |
. . . . . . . . . . . . . . 15

  |
39 | 38 | ad4antr 494 |
. . . . . . . . . . . . . 14
       
        
   |
40 | | simplr 528 |
. . . . . . . . . . . . . 14
       
        
   |
41 | 39, 40 | sseldd 3158 |
. . . . . . . . . . . . 13
       
        
   |
42 | | ltdfpr 7507 |
. . . . . . . . . . . . 13
        
   
           
     
        |
43 | 35, 41, 42 | syl2anc 411 |
. . . . . . . . . . . 12
       
        
     

 
                     |
44 | 34, 43 | mpbid 147 |
. . . . . . . . . . 11
       
        
  
    
     
       |
45 | | vex 2742 |
. . . . . . . . . . . . . 14
 |
46 | | breq2 4009 |
. . . . . . . . . . . . . 14
 
   |
47 | | ltnqex 7550 |
. . . . . . . . . . . . . . 15
 
 |
48 | | gtnqex 7551 |
. . . . . . . . . . . . . . 15

  |
49 | 47, 48 | op2nd 6150 |
. . . . . . . . . . . . . 14
    
         |
50 | 45, 46, 49 | elab2 2887 |
. . . . . . . . . . . . 13
           
  |
51 | 50 | anbi1i 458 |
. . . . . . . . . . . 12
      
     
     
       |
52 | 51 | rexbii 2484 |
. . . . . . . . . . 11
       
     
     

       |
53 | 44, 52 | sylib 122 |
. . . . . . . . . 10
       
        
  
       |
54 | | simpllr 534 |
. . . . . . . . . . . . . 14
     
   
  
     
 
         |
55 | | simprrl 539 |
. . . . . . . . . . . . . . 15
     
   
  
     
 
         |
56 | 41 | adantr 276 |
. . . . . . . . . . . . . . . . 17
     
   
  
     
 
         |
57 | | prop 7476 |
. . . . . . . . . . . . . . . . 17
              |
58 | 56, 57 | syl 14 |
. . . . . . . . . . . . . . . 16
     
   
  
     
 
                    |
59 | | simprrr 540 |
. . . . . . . . . . . . . . . 16
     
   
  
     
 
             |
60 | | prcdnql 7485 |
. . . . . . . . . . . . . . . 16
                          |
61 | 58, 59, 60 | syl2anc 411 |
. . . . . . . . . . . . . . 15
     
   
  
     
 
               |
62 | 55, 61 | mpd 13 |
. . . . . . . . . . . . . 14
     
   
  
     
 
             |
63 | 54, 62 | jca 306 |
. . . . . . . . . . . . 13
     
   
  
     
 
               |
64 | 63 | 19.8ad 1591 |
. . . . . . . . . . . 12
     
   
  
     
 
                 |
65 | | df-rex 2461 |
. . . . . . . . . . . 12
                |
66 | 64, 65 | sylibr 134 |
. . . . . . . . . . 11
     
   
  
     
 
       
      |
67 | | suplocexprlemell 7714 |
. . . . . . . . . . 11
     

      |
68 | 66, 67 | sylibr 134 |
. . . . . . . . . 10
     
   
  
     
 
              |
69 | 53, 68 | rexlimddv 2599 |
. . . . . . . . 9
       
        
        |
70 | 69 | rexlimdva2 2597 |
. . . . . . . 8
   
 

 
      
        |
71 | | fo2nd 6161 |
. . . . . . . . . . . . . . 15
     |
72 | | fofun 5441 |
. . . . . . . . . . . . . . 15
       |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
 |
74 | | fvelima 5569 |
. . . . . . . . . . . . . 14
 
     
      |
75 | 73, 74 | mpan 424 |
. . . . . . . . . . . . 13
    

      |
76 | 75 | adantl 277 |
. . . . . . . . . . . 12
       
 
             
      |
77 | | breq1 4008 |
. . . . . . . . . . . . . . 15
   
    
          |
78 | | simpllr 534 |
. . . . . . . . . . . . . . 15
     
      
     
            
         |
79 | | simprl 529 |
. . . . . . . . . . . . . . 15
     
      
     
              |
80 | 77, 78, 79 | rspcdva 2848 |
. . . . . . . . . . . . . 14
     
      
     
                     |
81 | 29 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
     
      
     
              |
82 | 38 | ad5antr 496 |
. . . . . . . . . . . . . . . 16
     
      
     
              |
83 | 82, 79 | sseldd 3158 |
. . . . . . . . . . . . . . 15
     
      
     
              |
84 | | nqpru 7553 |
. . . . . . . . . . . . . . 15
 
       
        |
85 | 81, 83, 84 | syl2anc 411 |
. . . . . . . . . . . . . 14
     
      
     
                
          |
86 | 80, 85 | mpbird 167 |
. . . . . . . . . . . . 13
     
      
     
                  |
87 | | simprr 531 |
. . . . . . . . . . . . 13
     
      
     
                  |
88 | 86, 87 | eleqtrd 2256 |
. . . . . . . . . . . 12
     
      
     
              |
89 | 76, 88 | rexlimddv 2599 |
. . . . . . . . . . 11
       
 
               |
90 | 89 | ralrimiva 2550 |
. . . . . . . . . 10
      
 
                |
91 | | vex 2742 |
. . . . . . . . . . 11
 |
92 | 91 | elint2 3853 |
. . . . . . . . . 10
              |
93 | 90, 92 | sylibr 134 |
. . . . . . . . 9
      
 
               |
94 | 93 | ex 115 |
. . . . . . . 8
   
 

 
      
        |
95 | 70, 94 | orim12d 786 |
. . . . . . 7
   
 

  
      
  
                     |
96 | 33, 95 | mpd 13 |
. . . . . 6
   
 

              |
97 | 8, 9, 96 | syl2anc 411 |
. . . . 5
      
                    |
98 | | breq2 4009 |
. . . . . . . . . 10
 
   |
99 | 98 | rexbidv 2478 |
. . . . . . . . 9
  
     
      
   |
100 | | simprr 531 |
. . . . . . . . . 10
 
     |
101 | 100 | ad3antrrr 492 |
. . . . . . . . 9
       
           
  |
102 | | simpr 110 |
. . . . . . . . . 10
       
           
       |
103 | | simprrr 540 |
. . . . . . . . . . 11
      
        |
104 | 103 | adantr 276 |
. . . . . . . . . 10
       
           
  |
105 | | breq1 4008 |
. . . . . . . . . . 11
 
   |
106 | 105 | rspcev 2843 |
. . . . . . . . . 10
        
        |
107 | 102, 104,
106 | syl2anc 411 |
. . . . . . . . 9
       
           
         |
108 | 99, 101, 107 | elrabd 2897 |
. . . . . . . 8
       
           
 
         |
109 | | suplocexpr.b |
. . . . . . . . . . . 12
                  |
110 | 109 | suplocexprlem2b 7715 |
. . . . . . . . . . 11

     
         |
111 | 38, 110 | syl 14 |
. . . . . . . . . 10
                |
112 | 111 | eleq2d 2247 |
. . . . . . . . 9
                  |
113 | 112 | ad4antr 494 |
. . . . . . . 8
       
           
      
          |
114 | 108, 113 | mpbird 167 |
. . . . . . 7
       
           
      |
115 | 114 | ex 115 |
. . . . . 6
      
           
       |
116 | 115 | orim2d 788 |
. . . . 5
      
                                 |
117 | 97, 116 | mpd 13 |
. . . 4
      
                   |
118 | 3, 117 | rexlimddv 2599 |
. . 3
   
 

             |
119 | 118 | ex 115 |
. 2
 
                  |
120 | 119 | ralrimivva 2559 |
1
                  |