Step | Hyp | Ref
| Expression |
1 | | ordtrest2NEW.2 |
. . . 4
 Toset |
2 | | tospos 28419 |
. . . 4
 Toset   |
3 | | posprs 16194 |
. . . 4

 |
4 | 1, 2, 3 | 3syl 18 |
. . 3
  |
5 | | ordtrest2NEW.3 |
. . 3

  |
6 | | ordtNEW.b |
. . . 4
     |
7 | | ordtNEW.l |
. . . 4
    
    |
8 | 6, 7 | ordtrestNEW 28727 |
. . 3
   ordTop
   
 ordTop
↾t    |
9 | 4, 5, 8 | syl2anc 667 |
. 2
 ordTop      ordTop
↾t    |
10 | | eqid 2451 |
. . . . . . . 8
 
   
   |
11 | | eqid 2451 |
. . . . . . . 8
 
   
   |
12 | 6, 7, 10, 11 | ordtprsval 28724 |
. . . . . . 7
 ordTop
           
   
        |
13 | 4, 12 | syl 17 |
. . . . . 6
 ordTop
           
   
        |
14 | 13 | oveq1d 6305 |
. . . . 5
  ordTop ↾t                         ↾t    |
15 | | fibas 19993 |
. . . . . 6
     
      
      |
16 | | fvex 5875 |
. . . . . . . . 9
     |
17 | 6, 16 | eqeltri 2525 |
. . . . . . . 8
 |
18 | 17 | a1i 11 |
. . . . . . 7
   |
19 | 18, 5 | ssexd 4550 |
. . . . . 6
   |
20 | | tgrest 20175 |
. . . . . 6
              
    

                     
↾t            
      
      ↾t    |
21 | 15, 19, 20 | sylancr 669 |
. . . . 5
          
      
     ↾t               
   
      ↾t    |
22 | 14, 21 | eqtr4d 2488 |
. . . 4
  ordTop ↾t                       
↾t     |
23 | | firest 15331 |
. . . . 5
             
    ↾t                
     ↾t   |
24 | 23 | fveq2i 5868 |
. . . 4
            
   
   
↾t                    
     ↾t    |
25 | 22, 24 | syl6eqr 2503 |
. . 3
  ordTop ↾t              
   
   
↾t      |
26 | | fvex 5875 |
. . . . . . . 8
     |
27 | 26 | inex1 4544 |
. . . . . . 7
         |
28 | 7, 27 | eqeltri 2525 |
. . . . . 6
 |
29 | 28 | inex1 4544 |
. . . . 5
    |
30 | | ordttop 20216 |
. . . . 5
    ordTop       |
31 | 29, 30 | mp1i 13 |
. . . 4
 ordTop       |
32 | 6, 7, 10, 11 | ordtprsuni 28725 |
. . . . . . . . 9
                  |
33 | 4, 32 | syl 17 |
. . . . . . . 8
           
      |
34 | 33, 18 | eqeltrrd 2530 |
. . . . . . 7
    
      
      |
35 | | uniexb 6601 |
. . . . . . 7
              
          
      |
36 | 34, 35 | sylibr 216 |
. . . . . 6
      
   
      |
37 | | restval 15325 |
. . . . . 6
       
   
        
      
    ↾t     
      
         |
38 | 36, 19, 37 | syl2anc 667 |
. . . . 5
    
      
    ↾t     
      
         |
39 | | dfss1 3637 |
. . . . . . . . . . . 12

    |
40 | 5, 39 | sylib 200 |
. . . . . . . . . . 11
     |
41 | | eqid 2451 |
. . . . . . . . . . . . . . 15
       |
42 | 41 | ordttopon 20209 |
. . . . . . . . . . . . . 14
    ordTop     TopOn       |
43 | 29, 42 | mp1i 13 |
. . . . . . . . . . . . 13
 ordTop     TopOn       |
44 | 6, 7 | prsssdm 28723 |
. . . . . . . . . . . . . . 15
  
     |
45 | 4, 5, 44 | syl2anc 667 |
. . . . . . . . . . . . . 14
      |
46 | 45 | fveq2d 5869 |
. . . . . . . . . . . . 13
 TopOn     TopOn    |
47 | 43, 46 | eleqtrd 2531 |
. . . . . . . . . . . 12
 ordTop     TopOn    |
48 | | toponmax 19943 |
. . . . . . . . . . . 12
 ordTop
    TopOn  ordTop       |
