Step | Hyp | Ref
| Expression |
1 | | remet.1 |
. . . 4
 
    |
2 | 1 | rexmet 13708 |
. . 3
      |
3 | | tgioo.2 |
. . . 4
     |
4 | 3 | mopnval 13609 |
. . 3
                |
5 | 2, 4 | ax-mp 5 |
. 2
         |
6 | | blex 13554 |
. . . . 5
            |
7 | 2, 6 | ax-mp 5 |
. . . 4
     |
8 | 7 | rnex 4890 |
. . 3
     |
9 | 1 | blssioo 13712 |
. . 3
     |
10 | | elssuni 3835 |
. . . . . . 7
    |
11 | | unirnioo 9960 |
. . . . . . 7
  |
12 | 10, 11 | sseqtrrdi 3204 |
. . . . . 6
   |
13 | | retopbas 13690 |
. . . . . . . . . 10
 |
14 | 13 | a1i 9 |
. . . . . . . . 9
  
  |
15 | | simpl 109 |
. . . . . . . . 9
     |
16 | 12 | sselda 3155 |
. . . . . . . . . 10
     |
17 | | 1re 7947 |
. . . . . . . . . . . 12
 |
18 | 1 | bl2ioo 13709 |
. . . . . . . . . . . 12
 
                   |
19 | 17, 18 | mpan2 425 |
. . . . . . . . . . 11
                   |
20 | | peano2rem 8214 |
. . . . . . . . . . . . 13
     |
21 | 20 | rexrd 7997 |
. . . . . . . . . . . 12
     |
22 | | peano2re 8083 |
. . . . . . . . . . . . 13
     |
23 | 22 | rexrd 7997 |
. . . . . . . . . . . 12
     |
24 | | ioorebasg 9962 |
. . . . . . . . . . . 12
                 |
25 | 21, 23, 24 | syl2anc 411 |
. . . . . . . . . . 11
           |
26 | 19, 25 | eqeltrd 2254 |
. . . . . . . . . 10
           |
27 | 16, 26 | syl 14 |
. . . . . . . . 9
             |
28 | | simpr 110 |
. . . . . . . . . 10
     |
29 | | 1rp 9644 |
. . . . . . . . . . . 12
 |
30 | | blcntr 13583 |
. . . . . . . . . . . 12
                  |
31 | 2, 29, 30 | mp3an13 1328 |
. . . . . . . . . . 11
           |
32 | 16, 31 | syl 14 |
. . . . . . . . . 10
             |
33 | 28, 32 | elind 3320 |
. . . . . . . . 9
               |
34 | | basis2 13213 |
. . . . . . . . 9
                                         |
35 | 14, 15, 27, 33, 34 | syl22anc 1239 |
. . . . . . . 8
      
            |
36 | | ioof 9958 |
. . . . . . . . . . 11
  
     |
37 | | ffn 5361 |
. . . . . . . . . . 11
        
   |
38 | | ovelrn 6017 |
. . . . . . . . . . 11
             |
39 | 36, 37, 38 | mp2b 8 |
. . . . . . . . . 10

        |
40 | | eleq2 2241 |
. . . . . . . . . . . . . . 15
     
       |
41 | | sseq1 3178 |
. . . . . . . . . . . . . . 15
     
              
            |
42 | 40, 41 | anbi12d 473 |
. . . . . . . . . . . . . 14
       
                   
             |
43 | | inss2 3356 |
. . . . . . . . . . . . . . . . . . . . . 22
                   |
44 | | sstr 3163 |
. . . . . . . . . . . . . . . . . . . . . 22
     
                            
              |
45 | 43, 44 | mpan2 425 |
. . . . . . . . . . . . . . . . . . . . 21
              
              |
46 | 45 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
         
                         |
47 | | elioore 9899 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
48 | 47 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
         
             |
49 | 48, 19 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
         
                             |
50 | 46, 49 | sseqtrd 3193 |
. . . . . . . . . . . . . . . . . . 19
         
                         |
51 | | dfss 3143 |
. . . . . . . . . . . . . . . . . . 19
            
        
           |
52 | 50, 51 | sylib 122 |
. . . . . . . . . . . . . . . . . 18
         
                               |
53 | | eliooxr 9914 |
. . . . . . . . . . . . . . . . . . . 20
         |
54 | 21, 23 | jca 306 |
. . . . . . . . . . . . . . . . . . . . 21
         |
55 | 47, 54 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
             |
56 | | iooinsup 11269 |
. . . . . . . . . . . . . . . . . . . 20
          
                         inf           |
57 | 53, 55, 56 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
         
                    inf           |
58 | 57 | adantr 276 |
. . . . . . . . . . . . . . . . . 18
         
               
                    inf           |
59 | 52, 58 | eqtrd 2210 |
. . . . . . . . . . . . . . . . 17
         
                          inf           |
60 | | mnfxr 8004 |
. . . . . . . . . . . . . . . . . . . 20
 |
61 | 60 | a1i 9 |
. . . . . . . . . . . . . . . . . . 19
         
             |
62 | 53 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
         
               |
63 | 62 | simpld 112 |
. . . . . . . . . . . . . . . . . . . 20
         
             |
64 | 48, 21 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
         
               |
65 | | xrmaxcl 11244 |
. . . . . . . . . . . . . . . . . . . 20
                |
66 | 63, 64, 65 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
         
                      |
67 | 62 | simprd 114 |
. . . . . . . . . . . . . . . . . . . 20
         
             |
68 | 48, 22 | syl 14 |
. . . . . . . . . . . . . . . . . . . . 21
         
               |
69 | 68 | rexrd 7997 |
. . . . . . . . . . . . . . . . . . . 20
         
               |
