Step | Hyp | Ref
| Expression |
1 | | haustop 20424 |
. . 3

  |
2 | | xkotop 20680 |
. . 3
 
       |
3 | 1, 2 | sylan2 482 |
. 2
 
       |
4 | | eqid 2471 |
. . . . . . . 8
         |
5 | 4 | xkouni 20691 |
. . . . . . 7
 
          |
6 | 1, 5 | sylan2 482 |
. . . . . 6
 
          |
7 | 6 | eleq2d 2534 |
. . . . 5
 
            |
8 | 6 | eleq2d 2534 |
. . . . 5
 
            |
9 | 7, 8 | anbi12d 725 |
. . . 4
 
    

 
       
       |
10 | | simprl 772 |
. . . . . . . . . 10
               |
11 | | eqid 2471 |
. . . . . . . . . . 11
   |
12 | | eqid 2471 |
. . . . . . . . . . 11
   |
13 | 11, 12 | cnf 20339 |
. . . . . . . . . 10
           |
14 | 10, 13 | syl 17 |
. . . . . . . . 9
                   |
15 | | ffn 5739 |
. . . . . . . . 9
          |
16 | 14, 15 | syl 17 |
. . . . . . . 8
              |
17 | | simprr 774 |
. . . . . . . . . 10
               |
18 | 11, 12 | cnf 20339 |
. . . . . . . . . 10
           |
19 | 17, 18 | syl 17 |
. . . . . . . . 9
                   |
20 | | ffn 5739 |
. . . . . . . . 9
          |
21 | 19, 20 | syl 17 |
. . . . . . . 8
              |
22 | | eqfnfv 5991 |
. . . . . . . 8
  
 

              |
23 | 16, 21, 22 | syl2anc 673 |
. . . . . . 7
           
              |
24 | 23 | necon3abid 2679 |
. . . . . 6
           
              |
25 | | rexnal 2836 |
. . . . . . 7
          
             |
26 | | df-ne 2643 |
. . . . . . . . . 10
        
          |
27 | | simpllr 777 |
. . . . . . . . . . . 12
   
        
          
  |
28 | 14 | adantr 472 |
. . . . . . . . . . . . 13
   
        
          
        |
29 | | simprl 772 |
. . . . . . . . . . . . 13
   
        
          
   |
30 | 28, 29 | ffvelrnd 6038 |
. . . . . . . . . . . 12
   
        
          
       |
31 | 19 | adantr 472 |
. . . . . . . . . . . . 13
   
        
          
        |
32 | 31, 29 | ffvelrnd 6038 |
. . . . . . . . . . . 12
   
        
          
       |
33 | | simprr 774 |
. . . . . . . . . . . 12
   
        
          
          |
34 | 12 | hausnei 20421 |
. . . . . . . . . . . 12
                      


    
   

    |
35 | 27, 30, 32, 33, 34 | syl13anc 1294 |
. . . . . . . . . . 11
   
        
          


    
   

    |
36 | 35 | expr 626 |
. . . . . . . . . 10
   
       
          


    
   

     |
37 | 26, 36 | syl5bir 226 |
. . . . . . . . 9
   
       
           

    
   

     |
38 | | simp-4l 784 |
. . . . . . . . . . . . 13
        
       

    
   

      |
39 | 1 | ad4antlr 747 |
. . . . . . . . . . . . 13
        
       

    
   

      |
40 | | simplr 770 |
. . . . . . . . . . . . . 14
        
       

    
   

       |
41 | 40 | snssd 4108 |
. . . . . . . . . . . . 13
        
       

    
   

         |
42 | 11 | toptopon 20025 |
. . . . . . . . . . . . . . . 16

TopOn     |
43 | 38, 42 | sylib 201 |
. . . . . . . . . . . . . . 15
        
       

    
   

    TopOn     |
44 | | restsn2 20264 |
. . . . . . . . . . . . . . 15
  TopOn     
