Step | Hyp | Ref
| Expression |
1 | | simpr 461 |
. . . . . . 7
    
    
 
         
  
     |
2 | | simplr1 1030 |
. . . . . . . . . 10
    
    
 
         
  
     |
3 | | n0 3749 |
. . . . . . . . . . 11
  
   
   |
4 | | inss2 3674 |
. . . . . . . . . . . . . 14
   
 |
5 | 4 | sseli 3455 |
. . . . . . . . . . . . 13
  
    |
6 | | eliun 4278 |
. . . . . . . . . . . . . 14
 

  |
7 | | rexn0 3885 |
. . . . . . . . . . . . . 14
    |
8 | 6, 7 | sylbi 195 |
. . . . . . . . . . . . 13
    |
9 | 5, 8 | syl 16 |
. . . . . . . . . . . 12
  
   |
10 | 9 | exlimiv 1689 |
. . . . . . . . . . 11
   
   |
11 | 3, 10 | sylbi 195 |
. . . . . . . . . 10
  

  |
12 | 2, 11 | syl 16 |
. . . . . . . . 9
    
    
 
         
  
  |
13 | | simplll 757 |
. . . . . . . . . 10
    
    
 
         
  
  |
14 | | iuncon.4 |
. . . . . . . . . . 11
 
   |
15 | 14 | ralrimiva 2827 |
. . . . . . . . . 10
 
  |
16 | 13, 15 | syl 16 |
. . . . . . . . 9
    
    
 
         
  

  |
17 | | r19.2z 3872 |
. . . . . . . . 9
  
 
  |
18 | 12, 16, 17 | syl2anc 661 |
. . . . . . . 8
    
    
 
         
  

  |
19 | | eliun 4278 |
. . . . . . . 8
 

  |
20 | 18, 19 | sylibr 212 |
. . . . . . 7
    
    
 
         
  
   |
21 | 1, 20 | sseldd 3460 |
. . . . . 6
    
    
 
         
  

   |
22 | | elun 3600 |
. . . . . 6
  

   |
23 | 21, 22 | sylib 196 |
. . . . 5
    
    
 
         
  

   |
24 | | iuncon.2 |
. . . . . . . 8
 TopOn    |
25 | 13, 24 | syl 16 |
. . . . . . 7
    
    
 
         
  
TopOn    |
26 | | iuncon.3 |
. . . . . . . 8
 
   |
27 | 13, 26 | sylan 471 |
. . . . . . 7
     
    
 
         
      |
28 | 13, 14 | sylan 471 |
. . . . . . 7
     
    
 
         
      |
29 | | iuncon.5 |
. . . . . . . 8
 
  ↾t    |
30 | 13, 29 | sylan 471 |
. . . . . . 7
     
    
 
         
     ↾t    |
31 | | simpllr 758 |
. . . . . . . 8
    
    
 
         
  

   |
32 | 31 | simpld 459 |
. . . . . . 7
    
    
 
         
  
  |
33 | 31 | simprd 463 |
. . . . . . 7
    
    
 
         
  
  |
34 | | simplr2 1031 |
. . . . . . 7
    
    
 
         
  
     |
35 | | simplr3 1032 |
. . . . . . 7
    
    
 
         
  
       |
36 | | nfv 1674 |
. . . . . . . . 9
   
   |
37 | | nfcv 2614 |
. . . . . . . . . . . 12
   |
38 | | nfiu1 4303 |
. . . . . . . . . . . 12
  
 |
39 | 37, 38 | nfin 3660 |
. . . . . . . . . . 11
   
  |
40 | | nfcv 2614 |
. . . . . . . . . . 11
   |
41 | 39, 40 | nfne 2780 |
. . . . . . . . . 10
   
  |
42 | | nfcv 2614 |
. . . . . . . . . . . 12
   |
43 | 42, 38 | nfin 3660 |
. . . . . . . . . . 11
   
  |
44 | 43, 40 | nfne 2780 |
. . . . . . . . . 10
   
  |
45 | | nfcv 2614 |
. . . . . . . . . . 11
     |
46 | | nfcv 2614 |
. . . . . . . . . . . 12
   |
47 | 46, 38 | nfdif 3580 |
. . . . . . . . . . 11
   
  |
48 | 45, 47 | nfss 3452 |
. . . . . . . . . 10
   
    |
49 | 41, 44, 48 | nf3an 1867 |
. . . . . . . . 9
    
 
         |
50 | 36, 49 | nfan 1865 |
. . . . . . . 8
    
    
 
          |
51 | 37, 42 | nfun 3615 |
. . . . . . . . 9
     |
52 | 38, 51 | nfss 3452 |
. . . . . . . 8
      |
53 | 50, 52 | nfan 1865 |
. . . . . . 7
     
    
 
         
    |
54 | 25, 27, 28, 30, 32, 33, 34, 35, 1, 53 | iunconlem 19158 |
. . . . . 6
    
    
 
         
  
  |
55 | | incom 3646 |
. . . . . . . 8
     |
56 | 55, 35 | syl5eqss 3503 |
. . . . . . 7
    
    
 
         
  
       |
57 | | uncom 3603 |
. . . . . . . 8
     |
58 | 1, 57 | syl6sseq 3505 |
. . . . . . 7
    
    
 
         
  
     |
59 | 25, 27, 28, 30, 33, 32, 2, 56, 58, 53 | iunconlem 19158 |
. . . . . 6
    
    
 
         
  
  |
60 | | ioran 490 |
. . . . . 6
 
 
   |
61 | 54, 59, 60 | sylanbrc 664 |
. . . . 5
    
    
 
         
  

   |
62 | 23, 61 | pm2.65da 576 |
. . . 4
   
 
 
   
 
  
        |
63 | 62 | ex 434 |
. . 3
 

       
       
      |
64 | 63 | ralrimivva 2908 |
. 2
  
     
       
      |
65 | 26 | ralrimiva 2827 |
. . . 4
    |
66 | | iunss 4314 |
. . . 4
 
   |
67 | 65, 66 | sylibr 212 |
. . 3
    |
68 | | connsub 19152 |
. . 3
  TopOn  
  
↾t   

   
 
       
       |
69 | 24, 67, 68 | syl2anc 661 |
. 2
   ↾t 
  
     
       
       |
70 | 64, 69 | mpbird 232 |
1
 
↾t     |