Metamath Proof Explorer


Definition df-vdwpc

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 PolyAP=mkf|ad1mi1ma+diAPkdif-1fa+dirani1mfa+di=m

Detailed syntax breakdown

Step Hyp Ref Expression
0 cvdwp classPolyAP
1 vm setvarm
2 vk setvark
3 vf setvarf
4 va setvara
5 cn class
6 vd setvard
7 cmap class𝑚
8 c1 class1
9 cfz class
10 1 cv setvarm
11 8 10 9 co class1m
12 5 11 7 co class1m
13 vi setvari
14 4 cv setvara
15 caddc class+
16 6 cv setvard
17 13 cv setvari
18 17 16 cfv classdi
19 14 18 15 co classa+di
20 cvdwa classAP
21 2 cv setvark
22 21 20 cfv classAPk
23 19 18 22 co classa+diAPkdi
24 3 cv setvarf
25 24 ccnv classf-1
26 19 24 cfv classfa+di
27 26 csn classfa+di
28 25 27 cima classf-1fa+di
29 23 28 wss wffa+diAPkdif-1fa+di
30 29 13 11 wral wffi1ma+diAPkdif-1fa+di
31 chash class.
32 13 11 26 cmpt classi1mfa+di
33 32 crn classrani1mfa+di
34 33 31 cfv classrani1mfa+di
35 34 10 wceq wffrani1mfa+di=m
36 30 35 wa wffi1ma+diAPkdif-1fa+dirani1mfa+di=m
37 36 6 12 wrex wffd1mi1ma+diAPkdif-1fa+dirani1mfa+di=m
38 37 4 5 wrex wffad1mi1ma+diAPkdif-1fa+dirani1mfa+di=m
39 38 1 2 3 coprab classmkf|ad1mi1ma+diAPkdif-1fa+dirani1mfa+di=m
40 0 39 wceq wffPolyAP=mkf|ad1mi1ma+diAPkdif-1fa+dirani1mfa+di=m