Step | Hyp | Ref
| Expression |
1 | | lmxrge0.j |
. . . . . . 7
     ↾s       |
2 | | eqid 2462 |
. . . . . . . 8
  ↾s      
↾s      |
3 | | xrstopn 20273 |
. . . . . . . 8
ordTop       |
4 | 2, 3 | resstopn 20251 |
. . . . . . 7
 ordTop
↾t          ↾s  
    |
5 | 1, 4 | eqtr4i 2487 |
. . . . . 6
 ordTop ↾t      |
6 | | letopon 20270 |
. . . . . . 7
ordTop TopOn   |
7 | | iccssxr 11746 |
. . . . . . 7
    |
8 | | resttopon 20226 |
. . . . . . 7
  ordTop
TopOn       ordTop ↾t     TopOn  
    |
9 | 6, 7, 8 | mp2an 683 |
. . . . . 6
 ordTop
↾t     TopOn      |
10 | 5, 9 | eqeltri 2536 |
. . . . 5
TopOn      |
11 | 10 | a1i 11 |
. . . 4
 TopOn       |
12 | | nnuz 11223 |
. . . 4
     |
13 | | 1zzd 10997 |
. . . 4
   |
14 | | lmxrge0.6 |
. . . 4
          |
15 | | lmxrge0.7 |
. . . 4
 

      |
16 | 11, 12, 13, 14, 15 | lmbrf 20325 |
. . 3
       
                |
17 | | 0xr 9713 |
. . . . 5
 |
18 | | pnfxr 11441 |
. . . . 5
 |
19 | | 0lepnf 11462 |
. . . . 5
 |
20 | | ubicc2 11778 |
. . . . 5
  
     |
21 | 17, 18, 19, 20 | mp3an 1373 |
. . . 4
    |
22 | 21 | biantrur 513 |
. . 3
 
      
     
          |
23 | 16, 22 | syl6bbr 271 |
. 2
       

      
    |
24 | | rexr 9712 |
. . . . . . . . . 10
   |
25 | 18 | a1i 11 |
. . . . . . . . . 10
   |
26 | | ltpnf 11451 |
. . . . . . . . . 10
   |
27 | | ubioc1 11717 |
. . . . . . . . . 10
  
     |
28 | 24, 25, 26, 27 | syl3anc 1276 |
. . . . . . . . 9
      |
29 | | 0ltpnf 11453 |
. . . . . . . . . 10
 |
30 | | ubioc1 11717 |
. . . . . . . . . 10
  
     |
31 | 17, 18, 29, 30 | mp3an 1373 |
. . . . . . . . 9
    |
32 | 28, 31 | jctir 545 |
. . . . . . . 8
   
      |
33 | | elin 3629 |
. . . . . . . 8
   
 
           |
34 | 32, 33 | sylibr 217 |
. . . . . . 7
    
 
    |
35 | 34 | ad2antlr 738 |
. . . . . 6
    
      
 
          |
36 | | letop 20271 |
. . . . . . . . . . 11
ordTop  |
37 | | ovex 6343 |
. . . . . . . . . . 11
    |
38 | | iocpnfordt 20280 |
. . . . . . . . . . . 12
   ordTop
 |
39 | | iocpnfordt 20280 |
. . . . . . . . . . . 12
   ordTop
 |
40 | | inopn 19978 |
. . . . . . . . . . . 12
  ordTop
   ordTop  
 ordTop
         ordTop   |
41 | 36, 38, 39, 40 | mp3an 1373 |
. . . . . . . . . . 11
        ordTop  |
42 | | elrestr 15376 |
. . . . . . . . . . 11
  ordTop
  
  
     ordTop            
   ordTop
↾t       |
43 | 36, 37, 41, 42 | mp3an 1373 |
. . . . . . . . . 10
          
   ordTop
↾t      |
44 | | inss2 3665 |
. . . . . . . . . . . . 13
         
  |
45 | | iocssicc 11751 |
. . . . . . . . . . . . 13
       |
46 | 44, 45 | sstri 3453 |
. . . . . . . . . . . 12
         
  |
47 | | sseqin2 3663 |
. . . . . . . . . . . 12
          
                 
 
    |
48 | 46, 47 | mpbi 213 |
. . . . . . . . . . 11
       
 
            |
49 | | incom 3637 |
. . . . . . . . . . 11
       
 
       
 
 
     |
50 | 48, 49 | eqtr3i 2486 |
. . . . . . . . . 10
            
 
 
     |
51 | 43, 50, 5 | 3eltr4i 2553 |
. . . . . . . . 9
         |
52 | 51 | a1i 11 |
. . . . . . . 8
 

          |
53 | | eleq2 2529 |
. . . . . . . . . . 11
        
           |
54 | 53 | adantl 472 |
. . . . . . . . . 10
            
           |
55 | 54 | biimprd 231 |
. . . . . . . . 9
            
           |
56 | | simp-5r 784 |
. . . . . . . . . . . . . . 15
     

        

     
  |
57 | 56 | rexrd 9716 |
. . . . . . . . . . . . . 14
     

        

     
  |
58 | | simpr 467 |
. . . . . . . . . . . . . . . 16
     

        

     
  |
59 | | simp-4r 782 |
. . . . . . . . . . . . . . . 16
     

        

     
   
 
    |
60 | 58, 59 | eleqtrd 2542 |
. . . . . . . . . . . . . . 15
     

        

     
   
 
    |
61 | | elin 3629 |
. . . . . . . . . . . . . . . 16
        
          |
62 | 61 | simplbi 466 |
. . . . . . . . . . . . . . 15
              |
63 | 60, 62 | syl 17 |
. . . . . . . . . . . . . 14
     

        

     
     |