49 | 47, 48 | syl 17 |
. . . . . . . . . . 11
 ordTop
      |
50 | 40, 49 | eqeltrd 2529 |
. . . . . . . . . 10
   ordTop
      |
51 | | elsni 3993 |
. . . . . . . . . . . 12
     |
52 | 51 | ineq1d 3633 |
. . . . . . . . . . 11
         |
53 | 52 | eleq1d 2513 |
. . . . . . . . . 10
      ordTop
      ordTop
       |
54 | 50, 53 | syl5ibrcom 226 |
. . . . . . . . 9
   
  ordTop        |
55 | 54 | ralrimiv 2800 |
. . . . . . . 8
   
  ordTop
      |
56 | | ordtrest2NEW.4 |
. . . . . . . . . 10
 

     
  |
57 | 6, 7, 1, 5, 56 | ordtrest2NEWlem 28728 |
. . . . . . . . 9
         ordTop
      |
58 | | eqid 2451 |
. . . . . . . . . . . 12
ODual  ODual   |
59 | 58, 6 | odubas 16379 |
. . . . . . . . . . 11
   ODual    |
60 | 7 | cnveqi 5009 |
. . . . . . . . . . . 12
          |
61 | | cnvin 5243 |
. . . . . . . . . . . . 13
     
              |
62 | | cnvxp 5254 |
. . . . . . . . . . . . . 14
      |
63 | 62 | ineq2i 3631 |
. . . . . . . . . . . . 13
     
              |
64 | | eqid 2451 |
. . . . . . . . . . . . . . 15
         |
65 | 58, 64 | oduleval 16377 |
. . . . . . . . . . . . . 14
        ODual    |
66 | 65 | ineq1i 3630 |
. . . . . . . . . . . . 13
     
       ODual       |
67 | 61, 63, 66 | 3eqtri 2477 |
. . . . . . . . . . . 12
     
       ODual       |
68 | 60, 67 | eqtri 2473 |
. . . . . . . . . . 11
    ODual       |
69 | 58 | odutos 28424 |
. . . . . . . . . . . 12
 Toset ODual 
Toset |
70 | 1, 69 | syl 17 |
. . . . . . . . . . 11
 ODual  Toset |
71 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
72 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
73 | 71, 72 | brcnv 5017 |
. . . . . . . . . . . . . . . 16
 
  |
74 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
75 | 72, 74 | brcnv 5017 |
. . . . . . . . . . . . . . . 16
 
  |
76 | 73, 75 | anbi12ci 704 |
. . . . . . . . . . . . . . 15
   
     |
77 | 76 | a1i 11 |
. . . . . . . . . . . . . 14
           |
78 | 77 | rabbiia 3033 |
. . . . . . . . . . . . 13
   
   
   |
79 | 78, 56 | syl5eqss 3476 |
. . . . . . . . . . . 12
 

    
     |
80 | 79 | ancom2s 811 |
. . . . . . . . . . 11
 

    
     |
81 | 59, 68, 70, 5, 80 | ordtrest2NEWlem 28728 |
. . . . . . . . . 10
          ordTop        |
82 | | vex 3048 |
. . . . . . . . . . . . . . . . . 18
 |
83 | 82, 72 | brcnv 5017 |
. . . . . . . . . . . . . . . . 17
 
  |
84 | 83 | bicomi 206 |
. . . . . . . . . . . . . . . 16
    |
85 | 84 | a1i 11 |
. . . . . . . . . . . . . . 15
 
    |
86 | 85 | notbid 296 |
. . . . . . . . . . . . . 14
      |
87 | 86 | rabbidv 3036 |
. . . . . . . . . . . . 13
        |
88 | 87 | mpteq2dv 4490 |
. . . . . . . . . . . 12
      

    |
89 | 88 | rneqd 5062 |
. . . . . . . . . . 11
            |
90 | | cnvin 5243 |
. . . . . . . . . . . . . . 15
      
   |
91 | | cnvxp 5254 |
. . . . . . . . . . . . . . . 16
      |
92 | 91 | ineq2i 3631 |
. . . . . . . . . . . . . . 15
          |
93 | 90, 92 | eqtri 2473 |
. . . . . . . . . . . . . 14
         |
94 | 93 | fveq2i 5868 |
. . . . . . . . . . . . 13
ordTop 
    ordTop 
     |
95 | 6 | ressprs 28416 |
. . . . . . . . . . . . . . . 16
    ↾s   |
