Step | Hyp | Ref
| Expression |
1 | | ordtrest2.2 |
. . . 4
  |
2 | | tsrps 16460 |
. . . 4
   |
3 | 1, 2 | syl 17 |
. . 3
   |
4 | | ordtrest2.1 |
. . . . 5
 |
5 | | dmexg 6721 |
. . . . . 6

  |
6 | 1, 5 | syl 17 |
. . . . 5
   |
7 | 4, 6 | syl5eqel 2532 |
. . . 4
   |
8 | | ordtrest2.3 |
. . . 4

  |
9 | 7, 8 | ssexd 4549 |
. . 3
   |
10 | | ordtrest 20211 |
. . 3
   ordTop     
 ordTop 
↾t    |
11 | 3, 9, 10 | syl2anc 666 |
. 2
 ordTop       ordTop  ↾t    |
12 | | eqid 2450 |
. . . . . . . 8
             |
13 | | eqid 2450 |
. . . . . . . 8
             |
14 | 4, 12, 13 | ordtval 20198 |
. . . . . . 7
 ordTop          
                   |
15 | 1, 14 | syl 17 |
. . . . . 6
 ordTop          
                   |
16 | 15 | oveq1d 6303 |
. . . . 5
  ordTop  ↾t              
     
        ↾t    |
17 | | fibas 19986 |
. . . . . 6
     
                 |
18 | | tgrest 20168 |
. . . . . 6
                                  
                ↾t            
                
↾t    |
19 | 17, 9, 18 | sylancr 668 |
. . . . 5
          
                ↾t            
                
↾t    |
20 | 16, 19 | eqtr4d 2487 |
. . . 4
  ordTop  ↾t           
                ↾t     |
21 | | firest 15324 |
. . . . 5
                      ↾t                          ↾t   |
22 | 21 | fveq2i 5866 |
. . . 4
            
     
     
↾t                              ↾t    |
23 | 20, 22 | syl6eqr 2502 |
. . 3
  ordTop  ↾t           
               ↾t      |
24 | | inex1g 4545 |
. . . . . 6
  
    |
25 | 1, 24 | syl 17 |
. . . . 5
       |
26 | | ordttop 20209 |
. . . . 5
     ordTop        |
27 | 25, 26 | syl 17 |
. . . 4
 ordTop        |
28 | 4, 12, 13 | ordtuni 20199 |
. . . . . . . . 9
             
        |
29 | 1, 28 | syl 17 |
. . . . . . . 8
                      |
30 | 29, 7 | eqeltrrd 2529 |
. . . . . . 7
    
                 |
31 | | uniexb 6598 |
. . . . . . 7
            
            
     
        |
32 | 30, 31 | sylibr 216 |
. . . . . 6
      
     
        |
33 | | restval 15318 |
. . . . . 6
       
     
          
               ↾t                          |
34 | 32, 9, 33 | syl2anc 666 |
. . . . 5
    
               ↾t                          |
35 | | dfss1 3636 |
. . . . . . . . . . . 12

    |
36 | 8, 35 | sylib 200 |
. . . . . . . . . . 11
     |
37 | | eqid 2450 |
. . . . . . . . . . . . . . 15
     
   |
38 | 37 | ordttopon 20202 |
. . . . . . . . . . . . . 14
     ordTop      TopOn        |
39 | 25, 38 | syl 17 |
. . . . . . . . . . . . 13
 ordTop      TopOn        |
40 | 4 | psssdm 16455 |
. . . . . . . . . . . . . . 15
   
     |
41 | 3, 8, 40 | syl2anc 666 |
. . . . . . . . . . . . . 14
  
    |
42 | 41 | fveq2d 5867 |
. . . . . . . . . . . . 13
 TopOn      TopOn    |
43 | 39, 42 | eleqtrd 2530 |
. . . . . . . . . . . 12
 ordTop      TopOn    |
44 | | toponmax 19936 |
. . . . . . . . . . . 12
 ordTop      TopOn  ordTop        |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
 ordTop 
      |
46 | 36, 45 | eqeltrd 2528 |
. . . . . . . . . 10
   ordTop 
      |
47 | | elsni 3992 |
. . . . . . . . . . . 12
     |
48 | 47 | ineq1d 3632 |
. . . . . . . . . . 11
         |
49 | 48 | eleq1d 2512 |
. . . . . . . . . 10
      ordTop        ordTop 
       |
50 | 46, 49 | syl5ibrcom 226 |
. . . . . . . . 9
   
  ordTop         |
51 | 50 | ralrimiv 2799 |
. . . . . . . 8
   
  ordTop        |
52 | | ordtrest2.4 |
. . . . . . . . . 10
 

            |
53 | 4, 1, 8, 52 | ordtrest2lem 20212 |
. . . . . . . . 9
           ordTop        |
54 | | df-rn 4844 |
. . . . . . . . . . 11
  |
55 | | cnvtsr 16461 |
. . . . . . . . . . . 12
   |
56 | 1, 55 | syl 17 |
. . . . . . . . . . 11
 
 |
57 | 4 | psrn 16448 |
. . . . . . . . . . . . 13
   |
58 | 3, 57 | syl 17 |
. . . . . . . . . . . 12
   |
