Definition df-vdwpc 15512

Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc 15522 for more information. (Contributed by Mario Carneiro, 18-Aug-2014.)

Assertion

Ref	Expression
df-vdwpc	⊢ PolyAP = {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)}

Distinct variable group:   𝑎,𝑑,𝑓,𝑖,𝑘,𝑚

Detailed syntax breakdown of Definition df-vdwpc

Step	Hyp	Ref	Expression
1		cvdwp 15509	. 2 class PolyAP
2		va	. . . . . . . . . . 11 setvar 𝑎
3	2	cv 1474	. . . . . . . . . 10 class 𝑎
4		vi	. . . . . . . . . . . 12 setvar 𝑖
5	4	cv 1474	. . . . . . . . . . 11 class 𝑖
6		vd	. . . . . . . . . . . 12 setvar 𝑑
7	6	cv 1474	. . . . . . . . . . 11 class 𝑑
8	5, 7	cfv 5804	. . . . . . . . . 10 class (𝑑‘𝑖)
9		caddc 9818	. . . . . . . . . 10 class +
10	3, 8, 9	co 6549	. . . . . . . . 9 class (𝑎 + (𝑑‘𝑖))
11		vk	. . . . . . . . . . 11 setvar 𝑘
12	11	cv 1474	. . . . . . . . . 10 class 𝑘
13		cvdwa 15507	. . . . . . . . . 10 class AP
14	12, 13	cfv 5804	. . . . . . . . 9 class (AP‘𝑘)
15	10, 8, 14	co 6549	. . . . . . . 8 class ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖))
16		vf	. . . . . . . . . . 11 setvar 𝑓
17	16	cv 1474	. . . . . . . . . 10 class 𝑓
18	17	ccnv 5037	. . . . . . . . 9 class ◡𝑓
19	10, 17	cfv 5804	. . . . . . . . . 10 class (𝑓‘(𝑎 + (𝑑‘𝑖)))
20	19	csn 4125	. . . . . . . . 9 class {(𝑓‘(𝑎 + (𝑑‘𝑖)))}
21	18, 20	cima 5041	. . . . . . . 8 class (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))})
22	15, 21	wss 3540	. . . . . . 7 wff ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))})
23		c1 9816	. . . . . . . 8 class 1
24		vm	. . . . . . . . 9 setvar 𝑚
25	24	cv 1474	. . . . . . . 8 class 𝑚
26		cfz 12197	. . . . . . . 8 class ...
27	23, 25, 26	co 6549	. . . . . . 7 class (1...𝑚)
28	22, 4, 27	wral 2896	. . . . . 6 wff ∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))})
29	4, 27, 19	cmpt 4643	. . . . . . . . 9 class (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))
30	29	crn 5039	. . . . . . . 8 class ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))
31		chash 12979	. . . . . . . 8 class #
32	30, 31	cfv 5804	. . . . . . 7 class (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖)))))
33	32, 25	wceq 1475	. . . . . 6 wff (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚
34	28, 33	wa 383	. . . . 5 wff (∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)
35		cn 10897	. . . . . 6 class ℕ
36		cmap 7744	. . . . . 6 class ↑𝑚
37	35, 27, 36	co 6549	. . . . 5 class (ℕ ↑𝑚 (1...𝑚))
38	34, 6, 37	wrex 2897	. . . 4 wff ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)
39	38, 2, 35	wrex 2897	. . 3 wff ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)
40	39, 24, 11, 16	coprab 6550	. 2 class {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)}
41	1, 40	wceq 1475	1 wff PolyAP = {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)}

This definition is referenced by:  vdwpc  15522