Step | Hyp | Ref
| Expression |
1 | | selpw 3974 |
. . . 4
 
  |
2 | | simp1l 1012 |
. . . . . . 7
         
  |
3 | | simp2 989 |
. . . . . . . 8
         
  |
4 | | eqid 2454 |
. . . . . . . . . . . 12
   |
5 | 4 | cldopn 18766 |
. . . . . . . . . . 11
    
     |
6 | 5 | adantl 466 |
. . . . . . . . . 10
        
   |
7 | 6 | 3ad2ant1 1009 |
. . . . . . . . 9
               |
8 | 7 | snssd 4125 |
. . . . . . . 8
                 |
9 | 3, 8 | unssd 3639 |
. . . . . . 7
                   |
10 | | simp3 990 |
. . . . . . . . . . . . 13
             |
11 | | uniss 4219 |
. . . . . . . . . . . . . 14
     |
12 | 11 | 3ad2ant2 1010 |
. . . . . . . . . . . . 13
          
   |
13 | 10, 12 | sstrd 3473 |
. . . . . . . . . . . 12
             |
14 | | undif 3866 |
. . . . . . . . . . . 12
 
        |
15 | 13, 14 | sylib 196 |
. . . . . . . . . . 11
            
     |
16 | | unss1 3632 |
. . . . . . . . . . . 12
  
            |
17 | 16 | 3ad2ant3 1011 |
. . . . . . . . . . 11
            
 
 
      |
18 | 15, 17 | eqsstr3d 3498 |
. . . . . . . . . 10
          
 
      |
19 | | difss 3590 |
. . . . . . . . . . . 12
     |
20 | 12, 19 | jctir 538 |
. . . . . . . . . . 11
                    |
21 | | unss 3637 |
. . . . . . . . . . 11
                  |
22 | 20, 21 | sylib 196 |
. . . . . . . . . 10
                   |
23 | 18, 22 | eqssd 3480 |
. . . . . . . . 9
          
 
 
    |
24 | | uniexg 6486 |
. . . . . . . . . . . . 13

   |
25 | 24 | ad2antrr 725 |
. . . . . . . . . . . 12
         
  |
26 | 25 | 3adant3 1008 |
. . . . . . . . . . 11
          
  |
27 | | difexg 4547 |
. . . . . . . . . . 11
 
     |
28 | | unisng 4214 |
. . . . . . . . . . 11
               |
29 | 26, 27, 28 | 3syl 20 |
. . . . . . . . . 10
                     |
30 | 29 | uneq2d 3617 |
. . . . . . . . 9
                    
      |
31 | 23, 30 | eqtr4d 2498 |
. . . . . . . 8
          
 
         |
32 | | uniun 4217 |
. . . . . . . 8
                  |
33 | 31, 32 | syl6eqr 2513 |
. . . . . . 7
          
          |
34 | 4 | cmpcov 19123 |
. . . . . . 7
                  
            
   |
35 | 2, 9, 33, 34 | syl3anc 1219 |
. . . . . 6
          
           
   |
36 | | elfpw 7723 |
. . . . . . . 8
          
           |
37 | | simp2l 1014 |
. . . . . . . . . . . 12
        
 
                     |
38 | | uncom 3607 |
. . . . . . . . . . . 12
               |
39 | 37, 38 | syl6sseq 3509 |
. . . . . . . . . . 11
        
 
                     |
40 | | ssundif 3869 |
. . . . . . . . . . 11
                 |
41 | 39, 40 | sylib 196 |
. . . . . . . . . 10
        
 
                     |
42 | | diffi 7653 |
. . . . . . . . . . . 12
 
  
     |
43 | 42 | ad2antll 728 |
. . . . . . . . . . 11
        
 
          
  
     |
44 | 43 | 3adant3 1008 |
. . . . . . . . . 10
        
 
                     |
45 | | elfpw 7723 |
. . . . . . . . . 10
          
 
  
             |
46 | 41, 44, 45 | sylanbrc 664 |
. . . . . . . . 9
        
 
                        |
47 | 10 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . . 16
        
 
               |
48 | 12 | 3ad2ant1 1009 |
. . . . . . . . . . . . . . . . 17
        
 
            
   |
49 | | simp3 990 |
. . . . . . . . . . . . . . . . 17
        
 
            
   |