↾t         |
45 | 43, 40, 44 | syl2anc 673 |
. . . . . . . . . . . . . 14
        
       

    
   

     ↾t         |
46 | | snfi 7668 |
. . . . . . . . . . . . . . 15
 
 |
47 | | discmp 20490 |
. . . . . . . . . . . . . . 15
        |
48 | 46, 47 | mpbi 213 |
. . . . . . . . . . . . . 14
    |
49 | 45, 48 | syl6eqel 2557 |
. . . . . . . . . . . . 13
        
       

    
   

     ↾t      |
50 | | simprll 780 |
. . . . . . . . . . . . 13
        
       

    
   

      |
51 | 11, 38, 39, 41, 49, 50 | xkoopn 20681 |
. . . . . . . . . . . 12
        
       

    
   

            
       |
52 | | simprlr 781 |
. . . . . . . . . . . . 13
        
       

    
   

      |
53 | 11, 38, 39, 41, 49, 52 | xkoopn 20681 |
. . . . . . . . . . . 12
        
       

    
   

            
       |
54 | 10 | ad2antrr 740 |
. . . . . . . . . . . . 13
        
       

    
   

        |
55 | 16 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
        
       

    
   

       |
56 | | fnsnfv 5940 |
. . . . . . . . . . . . . . 15
  
 
     
        |
57 | 55, 40, 56 | syl2anc 673 |
. . . . . . . . . . . . . 14
        
       

    
   

                  |
58 | | simprr1 1078 |
. . . . . . . . . . . . . . 15
        
       

    
   

          |
59 | 58 | snssd 4108 |
. . . . . . . . . . . . . 14
        
       

    
   

            |
60 | 57, 59 | eqsstr3d 3453 |
. . . . . . . . . . . . 13
        
       

    
   

            |
61 | | imaeq1 5169 |
. . . . . . . . . . . . . . 15
               |
62 | 61 | sseq1d 3445 |
. . . . . . . . . . . . . 14
                 |
63 | 62 | elrab 3184 |
. . . . . . . . . . . . 13
         
             |
64 | 54, 60, 63 | sylanbrc 677 |
. . . . . . . . . . . 12
        
       

    
   

                |
65 | 17 | ad2antrr 740 |
. . . . . . . . . . . . 13
        
       

    
   

        |
66 | 21 | ad2antrr 740 |
. . . . . . . . . . . . . . 15
        
       

    
   

       |
67 | | fnsnfv 5940 |
. . . . . . . . . . . . . . 15
  
 
     
        |
68 | 66, 40, 67 | syl2anc 673 |
. . . . . . . . . . . . . 14
        
       

    
   

                  |
69 | | simprr2 1079 |
. . . . . . . . . . . . . . 15
        
       

    
   

          |
70 | 69 | snssd 4108 |
. . . . . . . . . . . . . 14
        
       

    
   

            |
71 | 68, 70 | eqsstr3d 3453 |
. . . . . . . . . . . . 13
        
       

    
   

            |
72 | | imaeq1 5169 |
. . . . . . . . . . . . . . 15
               |
73 | 72 | sseq1d 3445 |
. . . . . . . . . . . . . 14
                 |
74 | 73 | elrab 3184 |
. . . . . . . . . . . . 13
         
             |
75 | 65, 71, 74 | sylanbrc 677 |
. . . . . . . . . . . 12
        
       

    
   

                |
76 | | inrab 3706 |
. . . . . . . . . . . . 13
          
        
                     |
77 | | simpllr 777 |
. . . . . . . . . . . . . . . . . 18
     
                                 |
78 | 11, 12 | cnf 20339 |
. . . . . . . . . . . . . . . . . . . 20
           |
79 | | fdm 5745 |
. . . . . . . . . . . . . . . . . . . 20
          |
80 | 78, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
  
   |
81 | 80 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
     
                             
   |
