Step | Hyp | Ref
| Expression |
1 | | ncaddccl 6145 |
. . 3
  NC NC   NC  |
2 | 1 | 3adant1 973 |
. 2
  NC NC NC   NC  |
3 | | elncs 6120 |
. . 3
   NC    
Nc   |
4 | | vex 2863 |
. . . . . . 7
 |
5 | 4 | ncid 6124 |
. . . . . 6
Nc  |
6 | | eleq2 2414 |
. . . . . 6
   Nc    Nc    |
7 | 5, 6 | mpbiri 224 |
. . . . 5
   Nc     |
8 | | eladdc 4399 |
. . . . . 6
  
          |
9 | | ncseqnc 6129 |
. . . . . . . . . 10
 NC  Nc    |
10 | | ncseqnc 6129 |
. . . . . . . . . 10
 NC  Nc    |
11 | 9, 10 | bi2anan9 843 |
. . . . . . . . 9
  NC NC   Nc Nc  
    |
12 | 11 | 3adant1 973 |
. . . . . . . 8
  NC NC NC   Nc Nc  
    |
13 | | elncs 6120 |
. . . . . . . . . . . 12
 NC  Nc   |
14 | | vex 2863 |
. . . . . . . . . . . . . . . . 17
 |
15 | | vex 2863 |
. . . . . . . . . . . . . . . . 17
 |
16 | 14, 15 | ncdisjun 6137 |
. . . . . . . . . . . . . . . 16
  
Nc  
Nc Nc    |
17 | 16 | oveq2d 5539 |
. . . . . . . . . . . . . . 15
  
Nc
·c Nc    Nc ·c Nc Nc     |
18 | | xpdisj2 5049 |
. . . . . . . . . . . . . . . . 17
  
 
      |
19 | 4, 14 | xpex 5116 |
. . . . . . . . . . . . . . . . . 18
   |
20 | 4, 15 | xpex 5116 |
. . . . . . . . . . . . . . . . . 18
   |
21 | 19, 20 | ncdisjun 6137 |
. . . . . . . . . . . . . . . . 17
       Nc  
    Nc   Nc      |
22 | 18, 21 | syl 15 |
. . . . . . . . . . . . . . . 16
  
Nc   
   Nc   Nc 
    |
23 | 14, 15 | unex 4107 |
. . . . . . . . . . . . . . . . . 18
   |
24 | 4, 23 | mucnc 6132 |
. . . . . . . . . . . . . . . . 17
Nc ·c Nc    Nc 
    |
25 | | xpundi 4833 |
. . . . . . . . . . . . . . . . . 18
   
 
     |
26 | 25 | nceqi 6110 |
. . . . . . . . . . . . . . . . 17
Nc     Nc        |
27 | 24, 26 | eqtri 2373 |
. . . . . . . . . . . . . . . 16
Nc ·c Nc    Nc        |
28 | 4, 14 | mucnc 6132 |
. . . . . . . . . . . . . . . . 17
Nc ·c Nc  Nc 
  |
29 | 4, 15 | mucnc 6132 |
. . . . . . . . . . . . . . . . 17
Nc ·c Nc  Nc 
  |
30 | 28, 29 | addceq12i 4389 |
. . . . . . . . . . . . . . . 16
 Nc
·c Nc  Nc ·c Nc   Nc   Nc 
   |
31 | 22, 27, 30 | 3eqtr4g 2410 |
. . . . . . . . . . . . . . 15
  
Nc
·c Nc     Nc ·c Nc 
Nc ·c Nc     |
32 | 17, 31 | eqtr3d 2387 |
. . . . . . . . . . . . . 14
  
Nc
·c Nc Nc    Nc ·c Nc  Nc
·c Nc     |
33 | | oveq1 5531 |
. . . . . . . . . . . . . . 15
 Nc 
·c Nc Nc   Nc
·c Nc Nc     |
34 | | oveq1 5531 |
. . . . . . . . . . . . . . . 16
 Nc 
