Step | Hyp | Ref
| Expression |
1 | | simpll3 1050 |
. . . . 5
    TopOn 

↾t                 
                        ↾t    |
2 | | simpll1 1048 |
. . . . . . 7
    TopOn 

↾t                  
                                 
TopOn    |
3 | | simpll2 1049 |
. . . . . . 7
    TopOn 

↾t                  
                                    |
4 | | simplrl 775 |
. . . . . . 7
    TopOn 

↾t                  
                                 
  |
5 | | simplrr 776 |
. . . . . . 7
    TopOn 

↾t                  
                                    |
6 | | simprl1 1054 |
. . . . . . . . 9
    TopOn 

↾t                  
                                              |
7 | | n0 3709 |
. . . . . . . . 9
                        |
8 | 6, 7 | sylib 201 |
. . . . . . . 8
    TopOn 

↾t                  
                                  

           |
9 | 2 | adantr 471 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
           TopOn    |
10 | | topontop 19952 |
. . . . . . . . . 10
 TopOn 
  |
11 | 9, 10 | syl 17 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
             |
12 | 3 | adantr 471 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
             |
13 | | toponuni 19953 |
. . . . . . . . . . 11
 TopOn 
   |
14 | 9, 13 | syl 17 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
              |
15 | 12, 14 | sseqtrd 3436 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
              |
16 | | inss2 3621 |
. . . . . . . . . 10
                   |
17 | | simpr 467 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
                       |
18 | 16, 17 | sseldi 3398 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
                     |
19 | 4 | adantr 471 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
             |
20 | | inss1 3620 |
. . . . . . . . . 10
           |
21 | 20, 17 | sseldi 3398 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
             |
22 | | eqid 2452 |
. . . . . . . . . 10
   |
23 | 22 | clsndisj 20102 |
. . . . . . . . 9
  

         
  
   |
24 | 11, 15, 18, 19, 21, 23 | syl32anc 1279 |
. . . . . . . 8
     TopOn 

↾t                  
                                 
           
   |
25 | 8, 24 | exlimddv 1785 |
. . . . . . 7
    TopOn 

↾t                  
                                      |
26 | | simprl2 1055 |
. . . . . . . . 9
    TopOn 

↾t                  
                                              |
27 | | n0 3709 |
. . . . . . . . 9
                        |
28 | 26, 27 | sylib 201 |
. . . . . . . 8
    TopOn 

↾t                  
                                  
            |
29 | 2 | adantr 471 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
           TopOn    |
30 | 29, 10 | syl 17 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
             |
31 | 3 | adantr 471 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
             |
32 | 29, 13 | syl 17 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
              |
33 | 31, 32 | sseqtrd 3436 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
              |
34 | | inss2 3621 |
. . . . . . . . . 10
                   |
35 | | simpr 467 |
. . . . . . . . . 10
     TopOn 

↾t                  
                                 
                       |
36 | 34, 35 | sseldi 3398 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
                     |
37 | 5 | adantr 471 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
             |
38 | | inss1 3620 |
. . . . . . . . . 10
           |
39 | 38, 35 | sseldi 3398 |
. . . . . . . . 9
     TopOn 

↾t                  
                                 
             |
40 | 22 | clsndisj 20102 |
. . . . . . . . 9
  

         
  
   |
41 | 30, 33, 36, 37, 39, 40 | syl32anc 1279 |
. . . . . . . 8
     TopOn 

↾t                  
                                 
           
   |
42 | 28, 41 | exlimddv 1785 |
. . . . . . 7
    TopOn 

↾t                  
                                      |
43 | | simprl3 1056 |
. . . . . . . . . 10
    TopOn 

↾t                  
                                   
            |
44 | 2, 10 | syl 17 |
. . . . . . . . . . . 12
    TopOn 

↾t                  
                                 
  |
45 | 2, 13 | syl 17 |
. . . . . . . . . . . . 13
    TopOn 

↾t                  
                                 
   |
46 | 3, 45 | sseqtrd 3436 |
. . . . . . . . . . . 12
    TopOn 

↾t                  
                                     |
47 | 22 | sscls 20082 |
. . . . . . . . . . . 12
              |
48 | 44, 46, 47 | syl2anc 671 |
. . . . . . . . . . 11
    TopOn 

↾t                  
                                            |
49 | 48 | sscond 3538 |
. . . . . . . . . 10
    TopOn 

↾t                  
                                           
    |
50 | 43, 49 | sstrd 3410 |
. . . . . . . . 9
    TopOn 

↾t                  
                                   
    |
51 | | ssv 3420 |
. . . . . . . . . 10
 |
52 | | ssdif 3536 |
. . . . . . . . . 10

  
   |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . 9
  
  |
54 | 50, 53 | syl6ss 3412 |
. . . . . . . 8
    TopOn 

↾t                  
                                   
    |
55 | | disj2 3780 |
. . . . . . . 8
   
       |
56 | 54, 55 | sylibr 217 |
. . . . . . 7
    TopOn 

↾t                  
                                        |
57 | | simprr 771 |
. . . . . . . 8
    TopOn 

↾t                  
                                              |
58 | 48, 57 | sstrd 3410 |
. . . . . . 7
    TopOn 

↾t                  
                                      |
59 | 2, 3, 4, 5, 25, 42, 56, 58 | nconsubb 20449 |
. . . . . 6
    TopOn 

↾t                  
                                  
↾t    |
60 | 59 | expr 624 |
. . . . 5
    TopOn 

↾t                 
                                

 ↾t     |
61 | 1, 60 | mt2d 122 |
. . . 4
    TopOn 

↾t                 
                      
            |
62 | 61 | ex 440 |
. . 3
   TopOn   ↾t   
              
                                   |
63 | 62 | ralrimivva 2795 |
. 2
  TopOn   ↾t    
            
                                   |
64 | | simp1 1009 |
. . 3
  TopOn   ↾t   TopOn    |
65 | 13 | sseq2d 3428 |
. . . . . . 7
 TopOn 

    |
66 | 65 | biimpa 491 |
. . . . . 6
  TopOn      |
67 | 22 | clsss3 20085 |
. . . . . . 7
           
   |
68 | 10, 67 | sylan 478 |
. . . . . 6
  TopOn               |
69 | 66, 68 | syldan 477 |
. . . . 5
  TopOn              |
70 | 13 | adantr 471 |
. . . . 5
  TopOn      |
71 | 69, 70 | sseqtr4d 3437 |
. . . 4
  TopOn             |
72 | 71 | 3adant3 1029 |
. . 3
  TopOn   ↾t             |
73 | | connsub 20447 |
. . 3
  TopOn            
↾t          

            
                                    |
74 | 64, 72, 73 | syl2anc 671 |
. 2
  TopOn   ↾t     ↾t         


            
                                    |
75 | 63, 74 | mpbird 240 |
1
  TopOn   ↾t   
↾t            |