Step | Hyp | Ref
| Expression |
1 | | remet.1 |
. . . 4
 
    |
2 | 1 | rexmet 21809 |
. . 3
      |
3 | | tgioo.2 |
. . . 4
     |
4 | 3 | mopnval 21453 |
. . 3
                |
5 | 2, 4 | ax-mp 5 |
. 2
         |
6 | 1 | blssioo 21813 |
. . 3
     |
7 | | elssuni 4227 |
. . . . . . 7
    |
8 | | unirnioo 11734 |
. . . . . . 7
  |
9 | 7, 8 | syl6sseqr 3479 |
. . . . . 6
   |
10 | | retopbas 21781 |
. . . . . . . . . 10
 |
11 | 10 | a1i 11 |
. . . . . . . . 9
  
  |
12 | | simpl 459 |
. . . . . . . . 9
     |
13 | 9 | sselda 3432 |
. . . . . . . . . 10
     |
14 | | 1re 9642 |
. . . . . . . . . . . 12
 |
15 | 1 | bl2ioo 21810 |
. . . . . . . . . . . 12
 
                   |
16 | 14, 15 | mpan2 677 |
. . . . . . . . . . 11
                   |
17 | | peano2rem 9941 |
. . . . . . . . . . . . 13
     |
18 | 17 | rexrd 9690 |
. . . . . . . . . . . 12
     |
19 | | peano2re 9806 |
. . . . . . . . . . . . 13
     |
20 | 19 | rexrd 9690 |
. . . . . . . . . . . 12
     |
21 | | ioof 11732 |
. . . . . . . . . . . . . 14
  
     |
22 | | ffn 5728 |
. . . . . . . . . . . . . 14
        
   |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . . 13
   |
24 | | fnovrn 6444 |
. . . . . . . . . . . . 13
     
             |
25 | 23, 24 | mp3an1 1351 |
. . . . . . . . . . . 12
                 |
26 | 18, 20, 25 | syl2anc 667 |
. . . . . . . . . . 11
           |
27 | 16, 26 | eqeltrd 2529 |
. . . . . . . . . 10
           |
28 | 13, 27 | syl 17 |
. . . . . . . . 9
             |
29 | | simpr 463 |
. . . . . . . . . 10
     |
30 | | 1rp 11306 |
. . . . . . . . . . . 12
 |
31 | | blcntr 21428 |
. . . . . . . . . . . 12
                  |
32 | 2, 30, 31 | mp3an13 1355 |
. . . . . . . . . . 11
           |
33 | 13, 32 | syl 17 |
. . . . . . . . . 10
             |
34 | 29, 33 | elind 3618 |
. . . . . . . . 9
               |
35 | | basis2 19966 |
. . . . . . . . 9
                                         |
36 | 11, 12, 28, 34, 35 | syl22anc 1269 |
. . . . . . . 8
      
            |
37 | | ovelrn 6445 |
. . . . . . . . . . 11
             |
38 | 23, 37 | ax-mp 5 |
. . . . . . . . . 10

        |
39 | | eleq2 2518 |
. . . . . . . . . . . . . . 15
     
       |
40 | | sseq1 3453 |
. . . . . . . . . . . . . . 15
     
              
            |
41 | 39, 40 | anbi12d 717 |
. . . . . . . . . . . . . 14
       
                   
             |
42 | | inss2 3653 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
43 | | sstr 3440 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                            
              |
44 | 42, 43 | mpan2 677 |
. . . . . . . . . . . . . . . . . . . . 21
              
              |
45 | 44 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
         
                         |
46 | | elioore 11666 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
47 | 46 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
         
             |
48 | 47, 16 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         
                             |
49 | 45, 48 | sseqtrd 3468 |
. . . . . . . . . . . . . . . . . . 19
         
                         |
50 | | dfss 3419 |
. . . . . . . . . . . . . . . . . . 19
            
        
           |
51 | 49, 50 | sylib 200 |
. . . . . . . . . . . . . . . . . 18
         
                               |
52 | | eliooxr 11693 |
. . . . . . . . . . . . . . . . . . . 20
         |
53 | 18, 20 | jca 535 |
. . . . . . . . . . . . . . . . . . . . 21
         |
54 | 46, 53 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
             |
55 | | iooin 11670 |
. . . . . . . . . . . . . . . . . . . 20
          
                                      |
56 | 52, 54, 55 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
         
           
                     |
57 | 56 | adantr 467 |
. . . . . . . . . . . . . . . . . 18
         
               
           
                     |
58 | 51, 57 | eqtrd 2485 |
. . . . . . . . . . . . . . . . 17
         
                 
                     |
59 | | mnfxr 11414 |
. . . . . . . . . . . . . . . . . . . 20
 |
60 | 59 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
         
             |
61 | 47, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         
               |
62 | 52 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
         
               |
63 | 62 | simpld 461 |
. . . . . . . . . . . . . . . . . . . 20
         
             |
64 | 61, 63 | ifcld 3924 |
. . . . . . . . . . . . . . . . . . 19
         
                      |
65 | 62 | simprd 465 |
. . . . . . . . . . . . . . . . . . . 20
         
             |
66 | 47, 19 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
         
               |
