Step | Hyp | Ref
| Expression |
1 | | df-rab 2765 |
. . . . . 6
     
     
   |
2 | | clscld.1 |
. . . . . . . . . . . . 13
  |
3 | 2 | cldopn 20123 |
. . . . . . . . . . . 12
    
    |
4 | 3 | ad2antrl 742 |
. . . . . . . . . . 11
  
     
 
    |
5 | | sscon 3556 |
. . . . . . . . . . . . 13
   
   |
6 | 5 | ad2antll 743 |
. . . . . . . . . . . 12
  
     
 
      |
7 | 2 | topopn 20013 |
. . . . . . . . . . . . . 14
   |
8 | | difexg 4545 |
. . . . . . . . . . . . . 14
     |
9 | | elpwg 3950 |
. . . . . . . . . . . . . 14
        
       |
10 | 7, 8, 9 | 3syl 18 |
. . . . . . . . . . . . 13
      
       |
11 | 10 | ad2antrr 740 |
. . . . . . . . . . . 12
  
     
 
     
       |
12 | 6, 11 | mpbird 240 |
. . . . . . . . . . 11
  
     
 
   
   |
13 | 4, 12 | elind 3609 |
. . . . . . . . . 10
  
     
 
         |
14 | 2 | cldss 20121 |
. . . . . . . . . . . . 13
    
  |
15 | 14 | ad2antrl 742 |
. . . . . . . . . . . 12
  
     
 
  |
16 | | dfss4 3668 |
. . . . . . . . . . . 12

      |
17 | 15, 16 | sylib 201 |
. . . . . . . . . . 11
  
     
 
      |
18 | 17 | eqcomd 2477 |
. . . . . . . . . 10
  
     
 

     |
19 | | difeq2 3534 |
. . . . . . . . . . . 12
           |
20 | 19 | eqeq2d 2481 |
. . . . . . . . . . 11
     

      |
21 | 20 | rspcev 3136 |
. . . . . . . . . 10
             
   
       |
22 | 13, 18, 21 | syl2anc 673 |
. . . . . . . . 9
  
     
 
   
       |
23 | 22 | ex 441 |
. . . . . . . 8
        

   
        |
24 | | simpl 464 |
. . . . . . . . . . . 12
  
  |
25 | | elin 3608 |
. . . . . . . . . . . . 13
     

      |
26 | 25 | simplbi 467 |
. . . . . . . . . . . 12
        |
27 | 2 | opncld 20125 |
. . . . . . . . . . . 12
 
         |
28 | 24, 26, 27 | syl2an 485 |
. . . . . . . . . . 11
  

     
        |
29 | 25 | simprbi 471 |
. . . . . . . . . . . . . 14
           |
30 | 29 | adantl 473 |
. . . . . . . . . . . . 13
  

     
     |
31 | 30 | elpwid 3952 |
. . . . . . . . . . . 12
  

     
    |
32 | 31 | difss2d 3552 |
. . . . . . . . . . . . 13
  

     
  |
33 | | simplr 770 |
. . . . . . . . . . . . 13
  

     
  |
34 | | ssconb 3555 |
. . . . . . . . . . . . 13
 
   
     |
35 | 32, 33, 34 | syl2anc 673 |
. . . . . . . . . . . 12
  

     
  
     |
36 | 31, 35 | mpbid 215 |
. . . . . . . . . . 11
  

     
    |
37 | 28, 36 | jca 541 |
. . . . . . . . . 10
  

     
      
     |
38 | | eleq1 2537 |
. . . . . . . . . . 11
       
         |
39 | | sseq2 3440 |
. . . . . . . . . . 11
   
     |
40 | 38, 39 | anbi12d 725 |
. . . . . . . . . 10
        
       
      |
41 | 37, 40 | syl5ibrcom 230 |
. . . . . . . . 9
  

     
            |
42 | 41 | rexlimdva 2871 |
. . . . . . . 8
       
         
    |
43 | 23, 42 | impbid 195 |
. . . . . . 7
        
             |
44 | 43 | abbidv 2589 |
. . . . . 6
            
           |
45 | 1, 44 | syl5eq 2517 |
. . . . 5
       
              |
46 | 45 | inteqd 4231 |
. . . 4
        
      
        |
47 | | difexg 4545 |
. . . . . . 7
     |
48 | 47 | ralrimivw 2810 |
. . . . . 6
    
       |
49 | | dfiin2g 4302 |
. . . . . 6
 
           
          
        |
50 | 7, 48, 49 | 3syl 18 |
. . . . 5
    
          
        |
51 | 50 | adantr 472 |
. . . 4
                 
        |
52 | 46, 51 | eqtr4d 2508 |
. . 3
        
            |
53 | 2 | clsval 20129 |
. . 3
                    |
54 | | uniiun 4322 |
. . . . . 6
         
    |
55 | 54 | difeq2i 3537 |
. . . . 5
         
        |
56 | 55 | a1i 11 |
. . . 4
     
                |
57 | | 0opn 20011 |
. . . . . . 7
   |
58 | 57 | adantr 472 |
. . . . . 6
     |
59 | | 0elpw 4570 |
. . . . . . 7
 
  |
60 | 59 | a1i 11 |
. . . . . 6
        |
61 | 58, 60 | elind 3609 |
. . . . 5
          |
62 | | ne0i 3728 |
. . . . 5
   
 
       |
63 | | iindif2 4338 |
. . . . 5
     
   
         
      |
64 | 61, 62, 63 | 3syl 18 |
. . . 4
                       |
65 | 56, 64 | eqtr4d 2508 |
. . 3
     
        
       |
66 | 52, 53, 65 | 3eqtr4d 2515 |
. 2
               
     |
67 | | difssd 3550 |
. . . 4
     |
68 | 2 | ntrval 20128 |
. . . 4
  
                    |
69 | 67, 68 | sylan2 482 |
. . 3
                     |
70 | 69 | difeq2d 3540 |
. 2
                   
     |
71 | 66, 70 | eqtr4d 2508 |
1
                         |