Step | Hyp | Ref
| Expression |
1 | | n0 3732 |
. 2
            |
2 | | simpl2 1034 |
. . . . . 6
    CovMap 

    
  |
3 | | simpl1 1033 |
. . . . . . . . . . . 12
    CovMap 

    
 CovMap    |
4 | | cvmtop1 30055 |
. . . . . . . . . . . 12
  CovMap 
  |
5 | 3, 4 | syl 17 |
. . . . . . . . . . 11
    CovMap 

    
  |
6 | 5 | adantr 472 |
. . . . . . . . . 10
     CovMap 
         |
7 | | cvmcov.1 |
. . . . . . . . . . . . 13
                       
    ↾t    
↾t        |
8 | 7 | cvmsss 30062 |
. . . . . . . . . . . 12
       |
9 | 8 | adantl 473 |
. . . . . . . . . . 11
    CovMap 

       |
10 | 9 | sselda 3418 |
. . . . . . . . . 10
     CovMap 
         |
11 | | cvmcn 30057 |
. . . . . . . . . . . . 13
  CovMap 

   |
12 | 3, 11 | syl 17 |
. . . . . . . . . . . 12
    CovMap 

    
    |
13 | | cnima 20358 |
. . . . . . . . . . . 12
   
        |
14 | 12, 2, 13 | syl2anc 673 |
. . . . . . . . . . 11
    CovMap 

            |
15 | 14 | adantr 472 |
. . . . . . . . . 10
     CovMap 
              |
16 | | inopn 20006 |
. . . . . . . . . 10
 
               |
17 | 6, 10, 15, 16 | syl3anc 1292 |
. . . . . . . . 9
     CovMap 
       
        |
18 | | eqid 2471 |
. . . . . . . . 9
                   |
19 | 17, 18 | fmptd 6061 |
. . . . . . . 8
    CovMap 

                    |
20 | | frn 5747 |
. . . . . . . 8
             
           |
21 | 19, 20 | syl 17 |
. . . . . . 7
    CovMap 

                |
22 | 7 | cvmsn0 30063 |
. . . . . . . . 9
       |
23 | 22 | adantl 473 |
. . . . . . . 8
    CovMap 

       |
24 | | dmmptg 5339 |
. . . . . . . . . . . 12
 

                 |
25 | | inex1g 4539 |
. . . . . . . . . . . 12
 
        |
26 | 24, 25 | mprg 2770 |
. . . . . . . . . . 11
          |
27 | 26 | eqeq1i 2476 |
. . . . . . . . . 10
            |
28 | | dm0rn0 5057 |
. . . . . . . . . 10
                     |
29 | 27, 28 | bitr3i 259 |
. . . . . . . . 9

           |
30 | 29 | necon3bii 2695 |
. . . . . . . 8
            |
31 | 23, 30 | sylib 201 |
. . . . . . 7
    CovMap 

                |
32 | 21, 31 | jca 541 |
. . . . . 6
    CovMap 

     

                    |
33 | | inss2 3644 |
. . . . . . . . . . . 12
             |
34 | | elpw2g 4564 |
. . . . . . . . . . . . 13
                          
        |
35 | 15, 34 | syl 17 |
. . . . . . . . . . . 12
     CovMap 
                           
        |
36 | 33, 35 | mpbiri 241 |
. . . . . . . . . . 11
     CovMap 
       
              |
37 | 36, 18 | fmptd 6061 |
. . . . . . . . . 10
    CovMap 

                          |
38 | | frn 5747 |
. . . . . . . . . 10
                                     |
39 | 37, 38 | syl 17 |
. . . . . . . . 9
    CovMap 

                      |
40 | | sspwuni 4360 |
. . . . . . . . 9
                                 |
41 | 39, 40 | sylib 201 |
. . . . . . . 8
    CovMap 

                      |
42 | | simpl3 1035 |
. . . . . . . . . . . . . 14
    CovMap 

       |
43 | | imass2 5210 |
. . . . . . . . . . . . . 14
             |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . 13
    CovMap 

                 |
45 | 7 | cvmsuni 30064 |
. . . . . . . . . . . . . 14
             |
46 | 45 | adantl 473 |
. . . . . . . . . . . . 13
    CovMap 

     
       |
47 | 44, 46 | sseqtr4d 3455 |
. . . . . . . . . . . 12
    CovMap 

             |
48 | 47 | sselda 3418 |
. . . . . . . . . . 11
     CovMap 
               |
49 | | eqid 2471 |
. . . . . . . . . . . . . . . . 17
               |
50 | | ineq1 3618 |
. . . . . . . . . . . . . . . . . . 19
 
               |
