Step | Hyp | Ref
| Expression |
1 | | suplocexpr.ub |
. . . 4
     |
2 | | prop 7465 |
. . . . . . 7
              |
3 | | prmu 7468 |
. . . . . . 7
            
      |
4 | 2, 3 | syl 14 |
. . . . . 6
        |
5 | 4 | ad2antrl 490 |
. . . . 5
 
 
         |
6 | | fo2nd 6153 |
. . . . . . . . . . . . 13
     |
7 | | fofun 5435 |
. . . . . . . . . . . . 13
       |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
 |
9 | | fvelima 5563 |
. . . . . . . . . . . 12
 
     
      |
10 | 8, 9 | mpan 424 |
. . . . . . . . . . 11
    

      |
11 | 10 | adantl 277 |
. . . . . . . . . 10
                    
      |
12 | | suplocexpr.m |
. . . . . . . . . . . . . . . 16
    |
13 | | suplocexpr.loc |
. . . . . . . . . . . . . . . 16
     

    |
14 | 12, 1, 13 | suplocexprlemss 7705 |
. . . . . . . . . . . . . . 15

  |
15 | 14 | ad5antr 496 |
. . . . . . . . . . . . . 14
     
 
                      |
16 | | simprl 529 |
. . . . . . . . . . . . . 14
     
 
                      |
17 | 15, 16 | sseldd 3156 |
. . . . . . . . . . . . 13
     
 
                      |
18 | | simprl 529 |
. . . . . . . . . . . . . 14
 
 
    |
19 | 18 | ad4antr 494 |
. . . . . . . . . . . . 13
     
 
                      |
20 | | breq1 4003 |
. . . . . . . . . . . . . . 15
 
   |
21 | | simprr 531 |
. . . . . . . . . . . . . . . 16
 
 
  
  |
22 | 21 | ad4antr 494 |
. . . . . . . . . . . . . . 15
     
 
                       |
23 | 20, 22, 16 | rspcdva 2846 |
. . . . . . . . . . . . . 14
     
 
                      |
24 | | ltsopr 7586 |
. . . . . . . . . . . . . . . . 17
 |
25 | | so2nr 4318 |
. . . . . . . . . . . . . . . . 17
 
 
    |
26 | 24, 25 | mpan 424 |
. . . . . . . . . . . . . . . 16
 
     |
27 | 17, 19, 26 | syl2anc 411 |
. . . . . . . . . . . . . . 15
     
 
                   
    |
28 | | imnan 690 |
. . . . . . . . . . . . . . 15
 
 
   |
29 | 27, 28 | sylibr 134 |
. . . . . . . . . . . . . 14
     
 
                    
   |
30 | 23, 29 | mpd 13 |
. . . . . . . . . . . . 13
     
 
                   
  |
31 | | aptiprlemu 7630 |
. . . . . . . . . . . . 13
 
    
      |
32 | 17, 19, 30, 31 | syl3anc 1238 |
. . . . . . . . . . . 12
     
 
                       
      |
33 | | simpllr 534 |
. . . . . . . . . . . 12
     
 
                          |
34 | 32, 33 | sseldd 3156 |
. . . . . . . . . . 11
     
 
                          |
35 | | simprr 531 |
. . . . . . . . . . 11
     
 
                          |
36 | 34, 35 | eleqtrd 2256 |
. . . . . . . . . 10
     
 
                      |
37 | 11, 36 | rexlimddv 2599 |
. . . . . . . . 9
                      |
38 | 37 | ralrimiva 2550 |
. . . . . . . 8
    
        
        |
39 | | vex 2740 |
. . . . . . . . 9
 |
40 | 39 | elint2 3849 |
. . . . . . . 8
              |
41 | 38, 40 | sylibr 134 |
. . . . . . 7
    
        
       |
42 | 41 | ex 115 |
. . . . . 6
      
              |
43 | 42 | reximdva 2579 |
. . . . 5
 
 
   
             |
44 | 5, 43 | mpd 13 |
. . . 4
 
 
          |
45 | 1, 44 | rexlimddv 2599 |
. . 3
 
       |
46 | | simprr 531 |
. . . . . . 7
 
               |
47 | | simprl 529 |
. . . . . . . . 9
 
          |
48 | | 1nq 7356 |
. . . . . . . . 9
 |
49 | | addclnq 7365 |
. . . . . . . . 9
    
  |
50 | 47, 48, 49 | sylancl 413 |
. . . . . . . 8
 
         
  |
51 | | ltaddnq 7397 |
. . . . . . . . 9
       |
52 | 47, 48, 51 | sylancl 413 |
. . . . . . . 8
 
            |
53 | | breq2 4004 |
. . . . . . . . 9
   
     |
54 | 53 | rspcev 2841 |
. . . . . . . 8
   
      |
55 | 50, 52, 54 | syl2anc 411 |
. . . . . . 7
 
        
  |
56 | | breq1 4003 |
. . . . . . . . 9
 
   |
57 | 56 | rexbidv 2478 |
. . . . . . . 8
  
    |
58 | 57 | rspcev 2841 |
. . . . . . 7
                   |
59 | 46, 55, 58 | syl2anc 411 |
. . . . . 6
 
        
         |
60 | | rexcom 2641 |
. . . . . 6
                   |
61 | 59, 60 | sylib 122 |
. . . . 5
 
        
         |
62 | | ssid 3175 |
. . . . . 6
 |
63 | | rexss 3222 |
. . . . . 6

 
                    |
64 | 62, 63 | ax-mp 5 |
. . . . 5
  
      
       
   |
65 | 61, 64 | sylib 122 |
. . . 4
 
        
       
   |
66 | | suplocexpr.b |
. . . . . . . . . 10
                  |
67 | 66 | suplocexprlem2b 7704 |
. . . . . . . . 9

     
         |
68 | 14, 67 | syl 14 |
. . . . . . . 8
                |
69 | 68 | eleq2d 2247 |
. . . . . . 7
                  |
70 | | breq2 4004 |
. . . . . . . . 9
 
   |
71 | 70 | rexbidv 2478 |
. . . . . . . 8
  
     
      
   |
72 | 71 | elrab 2893 |
. . . . . . 7
                 
   |
73 | 69, 72 | bitrdi 196 |
. . . . . 6
             
    |
74 | 73 | rexbidv 2478 |
. . . . 5
       
       
    |
75 | 74 | adantr 276 |
. . . 4
 
              
       
    |
76 | 65, 75 | mpbird 167 |
. . 3
 
        
      |
77 | 45, 76 | rexlimddv 2599 |
. 2
 
      |
78 | | eleq1w 2238 |
. . 3
     
       |
79 | 78 | cbvrexv 2704 |
. 2
      
      |
80 | 77, 79 | sylib 122 |
1
 
      |