Step | Hyp | Ref
| Expression |
1 | | iscn 13364 |
. . . 4
  TopOn  TopOn  
        
         |
2 | 1 | simprbda 383 |
. . 3
   TopOn  TopOn  

        |
3 | | eqid 2177 |
. . . . . . 7
   |
4 | 3 | cncnpi 13395 |
. . . . . 6
   
          |
5 | 4 | ralrimiva 2550 |
. . . . 5
              |
6 | 5 | adantl 277 |
. . . 4
   TopOn  TopOn  

             |
7 | | toponuni 13180 |
. . . . . 6
 TopOn 
   |
8 | 7 | ad2antrr 488 |
. . . . 5
   TopOn  TopOn  

     |
9 | 8 | raleqdv 2678 |
. . . 4
   TopOn  TopOn  

   
     
            |
10 | 6, 9 | mpbird 167 |
. . 3
   TopOn  TopOn  

  
        |
11 | 2, 10 | jca 306 |
. 2
   TopOn  TopOn  

                 |
12 | | simprl 529 |
. . 3
   TopOn  TopOn  
     
              |
13 | | cnvimass 4987 |
. . . . . . . . . 10
    
 |
14 | | fdm 5367 |
. . . . . . . . . . 11
       |
15 | 14 | adantl 277 |
. . . . . . . . . 10
    TopOn 
TopOn  
     
  |
16 | 13, 15 | sseqtrid 3205 |
. . . . . . . . 9
    TopOn 
TopOn  
             |
17 | | ssralv 3219 |
. . . . . . . . 9
       
                      |
18 | 16, 17 | syl 14 |
. . . . . . . 8
    TopOn 
TopOn  
       
                      |
19 | | simp-4l 541 |
. . . . . . . . . . . 12
     TopOn 
TopOn   
                   TopOn    |
20 | | simp-4r 542 |
. . . . . . . . . . . 12
     TopOn 
TopOn   
                   TopOn    |
21 | | topontop 13179 |
. . . . . . . . . . . . . 14
 TopOn 
  |
22 | 20, 21 | syl 14 |
. . . . . . . . . . . . 13
     TopOn 
TopOn   
                     |
23 | | simprr 531 |
. . . . . . . . . . . . 13
     TopOn 
TopOn   
                           |
24 | | cnprcl2k 13373 |
. . . . . . . . . . . . 13
  TopOn        
  |
25 | 19, 22, 23, 24 | syl3anc 1238 |
. . . . . . . . . . . 12
     TopOn 
TopOn   
                     |
26 | | simpllr 534 |
. . . . . . . . . . . 12
     TopOn 
TopOn   
                     |
27 | | ffn 5361 |
. . . . . . . . . . . . . 14
    
  |
28 | 27 | ad2antlr 489 |
. . . . . . . . . . . . 13
     TopOn 
TopOn   
                     |
29 | | simprl 529 |
. . . . . . . . . . . . 13
     TopOn 
TopOn   
                          |
30 | | elpreima 5631 |
. . . . . . . . . . . . . 14
                |
31 | 30 | simplbda 384 |
. . . . . . . . . . . . 13
 
            |
32 | 28, 29, 31 | syl2anc 411 |
. . . . . . . . . . . 12
     TopOn 
TopOn   
                         |
33 | | icnpimaex 13378 |
. . . . . . . . . . . 12
   TopOn  TopOn 

            


       |
34 | 19, 20, 25, 23, 26, 32, 33 | syl33anc 1253 |
. . . . . . . . . . 11
     TopOn 
TopOn   
                   

       |
35 | | simpllr 534 |
. . . . . . . . . . . . . . 15
      TopOn  TopOn  
      
                    |
36 | 35 | ffund 5365 |
. . . . . . . . . . . . . 14
      TopOn  TopOn  
      
                |
37 | | toponss 13191 |
. . . . . . . . . . . . . . . 16
  TopOn     |
38 | 19, 37 | sylan 283 |
. . . . . . . . . . . . . . 15
      TopOn  TopOn  
      
                |
39 | 35 | fdmd 5368 |
. . . . . . . . . . . . . . 15
      TopOn  TopOn  
      
                |
40 | 38, 39 | sseqtrrd 3194 |
. . . . . . . . . . . . . 14
      TopOn  TopOn  
      
                |
41 | | funimass3 5628 |
. . . . . . . . . . . . . 14
                |
42 | 36, 40, 41 | syl2anc 411 |
. . . . . . . . . . . . 13
      TopOn  TopOn  
      
                  
        |
43 | 42 | anbi2d 464 |
. . . . . . . . . . . 12
      TopOn  TopOn  
      
                   
           |
44 | 43 | rexbidva 2474 |
. . . . . . . . . . 11
     TopOn 
TopOn   
                    

   
            |
45 | 34, 44 | mpbid 147 |
. . . . . . . . . 10
     TopOn 
TopOn   
                   

        |
46 | 45 | expr 375 |
. . . . . . . . 9
     TopOn 
TopOn   
                   
         |
47 | 46 | ralimdva 2544 |
. . . . . . . 8
    TopOn 
TopOn  
                            
         |
48 | 18, 47 | syld 45 |
. . . . . . 7
    TopOn 
TopOn  
       
              
         |
49 | 48 | impr 379 |
. . . . . 6
    TopOn 
TopOn  
                      

        |
50 | 49 | an32s 568 |
. . . . 5
    TopOn 
TopOn                         

        |
51 | | topontop 13179 |
. . . . . . 7
 TopOn 
  |
52 | 51 | ad3antrrr 492 |
. . . . . 6
    TopOn 
TopOn                    |
53 | | eltop2 13237 |
. . . . . 6
               
         |
54 | 52, 53 | syl 14 |
. . . . 5
    TopOn 
TopOn                                
         |
55 | 50, 54 | mpbird 167 |
. . . 4
    TopOn 
TopOn                         |
56 | 55 | ralrimiva 2550 |
. . 3
   TopOn  TopOn  
     
        
       |
57 | 1 | adantr 276 |
. . 3
   TopOn  TopOn  
     
        
 
     
         |
58 | 12, 56, 57 | mpbir2and 944 |
. 2
   TopOn  TopOn  
     
            |
59 | 11, 58 | impbida 596 |
1
  TopOn  TopOn  
        
          |