51 | 50 | eqeq2d 2481 |
. . . . . . . . . . . . . . . . . 18
               
                 |
52 | 51 | rspcev 3136 |
. . . . . . . . . . . . . . . . 17
                                  |
53 | 49, 52 | mpan2 685 |
. . . . . . . . . . . . . . . 16
 
                |
54 | 53 | ad2antrl 742 |
. . . . . . . . . . . . . . 15
      CovMap 

           
  
                |
55 | | vex 3034 |
. . . . . . . . . . . . . . . . 17
 |
56 | 55 | inex1 4537 |
. . . . . . . . . . . . . . . 16
        |
57 | 18 | elrnmpt 5087 |
. . . . . . . . . . . . . . . 16
                        

                 |
58 | 56, 57 | ax-mp 5 |
. . . . . . . . . . . . . . 15
                

                |
59 | 54, 58 | sylibr 217 |
. . . . . . . . . . . . . 14
      CovMap 

           
  
                 |
60 | | simprr 774 |
. . . . . . . . . . . . . . 15
      CovMap 

           
    |
61 | | simplr 770 |
. . . . . . . . . . . . . . 15
      CovMap 

           
         |
62 | 60, 61 | elind 3609 |
. . . . . . . . . . . . . 14
      CovMap 

           
           |
63 | | eleq2 2538 |
. . . . . . . . . . . . . . 15
                   |
64 | 63 | rspcev 3136 |
. . . . . . . . . . . . . 14
                                       |
65 | 59, 62, 64 | syl2anc 673 |
. . . . . . . . . . . . 13
      CovMap 

           
               |
66 | 65 | rexlimdvaa 2872 |
. . . . . . . . . . . 12
     CovMap 
                            |
67 | | eluni2 4194 |
. . . . . . . . . . . 12
 

  |
68 | | eluni2 4194 |
. . . . . . . . . . . 12
          
             |
69 | 66, 67, 68 | 3imtr4g 278 |
. . . . . . . . . . 11
     CovMap 
                           |
70 | 48, 69 | mpd 15 |
. . . . . . . . . 10
     CovMap 
                        |
71 | 70 | ex 441 |
. . . . . . . . 9
    CovMap 

                        |
72 | 71 | ssrdv 3424 |
. . . . . . . 8
    CovMap 

                      |
73 | 41, 72 | eqssd 3435 |
. . . . . . 7
    CovMap 

                      |
74 | | eldifsn 4088 |
. . . . . . . . . . . 12
                    
          
         |
75 | | vex 3034 |
. . . . . . . . . . . . . . 15
 |
76 | 18 | elrnmpt 5087 |
. . . . . . . . . . . . . . 15
          

          |
77 | 75, 76 | ax-mp 5 |
. . . . . . . . . . . . . 14
          
         |
78 | 50 | equcoms 1872 |
. . . . . . . . . . . . . . . . . 18
 
               |
79 | 78 | necon3ai 2668 |
. . . . . . . . . . . . . . . . 17
              
  |
80 | | simpllr 777 |
. . . . . . . . . . . . . . . . . . 19
      CovMap 

             |
81 | | simplr 770 |
. . . . . . . . . . . . . . . . . . 19
      CovMap 

         |
82 | | simpr 468 |
. . . . . . . . . . . . . . . . . . 19
      CovMap 

         |
83 | 7 | cvmsdisj 30065 |
. . . . . . . . . . . . . . . . . . 19
     
       |
84 | 80, 81, 82, 83 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . 18
      CovMap 

             |
85 | 84 | ord 384 |
. . . . . . . . . . . . . . . . 17
      CovMap 

       
     |
86 | | inss1 3643 |
. . . . . . . . . . . . . . . . . 18
            |
87 | | sseq0 3769 |
. . . . . . . . . . . . . . . . . 18
          
  
    
        |
88 | 86, 87 | mpan 684 |
. . . . . . . . . . . . . . . . 17
  
           |
89 | 79, 85, 88 | syl56 34 |
. . . . . . . . . . . . . . . 16
      CovMap 

                                  |
90 | | neeq1 2705 |
. . . . . . . . . . . . . . . . 17
         
                       |
91 | | ineq2 3619 |
. . . . . . . . . . . . . . . . . . 19
                                   |
92 | | inindir 3641 |
. . . . . . . . . . . . . . . . . . 19
                          |
93 | 91, 92 | syl6eqr 2523 |
. . . . . . . . . . . . . . . . . 18
                   
        |
94 | 93 | eqeq1d 2473 |
. . . . . . . . . . . . . . . . 17
                    
         |
