Proof of Theorem cvmliftlem8
Step | Hyp | Ref
| Expression |
1 | | elfznn 11579 |
. . 3
       |
2 | | cvmliftlem.1 |
. . . 4
                       
    ↾t    
↾t        |
3 | | cvmliftlem.b |
. . . 4
  |
4 | | cvmliftlem.x |
. . . 4
  |
5 | | cvmliftlem.f |
. . . 4
  CovMap    |
6 | | cvmliftlem.g |
. . . 4
     |
7 | | cvmliftlem.p |
. . . 4
   |
8 | | cvmliftlem.e |
. . . 4
           |
9 | | cvmliftlem.n |
. . . 4
   |
10 | | cvmliftlem.t |
. . . 4
                    |
11 | | cvmliftlem.a |
. . . 4
                ![[,] [,]](_icc.gif)    
          |
12 | | cvmliftlem.l |
. . . 4
     |
13 | | cvmliftlem.q |
. . . 4
    
       ![[,] [,]](_icc.gif)                                                     |
14 | | cvmliftlem5.3 |
. . . 4
      ![[,] [,]](_icc.gif)     |
15 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cvmliftlem5 27312 |
. . 3
 

                       
                     |
16 | 1, 15 | sylan2 474 |
. 2
 
            
                                     |
17 | 5 | adantr 465 |
. . . 4
 
      CovMap    |
18 | | cvmtop1 27283 |
. . . 4
  CovMap 
  |
19 | | cnrest2r 19007 |
. . . 4
  
↾t   ↾t                
             
↾t     |
20 | 17, 18, 19 | 3syl 20 |
. . 3
 
      
↾t   ↾t                
             
↾t     |
21 | | retopon 20458 |
. . . . . 6
    TopOn   |
22 | 12, 21 | eqeltri 2535 |
. . . . 5
TopOn   |
23 | | simpr 461 |
. . . . . . 7
 
           |
24 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14 | cvmliftlem2 27309 |
. . . . . 6
 
       ![[,] [,]](_icc.gif)    |
25 | | unitssre 11533 |
. . . . . 6
  ![[,] [,]](_icc.gif)   |
26 | 24, 25 | syl6ss 3466 |
. . . . 5
 
       |
27 | | resttopon 18881 |
. . . . 5
  TopOn 

 ↾t  TopOn    |
28 | 22, 26, 27 | sylancr 663 |
. . . 4
 
      ↾t  TopOn    |
29 | | eqid 2451 |
. . . . . . 7
 ↾t   ↾t   |
30 | | iitopon 20571 |
. . . . . . . 8
TopOn   ![[,] [,]](_icc.gif)    |
31 | 30 | a1i 11 |
. . . . . . 7
 
     TopOn   ![[,] [,]](_icc.gif)     |
32 | 6 | adantr 465 |
. . . . . . . . . 10
 
         |
33 | | iiuni 20573 |
. . . . . . . . . . 11
  ![[,] [,]](_icc.gif)    |
34 | 33, 4 | cnf 18966 |
. . . . . . . . . 10
       ![[,] [,]](_icc.gif)      |
35 | 32, 34 | syl 16 |
. . . . . . . . 9
 
         ![[,] [,]](_icc.gif)      |
36 | 35 | feqmptd 5843 |
. . . . . . . 8
 
        ![[,] [,]](_icc.gif)         |
37 | 36, 32 | eqeltrrd 2540 |
. . . . . . 7
 
        ![[,] [,]](_icc.gif)           |
38 | 29, 31, 24, 37 | cnmpt1res 19365 |
. . . . . 6
 
             ↾t     |
39 | | dfii2 20574 |
. . . . . . . . . 10
     ↾t   ![[,] [,]](_icc.gif)    |
40 | 12 | oveq1i 6200 |
. . . . . . . . . 10
 ↾t   ![[,] [,]](_icc.gif)        ↾t   ![[,] [,]](_icc.gif)    |
41 | 39, 40 | eqtr4i 2483 |
. . . . . . . . 9

↾t   ![[,] [,]](_icc.gif)    |
42 | 41 | oveq1i 6200 |
. . . . . . . 8
 ↾t    ↾t   ![[,] [,]](_icc.gif)  
↾t   |
43 | | retop 20456 |
. . . . . . . . . . 11
     |
44 | 12, 43 | eqeltri 2535 |
. . . . . . . . . 10
 |
45 | 44 | a1i 11 |
. . . . . . . . 9
 
       |
46 | | ovex 6215 |
. . . . . . . . . 10
  ![[,] [,]](_icc.gif)   |
47 | 46 | a1i 11 |
. . . . . . . . 9
 
       ![[,] [,]](_icc.gif)    |
48 | | restabs 18885 |
. . . . . . . . 9
    ![[,] [,]](_icc.gif)    ![[,] [,]](_icc.gif)     ↾t   ![[,] [,]](_icc.gif)   ↾t   ↾t    |
49 | 45, 24, 47, 48 | syl3anc 1219 |
. . . . . . . 8
 
      
↾t   ![[,] [,]](_icc.gif)   ↾t   ↾t    |
50 | 42, 49 | syl5eq 2504 |
. . . . . . 7
 
      ↾t   ↾t    |
51 | 50 | oveq1d 6205 |
. . . . . 6
 
      
↾t     ↾t     |
52 | 38, 51 | eleqtrd 2541 |
. . . . 5
 
             ↾t     |
53 | | cvmtop2 27284 |
. . . . . . . 8
  CovMap 
  |
54 | 17, 53 | syl 16 |
. . . . . . 7
 
       |
55 | 4 | toptopon 18654 |
. . . . . . 7

TopOn    |
56 | 54, 55 | sylib 196 |
. . . . . 6
 
     TopOn    |
