Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdwpc Structured version   Unicode version

Definition df-vdwpc 13338
 Description: Define the "contains a polychromatic colleciton of APs" predicate. See vdwpc 13348 for more information. (Contributed by Mario Carneiro, 18-Aug-2014.)
Assertion
Ref Expression
df-vdwpc PolyAP AP
Distinct variable group:   ,,,,,

Detailed syntax breakdown of Definition df-vdwpc
StepHypRef Expression
1 cvdwp 13335 . 2 PolyAP
2 va . . . . . . . . . . 11
32cv 1651 . . . . . . . . . 10
4 vi . . . . . . . . . . . 12
54cv 1651 . . . . . . . . . . 11
6 vd . . . . . . . . . . . 12
76cv 1651 . . . . . . . . . . 11
85, 7cfv 5454 . . . . . . . . . 10
9 caddc 8993 . . . . . . . . . 10
103, 8, 9co 6081 . . . . . . . . 9
11 vk . . . . . . . . . . 11
1211cv 1651 . . . . . . . . . 10
13 cvdwa 13333 . . . . . . . . . 10 AP
1412, 13cfv 5454 . . . . . . . . 9 AP
1510, 8, 14co 6081 . . . . . . . 8 AP
16 vf . . . . . . . . . . 11
1716cv 1651 . . . . . . . . . 10
1817ccnv 4877 . . . . . . . . 9
1910, 17cfv 5454 . . . . . . . . . 10
2019csn 3814 . . . . . . . . 9
2118, 20cima 4881 . . . . . . . 8
2215, 21wss 3320 . . . . . . 7 AP
23 c1 8991 . . . . . . . 8
24 vm . . . . . . . . 9
2524cv 1651 . . . . . . . 8
26 cfz 11043 . . . . . . . 8
2723, 25, 26co 6081 . . . . . . 7
2822, 4, 27wral 2705 . . . . . 6 AP
294, 27, 19cmpt 4266 . . . . . . . . 9
3029crn 4879 . . . . . . . 8
31 chash 11618 . . . . . . . 8
3230, 31cfv 5454 . . . . . . 7
3332, 25wceq 1652 . . . . . 6
3428, 33wa 359 . . . . 5 AP
35 cn 10000 . . . . . 6
36 cmap 7018 . . . . . 6
3735, 27, 36co 6081 . . . . 5
3834, 6, 37wrex 2706 . . . 4 AP
3938, 2, 35wrex 2706 . . 3 AP
4039, 24, 11, 16coprab 6082 . 2 AP
411, 40wceq 1652 1 PolyAP AP
 Colors of variables: wff set class This definition is referenced by:  vdwpc  13348
 Copyright terms: Public domain W3C validator