Step | Hyp | Ref
| Expression |
1 | | simp1r 1055 |
. . . . 5
   TopOn        
   |
2 | | simp2l 1056 |
. . . . 5
   TopOn        
       |
3 | | simp2r 1057 |
. . . . . 6
   TopOn        
   |
4 | | simp1l 1054 |
. . . . . . 7
   TopOn        
 TopOn    |
5 | | toponuni 20019 |
. . . . . . 7
 TopOn 
   |
6 | 4, 5 | syl 17 |
. . . . . 6
   TopOn        
    |
7 | 3, 6 | eleqtrd 2551 |
. . . . 5
   TopOn        
    |
8 | | simp3 1032 |
. . . . 5
   TopOn        
   |
9 | | eqid 2471 |
. . . . . 6
   |
10 | 9 | regsep2 20469 |
. . . . 5
      
   

      |
11 | 1, 2, 7, 8, 10 | syl13anc 1294 |
. . . 4
   TopOn        
  

     |
12 | 11 | 3expia 1233 |
. . 3
   TopOn          


       |
13 | 12 | ralrimivva 2814 |
. 2
  TopOn          


       |
14 | | topontop 20018 |
. . . 4
 TopOn 
  |
15 | 14 | adantr 472 |
. . 3
  TopOn  
     

 

    
  |
16 | 5 | adantr 472 |
. . . . . . . . 9
  TopOn      |
17 | 16 | difeq1d 3539 |
. . . . . . . 8
  TopOn          |
18 | 9 | opncld 20125 |
. . . . . . . . 9
 
          |
19 | 14, 18 | sylan 479 |
. . . . . . . 8
  TopOn    
       |
20 | 17, 19 | eqeltrd 2549 |
. . . . . . 7
  TopOn           |
21 | | eleq2 2538 |
. . . . . . . . . . . 12
   

    |
22 | 21 | notbid 301 |
. . . . . . . . . . 11
   
     |
23 | | eldif 3400 |
. . . . . . . . . . . . 13
  

   |
24 | 23 | baibr 920 |
. . . . . . . . . . . 12
 
     |
25 | 24 | con1bid 337 |
. . . . . . . . . . 11
 
 
   |
26 | 22, 25 | sylan9bb 714 |
. . . . . . . . . 10
   
 
   |
27 | | simpl 464 |
. . . . . . . . . . . . 13
   
     |
28 | 27 | sseq1d 3445 |
. . . . . . . . . . . 12
   
       |
29 | 28 | 3anbi1d 1369 |
. . . . . . . . . . 11
   
     
         |
30 | 29 | 2rexbidv 2897 |
. . . . . . . . . 10
   
       


         |
31 | 26, 30 | imbi12d 327 |
. . . . . . . . 9
   
  


    



          |
32 | 31 | ralbidva 2828 |
. . . . . . . 8
    

 

    

 
  
       |
33 | 32 | rspcv 3132 |
. . . . . . 7
      
 
     

 

     
 
  
       |
34 | 20, 33 | syl 17 |
. . . . . 6
  TopOn    
     

 

     
 
  
       |
35 | | ralcom3 2942 |
. . . . . . 7
 
 

  
    
  
  
      |
36 | | toponss 20021 |
. . . . . . . . . 10
  TopOn     |
37 | 36 | sselda 3418 |
. . . . . . . . 9
   TopOn      |
38 | | simprr2 1079 |
. . . . . . . . . . . . . 14
    TopOn 

  

       
  |
39 | 5 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . 18
    TopOn 

  

       
   |
40 | 39 | difeq1d 3539 |
. . . . . . . . . . . . . . . . 17
    TopOn 

  

       
       |
41 | 14 | ad3antrrr 744 |
. . . . . . . . . . . . . . . . . 18
    TopOn 

  

       
  |
42 | | simprll 780 |
. . . . . . . . . . . . . . . . . 18
    TopOn 

  

       
  |
43 | 9 | opncld 20125 |
. . . . . . . . . . . . . . . . . 18
 
          |
44 | 41, 42, 43 | syl2anc 673 |
. . . . . . . . . . . . . . . . 17
    TopOn 

  

       
         |
45 | 40, 44 | eqeltrd 2549 |
. . . . . . . . . . . . . . . 16
    TopOn 

  

       
        |
46 | | incom 3616 |
. . . . . . . . . . . . . . . . . 18
     |
47 | | simprr3 1080 |
. . . . . . . . . . . . . . . . . 18
    TopOn 

  

       
    |
48 | 46, 47 | syl5eq 2517 |
. . . . . . . . . . . . . . . . 17
    TopOn 

  

       
    |
49 | | simplll 776 |
. . . . . . . . . . . . . . . . . . 19
    TopOn 

  

       
TopOn    |
50 | | simprlr 781 |
. . . . . . . . . . . . . . . . . . 19
    TopOn 

  

       
  |
51 | | toponss 20021 |
. . . . . . . . . . . . . . . . . . 19
  TopOn     |
52 | 49, 50, 51 | syl2anc 673 |
. . . . . . . . . . . . . . . . . 18
    TopOn 

  

       
  |
53 | | reldisj 3812 |
. . . . . . . . . . . . . . . . . 18
   
     |
54 | 52, 53 | syl 17 |
. . . . . . . . . . . . . . . . 17
    TopOn 

  

       
 

     |
55 | 48, 54 | mpbid 215 |
. . . . . . . . . . . . . . . 16
    TopOn 

  

       
    |
56 | 9 | clsss2 20165 |
. . . . . . . . . . . . . . . 16
                       |
57 | 45, 55, 56 | syl2anc 673 |
. . . . . . . . . . . . . . 15
    TopOn 

  

       
            |
58 | | simprr1 1078 |
. . . . . . . . . . . . . . . 16
    TopOn 

  

       
    |
59 | | difcom 3843 |
. . . . . . . . . . . . . . . 16
  
    |
60 | 58, 59 | sylib 201 |
. . . . . . . . . . . . . . 15
    TopOn 

  

       
    |
61 | 57, 60 | sstrd 3428 |
. . . . . . . . . . . . . 14
    TopOn 

  

       
          |
62 | 38, 61 | jca 541 |
. . . . . . . . . . . . 13
    TopOn 

  

       

           |
63 | 62 | expr 626 |
. . . . . . . . . . . 12
    TopOn 

 
 
   
                |
64 | 63 | anassrs 660 |
. . . . . . . . . . 11
     TopOn 
       
                |
65 | 64 | reximdva 2858 |
. . . . . . . . . 10
    TopOn 

   
  
   

            |
66 | 65 | rexlimdva 2871 |
. . . . . . . . 9
   TopOn     

  
   

            |
67 | 37, 66 | embantd 55 |
. . . . . . . 8
   TopOn       
  
     
            |
68 | 67 | ralimdva 2805 |
. . . . . . 7
  TopOn    
  
  
      
            |
69 | 35, 68 | syl5bi 225 |
. . . . . 6
  TopOn    

 
  
      
            |
70 | 34, 69 | syld 44 |
. . . . 5
  TopOn    
     

 

      
            |
71 | 70 | ralrimdva 2812 |
. . . 4
 TopOn 
 
     

 

     


            |
72 | 71 | imp 436 |
. . 3
  TopOn  
     

 

    




           |
73 | | isreg 20425 |
. . 3

 



            |
74 | 15, 72, 73 | sylanbrc 677 |
. 2
  TopOn  
     

 

    
  |
75 | 13, 74 | impbida 850 |
1
 TopOn 
       

 

       |