Step | Hyp | Ref
| Expression |
1 | | eqid 2412 |
. . . 4
           |
2 | | eqid 2412 |
. . . 4
           |
3 | | eqid 2412 |
. . . 4
 |
4 | 1, 2, 3 | leordtval 17239 |
. . 3
ordTop                    |
5 | 4 | eleq2i 2476 |
. 2
 ordTop                     |
6 | | tg2 16993 |
. . 3
                   

               
   |
7 | | elun 3456 |
. . . . 5
                 
             |
8 | | elun 3456 |
. . . . . . 7
                           |
9 | | vex 2927 |
. . . . . . . . . 10
 |
10 | | eqid 2412 |
. . . . . . . . . . 11

          |
11 | 10 | elrnmpt 5084 |
. . . . . . . . . 10
      
       |
12 | 9, 11 | ax-mp 8 |
. . . . . . . . 9
 
   
      |
13 | | mnfxr 10678 |
. . . . . . . . . . . . . 14
 |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
 
 
       |
15 | | simprl 733 |
. . . . . . . . . . . . . 14
 
 
       |
16 | | 0xr 9095 |
. . . . . . . . . . . . . 14
 |
17 | | ifcl 3743 |
. . . . . . . . . . . . . 14
          |
18 | 15, 16, 17 | sylancl 644 |
. . . . . . . . . . . . 13
 
 
            |
19 | | pnfxr 10677 |
. . . . . . . . . . . . . 14
 |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
 
 
       |
21 | | xrmax1 10727 |
. . . . . . . . . . . . . . 15
          |
22 | 16, 15, 21 | sylancr 645 |
. . . . . . . . . . . . . 14
 
 
    
 
     |
23 | | ge0gtmnf 10724 |
. . . . . . . . . . . . . 14
      
 
   
       |
24 | 18, 22, 23 | syl2anc 643 |
. . . . . . . . . . . . 13
 
 
            |
25 | | simpll 731 |
. . . . . . . . . . . . . . . . 17
 
 
       |
26 | | simprr 734 |
. . . . . . . . . . . . . . . . 17
 
 
    
     |
27 | 25, 26 | eleqtrd 2488 |
. . . . . . . . . . . . . . . 16
 
 
          |
28 | | elioc1 10922 |
. . . . . . . . . . . . . . . . 17
     
    |
29 | 15, 19, 28 | sylancl 644 |
. . . . . . . . . . . . . . . 16
 
 
    
 

    |
30 | 27, 29 | mpbid 202 |
. . . . . . . . . . . . . . 15
 
 
    
   |
31 | 30 | simp2d 970 |
. . . . . . . . . . . . . 14
 
 
    
  |
32 | | 0re 9055 |
. . . . . . . . . . . . . . 15
 |
33 | | ltpnf 10685 |
. . . . . . . . . . . . . . 15
   |
34 | 32, 33 | ax-mp 8 |
. . . . . . . . . . . . . 14
 |
35 | | breq1 4183 |
. . . . . . . . . . . . . . 15
               |
36 | | breq1 4183 |
. . . . . . . . . . . . . . 15
               |
37 | 35, 36 | ifboth 3738 |
. . . . . . . . . . . . . 14
          |
38 | 31, 34, 37 | sylancl 644 |
. . . . . . . . . . . . 13
 
 
            |
39 | | xrre2 10722 |
. . . . . . . . . . . . 13
      

 
                 |
40 | 14, 18, 20, 24, 38, 39 | syl32anc 1192 |
. . . . . . . . . . . 12
 
 
            |
41 | | xrmax2 10728 |
. . . . . . . . . . . . . . 15
          |
42 | 16, 15, 41 | sylancr 645 |
. . . . . . . . . . . . . 14
 
 
    
 
     |
43 | | df-ioc 10885 |
. . . . . . . . . . . . . . 15
  

    |
44 | | xrlelttr 10710 |
. . . . . . . . . . . . . . 15
                
   
   |