95 | 90, 94 | imbi12d 327 |
. . . . . . . . . . . . . . . 16
                
 
       
              
 
           |
96 | 89, 95 | syl5ibrcom 230 |
. . . . . . . . . . . . . . 15
      CovMap 

                
                   |
97 | 96 | rexlimdva 2871 |
. . . . . . . . . . . . . 14
     CovMap 
        
        
                   |
98 | 77, 97 | syl5bi 225 |
. . . . . . . . . . . . 13
     CovMap 
                                      |
99 | 98 | impd 438 |
. . . . . . . . . . . 12
     CovMap 
                                      |
100 | 74, 99 | syl5bi 225 |
. . . . . . . . . . 11
     CovMap 
                                        |
101 | 100 | ralrimiv 2808 |
. . . . . . . . . 10
     CovMap 
                                        |
102 | | inss1 3643 |
. . . . . . . . . . . . 13
        |
103 | | resabs1 5139 |
. . . . . . . . . . . . 13
       
                      |
104 | 102, 103 | ax-mp 5 |
. . . . . . . . . . . 12
 
         
         |
105 | 7 | cvmshmeo 30066 |
. . . . . . . . . . . . . 14
     
     ↾t     ↾t     |
106 | 105 | adantll 728 |
. . . . . . . . . . . . 13
     CovMap 
           ↾t    
↾t     |
107 | 5 | adantr 472 |
. . . . . . . . . . . . . . 15
     CovMap 
         |
108 | 9 | sselda 3418 |
. . . . . . . . . . . . . . . 16
     CovMap 
         |
109 | | elssuni 4219 |
. . . . . . . . . . . . . . . 16
    |
110 | 108, 109 | syl 17 |
. . . . . . . . . . . . . . 15
     CovMap 
          |
111 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
   |
112 | 111 | restuni 20255 |
. . . . . . . . . . . . . . 15
     
↾t    |
113 | 107, 110,
112 | syl2anc 673 |
. . . . . . . . . . . . . 14
     CovMap 
         ↾t    |
114 | 102, 113 | syl5sseq 3466 |
. . . . . . . . . . . . 13
     CovMap 
       
        ↾t    |
115 | | eqid 2471 |
. . . . . . . . . . . . . 14
  ↾t   
↾t   |
116 | 115 | hmeores 20863 |
. . . . . . . . . . . . 13
      ↾t     ↾t   
        ↾t  
              ↾t  ↾t             ↾t 
↾t      
           |
117 | 106, 114,
116 | syl2anc 673 |
. . . . . . . . . . . 12
     CovMap 
                     ↾t 
↾t             ↾t  ↾t                  |
118 | 104, 117 | syl5eqelr 2554 |
. . . . . . . . . . 11
     CovMap 
                   ↾t 
↾t             ↾t  ↾t                  |
119 | 102 | a1i 11 |
. . . . . . . . . . . . 13
     CovMap 
       
        |
120 | | simpr 468 |
. . . . . . . . . . . . 13
     CovMap 
         |
121 | | restabs 20258 |
. . . . . . . . . . . . 13
        
   ↾t  ↾t          ↾t           |
122 | 107, 119,
120, 121 | syl3anc 1292 |
. . . . . . . . . . . 12
     CovMap 
        
↾t  ↾t          ↾t           |
123 | | incom 3616 |
. . . . . . . . . . . . . . . . 17
               |
124 | | cnvresima 5331 |
. . . . . . . . . . . . . . . . 17
               |
125 | 123, 124 | eqtr4i 2496 |
. . . . . . . . . . . . . . . 16
               |
126 | 125 | imaeq2i 5172 |
. . . . . . . . . . . . . . 15
 
                         |
127 | 3 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
     CovMap 
        CovMap    |
128 | | simplr 770 |
. . . . . . . . . . . . . . . . . 18
     CovMap 
             |
129 | 7 | cvmsf1o 30067 |
. . . . . . . . . . . . . . . . . 18
   CovMap     
         |
130 | 127, 128,
120, 129 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
     CovMap 
               |
131 | | f1ofo 5835 |
. . . . . . . . . . . . . . . . 17
 
    
        |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . 16
     CovMap 
               |
133 | 42 | adantr 472 |
. . . . . . . . . . . . . . . 16
     CovMap 
         |
134 | | foimacnv 5845 |
. . . . . . . . . . . . . . . 16
        
               |
135 | 132, 133,
134 | syl2anc 673 |
. . . . . . . . . . . . . . 15
     CovMap 
                      |
