Step | Hyp | Ref
| Expression |
1 | | cvmtop1 30055 |
. . . . . 6
  CovMap 
  |
2 | 1 | 3ad2ant1 1051 |
. . . . 5
   CovMap     
   |
3 | | cvmcov.1 |
. . . . . . . 8
                       
    ↾t    
↾t        |
4 | 3 | cvmsuni 30064 |
. . . . . . 7
             |
5 | 4 | 3ad2ant2 1052 |
. . . . . 6
   CovMap     
         |
6 | 3 | cvmsss 30062 |
. . . . . . . 8
       |
7 | 6 | 3ad2ant2 1052 |
. . . . . . 7
   CovMap     
   |
8 | 7 | unissd 4214 |
. . . . . 6
   CovMap     
     |
9 | 5, 8 | eqsstr3d 3453 |
. . . . 5
   CovMap     
         |
10 | | eqid 2471 |
. . . . . 6
   |
11 | 10 | restuni 20255 |
. . . . 5
               
↾t         |
12 | 2, 9, 11 | syl2anc 673 |
. . . 4
   CovMap     
        ↾t         |
13 | 12 | difeq1d 3539 |
. . 3
   CovMap     
        
       ↾t               |
14 | | unisng 4206 |
. . . . . . 7
   
  |
15 | 14 | 3ad2ant3 1053 |
. . . . . 6
   CovMap     
   
  |
16 | 15 | uneq2d 3579 |
. . . . 5
   CovMap     
                    |
17 | | uniun 4209 |
. . . . . 6
                    |
18 | | undif1 3833 |
. . . . . . . . 9
             |
19 | | simp3 1032 |
. . . . . . . . . . 11
   CovMap     
   |
20 | 19 | snssd 4108 |
. . . . . . . . . 10
   CovMap     
     |
21 | | ssequn2 3598 |
. . . . . . . . . 10
         |
22 | 20, 21 | sylib 201 |
. . . . . . . . 9
   CovMap     
 
     |
23 | 18, 22 | syl5eq 2517 |
. . . . . . . 8
   CovMap     
           |
24 | 23 | unieqd 4200 |
. . . . . . 7
   CovMap     
             |
25 | 24, 5 | eqtrd 2505 |
. . . . . 6
   CovMap     
                 |
26 | 17, 25 | syl5eqr 2519 |
. . . . 5
   CovMap     
                  |
27 | 16, 26 | eqtr3d 2507 |
. . . 4
   CovMap     
               |
28 | | difss 3549 |
. . . . . . 7
   
 |
29 | 28 | unissi 4213 |
. . . . . 6
    
  |
30 | 29, 5 | syl5sseq 3466 |
. . . . 5
   CovMap     
     
       |
31 | | uniiun 4322 |
. . . . . . . 8
            |
32 | 31 | ineq2i 3622 |
. . . . . . 7
                |
33 | | incom 3616 |
. . . . . . 7
  
            |
34 | | iunin2 4333 |
. . . . . . 7
         
       |
35 | 32, 33, 34 | 3eqtr4i 2503 |
. . . . . 6
  
             |
36 | | eldifsn 4088 |
. . . . . . . . . 10
    

   |
37 | | nesym 2699 |
. . . . . . . . . . . 12

  |
38 | 3 | cvmsdisj 30065 |
. . . . . . . . . . . . . 14
     
       |
39 | 38 | 3expa 1231 |
. . . . . . . . . . . . 13
       
 

    |
40 | 39 | ord 384 |
. . . . . . . . . . . 12
       
 
     |
41 | 37, 40 | syl5bi 225 |
. . . . . . . . . . 11
       
       |
42 | 41 | impr 631 |
. . . . . . . . . 10
       

      |
43 | 36, 42 | sylan2b 483 |
. . . . . . . . 9
       

        |
44 | 43 | iuneq2dv 4291 |
. . . . . . . 8
     
                 |
45 | 44 | 3adant1 1048 |
. . . . . . 7
   CovMap     
                 |
46 | | iun0 4325 |
. . . . . . 7
       |
47 | 45, 46 | syl6eq 2521 |
. . . . . 6
   CovMap     
           |
48 | 35, 47 | syl5eq 2517 |
. . . . 5
   CovMap     
          |
49 | | uneqdifeq 3847 |
. . . . 5
                 
              
               |
50 | 30, 48, 49 | syl2anc 673 |
. . . 4
   CovMap     
             
               |
51 | 27, 50 | mpbid 215 |
. . 3
   CovMap     
        
      |
52 | 13, 51 | eqtr3d 2507 |
. 2
   CovMap     
   
↾t               |
53 | | uniexg 6607 |
. . . . . 6
        |
54 | 53 | 3ad2ant2 1052 |
. . . . 5
   CovMap     
    |
55 | 5, 54 | eqeltrrd 2550 |
. . . 4
   CovMap     
        |
56 | | resttop 20253 |
. . . 4
        
↾t         |
57 | 2, 55, 56 | syl2anc 673 |
. . 3
   CovMap     
  ↾t         |
58 | | elssuni 4219 |
. . . . . . . . . . 11
    |
59 | 58 | adantl 473 |
. . . . . . . . . 10
    CovMap 
         |
60 | 5 | adantr 472 |
. . . . . . . . . 10
    CovMap 
              |
61 | 59, 60 | sseqtrd 3454 |
. . . . . . . . 9
    CovMap 
             |
62 | | df-ss 3404 |
. . . . . . . . 9
     
         |
63 | 61, 62 | sylib 201 |
. . . . . . . 8
    CovMap 
      
        |
64 | 2 | adantr 472 |
. . . . . . . . 9
    CovMap 
        |
65 | 55 | adantr 472 |
. . . . . . . . 9
    CovMap 
             |
66 | 7 | sselda 3418 |
. . . . . . . . 9
    CovMap 
        |
67 | | elrestr 15405 |
. . . . . . . . 9
        
       ↾t         |
68 | 64, 65, 66, 67 | syl3anc 1292 |
. . . . . . . 8
    CovMap 
      
       ↾t         |
69 | 63, 68 | eqeltrrd 2550 |
. . . . . . 7
    CovMap 
      
↾t         |
70 | 69 | ex 441 |
. . . . . 6
   CovMap     
 
 ↾t          |
71 | 70 | ssrdv 3424 |
. . . . 5
   CovMap     
 
↾t         |
72 | 71 | ssdifssd 3560 |
. . . 4
   CovMap     
    
 ↾t         |
73 | | uniopn 20004 |
. . . 4
  
↾t      
     ↾t              ↾t         |
74 | 57, 72, 73 | syl2anc 673 |
. . 3
   CovMap     
       ↾t         |
75 | | eqid 2471 |
. . . 4
  ↾t         ↾t        |
76 | 75 | opncld 20125 |
. . 3
  
↾t      
      ↾t          
↾t                 ↾t          |
77 | 57, 74, 76 | syl2anc 673 |
. 2
   CovMap     
   
↾t                 ↾t          |
78 | 52, 77 | eqeltrrd 2550 |
1
   CovMap     
     ↾t          |