45 | 43, 43, 44 | ixxss1 10898 |
. . . . . . . . . . . . . 14
                 
   |
46 | 15, 42, 45 | syl2anc 643 |
. . . . . . . . . . . . 13
 
 
              
   |
47 | | simplr 732 |
. . . . . . . . . . . . . 14
 
 
       |
48 | 26, 47 | eqsstr3d 3351 |
. . . . . . . . . . . . 13
 
 
          |
49 | 46, 48 | sstrd 3326 |
. . . . . . . . . . . 12
 
 
               |
50 | | oveq1 6055 |
. . . . . . . . . . . . . 14
        
          |
51 | 50 | sseq1d 3343 |
. . . . . . . . . . . . 13
                     |
52 | 51 | rspcev 3020 |
. . . . . . . . . . . 12
               
      |
53 | 40, 49, 52 | syl2anc 643 |
. . . . . . . . . . 11
 
 
     
     |
54 | 53 | rexlimdvaa 2799 |
. . . . . . . . . 10

             |
55 | 54 | com12 29 |
. . . . . . . . 9
     
        |
56 | 12, 55 | sylbi 188 |
. . . . . . . 8
 
     
       |
57 | | eqid 2412 |
. . . . . . . . . . 11

          |
58 | 57 | elrnmpt 5084 |
. . . . . . . . . 10
      
       |
59 | 9, 58 | ax-mp 8 |
. . . . . . . . 9
 
   
      |
60 | | pnfnlt 10689 |
. . . . . . . . . . . . . 14

  |
61 | | elico1 10923 |
. . . . . . . . . . . . . . . 16

   
    |
62 | 13, 61 | mpan 652 |
. . . . . . . . . . . . . . 15

  
    |
63 | | simp3 959 |
. . . . . . . . . . . . . . 15


  |
64 | 62, 63 | syl6bi 220 |
. . . . . . . . . . . . . 14

  
   |
65 | 60, 64 | mtod 170 |
. . . . . . . . . . . . 13

     |
66 | | eleq2 2473 |
. . . . . . . . . . . . . 14
   
      |
67 | 66 | notbid 286 |
. . . . . . . . . . . . 13
    
      |
68 | 65, 67 | syl5ibrcom 214 |
. . . . . . . . . . . 12

       |
69 | 68 | rexlimiv 2792 |
. . . . . . . . . . 11
 
  
  |
70 | 69 | pm2.21d 100 |
. . . . . . . . . 10
 
  
       |
71 | 70 | adantrd 455 |
. . . . . . . . 9
 
  
         |
72 | 59, 71 | sylbi 188 |
. . . . . . . 8
 
     
       |
73 | 56, 72 | jaoi 369 |
. . . . . . 7
             
        |
74 | 8, 73 | sylbi 188 |
. . . . . 6
             
        |
75 | | pnfnre 9091 |
. . . . . . . . . 10
 |
76 | | df-nel 2578 |
. . . . . . . . . 10
  |
77 | 75, 76 | mpbi 200 |
. . . . . . . . 9
 |
78 | | elssuni 4011 |
. . . . . . . . . . 11
    |
79 | | unirnioo 10968 |
. . . . . . . . . . 11
  |
80 | 78, 79 | syl6sseqr 3363 |
. . . . . . . . . 10
   |
81 | 80 | sseld 3315 |
. . . . . . . . 9

   |
82 | 77, 81 | mtoi 171 |
. . . . . . . 8

  |
83 | 82 | pm2.21d 100 |
. . . . . . 7

  
    |
84 | 83 | adantrd 455 |
. . . . . 6
 
        |
85 | 74, 84 | jaoi 369 |
. . . . 5
                
       |
86 | 7, 85 | sylbi 188 |
. . . 4
              
         |
87 | 86 | rexlimiv 2792 |
. . 3
                
       |
88 | 6, 87 | syl 16 |
. 2
                   

      |
89 | 5, 88 | sylanb 459 |
1
  ordTop        |