136 | 126, 135 | syl5eq 2517 |
. . . . . . . . . . . . . 14
     CovMap 
                      |
137 | 136 | oveq2d 6324 |
. . . . . . . . . . . . 13
     CovMap 
        
↾t 
↾t      
         
↾t 
↾t    |
138 | | cvmtop2 30056 |
. . . . . . . . . . . . . . . 16
  CovMap 
  |
139 | 3, 138 | syl 17 |
. . . . . . . . . . . . . . 15
    CovMap 

    
  |
140 | 7 | cvmsrcl 30059 |
. . . . . . . . . . . . . . . 16
       |
141 | 140 | adantl 473 |
. . . . . . . . . . . . . . 15
    CovMap 

    
  |
142 | | restabs 20258 |
. . . . . . . . . . . . . . 15
    
↾t 
↾t   ↾t    |
143 | 139, 42, 141, 142 | syl3anc 1292 |
. . . . . . . . . . . . . 14
    CovMap 

       ↾t  ↾t   ↾t    |
144 | 143 | adantr 472 |
. . . . . . . . . . . . 13
     CovMap 
        
↾t 
↾t   ↾t    |
145 | 137, 144 | eqtrd 2505 |
. . . . . . . . . . . 12
     CovMap 
        
↾t 
↾t      
         ↾t    |
146 | 122, 145 | oveq12d 6326 |
. . . . . . . . . . 11
     CovMap 
          ↾t  ↾t             ↾t 
↾t      
           ↾t           
↾t     |
147 | 118, 146 | eleqtrd 2551 |
. . . . . . . . . 10
     CovMap 
                  ↾t            ↾t     |
148 | 101, 147 | jca 541 |
. . . . . . . . 9
     CovMap 
        
                             
           ↾t            ↾t      |
149 | 148 | ralrimiva 2809 |
. . . . . . . 8
    CovMap 

     
                                 
         ↾t            ↾t      |
150 | 56 | rgenw 2768 |
. . . . . . . . 9

        |
151 | 50 | cbvmptv 4488 |
. . . . . . . . . 10
                   |
152 | | sneq 3969 |
. . . . . . . . . . . . 13
                     |
153 | 152 | difeq2d 3540 |
. . . . . . . . . . . 12
        

                                 |
154 | | ineq1 3618 |
. . . . . . . . . . . . 13
                     |
155 | 154 | eqeq1d 2473 |
. . . . . . . . . . . 12
                       |
156 | 153, 155 | raleqbidv 2987 |
. . . . . . . . . . 11
                          
                                 |
157 | | reseq2 5106 |
. . . . . . . . . . . 12
                     |
158 | | oveq2 6316 |
. . . . . . . . . . . . 13
        
↾t   ↾t           |
159 | 158 | oveq1d 6323 |
. . . . . . . . . . . 12
          ↾t    
↾t     ↾t           
↾t     |
160 | 157, 159 | eleq12d 2543 |
. . . . . . . . . . 11
            
↾t     ↾t  
          
↾t           
↾t      |
161 | 156, 160 | anbi12d 725 |
. . . . . . . . . 10
                               ↾t     ↾t   
 
                             
           ↾t            ↾t       |
162 | 151, 161 | ralrnmpt 6046 |
. . . . . . . . 9
 

       
           
               
    ↾t    
↾t    
                                 
         ↾t            ↾t       |
163 | 150, 162 | ax-mp 5 |
. . . . . . . 8
 
                                ↾t     ↾t   

 
                             
           ↾t            ↾t      |
164 | 149, 163 | sylibr 217 |
. . . . . . 7
    CovMap 

     
           
               
    ↾t    
↾t      |
165 | 73, 164 | jca 541 |
. . . . . 6
    CovMap 

                                                      ↾t     ↾t       |
166 | 7 | cvmscbv 30053 |
. . . . . . . 8
                       
    ↾t    
↾t        |
167 | 166 | cvmsval 30061 |
. . . . . . 7
                                                    
                                ↾t     ↾t         |
168 | 5, 167 | syl 17 |
. . . . . 6
    CovMap 

     

           

                                    
                                ↾t     ↾t         |
169 | 2, 32, 165, 168 | mpbir3and 1213 |
. . . . 5
    CovMap 

                    |
170 | | ne0i 3728 |
. . . . 5
                    |
171 | 169, 170 | syl 17 |
. . . 4
    CovMap 

           |
172 | 171 | ex 441 |
. . 3
   CovMap 
             |
173 | 172 | exlimdv 1787 |
. 2
   CovMap 
  
           |
174 | 1, 173 | syl5bi 225 |
1
   CovMap 
             |