96 | 4, 5, 95 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 
↾s   |
97 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
   
↾s       ↾s    |
98 | | eqid 2451 |
. . . . . . . . . . . . . . . 16
     ↾s        ↾s       ↾s         
↾s        ↾s       ↾s      |
99 | 97, 98 | ordtcnvNEW 28726 |
. . . . . . . . . . . . . . 15
  ↾s  ordTop       ↾s        ↾s       ↾s      ordTop     
↾s        ↾s       ↾s        |
100 | 96, 99 | syl 17 |
. . . . . . . . . . . . . 14
 ordTop       ↾s        ↾s       ↾s      ordTop     
↾s        ↾s       ↾s        |
101 | 6, 7 | prsss 28722 |
. . . . . . . . . . . . . . . . . 18
                |
102 | 4, 5, 101 | syl2anc 667 |
. . . . . . . . . . . . . . . . 17

             |
103 | | eqid 2451 |
. . . . . . . . . . . . . . . . . . . 20
 ↾s   ↾s   |
104 | 103, 64 | ressle 15297 |
. . . . . . . . . . . . . . . . . . 19
         ↾s     |
105 | 19, 104 | syl 17 |
. . . . . . . . . . . . . . . . . 18
         ↾s     |
106 | 103, 6 | ressbas2 15180 |
. . . . . . . . . . . . . . . . . . . 20
     ↾s     |
107 | 5, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
    
↾s     |
108 | 107 | sqxpeqd 4860 |
. . . . . . . . . . . . . . . . . 18
        ↾s       ↾s      |
109 | 105, 108 | ineq12d 3635 |
. . . . . . . . . . . . . . . . 17
              ↾s        ↾s       ↾s       |
110 | 102, 109 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16

        ↾s        ↾s       ↾s       |
111 | 110 | cnveqd 5010 |
. . . . . . . . . . . . . . 15
 
         ↾s        ↾s       ↾s       |
112 | 111 | fveq2d 5869 |
. . . . . . . . . . . . . 14
 ordTop      ordTop      
↾s        ↾s       ↾s        |
113 | 110 | fveq2d 5869 |
. . . . . . . . . . . . . 14
 ordTop     ordTop      ↾s        ↾s       ↾s        |
114 | 100, 112,
113 | 3eqtr4d 2495 |
. . . . . . . . . . . . 13
 ordTop      ordTop       |
115 | 94, 114 | syl5reqr 2500 |
. . . . . . . . . . . 12
 ordTop     ordTop        |
116 | 115 | eleq2d 2514 |
. . . . . . . . . . 11
    ordTop
      ordTop         |
117 | 89, 116 | raleqbidv 3001 |
. . . . . . . . . 10
          ordTop     
        ordTop         |
118 | 81, 117 | mpbird 236 |
. . . . . . . . 9
         ordTop
      |
119 | | ralunb 3615 |
. . . . . . . . 9
 
      
      ordTop    
 
 
     ordTop
            ordTop        |
120 | 57, 118, 119 | sylanbrc 670 |
. . . . . . . 8
               ordTop
      |
121 | | ralunb 3615 |
. . . . . . . 8
 
  
      
       ordTop         
 ordTop            
      ordTop        |
122 | 55, 120, 121 | sylanbrc 670 |
. . . . . . 7
                   ordTop
      |
123 | | eqid 2451 |
. . . . . . . 8
   
      
          
      
        |
124 | 123 | fmpt 6043 |
. . . . . . 7
 
  
      
       ordTop                              
   
      ordTop
      |
125 | 122, 124 | sylib 200 |
. . . . . 6
                          
   
      ordTop
      |
126 | | frn 5735 |
. . . . . 6
           
                  
      ordTop
   
   
      
      
ordTop       |
127 | 125, 126 | syl 17 |
. . . . 5
       
   
       ordTop       |
128 | 38, 127 | eqsstrd 3466 |
. . . 4
    
      
    ↾t  ordTop       |
129 | | tgfiss 20007 |
. . . 4
  ordTop    
          
    ↾t  ordTop                      
    ↾t    ordTop
      |
130 | 31, 128, 129 | syl2anc 667 |
. . 3
          
      
    ↾t    ordTop
      |
131 | 25, 130 | eqsstrd 3466 |
. 2
  ordTop ↾t 
ordTop       |
132 | 9, 131 | eqssd 3449 |
1
 ordTop      ordTop ↾t    |