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 ${⊢}\mathrm{PolyAP}=\left\{⟨⟨{m},{k}⟩,{f}⟩|\exists {a}\in ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\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 ${setvar}{m}$
2 vk ${setvar}{k}$
3 vf ${setvar}{f}$
4 va ${setvar}{a}$
5 cn ${class}ℕ$
6 vd ${setvar}{d}$
7 cmap ${class}{↑}_{𝑚}$
8 c1 ${class}1$
9 cfz ${class}\dots$
10 1 cv ${setvar}{m}$
11 8 10 9 co ${class}\left(1\dots {m}\right)$
12 5 11 7 co ${class}\left({ℕ}^{\left(1\dots {m}\right)}\right)$
13 vi ${setvar}{i}$
14 4 cv ${setvar}{a}$
15 caddc ${class}+$
16 6 cv ${setvar}{d}$
17 13 cv ${setvar}{i}$
18 17 16 cfv ${class}{d}\left({i}\right)$
19 14 18 15 co ${class}\left({a}+{d}\left({i}\right)\right)$
20 cvdwa ${class}\mathrm{AP}$
21 2 cv ${setvar}{k}$
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 ${setvar}{f}$
25 24 ccnv ${class}{{f}}^{-1}$
26 19 24 cfv ${class}{f}\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)\phantom{\rule{.4em}{0ex}}\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)\phantom{\rule{.4em}{0ex}}\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({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\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 ℕ\phantom{\rule{.4em}{0ex}}\exists {d}\in \left({ℕ}^{\left(1\dots {m}\right)}\right)\phantom{\rule{.4em}{0ex}}\left(\forall {i}\in \left(1\dots {m}\right)\phantom{\rule{.4em}{0ex}}\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\}$