Step | Hyp | Ref
| Expression |
1 | | suplocsrlem.ss |
. . . . . . . 8

  |
2 | | suplocsrlem.c |
. . . . . . . 8
   |
3 | 1, 2 | sseldd 3156 |
. . . . . . 7
   |
4 | | 0idsr 7765 |
. . . . . . 7
     |
5 | 3, 4 | syl 14 |
. . . . . 6
  
  |
6 | 5, 2 | eqeltrd 2254 |
. . . . 5
  
  |
7 | | 1pr 7552 |
. . . . 5
 |
8 | 6, 7 | jctil 312 |
. . . 4
   
   |
9 | | opeq1 3778 |
. . . . . . . . 9
   
     |
10 | 9 | eceq1d 6570 |
. . . . . . . 8
            |
11 | | df-0r 7729 |
. . . . . . . 8
      |
12 | 10, 11 | eqtr4di 2228 |
. . . . . . 7
        |
13 | 12 | oveq2d 5890 |
. . . . . 6
           |
14 | 13 | eleq1d 2246 |
. . . . 5
             |
15 | | suplocsrlem.b |
. . . . 5
         |
16 | 14, 15 | elrab2 2896 |
. . . 4

      |
17 | 8, 16 | sylibr 134 |
. . 3
   |
18 | | elex2 2753 |
. . 3
    |
19 | 17, 18 | syl 14 |
. 2
    |
20 | | suplocsrlem.ub |
. . . 4
     |
21 | | breq1 4006 |
. . . . . . . . . 10
 
   |
22 | 21 | rspccv 2838 |
. . . . . . . . 9
 

   |
23 | 2, 22 | mpan9 281 |
. . . . . . . 8
 


  |
24 | | 0lt1sr 7763 |
. . . . . . . . . . . . . 14
 |
25 | | 0r 7748 |
. . . . . . . . . . . . . . 15
 |
26 | | 1sr 7749 |
. . . . . . . . . . . . . . 15
 |
27 | | m1r 7750 |
. . . . . . . . . . . . . . 15
 |
28 | | ltasrg 7768 |
. . . . . . . . . . . . . . 15
   
 
     |
29 | 25, 26, 27, 28 | mp3an 1337 |
. . . . . . . . . . . . . 14
  
    |
30 | 24, 29 | mpbi 145 |
. . . . . . . . . . . . 13
  
  |
31 | | 0idsr 7765 |
. . . . . . . . . . . . . 14

    |
32 | 27, 31 | ax-mp 5 |
. . . . . . . . . . . . 13
   |
33 | | m1p1sr 7758 |
. . . . . . . . . . . . 13
   |
34 | 30, 32, 33 | 3brtr3i 4032 |
. . . . . . . . . . . 12
 |
35 | | ltasrg 7768 |
. . . . . . . . . . . . 13
   
       |
36 | 27, 25, 3, 35 | mp3an12i 1341 |
. . . . . . . . . . . 12
 
       |
37 | 34, 36 | mpbii 148 |
. . . . . . . . . . 11
       |
38 | 37, 5 | breqtrd 4029 |
. . . . . . . . . 10
     |
39 | | ltsosr 7762 |
. . . . . . . . . . 11
 |
40 | | ltrelsr 7736 |
. . . . . . . . . . 11
   |
41 | 39, 40 | sotri 5024 |
. . . . . . . . . 10
         |
42 | 38, 41 | sylan 283 |
. . . . . . . . 9
 

    |
43 | | map2psrprg 7803 |
. . . . . . . . . . 11
   
          |
44 | 3, 43 | syl 14 |
. . . . . . . . . 10
   
          |
45 | 44 | adantr 276 |
. . . . . . . . 9
 

    
    
   |
46 | 42, 45 | mpbid 147 |
. . . . . . . 8
 

         |
47 | 23, 46 | syldan 282 |
. . . . . . 7
 


         |
48 | | breq1 4006 |
. . . . . . . . . . 11
             
               |
49 | | simpllr 534 |
. . . . . . . . . . . . 13
              
  |
50 | | breq2 4007 |
. . . . . . . . . . . . . . 15
      

     
   |
51 | 50 | ralbidv 2477 |
. . . . . . . . . . . . . 14
      
       

   |
52 | 51 | adantl 277 |
. . . . . . . . . . . . 13
               
     

   |
53 | 49, 52 | mpbird 167 |
. . . . . . . . . . . 12
              
        |
54 | 53 | adantr 276 |
. . . . . . . . . . 11
      
         
        |
55 | 15 | rabeq2i 2734 |
. . . . . . . . . . . . 13

          |
56 | 55 | simprbi 275 |
. . . . . . . . . . . 12
         |
57 | 56 | adantl 277 |
. . . . . . . . . . 11
      
                 |
58 | 48, 54, 57 | rspcdva 2846 |
. . . . . . . . . 10
      
                       |
59 | 58 | ralrimiva 2550 |
. . . . . . . . 9
              
              |
60 | 59 | ex 115 |
. . . . . . . 8
   
          
              |
61 | 60 | reximdva 2579 |
. . . . . . 7
 


 
     
                 |
62 | 47, 61 | mpd 13 |
. . . . . 6
 


                |
63 | 62 | ex 115 |
. . . . 5
                    |
64 | 63 | rexlimdvw 2598 |
. . . 4
                     |
65 | 20, 64 | mpd 13 |
. . 3
                 |
66 | | elrabi 2890 |
. . . . . . . 8
           |
67 | | opeq1 3778 |
. . . . . . . . . . . . 13
   
     |
68 | 67 | eceq1d 6570 |
. . . . . . . . . . . 12
            |
69 | 68 | oveq2d 5890 |
. . . . . . . . . . 11
               |
70 | 69 | eleq1d 2246 |
. . . . . . . . . 10
             
   |
71 | 70 | cbvrabv 2736 |
. . . . . . . . 9
                 |
72 | 15, 71 | eqtri 2198 |
. . . . . . . 8
         |
73 | 66, 72 | eleq2s 2272 |
. . . . . . 7
   |
74 | 73 | adantl 277 |
. . . . . 6
       |
75 | | simplr 528 |
. . . . . 6
       |
76 | 3 | ad2antrr 488 |
. . . . . 6
       |
77 | | ltpsrprg 7801 |
. . . . . 6
 
                 |
78 | 74, 75, 76, 77 | syl3anc 1238 |
. . . . 5
                     |
79 | 78 | ralbidva 2473 |
. . . 4
 

 
           

   |
80 | 79 | rexbidva 2474 |
. . 3
    
          
     |
81 | 65, 80 | mpbid 147 |
. 2
     |
82 | | suplocsrlem.loc |
. . 3
     

    |
83 | 15, 1, 2, 20, 82 | suplocsrlemb 7804 |
. 2
     

    |
84 | 19, 81, 83 | suplocexpr 7723 |
1
   
  
    |