Step | Hyp | Ref
| Expression |
1 | | ncaddccl 6144 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![C](_cc.gif) NC ![)](rp.gif) |
2 | 1 | 3adant1 973 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![C](_cc.gif) NC ![)](rp.gif) |
3 | | elncs 6119 |
. . 3
![(](lp.gif) ![(](lp.gif) ![C](_cc.gif) NC ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![C](_cc.gif)
Nc ![x](_x.gif) ![)](rp.gif) |
4 | | vex 2862 |
. . . . . . 7
![_V](rmcv.gif) |
5 | 4 | ncid 6123 |
. . . . . 6
Nc ![x](_x.gif) |
6 | | eleq2 2414 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![C](_cc.gif) Nc ![(](lp.gif) ![(](lp.gif) ![C](_cc.gif) Nc ![x](_x.gif) ![)](rp.gif) ![)](rp.gif) |
7 | 5, 6 | mpbiri 224 |
. . . . 5
![(](lp.gif) ![(](lp.gif) ![C](_cc.gif) Nc ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) |
8 | | eladdc 4398 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) ![C](_cc.gif)
![E.](exists.gif) ![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
9 | | ncseqnc 6128 |
. . . . . . . . . 10
![(](lp.gif) NC ![(](lp.gif) Nc ![B](_cb.gif) ![)](rp.gif) ![)](rp.gif) |
10 | | ncseqnc 6128 |
. . . . . . . . . 10
![(](lp.gif) NC ![(](lp.gif) Nc ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) |
11 | 9, 10 | bi2anan9 843 |
. . . . . . . . 9
![(](lp.gif) ![(](lp.gif) NC NC ![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif)
![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
12 | 11 | 3adant1 973 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif)
![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
13 | | elncs 6119 |
. . . . . . . . . . . 12
![(](lp.gif) NC ![E.](exists.gif) Nc ![x](_x.gif) ![)](rp.gif) |
14 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
![_V](rmcv.gif) |
15 | | vex 2862 |
. . . . . . . . . . . . . . . . 17
![_V](rmcv.gif) |
16 | 14, 15 | ncdisjun 6136 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
Nc ![(](lp.gif) ![z](_z.gif)
Nc Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
17 | 16 | oveq2d 5538 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
Nc
·c Nc ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) Nc ·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
18 | | xpdisj2 5048 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![(/)](varnothing.gif) ![)](rp.gif) |
19 | 4, 14 | xpex 5115 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![y](_y.gif) ![_V](rmcv.gif) |
20 | 4, 15 | xpex 5115 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![z](_z.gif) ![_V](rmcv.gif) |
21 | 19, 20 | ncdisjun 6136 |
. . . . . . . . . . . . . . . . 17
![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) Nc ![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) Nc ![(](lp.gif) ![y](_y.gif) Nc ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
22 | 18, 21 | syl 15 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
Nc ![(](lp.gif) ![(](lp.gif) ![y](_y.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) Nc ![(](lp.gif) ![y](_y.gif) Nc ![(](lp.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
23 | 14, 15 | unex 4106 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![z](_z.gif) ![_V](rmcv.gif) |
24 | 4, 23 | mucnc 6131 |
. . . . . . . . . . . . . . . . 17
Nc ·c Nc ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) Nc ![(](lp.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
25 | | xpundi 4832 |
. . . . . . . . . . . . . . . . . 18
![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
![y](_y.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
26 | 25 | nceqi 6109 |
. . . . . . . . . . . . . . . . 17
Nc ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) Nc ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
27 | 24, 26 | eqtri 2373 |
. . . . . . . . . . . . . . . 16
Nc ·c Nc ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) Nc ![(](lp.gif) ![(](lp.gif) ![y](_y.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
28 | 4, 14 | mucnc 6131 |
. . . . . . . . . . . . . . . . 17
Nc ·c Nc ![y](_y.gif) Nc ![(](lp.gif)
![y](_y.gif) ![)](rp.gif) |
29 | 4, 15 | mucnc 6131 |
. . . . . . . . . . . . . . . . 17
Nc ·c Nc ![z](_z.gif) Nc ![(](lp.gif)
![z](_z.gif) ![)](rp.gif) |
30 | 28, 29 | addceq12i 4388 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nc
·c Nc ![y](_y.gif) Nc ·c Nc ![z](_z.gif) ![)](rp.gif) Nc ![(](lp.gif) ![y](_y.gif) Nc ![(](lp.gif)
![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
31 | 22, 27, 30 | 3eqtr4g 2410 |
. . . . . . . . . . . . . . 15
![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
Nc
·c Nc ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) Nc ·c Nc ![y](_y.gif)
Nc ·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
32 | 17, 31 | eqtr3d 2387 |
. . . . . . . . . . . . . 14
![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
Nc
·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) Nc ·c Nc ![y](_y.gif) Nc
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
33 | | oveq1 5530 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Nc ![(](lp.gif)
·c Nc Nc ![z](_z.gif) ![)](rp.gif) Nc
·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
34 | | oveq1 5530 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nc ![(](lp.gif)
·c Nc ![y](_y.gif)
Nc ·c Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
35 | | oveq1 5530 |
. . . . . . . . . . . . . . . 16
![(](lp.gif) Nc ![(](lp.gif)
·c Nc ![z](_z.gif)
Nc ·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
36 | 34, 35 | addceq12d 4391 |
. . . . . . . . . . . . . . 15
![(](lp.gif) Nc ![(](lp.gif) ![(](lp.gif) ·c Nc ![y](_y.gif) ![(](lp.gif) ·c Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) Nc ·c Nc ![y](_y.gif)
Nc ·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
37 | 33, 36 | eqeq12d 2367 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nc ![(](lp.gif) ![(](lp.gif) ·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif)
Nc ·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) Nc ·c Nc ![y](_y.gif) Nc
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
38 | 32, 37 | syl5ibr 212 |
. . . . . . . . . . . . 13
![(](lp.gif) Nc ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif)
·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
39 | 38 | exlimiv 1634 |
. . . . . . . . . . . 12
![(](lp.gif) ![E.](exists.gif)
Nc ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
![(](lp.gif) ·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
40 | 13, 39 | sylbi 187 |
. . . . . . . . . . 11
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif)
·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
41 | 40 | adantrd 454 |
. . . . . . . . . 10
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![(](lp.gif)
·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
42 | | addceq12 4385 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif) ![C](_cc.gif)
Nc Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
43 | 42 | oveq2d 5538 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif)
·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif)
![(](lp.gif) ·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
44 | | oveq2 5531 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nc ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
45 | 44 | adantr 451 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c Nc ![y](_y.gif) ![)](rp.gif) ![)](rp.gif) |
46 | | oveq2 5531 |
. . . . . . . . . . . . . 14
![(](lp.gif) Nc ![(](lp.gif)
·c ![C](_cc.gif) ![(](lp.gif) ·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
47 | 46 | adantl 452 |
. . . . . . . . . . . . 13
![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif)
·c ![C](_cc.gif) ![(](lp.gif) ·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) |
48 | 45, 47 | addceq12d 4391 |
. . . . . . . . . . . 12
![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif)
·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
49 | 43, 48 | eqeq12d 2367 |
. . . . . . . . . . 11
![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif) ![(](lp.gif)
·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![(](lp.gif) ·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
50 | 49 | imbi2d 307 |
. . . . . . . . . 10
![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif)
![(](lp.gif) ·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif)
![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif)
![(](lp.gif) ·c Nc Nc ![z](_z.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c Nc ![y](_y.gif) ![(](lp.gif)
·c Nc ![z](_z.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
51 | 41, 50 | syl5ibrcom 213 |
. . . . . . . . 9
![(](lp.gif) NC ![(](lp.gif) ![(](lp.gif) Nc
Nc ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif)
![(](lp.gif) ![z](_z.gif) ![)](rp.gif)
![(](lp.gif) ·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif)
![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
52 | 51 | 3ad2ant1 976 |
. . . . . . . 8
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif) Nc Nc ![z](_z.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![(](lp.gif)
·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
53 | 12, 52 | sylbird 226 |
. . . . . . 7
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif)
![C](_cc.gif) ![(](lp.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![(](lp.gif)
·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
54 | 53 | rexlimdvv 2744 |
. . . . . 6
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![E.](exists.gif)
![E.](exists.gif) ![(](lp.gif) ![(](lp.gif) ![z](_z.gif) ![(](lp.gif) ![z](_z.gif) ![)](rp.gif) ![(](lp.gif)
·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
55 | 8, 54 | syl5bi 208 |
. . . . 5
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif) ![C](_cc.gif)
![(](lp.gif) ·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif)
![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
56 | 7, 55 | syl5 28 |
. . . 4
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif) ![C](_cc.gif) Nc ![(](lp.gif)
·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
57 | 56 | exlimdv 1636 |
. . 3
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![E.](exists.gif) ![x](_x.gif) ![(](lp.gif) ![C](_cc.gif)
Nc ![(](lp.gif) ·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif) ![(](lp.gif)
·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
58 | 3, 57 | syl5bi 208 |
. 2
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ![(](lp.gif) ![C](_cc.gif) NC ![(](lp.gif)
·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif)
![(](lp.gif) ![(](lp.gif)
·c ![B](_cb.gif) ![(](lp.gif) ·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |
59 | 2, 58 | mpd 14 |
1
![(](lp.gif) ![(](lp.gif) NC NC NC ![(](lp.gif) ·c ![(](lp.gif) ![C](_cc.gif) ![)](rp.gif) ![(](lp.gif) ![(](lp.gif) ·c ![B](_cb.gif) ![(](lp.gif)
·c ![C](_cc.gif) ![)](rp.gif) ![)](rp.gif) ![)](rp.gif) |