Step | Hyp | Ref
| Expression |
1 | | uniss 4222 |
. . . . . . 7
 𝑘Gen  
 𝑘Gen    |
2 | | kgenval 20562 |
. . . . . . . . 9
 TopOn 
𝑘Gen    
   ↾t 
  
↾t      |
3 | | ssrab2 3516 |
. . . . . . . . 9
  
   ↾t 
  
↾t   
  |
4 | 2, 3 | syl6eqss 3484 |
. . . . . . . 8
 TopOn 
𝑘Gen 
   |
5 | | sspwuni 4370 |
. . . . . . . 8
 𝑘Gen    𝑘Gen    |
6 | 4, 5 | sylib 200 |
. . . . . . 7
 TopOn 
 𝑘Gen    |
7 | 1, 6 | sylan9ssr 3448 |
. . . . . 6
  TopOn  𝑘Gen      |
8 | | iunin2 4345 |
. . . . . . . . . 10

   
  |
9 | | uniiun 4334 |
. . . . . . . . . . 11
   |
10 | 9 | ineq2i 3633 |
. . . . . . . . . 10
    
  |
11 | | incom 3627 |
. . . . . . . . . 10
       |
12 | 8, 10, 11 | 3eqtr2i 2481 |
. . . . . . . . 9

      |
13 | | cmptop 20422 |
. . . . . . . . . . 11
  ↾t  
↾t    |
14 | 13 | ad2antll 736 |
. . . . . . . . . 10
   TopOn  𝑘Gen      ↾t     ↾t    |
15 | | incom 3627 |
. . . . . . . . . . . 12
     |
16 | | simplr 763 |
. . . . . . . . . . . . . 14
   TopOn  𝑘Gen      ↾t    𝑘Gen    |
17 | 16 | sselda 3434 |
. . . . . . . . . . . . 13
    TopOn 
𝑘Gen     
↾t   
 𝑘Gen    |
18 | | simplrr 772 |
. . . . . . . . . . . . 13
    TopOn 
𝑘Gen     
↾t   
 
↾t    |
19 | | kgeni 20564 |
. . . . . . . . . . . . 13
  𝑘Gen 
 ↾t      ↾t    |
20 | 17, 18, 19 | syl2anc 667 |
. . . . . . . . . . . 12
    TopOn 
𝑘Gen     
↾t   
    ↾t    |
21 | 15, 20 | syl5eqelr 2536 |
. . . . . . . . . . 11
    TopOn 
𝑘Gen     
↾t   
    ↾t    |
22 | 21 | ralrimiva 2804 |
. . . . . . . . . 10
   TopOn  𝑘Gen      ↾t    
   ↾t    |
23 | | iunopn 19940 |
. . . . . . . . . 10
  
↾t 

   ↾t   
   ↾t    |
24 | 14, 22, 23 | syl2anc 667 |
. . . . . . . . 9
   TopOn  𝑘Gen      ↾t    
   ↾t    |
25 | 12, 24 | syl5eqelr 2536 |
. . . . . . . 8
   TopOn  𝑘Gen      ↾t     
  ↾t    |
26 | 25 | expr 620 |
. . . . . . 7
   TopOn  𝑘Gen      
↾t      ↾t     |
27 | 26 | ralrimiva 2804 |
. . . . . 6
  TopOn  𝑘Gen       ↾t      ↾t     |
28 | | elkgen 20563 |
. . . . . . 7
 TopOn 
 
𝑘Gen        ↾t      ↾t       |
29 | 28 | adantr 467 |
. . . . . 6
  TopOn  𝑘Gen     𝑘Gen 
  
   ↾t 
   
↾t       |
30 | 7, 27, 29 | mpbir2and 934 |
. . . . 5
  TopOn  𝑘Gen    𝑘Gen    |
31 | 30 | ex 436 |
. . . 4
 TopOn 
 𝑘Gen  
𝑘Gen     |
32 | 31 | alrimiv 1775 |
. . 3
 TopOn 
   𝑘Gen   𝑘Gen     |
33 | | inss1 3654 |
. . . . . 6
   |
34 | | elssuni 4230 |
. . . . . . . 8
 𝑘Gen   𝑘Gen    |
35 | 34 | ad2antrl 735 |
. . . . . . 7
  TopOn   𝑘Gen 
𝑘Gen   
 𝑘Gen    |
36 | | ssid 3453 |
. . . . . . . . . . . 12
 |
37 | 36 | a1i 11 |
. . . . . . . . . . 11
 TopOn 
  |
38 | | elpwi 3962 |
. . . . . . . . . . . . . . . 16
 
  |
39 | 38 | ad2antrl 735 |
. . . . . . . . . . . . . . 15
  TopOn    
↾t   
  |
40 | | dfss1 3639 |
. . . . . . . . . . . . . . 15

    |
41 | 39, 40 | sylib 200 |
. . . . . . . . . . . . . 14
  TopOn    
↾t        |
42 | 38 | adantr 467 |
. . . . . . . . . . . . . . . 16
   
↾t     |
43 | | resttopon 20189 |
. . . . . . . . . . . . . . . 16
  TopOn    ↾t  TopOn    |
