Step | Hyp | Ref
| Expression |
1 | | kgencn 20571 |
. 2
  TopOn  TopOn  
  𝑘Gen  
     
   ↾t 
   
↾t        |
2 | | rncmp 20411 |
. . . . . . . 8
      ↾t    |
3 | 2 | adantl 468 |
. . . . . . 7
    TopOn 
TopOn              ↾t    |
4 | | simprr 766 |
. . . . . . . . . . 11
    TopOn 
TopOn                 |
5 | | eqid 2451 |
. . . . . . . . . . . 12
   |
6 | | eqid 2451 |
. . . . . . . . . . . 12
   |
7 | 5, 6 | cnf 20262 |
. . . . . . . . . . 11
           |
8 | | frn 5735 |
. . . . . . . . . . 11
      
   |
9 | 4, 7, 8 | 3syl 18 |
. . . . . . . . . 10
    TopOn 
TopOn                |
10 | | toponuni 19942 |
. . . . . . . . . . 11
 TopOn 
   |
11 | 10 | ad3antrrr 736 |
. . . . . . . . . 10
    TopOn 
TopOn                |
12 | 9, 11 | sseqtr4d 3469 |
. . . . . . . . 9
    TopOn 
TopOn               |
13 | | vex 3048 |
. . . . . . . . . . 11
 |
14 | 13 | rnex 6727 |
. . . . . . . . . 10
 |
15 | 14 | elpw 3957 |
. . . . . . . . 9
 
  |
16 | 12, 15 | sylibr 216 |
. . . . . . . 8
    TopOn 
TopOn            
   |
17 | | oveq2 6298 |
. . . . . . . . . . 11
 
↾t  
↾t    |
18 | 17 | eleq1d 2513 |
. . . . . . . . . 10
   ↾t 
 ↾t     |
19 | | reseq2 5100 |
. . . . . . . . . . 11
       |
20 | 17 | oveq1d 6305 |
. . . . . . . . . . 11
   ↾t     ↾t     |
21 | 19, 20 | eleq12d 2523 |
. . . . . . . . . 10
     
↾t  
    ↾t      |
22 | 18, 21 | imbi12d 322 |
. . . . . . . . 9
    ↾t  
   ↾t      ↾t  
   ↾t       |
23 | 22 | rspcv 3146 |
. . . . . . . 8
       ↾t      ↾t     
↾t     
↾t       |
24 | 16, 23 | syl 17 |
. . . . . . 7
    TopOn 
TopOn              
   ↾t  
   ↾t      ↾t      ↾t       |
25 | 3, 24 | mpid 42 |
. . . . . 6
    TopOn 
TopOn              
   ↾t  
   ↾t       
↾t      |
26 | | simplll 768 |
. . . . . . . . . 10
    TopOn 
TopOn             TopOn    |
27 | | ssid 3451 |
. . . . . . . . . . 11
 |
28 | 27 | a1i 11 |
. . . . . . . . . 10
    TopOn 
TopOn               |
29 | | cnrest2 20302 |
. . . . . . . . . 10
  TopOn 
      ↾t      |
30 | 26, 28, 12, 29 | syl3anc 1268 |
. . . . . . . . 9
    TopOn 
TopOn               
  ↾t      |
31 | 4, 30 | mpbid 214 |
. . . . . . . 8
    TopOn 
TopOn               ↾t     |
32 | | cnco 20282 |
. . . . . . . . 9
    ↾t       ↾t            |
33 | 32 | ex 436 |
. . . . . . . 8
  
↾t        ↾t            |
34 | 31, 33 | syl 17 |
. . . . . . 7
    TopOn 
TopOn                  ↾t            |
35 | | cores 5338 |
. . . . . . . . 9

        |
36 | 27, 35 | ax-mp 5 |
. . . . . . . 8
 
     |
37 | 36 | eleq1i 2520 |
. . . . . . 7
      
      |
38 | 34, 37 | syl6ib 230 |
. . . . . 6
    TopOn 
TopOn                  ↾t   
      |
39 | 25, 38 | syld 45 |
. . . . 5
    TopOn 
TopOn              
   ↾t  
   ↾t           |
40 | 39 | ralrimdvva 2812 |
. . . 4
   TopOn  TopOn  
      
   ↾t  
   ↾t                |
41 | | oveq1 6297 |
. . . . . . . . 9
  ↾t     
↾t     |
42 | | oveq1 6297 |
. . . . . . . . . 10
  ↾t     
↾t     |
43 | 42 | eleq2d 2514 |
. . . . . . . . 9
  ↾t          
↾t      |
44 | 41, 43 | raleqbidv 3001 |
. . . . . . . 8
  ↾t           
 
↾t        ↾t      |
45 | 44 | rspcv 3146 |
. . . . . . 7
  ↾t            
 
↾t        ↾t      |
46 | | elpwi 3960 |
. . . . . . . . . . . 12
 
  |
47 | 46 | adantl 468 |
. . . . . . . . . . 11
    TopOn 
TopOn            |
48 | 47 | resabs1d 5134 |
. . . . . . . . . 10
    TopOn 
TopOn            
   |
49 | | idcn 20273 |
. . . . . . . . . . . 12
 TopOn 
     |
50 | 49 | ad3antrrr 736 |
. . . . . . . . . . 11
    TopOn 
TopOn               |
51 | 10 | ad3antrrr 736 |
. . . . . . . . . . . 12
    TopOn 
TopOn             |
52 | 47, 51 | sseqtrd 3468 |
. . . . . . . . . . 11
    TopOn 
TopOn             |
53 | 6 | cnrest 20301 |
. . . . . . . . . . 11
           
↾t     |
54 | 50, 52, 53 | syl2anc 667 |
. . . . . . . . . 10
    TopOn 
TopOn              
↾t     |
55 | 48, 54 | eqeltrrd 2530 |
. . . . . . . . 9
    TopOn 
TopOn             ↾t     |
56 | | coeq2 4993 |
. . . . . . . . . . 11
 
       |
57 | 56 | eleq1d 2513 |
. . . . . . . . . 10
 
 
   ↾t  

   
↾t      |
58 | 57 | rspcv 3146 |
. . . . . . . . 9

   ↾t       ↾t        ↾t   
    ↾t      |
59 | 55, 58 | syl 17 |
. . . . . . . 8
    TopOn 
TopOn           
 
↾t        ↾t        ↾t      |
60 | | coires1 5353 |
. . . . . . . . 9
   
  |
61 | 60 | eleq1i 2520 |
. . . . . . . 8
      ↾t  
   
↾t     |
62 | 59, 61 | syl6ib 230 |
. . . . . . 7
    TopOn 
TopOn           
 
↾t        ↾t       ↾t      |
63 | 45, 62 | syl9r 74 |
. . . . . 6
    TopOn 
TopOn           
↾t                ↾t       |
64 | 63 | com23 81 |
. . . . 5
    TopOn 
TopOn           
         
↾t     
↾t       |
65 | 64 | ralrimdva 2806 |
. . . 4
   TopOn  TopOn  
      
            ↾t      ↾t       |
66 | 40, 65 | impbid 194 |
. . 3
   TopOn  TopOn  
      
   ↾t  
   ↾t    
           |
67 | 66 | pm5.32da 647 |
. 2
  TopOn  TopOn  
          ↾t 
   
↾t                       |
68 | 1, 67 | bitrd 257 |
1
  TopOn  TopOn  
  𝑘Gen  
     
            |