59 | 8, 58 | sseqtrd 3467 |
. . . . . . . . . . 11

  |
60 | 58 | adantr 467 |
. . . . . . . . . . . . . . 15
 

 
  |
61 | | rabeq 3037 |
. . . . . . . . . . . . . . 15
                   |
62 | 60, 61 | syl 17 |
. . . . . . . . . . . . . 14
 

                    |
63 | | vex 3047 |
. . . . . . . . . . . . . . . . . 18
 |
64 | | vex 3047 |
. . . . . . . . . . . . . . . . . 18
 |
65 | 63, 64 | brcnv 5016 |
. . . . . . . . . . . . . . . . 17
   
    |
66 | | vex 3047 |
. . . . . . . . . . . . . . . . . 18
 |
67 | 64, 66 | brcnv 5016 |
. . . . . . . . . . . . . . . . 17
   
    |
68 | 65, 67 | anbi12ci 703 |
. . . . . . . . . . . . . . . 16
        
        |
69 | 68 | a1i 11 |
. . . . . . . . . . . . . . 15
         
         |
70 | 69 | rabbiia 3032 |
. . . . . . . . . . . . . 14
    
     
        |
71 | 62, 70 | syl6eqr 2502 |
. . . . . . . . . . . . 13
 

                      |
72 | 71, 52 | eqsstr3d 3466 |
. . . . . . . . . . . 12
 

              |
73 | 72 | ancom2s 810 |
. . . . . . . . . . 11
 

              |
74 | 54, 56, 59, 73 | ordtrest2lem 20212 |
. . . . . . . . . 10
            ordTop  
      |
75 | | vex 3047 |
. . . . . . . . . . . . . . . . . 18
 |
76 | 75, 64 | brcnv 5016 |
. . . . . . . . . . . . . . . . 17
   
    |
77 | 76 | bicomi 206 |
. . . . . . . . . . . . . . . 16
  
     |
78 | 77 | a1i 11 |
. . . . . . . . . . . . . . 15
          |
79 | 78 | notbid 296 |
. . . . . . . . . . . . . 14
   
      |
80 | 58, 79 | rabeqbidv 3039 |
. . . . . . . . . . . . 13
            |
81 | 58, 80 | mpteq12dv 4480 |
. . . . . . . . . . . 12
                |
82 | 81 | rneqd 5061 |
. . . . . . . . . . 11
                |
83 | | cnvin 5242 |
. . . . . . . . . . . . . . 15
            |
84 | | cnvxp 5253 |
. . . . . . . . . . . . . . . 16
      |
85 | 84 | ineq2i 3630 |
. . . . . . . . . . . . . . 15
            |
86 | 83, 85 | eqtri 2472 |
. . . . . . . . . . . . . 14
           |
87 | 86 | fveq2i 5866 |
. . . . . . . . . . . . 13
ordTop   
   ordTop        |
88 | | psss 16453 |
. . . . . . . . . . . . . . 15
  
    |
89 | 3, 88 | syl 17 |
. . . . . . . . . . . . . 14
       |
90 | | ordtcnv 20210 |
. . . . . . . . . . . . . 14
     ordTop       ordTop        |
91 | 89, 90 | syl 17 |
. . . . . . . . . . . . 13
 ordTop       ordTop        |
92 | 87, 91 | syl5reqr 2499 |
. . . . . . . . . . . 12
 ordTop      ordTop         |
93 | 92 | eleq2d 2513 |
. . . . . . . . . . 11
    ordTop        ordTop   
      |
94 | 82, 93 | raleqbidv 3000 |
. . . . . . . . . 10
            ordTop 
               ordTop  
       |
95 | 74, 94 | mpbird 236 |
. . . . . . . . 9
           ordTop        |
96 | | ralunb 3614 |
. . . . . . . . 9
 
                 ordTop                 ordTop 
              ordTop 
       |
97 | 53, 95, 96 | sylanbrc 669 |
. . . . . . . 8
          
        ordTop        |
98 | | ralunb 3614 |
. . . . . . . 8
 
  
                  ordTop 
        
 ordTop                        ordTop         |
99 | 51, 97, 98 | sylanbrc 669 |
. . . . . . 7
             
         ordTop        |
100 | | eqid 2450 |
. . . . . . . 8
   
                                         |
101 | 100 | fmpt 6041 |
. . . . . . 7
 
  
                  ordTop 
          
     
             
                 ordTop        |
102 | 99, 101 | sylib 200 |
. . . . . 6
             
             
                 ordTop        |
103 | | frn 5733 |
. . . . . 6
                                    
        ordTop 
   
   
                  ordTop        |
104 | 102, 103 | syl 17 |
. . . . 5
       
     
         ordTop        |
105 | 34, 104 | eqsstrd 3465 |
. . . 4
    
               ↾t 
ordTop        |
106 | | tgfiss 20000 |
. . . 4
  ordTop     
                   ↾t 
ordTop      
            
     
     
↾t    ordTop        |
107 | 27, 105, 106 | syl2anc 666 |
. . 3
          
               ↾t    ordTop  
     |
108 | 23, 107 | eqsstrd 3465 |
. 2
  ordTop  ↾t  ordTop        |
109 | 11, 108 | eqssd 3448 |
1
 ordTop       ordTop  ↾t    |