df-vdwpc - Metamath Proof Explorer

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

Definition df-vdwpc 15674

Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc 15684 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**
Step	Hyp	Ref	Expression
1		cvdwp 15671	. 2 PolyAP
2		va	. . . . . . . . . . 11
3	2	cv 1482	. . . . . . . . . 10
4		vi	. . . . . . . . . . . 12
5	4	cv 1482	. . . . . . . . . . 11
6		vd	. . . . . . . . . . . 12
7	6	cv 1482	. . . . . . . . . . 11
8	5, 7	cfv 5888	. . . . . . . . . 10
9		caddc 9939	. . . . . . . . . 10
10	3, 8, 9	co 6650	. . . . . . . . 9
11		vk	. . . . . . . . . . 11
12	11	cv 1482	. . . . . . . . . 10
13		cvdwa 15669	. . . . . . . . . 10 AP
14	12, 13	cfv 5888	. . . . . . . . 9 AP
15	10, 8, 14	co 6650	. . . . . . . 8 AP
16		vf	. . . . . . . . . . 11
17	16	cv 1482	. . . . . . . . . 10
18	17	ccnv 5113	. . . . . . . . 9
19	10, 17	cfv 5888	. . . . . . . . . 10
20	19	csn 4177	. . . . . . . . 9
21	18, 20	cima 5117	. . . . . . . 8
22	15, 21	wss 3574	. . . . . . 7 AP
23		c1 9937	. . . . . . . 8
24		vm	. . . . . . . . 9
25	24	cv 1482	. . . . . . . 8
26		cfz 12326	. . . . . . . 8
27	23, 25, 26	co 6650	. . . . . . 7
28	22, 4, 27	wral 2912	. . . . . 6 AP
29	4, 27, 19	cmpt 4729	. . . . . . . . 9
30	29	crn 5115	. . . . . . . 8
31		chash 13117	. . . . . . . 8
32	30, 31	cfv 5888	. . . . . . 7
33	32, 25	wceq 1483	. . . . . 6
34	28, 33	wa 384	. . . . 5 AP $/\$
35		cn 11020	. . . . . 6
36		cmap 7857	. . . . . 6
37	35, 27, 36	co 6650	. . . . 5
38	34, 6, 37	wrex 2913	. . . 4 AP $/\$
39	38, 2, 35	wrex 2913	. . 3 AP $/\$
40	39, 24, 11, 16	coprab 6651	. 2 AP $/\$
41	1, 40	wceq 1483	1 PolyAP AP $/\$

Colors of variables: wff setvar class

This definition is referenced by: vdwpc 15684

W3C validator