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

Definition df-vdwpc 14014
 Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc 14024 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 14011 . 2 PolyAP
2 va . . . . . . . . . . 11
32cv 1361 . . . . . . . . . 10
4 vi . . . . . . . . . . . 12
54cv 1361 . . . . . . . . . . 11
6 vd . . . . . . . . . . . 12
76cv 1361 . . . . . . . . . . 11
85, 7cfv 5406 . . . . . . . . . 10
9 caddc 9273 . . . . . . . . . 10
103, 8, 9co 6080 . . . . . . . . 9
11 vk . . . . . . . . . . 11
1211cv 1361 . . . . . . . . . 10
13 cvdwa 14009 . . . . . . . . . 10 AP
1412, 13cfv 5406 . . . . . . . . 9 AP
1510, 8, 14co 6080 . . . . . . . 8 AP
16 vf . . . . . . . . . . 11
1716cv 1361 . . . . . . . . . 10
1817ccnv 4826 . . . . . . . . 9
1910, 17cfv 5406 . . . . . . . . . 10
2019csn 3865 . . . . . . . . 9
2118, 20cima 4830 . . . . . . . 8
2215, 21wss 3316 . . . . . . 7 AP
23 c1 9271 . . . . . . . 8
24 vm . . . . . . . . 9
2524cv 1361 . . . . . . . 8
26 cfz 11424 . . . . . . . 8
2723, 25, 26co 6080 . . . . . . 7
2822, 4, 27wral 2705 . . . . . 6 AP
294, 27, 19cmpt 4338 . . . . . . . . 9
3029crn 4828 . . . . . . . 8
31 chash 12087 . . . . . . . 8
3230, 31cfv 5406 . . . . . . 7
3332, 25wceq 1362 . . . . . 6
3428, 33wa 369 . . . . 5 AP
35 cn 10310 . . . . . 6
36 cmap 7202 . . . . . 6
3735, 27, 36co 6080 . . . . 5
3834, 6, 37wrex 2706 . . . 4 AP
3938, 2, 35wrex 2706 . . 3 AP
4039, 24, 11, 16coprab 6081 . 2 AP
411, 40wceq 1362 1 PolyAP AP
 Colors of variables: wff setvar class This definition is referenced by:  vdwpc  14024
 Copyright terms: Public domain W3C validator