70 | | xrmincl 11258 |
. . . . . . . . . . . . . . . . . . . 20
     inf          |
71 | 67, 69, 70 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
         
           inf          |
72 | 47, 20 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
73 | 72 | adantr 276 |
. . . . . . . . . . . . . . . . . . . . 21
         
               |
74 | | mnflt 9770 |
. . . . . . . . . . . . . . . . . . . . 21
       |
75 | 73, 74 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
         
               |
76 | | xrmax2sup 11246 |
. . . . . . . . . . . . . . . . . . . . 21
                  |
77 | 63, 64, 76 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . . 20
         
                        |
78 | 61, 64, 66, 75, 77 | xrltletrd 9798 |
. . . . . . . . . . . . . . . . . . 19
         
                      |
79 | | simpl 109 |
. . . . . . . . . . . . . . . . . . . . 21
         
                 |
80 | 79, 59 | eleqtrd 2256 |
. . . . . . . . . . . . . . . . . . . 20
         
                      inf           |
81 | | eliooxr 9914 |
. . . . . . . . . . . . . . . . . . . . 21
            inf                  
inf           |
82 | | elex2 2753 |
. . . . . . . . . . . . . . . . . . . . . 22
            inf                     inf           |
83 | | ioom 10247 |
. . . . . . . . . . . . . . . . . . . . . 22
          
inf          
           inf        
         inf           |
84 | 82, 83 | imbitrid 154 |
. . . . . . . . . . . . . . . . . . . . 21
          
inf                     inf        
         inf           |
85 | 81, 84 | mpcom 36 |
. . . . . . . . . . . . . . . . . . . 20
            inf                  inf          |
86 | 80, 85 | syl 14 |
. . . . . . . . . . . . . . . . . . 19
         
                    inf          |
87 | | xrre2 9808 |
. . . . . . . . . . . . . . . . . . 19
          
inf                           inf                     |
88 | 61, 66, 71, 78, 86, 87 | syl32anc 1246 |
. . . . . . . . . . . . . . . . . 18
         
                      |
89 | | mnfle 9779 |
. . . . . . . . . . . . . . . . . . . . 21
         
           |
90 | 66, 89 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
         
                      |
91 | 61, 66, 71, 90, 86 | xrlelttrd 9797 |
. . . . . . . . . . . . . . . . . . 19
         
           inf          |
92 | | xrmin2inf 11260 |
. . . . . . . . . . . . . . . . . . . 20
     inf            |
93 | 67, 69, 92 | syl2anc 411 |
. . . . . . . . . . . . . . . . . . 19
         
           inf            |
94 | | xrre 9807 |
. . . . . . . . . . . . . . . . . . 19
  inf       
   inf        inf            inf          |
95 | 71, 68, 91, 93, 94 | syl22anc 1239 |
. . . . . . . . . . . . . . . . . 18
         
           inf          |
96 | 1 | ioo2blex 13711 |
. . . . . . . . . . . . . . . . . 18
          
inf                    inf               |
97 | 88, 95, 96 | syl2anc 411 |
. . . . . . . . . . . . . . . . 17
         
                      inf               |
98 | 59, 97 | eqeltrd 2254 |
. . . . . . . . . . . . . . . 16
         
                     |
99 | | inss1 3355 |
. . . . . . . . . . . . . . . . . 18
           |
100 | | sstr 3163 |
. . . . . . . . . . . . . . . . . 18
     
                           |
101 | 99, 100 | mpan2 425 |
. . . . . . . . . . . . . . . . 17
              
      |
102 | 101 | adantl 277 |
. . . . . . . . . . . . . . . 16
         
                 |
103 | | sseq1 3178 |
. . . . . . . . . . . . . . . . . 18
     
       |
104 | 40, 103 | anbi12d 473 |
. . . . . . . . . . . . . . . . 17
            
        |
105 | 104 | rspcev 2841 |
. . . . . . . . . . . . . . . 16
          
                    |
106 | 98, 79, 102, 105 | syl12anc 1236 |
. . . . . . . . . . . . . . 15
         
                     |
107 | | blssex 13597 |
. . . . . . . . . . . . . . . 16
                
            |
108 | 2, 48, 107 | sylancr 414 |
. . . . . . . . . . . . . . 15
         
            
                   |
109 | 106, 108 | mpbid 147 |
. . . . . . . . . . . . . 14
         
                      |
110 | 42, 109 | syl6bi 163 |
. . . . . . . . . . . . 13
       
                      |
111 | 110 | a1i 9 |
. . . . . . . . . . . 12
                    
             |
112 | 111 | rexlimivv 2600 |
. . . . . . . . . . 11
                   
            |
113 | 112 | imp 124 |
. . . . . . . . . 10
                     
          |
114 | 39, 113 | sylanb 284 |
. . . . . . . . 9
   
          
           |
115 | 114 | rexlimiva 2589 |
. . . . . . . 8
   
                      |
116 | 35, 115 | syl 14 |
. . . . . . 7
              |
117 | 116 | ralrimiva 2550 |
. . . . . 6
  
          |
118 | 3 | elmopn2 13616 |
. . . . . . 7
      
 
             |
119 | 2, 118 | ax-mp 5 |
. . . . . 6

 
            |
120 | 12, 117, 119 | sylanbrc 417 |
. . . . 5
   |
121 | 120 | ssriv 3159 |
. . . 4
 |
122 | 121, 5 | sseqtri 3189 |
. . 3
         |
123 | | 2basgeng 13249 |
. . 3
         
                       |
124 | 8, 9, 122, 123 | mp3an 1337 |
. 2
             |
125 | 5, 124 | eqtr2i 2199 |
1
     |