67 | 66 | rexrd 9690 |
. . . . . . . . . . . . . . . . . . . 20
         
               |
68 | 65, 67 | ifcld 3924 |
. . . . . . . . . . . . . . . . . . 19
         
                      |
69 | 46, 17 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
70 | 69 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . 21
         
               |
71 | | mnflt 11425 |
. . . . . . . . . . . . . . . . . . . . 21
       |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         
               |
73 | | xrmax2 11471 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
74 | 63, 61, 73 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . 20
         
                        |
75 | 60, 61, 64, 72, 74 | xrltletrd 11458 |
. . . . . . . . . . . . . . . . . . 19
         
                      |
76 | | simpl 459 |
. . . . . . . . . . . . . . . . . . . . 21
         
                 |
77 | 76, 58 | eleqtrd 2531 |
. . . . . . . . . . . . . . . . . . . 20
         
                                   |
78 | | eliooxr 11693 |
. . . . . . . . . . . . . . . . . . . . 21
   
                     
      
 
          |
79 | | ne0i 3737 |
. . . . . . . . . . . . . . . . . . . . . 22
   
                     
                     |
80 | | ioon0 11662 |
. . . . . . . . . . . . . . . . . . . . . 22
                                   
       
 
                   |
81 | 79, 80 | syl5ib 223 |
. . . . . . . . . . . . . . . . . . . . 21
                                                      
          |
82 | 78, 81 | mpcom 37 |
. . . . . . . . . . . . . . . . . . . 20
   
                                       |
83 | 77, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
         
                     
         |
84 | | xrre2 11465 |
. . . . . . . . . . . . . . . . . . 19
                               
                 
 
         |
85 | 60, 64, 68, 75, 83, 84 | syl32anc 1276 |
. . . . . . . . . . . . . . . . . 18
         
                      |
86 | | mnfle 11435 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
87 | 64, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         
                      |
88 | 60, 64, 68, 87, 83 | xrlelttrd 11457 |
. . . . . . . . . . . . . . . . . . 19
         
                      |
89 | | xrmin2 11473 |
. . . . . . . . . . . . . . . . . . . 20
             
    |
90 | 65, 67, 89 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . 19
         
                   
    |
91 | | xrre 11464 |
. . . . . . . . . . . . . . . . . . 19
           
                    
   
 
         |
92 | 68, 66, 88, 90, 91 | syl22anc 1269 |
. . . . . . . . . . . . . . . . . 18
         
                      |
93 | 1 | ioo2blex 21812 |
. . . . . . . . . . . . . . . . . 18
                       
                         |
94 | 85, 92, 93 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17
         
                        
              |
95 | 58, 94 | eqeltrd 2529 |
. . . . . . . . . . . . . . . 16
         
                     |
96 | | inss1 3652 |
. . . . . . . . . . . . . . . . . 18
           |
97 | | sstr 3440 |
. . . . . . . . . . . . . . . . . 18
     
                           |
98 | 96, 97 | mpan2 677 |
. . . . . . . . . . . . . . . . 17
              
      |
99 | 98 | adantl 468 |
. . . . . . . . . . . . . . . 16
         
                 |
100 | | sseq1 3453 |
. . . . . . . . . . . . . . . . . 18
     
       |
101 | 39, 100 | anbi12d 717 |
. . . . . . . . . . . . . . . . 17
            
        |
102 | 101 | rspcev 3150 |
. . . . . . . . . . . . . . . 16
          
                    |
103 | 95, 76, 99, 102 | syl12anc 1266 |
. . . . . . . . . . . . . . 15
         
                     |
104 | | blssex 21442 |
. . . . . . . . . . . . . . . 16
                
            |
105 | 2, 47, 104 | sylancr 669 |
. . . . . . . . . . . . . . 15
         
            
                   |
106 | 103, 105 | mpbid 214 |
. . . . . . . . . . . . . 14
         
                      |
107 | 41, 106 | syl6bi 232 |
. . . . . . . . . . . . 13
       
                      |
108 | 107 | a1i 11 |
. . . . . . . . . . . 12
                    
             |
109 | 108 | rexlimivv 2884 |
. . . . . . . . . . 11
                   
            |
110 | 109 | imp 431 |
. . . . . . . . . 10
                     
          |
111 | 38, 110 | sylanb 475 |
. . . . . . . . 9
   
          
           |
112 | 111 | rexlimiva 2875 |
. . . . . . . 8
   
                      |
113 | 36, 112 | syl 17 |
. . . . . . 7
              |
114 | 113 | ralrimiva 2802 |
. . . . . 6
  
          |
115 | 3 | elmopn2 21460 |
. . . . . . 7
      
 
             |
116 | 2, 115 | ax-mp 5 |
. . . . . 6

 
            |
117 | 9, 114, 116 | sylanbrc 670 |
. . . . 5
   |
118 | 117 | ssriv 3436 |
. . . 4
 |
119 | 118, 5 | sseqtri 3464 |
. . 3
         |
120 | | 2basgen 20006 |
. . 3
     
                       |
121 | 6, 119, 120 | mp2an 678 |
. 2
             |
122 | 5, 121 | eqtr2i 2474 |
1
     |