57 | | simprl 755 |
. . . . . . . . . 10
 
    
 
      |
58 | | simprr 756 |
. . . . . . . . . 10
 
    
    |
59 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 57, 14, 58 | cvmliftlem3 27310 |
. . . . . . . . 9
 
    
                |
60 | 59 | anassrs 648 |
. . . . . . . 8
                       |
61 | | eqid 2451 |
. . . . . . . 8
             |
62 | 60, 61 | fmptd 5966 |
. . . . . . 7
 
                         |
63 | | frn 5663 |
. . . . . . 7
                                   |
64 | 62, 63 | syl 16 |
. . . . . 6
 
                     |
65 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23 | cvmliftlem1 27308 |
. . . . . . . 8
 
                           |
66 | 2 | cvmsrcl 27287 |
. . . . . . . 8
                    
          |
67 | | elssuni 4219 |
. . . . . . . 8
                    |
68 | 65, 66, 67 | 3syl 20 |
. . . . . . 7
 
                |
69 | 68, 4 | syl6sseqr 3501 |
. . . . . 6
 
               |
70 | | cnrest2 19006 |
. . . . . 6
  TopOn                                  ↾t  

       ↾t   ↾t              |
71 | 56, 64, 69, 70 | syl3anc 1219 |
. . . . 5
 
             
↾t           ↾t   ↾t              |
72 | 52, 71 | mpbid 210 |
. . . 4
 
             ↾t   ↾t             |
73 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 | cvmliftlem7 27314 |
. . . . . . . . . 10
 
         
                          |
74 | | cvmcn 27285 |
. . . . . . . . . . . 12
  CovMap 

   |
75 | 3, 4 | cnf 18966 |
. . . . . . . . . . . 12
         |
76 | 17, 74, 75 | 3syl 20 |
. . . . . . . . . . 11
 
           |
77 | | ffn 5657 |
. . . . . . . . . . 11
    
  |
78 | | fniniseg 5923 |
. . . . . . . . . . 11
      
                       
     
                                       |
79 | 76, 77, 78 | 3syl 20 |
. . . . . . . . . 10
 
          
                       
     
                                       |
80 | 73, 79 | mpbid 210 |
. . . . . . . . 9
 
          
                                      |
81 | 80 | simpld 459 |
. . . . . . . 8
 
         
           |
82 | 80 | simprd 463 |
. . . . . . . . 9
 
                                 |
83 | 1 | adantl 466 |
. . . . . . . . . . . . . . . 16
 
       |
84 | 83 | nnred 10438 |
. . . . . . . . . . . . . . 15
 
       |
85 | | peano2rem 9776 |
. . . . . . . . . . . . . . 15
 
   |
86 | 84, 85 | syl 16 |
. . . . . . . . . . . . . 14
 
     
   |
87 | 9 | adantr 465 |
. . . . . . . . . . . . . 14
 
       |
88 | 86, 87 | nndivred 10471 |
. . . . . . . . . . . . 13
 
           |
89 | 88 | rexrd 9534 |
. . . . . . . . . . . 12
 
           |
90 | 84, 87 | nndivred 10471 |
. . . . . . . . . . . . 13
 
         |
91 | 90 | rexrd 9534 |
. . . . . . . . . . . 12
 
         |
92 | 84 | ltm1d 10366 |
. . . . . . . . . . . . . 14
 
     
   |
93 | 87 | nnred 10438 |
. . . . . . . . . . . . . . 15
 
       |
94 | 87 | nngt0d 10466 |
. . . . . . . . . . . . . . 15
 
       |
95 | | ltdiv1 10294 |
. . . . . . . . . . . . . . 15
   

              |
96 | 86, 84, 93, 94, 95 | syl112anc 1223 |
. . . . . . . . . . . . . 14
 
       
 
       |
97 | 92, 96 | mpbid 210 |
. . . . . . . . . . . . 13
 
             |
98 | 88, 90, 97 | ltled 9623 |
. . . . . . . . . . . 12
 
             |
99 | | lbicc2 11502 |
. . . . . . . . . . . 12
       
 
               ![[,] [,]](_icc.gif)      |
100 | 89, 91, 98, 99 | syl3anc 1219 |
. . . . . . . . . . 11
 
               ![[,] [,]](_icc.gif)      |
101 | 100, 14 | syl6eleqr 2550 |
. . . . . . . . . 10
 
           |
102 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 23, 14, 101 | cvmliftlem3 27310 |
. . . . . . . . 9
 
         
             |
103 | 82, 102 | eqeltrd 2539 |
. . . . . . . 8
 
                                 |
104 | | eqid 2451 |
. . . . . . . . 9
                                                     |
105 | 2, 3, 104 | cvmsiota 27300 |
. . . . . . . 8
   CovMap                           
                                                                            
                                      |
106 | 17, 65, 81, 103, 105 | syl13anc 1221 |
. . . . . . 7
 
                     
                 
                             
             |
107 | 106 | simpld 459 |
. . . . . 6
 
                                         |
108 | 2 | cvmshmeo 27294 |
. . . . . 6
                                                        
                
             ↾t                
              ↾t             |
109 | 65, 107, 108 | syl2anc 661 |
. . . . 5
 
                                  
↾t                               ↾t             |
110 | | hmeocnvcn 19450 |
. . . . 5
 
                            
↾t                               ↾t            
                            
↾t           ↾t                
              |
111 | 109, 110 | syl 16 |
. . . 4
 
      
                            
↾t           ↾t                
              |
112 | 28, 72, 111 | cnmpt11f 19353 |
. . 3
 
                        
                     ↾t   ↾t                
              |
113 | 20, 112 | sseldd 3455 |
. 2
 
                        
                     ↾t     |
114 | 16, 113 | eqeltrd 2539 |
1
 
           ↾t     |