Step | Hyp | Ref
| Expression |
1 | | elssuni 4241 |
. . . 4
 ordTop  ordTop   |
2 | | letopuni 20272 |
. . . 4
 ordTop
 |
3 | 1, 2 | syl6sseqr 3491 |
. . 3
 ordTop   |
4 | | eqid 2462 |
. . . . . . . . 9
           |
5 | 4 | rexmet 21858 |
. . . . . . . 8
           |
6 | 5 | a1i 11 |
. . . . . . 7
   ordTop    
          |
7 | | letop 20271 |
. . . . . . . . 9
ordTop  |
8 | | reex 9656 |
. . . . . . . . 9
 |
9 | | elrestr 15376 |
. . . . . . . . 9
  ordTop
ordTop   
 ordTop
↾t    |
10 | 7, 8, 9 | mp3an12 1363 |
. . . . . . . 8
 ordTop    ordTop
↾t    |
11 | 10 | ad2antrr 737 |
. . . . . . 7
   ordTop   
  ordTop ↾t    |
12 | | elin 3629 |
. . . . . . . . 9
  

   |
13 | 12 | biimpri 211 |
. . . . . . . 8
 
     |
14 | 13 | adantll 725 |
. . . . . . 7
   ordTop       |
15 | | eqid 2462 |
. . . . . . . . . 10
 ordTop
↾t   ordTop
↾t   |
16 | 15 | xrtgioo 21873 |
. . . . . . . . 9
     ordTop
↾t   |
17 | | eqid 2462 |
. . . . . . . . . 10
    
        
     |
18 | 4, 17 | tgioo 21863 |
. . . . . . . . 9
        
     |
19 | 16, 18 | eqtr3i 2486 |
. . . . . . . 8
 ordTop
↾t      
     |
20 | 19 | mopni2 21557 |
. . . . . . 7
   
        
  ordTop ↾t             
    
    |
21 | 6, 11, 14, 20 | syl3anc 1276 |
. . . . . 6
   ordTop           
    
    |
22 | | xrsxmet.1 |
. . . . . . . . . . . . 13
      |
23 | 22 | xrsxmet 21876 |
. . . . . . . . . . . 12
      |
24 | 23 | a1i 11 |
. . . . . . . . . . 11
    ordTop

         |
25 | | simplr 767 |
. . . . . . . . . . . 12
    ordTop

    |
26 | | ressxr 9710 |
. . . . . . . . . . . . 13
 |
27 | | dfss1 3649 |
. . . . . . . . . . . . 13
     |
28 | 26, 27 | mpbi 213 |
. . . . . . . . . . . 12
   |
29 | 25, 28 | syl6eleqr 2551 |
. . . . . . . . . . 11
    ordTop

  
   |
30 | | rpxr 11338 |
. . . . . . . . . . . 12

  |
31 | 30 | adantl 472 |
. . . . . . . . . . 11
    ordTop

    |
32 | 22 | xrsdsre 21877 |
. . . . . . . . . . . . 13
          |
33 | 32 | eqcomi 2471 |
. . . . . . . . . . . 12
     
    |
34 | 33 | blres 21495 |
. . . . . . . . . . 11
      
 
       
                  |
35 | 24, 29, 31, 34 | syl3anc 1276 |
. . . . . . . . . 10
    ordTop

         
                 |
36 | 22 | xrsblre 21878 |
. . . . . . . . . . . . 13
 
           |
37 | 30, 36 | sylan2 481 |
. . . . . . . . . . . 12
 
           |
38 | 37 | adantll 725 |
. . . . . . . . . . 11
    ordTop

            |
39 | | df-ss 3430 |
. . . . . . . . . . 11
                  
          |
40 | 38, 39 | sylib 201 |
. . . . . . . . . 10
    ordTop

                      |
41 | 35, 40 | eqtrd 2496 |
. . . . . . . . 9
    ordTop

         
               |
42 | 41 | sseq1d 3471 |
. . . . . . . 8
    ordTop

         
     
 
        
    |
43 | | inss1 3664 |
. . . . . . . . 9
   |
44 | | sstr 3452 |
. . . . . . . . 9
            
            |
45 | 43, 44 | mpan2 682 |
. . . . . . . 8
         
           |
46 | 42, 45 | syl6bi 236 |
. . . . . . 7
    ordTop

         
     
             |
47 | 46 | reximdva 2874 |
. . . . . 6
   ordTop    
      
     
              |
48 | 21, 47 | mpd 15 |
. . . . 5
   ordTop              |
49 | | 1rp 11335 |
. . . . . 6
 |
50 | 23 | a1i 11 |
. . . . . . . . 9
   ordTop 
        |