·c Nc 
Nc ·c Nc    |
35 | | oveq1 5531 |
. . . . . . . . . . . . . . . 16
 Nc 
·c Nc 
Nc ·c Nc    |
36 | 34, 35 | addceq12d 4392 |
. . . . . . . . . . . . . . 15
 Nc   ·c Nc   ·c Nc    Nc ·c Nc 
Nc ·c Nc     |
37 | 33, 36 | eqeq12d 2367 |
. . . . . . . . . . . . . 14
 Nc   ·c Nc Nc     ·c Nc  
·c Nc  
Nc ·c Nc Nc    Nc ·c Nc  Nc
·c Nc      |
38 | 32, 37 | syl5ibr 212 |
. . . . . . . . . . . . 13
 Nc    
·c Nc Nc    
·c Nc  
·c Nc      |
39 | 38 | exlimiv 1634 |
. . . . . . . . . . . 12
 
Nc   
 ·c Nc Nc     ·c Nc  
·c Nc      |
40 | 13, 39 | sylbi 187 |
. . . . . . . . . . 11
 NC    
·c Nc Nc    
·c Nc  
·c Nc      |
41 | 40 | adantrd 454 |
. . . . . . . . . 10
 NC        
·c Nc Nc    
·c Nc  
·c Nc      |
42 | | addceq12 4386 |
. . . . . . . . . . . . 13
  Nc Nc   
Nc Nc    |
43 | 42 | oveq2d 5539 |
. . . . . . . . . . . 12
  Nc Nc  
·c   
 ·c Nc Nc     |
44 | | oveq2 5532 |
. . . . . . . . . . . . . 14
 Nc 
·c   ·c Nc    |
45 | 44 | adantr 451 |
. . . . . . . . . . . . 13
  Nc Nc  
·c   ·c Nc    |
46 | | oveq2 5532 |
. . . . . . . . . . . . . 14
 Nc 
·c   ·c Nc    |
47 | 46 | adantl 452 |
. . . . . . . . . . . . 13
  Nc Nc  
·c   ·c Nc    |
48 | 45, 47 | addceq12d 4392 |
. . . . . . . . . . . 12
  Nc Nc   
·c   ·c    
·c Nc  
·c Nc     |
49 | 43, 48 | eqeq12d 2367 |
. . . . . . . . . . 11
  Nc Nc   
·c   
 
·c   ·c    ·c Nc Nc     ·c Nc  
·c Nc      |
50 | 49 | imbi2d 307 |
. . . . . . . . . 10
  Nc Nc      
  
 ·c      ·c 
 ·c       
  
 ·c Nc Nc     ·c Nc  
·c Nc       |
51 | 41, 50 | syl5ibrcom 213 |
. . . . . . . . 9
 NC   Nc
Nc     
  
 ·c      ·c 
 ·c       |
52 | 51 | 3ad2ant1 976 |
. . . . . . . 8
  NC NC NC   Nc Nc         
·c   
 
·c   ·c       |
53 | 12, 52 | sylbird 226 |
. . . . . . 7
  NC NC NC  
        
·c   
 
·c   ·c       |
54 | 53 | rexlimdvv 2745 |
. . . . . 6
  NC NC NC  
       
·c   
 
·c   ·c      |
55 | 8, 54 | syl5bi 208 |
. . . . 5
  NC NC NC   
 ·c      ·c 
 ·c      |
56 | 7, 55 | syl5 28 |
. . . 4
  NC NC NC    Nc 
·c   
 
·c   ·c      |
57 | 56 | exlimdv 1636 |
. . 3
  NC NC NC     
Nc  ·c      ·c  
·c      |
58 | 3, 57 | syl5bi 208 |
. 2
  NC NC NC    NC 
·c   
 
·c   ·c      |
59 | 2, 58 | mpd 14 |
1
  NC NC NC  ·c      ·c  
·c     |