82 | 77, 81 | eleqtrrd 2552 |
. . . . . . . . . . . . . . . . 17
     
                                |
83 | | simprr3 1080 |
. . . . . . . . . . . . . . . . . . . 20
        
       

    
   

        |
84 | 83 | adantr 472 |
. . . . . . . . . . . . . . . . . . 19
     
                              
   |
85 | | sseq0 3769 |
. . . . . . . . . . . . . . . . . . . 20
         
           |
86 | 85 | expcom 442 |
. . . . . . . . . . . . . . . . . . 19
  
       
          |
87 | 84, 86 | syl 17 |
. . . . . . . . . . . . . . . . . 18
     
                                      
         |
88 | | imadisj 5193 |
. . . . . . . . . . . . . . . . . . 19
             |
89 | | disjsn 4023 |
. . . . . . . . . . . . . . . . . . 19
       |
90 | 88, 89 | bitri 257 |
. . . . . . . . . . . . . . . . . 18
      
  |
91 | 87, 90 | syl6ib 234 |
. . . . . . . . . . . . . . . . 17
     
                                      
   |
92 | 82, 91 | mt2d 121 |
. . . . . . . . . . . . . . . 16
     
                                        |
93 | | ssin 3645 |
. . . . . . . . . . . . . . . 16
              
          |
94 | 92, 93 | sylnibr 312 |
. . . . . . . . . . . . . . 15
     
                                              |
95 | 94 | ralrimiva 2809 |
. . . . . . . . . . . . . 14
        
       

    
   

             
         |
96 | | rabeq0 3757 |
. . . . . . . . . . . . . 14
                   
                  |
97 | 95, 96 | sylibr 217 |
. . . . . . . . . . . . 13
        
       

    
   

                        |
98 | 76, 97 | syl5eq 2517 |
. . . . . . . . . . . 12
        
       

    
   

             
              |
99 | | eleq2 2538 |
. . . . . . . . . . . . . 14
         
          
    |
100 | | ineq1 3618 |
. . . . . . . . . . . . . . 15
         
             
   |
101 | 100 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
         
     
        
    |
102 | 99, 101 | 3anbi13d 1367 |
. . . . . . . . . . . . 13
         
     
          
                |
103 | | eleq2 2538 |
. . . . . . . . . . . . . 14
         
          
    |
104 | | ineq2 3619 |
. . . . . . . . . . . . . . 15
         
          
                          |
105 | 104 | eqeq1d 2473 |
. . . . . . . . . . . . . 14
         
           
   
        
        
     |
106 | 103, 105 | 3anbi23d 1368 |
. . . . . . . . . . . . 13
         
            
                       
                                    |
107 | 102, 106 | rspc2ev 3149 |
. . . . . . . . . . . 12
            
            
             

        
          
              
           

    |
108 | 51, 53, 64, 75, 98, 107 | syl113anc 1304 |
. . . . . . . . . . 11
        
       

    
   

                

    |
109 | 108 | expr 626 |
. . . . . . . . . 10
        
      
 
             
           

     |
110 | 109 | rexlimdvva 2878 |
. . . . . . . . 9
   
       
   

    
   

              

     |
111 | 37, 110 | syld 44 |
. . . . . . . 8
   
       
                       

     |
112 | 111 | rexlimdva 2871 |
. . . . . . 7
            
         
           

     |
113 | 25, 112 | syl5bir 226 |
. . . . . 6
                                   

     |
114 | 24, 113 | sylbid 223 |
. . . . 5
            
           

     |
115 | 114 | ex 441 |
. . . 4
 
    

   
           

      |
116 | 9, 115 | sylbird 243 |
. . 3
 
         
                 

      |
117 | 116 | ralrimivv 2813 |
. 2
 
 
                          

     |
118 | | eqid 2471 |
. . 3
           |
119 | 118 | ishaus 20415 |
. 2
            
                        

      |
120 | 3, 117, 119 | sylanbrc 677 |
1
 
       |