Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc for more information. (Contributed by Mario Carneiro, 18-Aug-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | df-vdwpc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | cvdwp | |
|
1 | vm | |
|
2 | vk | |
|
3 | vf | |
|
4 | va | |
|
5 | cn | |
|
6 | vd | |
|
7 | cmap | |
|
8 | c1 | |
|
9 | cfz | |
|
10 | 1 | cv | |
11 | 8 10 9 | co | |
12 | 5 11 7 | co | |
13 | vi | |
|
14 | 4 | cv | |
15 | caddc | |
|
16 | 6 | cv | |
17 | 13 | cv | |
18 | 17 16 | cfv | |
19 | 14 18 15 | co | |
20 | cvdwa | |
|
21 | 2 | cv | |
22 | 21 20 | cfv | |
23 | 19 18 22 | co | |
24 | 3 | cv | |
25 | 24 | ccnv | |
26 | 19 24 | cfv | |
27 | 26 | csn | |
28 | 25 27 | cima | |
29 | 23 28 | wss | |
30 | 29 13 11 | wral | |
31 | chash | |
|
32 | 13 11 26 | cmpt | |
33 | 32 | crn | |
34 | 33 31 | cfv | |
35 | 34 10 | wceq | |
36 | 30 35 | wa | |
37 | 36 6 12 | wrex | |
38 | 37 4 5 | wrex | |
39 | 38 1 2 3 | coprab | |
40 | 0 39 | wceq | |