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	$$⊢\mathrm{PolyAP}=\left\{⟨⟨m,k⟩,f⟩|\exists a\in \mathbb{N}\exists d\in \left({\mathbb{N}}^{\left(1\dots m\right)}\right)\left(\forall i\in \left(1\dots m\right)\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|=m\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cvdwp	$$class\mathrm{PolyAP}$$
1		vm	$$setvarm$$
2		vk	$$setvark$$
3		vf	$$setvarf$$
4		va	$$setvara$$
5		cn	$$class\mathbb{N}$$
6		vd	$$setvard$$
7		cmap	$$class{\uparrow }_{𝑚}$$
8		c1	$$class1$$
9		cfz	$$class\dots$$
10	1	cv	$$setvarm$$
11	8 10 9	co	$$class\left(1\dots m\right)$$
12	5 11 7	co	$$class\left({\mathbb{N}}^{\left(1\dots m\right)}\right)$$
13		vi	$$setvari$$
14	4	cv	$$setvara$$
15		caddc	$$class+$$
16	6	cv	$$setvard$$
17	13	cv	$$setvari$$
18	17 16	cfv	$$classd\left(i\right)$$
19	14 18 15	co	$$class\left(a+d\left(i\right)\right)$$
20		cvdwa	$$class\mathrm{AP}$$
21	2	cv	$$setvark$$
22	21 20	cfv	$$class\mathrm{AP}\left(k\right)$$
23	19 18 22	co	$$class\left(\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\right)$$
24	3	cv	$$setvarf$$
25	24	ccnv	$$class{f}^{-1}$$
26	19 24	cfv	$$classf\left(a+d\left(i\right)\right)$$
27	26	csn	$$class\left\{f\left(a+d\left(i\right)\right)\right\}$$
28	25 27	cima	$$class{f}^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]$$
29	23 28	wss	$$wff\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]$$
30	29 13 11	wral	$$wff\forall i\in \left(1\dots m\right)\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]$$
31		chash	$$class\left|.\right|$$
32	13 11 26	cmpt	$$class\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)$$
33	32	crn	$$class\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)$$
34	33 31	cfv	$$class\left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|$$
35	34 10	wceq	$$wff\left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|=m$$
36	30 35	wa	$$wff\left(\forall i\in \left(1\dots m\right)\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|=m\right)$$
37	36 6 12	wrex	$$wff\exists d\in \left({\mathbb{N}}^{\left(1\dots m\right)}\right)\left(\forall i\in \left(1\dots m\right)\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|=m\right)$$
38	37 4 5	wrex	$$wff\exists a\in \mathbb{N}\exists d\in \left({\mathbb{N}}^{\left(1\dots m\right)}\right)\left(\forall i\in \left(1\dots m\right)\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|=m\right)$$
39	38 1 2 3	coprab	$$class\left\{⟨⟨m,k⟩,f⟩|\exists a\in \mathbb{N}\exists d\in \left({\mathbb{N}}^{\left(1\dots m\right)}\right)\left(\forall i\in \left(1\dots m\right)\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|=m\right)\right\}$$
40	0 39	wceq	$$wff\mathrm{PolyAP}=\left\{⟨⟨m,k⟩,f⟩|\exists a\in \mathbb{N}\exists d\in \left({\mathbb{N}}^{\left(1\dots m\right)}\right)\left(\forall i\in \left(1\dots m\right)\left(a+d\left(i\right)\right)\mathrm{AP}\left(k\right)d\left(i\right)\subseteq f^{-1}\left[\left\{f\left(a+d\left(i\right)\right)\right\}\right]\wedge \left|\mathrm{ran}\left(i\in \left(1\dots m\right)⟼f\left(a+d\left(i\right)\right)\right)\right|=m\right)\right\}$$