44 | 42, 43 | sylan2 477 |
. . . . . . . . . . . . . . 15
  TopOn    
↾t    
↾t  TopOn    |
45 | | toponmax 19955 |
. . . . . . . . . . . . . . 15
  ↾t  TopOn  
↾t    |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . 14
  TopOn    
↾t     ↾t    |
47 | 41, 46 | eqeltrd 2531 |
. . . . . . . . . . . . 13
  TopOn    
↾t       ↾t    |
48 | 47 | expr 620 |
. . . . . . . . . . . 12
  TopOn      ↾t 
  
↾t     |
49 | 48 | ralrimiva 2804 |
. . . . . . . . . . 11
 TopOn 
    ↾t     ↾t     |
50 | | elkgen 20563 |
. . . . . . . . . . 11
 TopOn 
 𝑘Gen 
     ↾t     ↾t       |
51 | 37, 49, 50 | mpbir2and 934 |
. . . . . . . . . 10
 TopOn 
𝑘Gen    |
52 | | elssuni 4230 |
. . . . . . . . . 10
 𝑘Gen   𝑘Gen    |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
 TopOn 
 𝑘Gen    |
54 | 53, 6 | eqssd 3451 |
. . . . . . . 8
 TopOn 
 𝑘Gen    |
55 | 54 | adantr 467 |
. . . . . . 7
  TopOn   𝑘Gen 
𝑘Gen   
 𝑘Gen    |
56 | 35, 55 | sseqtr4d 3471 |
. . . . . 6
  TopOn   𝑘Gen 
𝑘Gen   
  |
57 | 33, 56 | syl5ss 3445 |
. . . . 5
  TopOn   𝑘Gen 
𝑘Gen   
    |
58 | | inindir 3652 |
. . . . . . . 8
       
   |
59 | 13 | ad2antll 736 |
. . . . . . . . 9
   TopOn   𝑘Gen 
𝑘Gen      
↾t    
↾t    |
60 | | simplrl 771 |
. . . . . . . . . 10
   TopOn   𝑘Gen 
𝑘Gen      
↾t   
𝑘Gen    |
61 | | simprr 767 |
. . . . . . . . . 10
   TopOn   𝑘Gen 
𝑘Gen      
↾t    
↾t    |
62 | | kgeni 20564 |
. . . . . . . . . 10
  𝑘Gen 
 ↾t      ↾t    |
63 | 60, 61, 62 | syl2anc 667 |
. . . . . . . . 9
   TopOn   𝑘Gen 
𝑘Gen      
↾t       ↾t    |
64 | | simplrr 772 |
. . . . . . . . . 10
   TopOn   𝑘Gen 
𝑘Gen      
↾t    𝑘Gen    |
65 | 64, 61, 19 | syl2anc 667 |
. . . . . . . . 9
   TopOn   𝑘Gen 
𝑘Gen      
↾t       ↾t    |
66 | | inopn 19941 |
. . . . . . . . 9
  
↾t 
   ↾t  
 
↾t          ↾t    |
67 | 59, 63, 65, 66 | syl3anc 1269 |
. . . . . . . 8
   TopOn   𝑘Gen 
𝑘Gen      
↾t       
   ↾t    |
68 | 58, 67 | syl5eqel 2535 |
. . . . . . 7
   TopOn   𝑘Gen 
𝑘Gen      
↾t         ↾t    |
69 | 68 | expr 620 |
. . . . . 6
   TopOn   𝑘Gen 
𝑘Gen        ↾t 
    
↾t     |
70 | 69 | ralrimiva 2804 |
. . . . 5
  TopOn   𝑘Gen 
𝑘Gen   
    ↾t       ↾t     |
71 | | elkgen 20563 |
. . . . . 6
 TopOn 
 
 𝑘Gen 
 
     ↾t       ↾t       |
72 | 71 | adantr 467 |
. . . . 5
  TopOn   𝑘Gen 
𝑘Gen   
 
 𝑘Gen 
 
     ↾t       ↾t       |
73 | 57, 70, 72 | mpbir2and 934 |
. . . 4
  TopOn   𝑘Gen 
𝑘Gen   
  𝑘Gen    |
74 | 73 | ralrimivva 2811 |
. . 3
 TopOn 
 𝑘Gen   
𝑘Gen     𝑘Gen    |
75 | | fvex 5880 |
. . . 4
𝑘Gen   |
76 | | istopg 19937 |
. . . 4
 𝑘Gen   𝑘Gen     
𝑘Gen 
 𝑘Gen    𝑘Gen   
𝑘Gen     𝑘Gen      |
77 | 75, 76 | ax-mp 5 |
. . 3
 𝑘Gen      𝑘Gen  
𝑘Gen    𝑘Gen    𝑘Gen     𝑘Gen     |
78 | 32, 74, 77 | sylanbrc 671 |
. 2
 TopOn 
𝑘Gen    |
79 | | istopon 19952 |
. 2
 𝑘Gen  TopOn 
 𝑘Gen   𝑘Gen     |
80 | 78, 54, 79 | sylanbrc 671 |
1
 TopOn 
𝑘Gen  TopOn    |