50 | 48, 49 | sseqtrd 3499 |
. . . . . . . . . . . . . . . 16
        
 
            
   |
51 | 47, 50 | sstrd 3473 |
. . . . . . . . . . . . . . 15
        
 
               |
52 | 51 | sselda 3463 |
. . . . . . . . . . . . . 14
    
       
          
    |
53 | | eluni 4201 |
. . . . . . . . . . . . . 14
 
  
   |
54 | 52, 53 | sylib 196 |
. . . . . . . . . . . . 13
    
       
          
       |
55 | | simpl 457 |
. . . . . . . . . . . . . . . 16
 
   |
56 | 55 | a1i 11 |
. . . . . . . . . . . . . . 15
    
       
          
       |
57 | | simpr 461 |
. . . . . . . . . . . . . . . . . 18
 
   |
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . . . 17
    
       
          
       |
59 | | elndif 3587 |
. . . . . . . . . . . . . . . . . . . . . 22

     |
60 | 59 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . 21
             
          


     |
61 | | eleq2 2527 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
    
      |
62 | 61 | biimpd 207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . 23
    
       
          
    

       |
64 | 63 | com23 78 |
. . . . . . . . . . . . . . . . . . . . . 22
    
       
          
     
       |
65 | 64 | imp 429 |
. . . . . . . . . . . . . . . . . . . . 21
             
          


          |
66 | 60, 65 | mtod 177 |
. . . . . . . . . . . . . . . . . . . 20
             
          


     |
67 | 66 | ex 434 |
. . . . . . . . . . . . . . . . . . 19
    
       
          
        |
68 | 67 | adantrd 468 |
. . . . . . . . . . . . . . . . . 18
    
       
          
   
      |
69 | | elsn 3998 |
. . . . . . . . . . . . . . . . . . 19
           |
70 | 69 | notbii 296 |
. . . . . . . . . . . . . . . . . 18
     
     |
71 | 68, 70 | syl6ibr 227 |
. . . . . . . . . . . . . . . . 17
    
       
          
   
  
     |
72 | 58, 71 | jcad 533 |
. . . . . . . . . . . . . . . 16
    
       
          
    
         |
73 | | eldif 3445 |
. . . . . . . . . . . . . . . 16
                 |
74 | 72, 73 | syl6ibr 227 |
. . . . . . . . . . . . . . 15
    
       
          
              |
75 | 56, 74 | jcad 533 |
. . . . . . . . . . . . . 14
    
       
          
    
           |
76 | 75 | eximdv 1677 |
. . . . . . . . . . . . 13
    
       
          
    
               |
77 | 54, 76 | mpd 15 |
. . . . . . . . . . . 12
    
       
          
              |
78 | 77 | ex 434 |
. . . . . . . . . . 11
        
 
                           |
79 | | eluni 4201 |
. . . . . . . . . . 11
                      |
80 | 78, 79 | syl6ibr 227 |
. . . . . . . . . 10
        
 
              
  
      |
81 | 80 | ssrdv 3469 |
. . . . . . . . 9
        
 
                      |
82 | | unieq 4206 |
. . . . . . . . . . 11
          
        |
83 | 82 | sseq2d 3491 |
. . . . . . . . . 10
         
 
  
      |
84 | 83 | rspcev 3177 |
. . . . . . . . 9
                    
        |
85 | 46, 81, 84 | syl2anc 661 |
. . . . . . . 8
        
 
            
 
     |
86 | 36, 85 | syl3an2b 1256 |
. . . . . . 7
        
 
            
        |
87 | 86 | rexlimdv3a 2947 |
. . . . . 6
                       
     
    |
88 | 35, 87 | mpd 15 |
. . . . 5
          
 
     |
89 | 88 | 3exp 1187 |
. . . 4
       

     
     |
90 | 1, 89 | syl5bi 217 |
. . 3
               
     |
91 | 90 | ralrimiv 2827 |
. 2
                    |
92 | | cmptop 19129 |
. . 3

  |
93 | 4 | cldss 18764 |
. . 3
    
   |
94 | 4 | cmpsub 19134 |
. . 3
      ↾t 
              |
95 | 92, 93, 94 | syl2an 477 |
. 2
        
↾t  
       
     |
96 | 91, 95 | mpbird 232 |
1
        ↾t    |