64 | | elioc1 11707 |
. . . . . . . . . . . . . . . . 17
   
  

    |
65 | 18, 64 | mpan2 682 |
. . . . . . . . . . . . . . . 16

   

    |
66 | 65 | biimpa 491 |
. . . . . . . . . . . . . . 15
      
   |
67 | 66 | simp2d 1027 |
. . . . . . . . . . . . . 14
        |
68 | 57, 63, 67 | syl2anc 671 |
. . . . . . . . . . . . 13
     

        

     
  |
69 | 68 | ex 440 |
. . . . . . . . . . . 12
              

     
   |
70 | 69 | ralimdva 2808 |
. . . . . . . . . . 11
   

        
       
         |
71 | 70 | reximdva 2874 |
. . . . . . . . . 10
                    
 
        |
72 | | fveq2 5888 |
. . . . . . . . . . . 12
           |
73 | 72 | raleqdv 3005 |
. . . . . . . . . . 11
  
    
     
   |
74 | 73 | cbvrexv 3032 |
. . . . . . . . . 10
  
              |
75 | 71, 74 | syl6ibr 235 |
. . . . . . . . 9
                    
 
        |
76 | 55, 75 | imim12d 77 |
. . . . . . . 8
                                    
    |
77 | 52, 76 | rspcimdv 3163 |
. . . . . . 7
 

 
      
               
    |
78 | 77 | imp 435 |
. . . . . 6
    
      
 
   
 
 
      
   |
79 | 35, 78 | mpd 15 |
. . . . 5
    
      
 
      
  |
80 | 79 | ex 440 |
. . . 4
 

 
      
           |
81 | 80 | ralrimdva 2818 |
. . 3
                  
   |
82 | | simplll 773 |
. . . . . 6
   
   
         |
83 | | simpllr 774 |
. . . . . . 7
   
   
         |
84 | | simpr 467 |
. . . . . . 7
   
   
         |
85 | 1 | pnfneige0 28806 |
. . . . . . 7
   
     |
86 | 83, 84, 85 | syl2anc 671 |
. . . . . 6
   
   
          
  |
87 | | simplr 767 |
. . . . . 6
   
   
              
  |
88 | | r19.29r 2938 |
. . . . . . . 8
      
      
     
 
        |
89 | | simp-4l 781 |
. . . . . . . . . . . . . . 15
        
         |
90 | | uznnssnn 11235 |
. . . . . . . . . . . . . . . . 17
       |
91 | 90 | ad2antlr 738 |
. . . . . . . . . . . . . . . 16
        
          
  |
92 | | simpr 467 |
. . . . . . . . . . . . . . . 16
        
             |
93 | 91, 92 | sseldd 3445 |
. . . . . . . . . . . . . . 15
        
         |
94 | 89, 93 | jca 539 |
. . . . . . . . . . . . . 14
        
       
   |
95 | | simp-4r 782 |
. . . . . . . . . . . . . 14
        
         |
96 | | simpllr 774 |
. . . . . . . . . . . . . 14
        
         
  |
97 | | simplr 767 |
. . . . . . . . . . . . . . . 16
         
 
     |
98 | | simplr 767 |
. . . . . . . . . . . . . . . . . . 19
   

 
  |
99 | 98 | rexrd 9716 |
. . . . . . . . . . . . . . . . . 18
   

 
  |
100 | 14 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . . . . . . 21
 

         |
101 | 15, 100 | eqeltrrd 2541 |
. . . . . . . . . . . . . . . . . . . 20
 

     |
102 | 7, 101 | sseldi 3442 |
. . . . . . . . . . . . . . . . . . 19
 

  |
103 | 102 | ad2antrr 737 |
. . . . . . . . . . . . . . . . . 18
   

 
  |
104 | | simpr 467 |
. . . . . . . . . . . . . . . . . 18
   

 
  |
105 | | pnfge 11461 |
. . . . . . . . . . . . . . . . . . 19

  |
106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   

 
  |
107 | 65 | biimpar 492 |
. . . . . . . . . . . . . . . . . 18
  
       |
108 | 99, 103, 104, 106, 107 | syl13anc 1278 |
. . . . . . . . . . . . . . . . 17
   

 
     |
109 | 108 | adantlr 726 |
. . . . . . . . . . . . . . . 16
         
 
     |
110 | 97, 109 | sseldd 3445 |
. . . . . . . . . . . . . . 15
         
 
  |
111 | 110 | ex 440 |
. . . . . . . . . . . . . 14
   

   
 
   |
112 | 94, 95, 96, 111 | syl21anc 1275 |
. . . . . . . . . . . . 13
        
       
   |
113 | 112 | ralimdva 2808 |
. . . . . . . . . . . 12
   
    
       
         |
114 | 113 | reximdva 2874 |
. . . . . . . . . . 11
     
   
     
      
   |
115 | 74, 114 | syl5bi 225 |
. . . . . . . . . 10
     
   
     
      
   |
116 | 115 | expimpd 612 |
. . . . . . . . 9
 

     
     
           |
117 | 116 | rexlimdva 2891 |
. . . . . . . 8
             
           |
118 | 88, 117 | syl5 33 |
. . . . . . 7
      
 
     
           |
119 | 118 | imp 435 |
. . . . . 6
 
 
 
        
 
      
  |
120 | 82, 86, 87, 119 | syl12anc 1274 |
. . . . 5
   
   
             
  |
121 | 120 | exp31 613 |
. . . 4
 
  
 
    
      
    |
122 | 121 | ralrimdva 2818 |
. . 3
         
 
          |
123 | 81, 122 | impbid 195 |
. 2
          
       
   |
124 | 23, 123 | bitrd 261 |
1
       
       
   |