51 | 3 | sselda 3444 |
. . . . . . . . . 10
  ordTop    |
52 | 51 | adantr 471 |
. . . . . . . . 9
   ordTop 
   |
53 | | rpxr 11338 |
. . . . . . . . . 10

  |
54 | 49, 53 | mp1i 13 |
. . . . . . . . 9
   ordTop 
   |
55 | | elbl 21452 |
. . . . . . . . 9
      
         
         |
56 | 50, 52, 54, 55 | syl3anc 1276 |
. . . . . . . 8
   ordTop 
         
         |
57 | | simp2 1015 |
. . . . . . . . . 10
   ordTop 
      
  |
58 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    ordTop
                |
59 | 51 | 3ad2ant1 1035 |
. . . . . . . . . . . . . . . . . 18
   ordTop 
         |
60 | 59 | adantr 471 |
. . . . . . . . . . . . . . . . 17
    ordTop
           |
61 | | simpl3l 1069 |
. . . . . . . . . . . . . . . . 17
    ordTop
           |
62 | | xmetcl 21395 |
. . . . . . . . . . . . . . . . 17
      
       |
63 | 58, 60, 61, 62 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
    ordTop
               |
64 | | 1red 9684 |
. . . . . . . . . . . . . . . 16
    ordTop
           |
65 | | xmetge0 21408 |
. . . . . . . . . . . . . . . . 17
      
       |
66 | 58, 60, 61, 65 | syl3anc 1276 |
. . . . . . . . . . . . . . . 16
    ordTop
               |
67 | | simpl3r 1070 |
. . . . . . . . . . . . . . . . 17
    ordTop
               |
68 | 49, 53 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
 |
69 | | xrltle 11477 |
. . . . . . . . . . . . . . . . . 18
               
   |
70 | 63, 68, 69 | sylancl 673 |
. . . . . . . . . . . . . . . . 17
    ordTop
                 
   |
71 | 67, 70 | mpd 15 |
. . . . . . . . . . . . . . . 16
    ordTop
               |
72 | | xrrege0 11498 |
. . . . . . . . . . . . . . . 16
                         |
73 | 63, 64, 66, 71, 72 | syl22anc 1277 |
. . . . . . . . . . . . . . 15
    ordTop
               |
74 | | simpr 467 |
. . . . . . . . . . . . . . . 16
    ordTop
           |
75 | 22 | xrsdsreclb 19064 |
. . . . . . . . . . . . . . . 16
       
     |
76 | 60, 61, 74, 75 | syl3anc 1276 |
. . . . . . . . . . . . . . 15
    ordTop
             
     |
77 | 73, 76 | mpbid 215 |
. . . . . . . . . . . . . 14
    ordTop
         
   |
78 | 77 | simpld 465 |
. . . . . . . . . . . . 13
    ordTop
           |
79 | 78 | ex 440 |
. . . . . . . . . . . 12
   ordTop 
       
   |
80 | 79 | necon1bd 2654 |
. . . . . . . . . . 11
   ordTop 
       
   |
81 | | simp1r 1039 |
. . . . . . . . . . . 12
   ordTop 
         |
82 | | elequ1 1905 |
. . . . . . . . . . . 12
 
   |
83 | 81, 82 | syl5ibcom 228 |
. . . . . . . . . . 11
   ordTop 
       
   |
84 | 80, 83 | syld 45 |
. . . . . . . . . 10
   ordTop 
       
   |
85 | 57, 84 | mpd 15 |
. . . . . . . . 9
   ordTop 
         |
86 | 85 | 3expia 1217 |
. . . . . . . 8
   ordTop 
  
        |
87 | 56, 86 | sylbid 223 |
. . . . . . 7
   ordTop 
             |
88 | 87 | ssrdv 3450 |
. . . . . 6
   ordTop 
           |
89 | | oveq2 6323 |
. . . . . . . 8
                   |
90 | 89 | sseq1d 3471 |
. . . . . . 7
         
           |
91 | 90 | rspcev 3162 |
. . . . . 6
                      |
92 | 49, 88, 91 | sylancr 674 |
. . . . 5
   ordTop 
            |
93 | 48, 92 | pm2.61dan 805 |
. . . 4
  ordTop             |
94 | 93 | ralrimiva 2814 |
. . 3
 ordTop  
          |
95 | | xrsmopn.1 |
. . . . 5
     |
96 | 95 | elmopn2 21509 |
. . . 4
      


             |
97 | 23, 96 | ax-mp 5 |
. . 3



            |
98 | 3, 94, 97 | sylanbrc 675 |
. 2
 ordTop   |
99 | 98 | ssriv 3448 |
1
ordTop
 |