Definition df-vdwpc 17008

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

Assertion

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

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

Detailed syntax breakdown of Definition df-vdwpc

Step	Hyp	Ref	Expression
1		cvdwp 17005	. 2 class PolyAP
2		va	. . . . . . . . . . 11 setvar 𝑎
3	2	cv 1539	. . . . . . . . . 10 class 𝑎
4		vi	. . . . . . . . . . . 12 setvar 𝑖
5	4	cv 1539	. . . . . . . . . . 11 class 𝑖
6		vd	. . . . . . . . . . . 12 setvar 𝑑
7	6	cv 1539	. . . . . . . . . . 11 class 𝑑
8	5, 7	cfv 6561	. . . . . . . . . 10 class (𝑑‘𝑖)
9		caddc 11158	. . . . . . . . . 10 class +
10	3, 8, 9	co 7431	. . . . . . . . 9 class (𝑎 + (𝑑‘𝑖))
11		vk	. . . . . . . . . . 11 setvar 𝑘
12	11	cv 1539	. . . . . . . . . 10 class 𝑘
13		cvdwa 17003	. . . . . . . . . 10 class AP
14	12, 13	cfv 6561	. . . . . . . . 9 class (AP‘𝑘)
15	10, 8, 14	co 7431	. . . . . . . 8 class ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖))
16		vf	. . . . . . . . . . 11 setvar 𝑓
17	16	cv 1539	. . . . . . . . . 10 class 𝑓
18	17	ccnv 5684	. . . . . . . . 9 class ◡𝑓
19	10, 17	cfv 6561	. . . . . . . . . 10 class (𝑓‘(𝑎 + (𝑑‘𝑖)))
20	19	csn 4626	. . . . . . . . 9 class {(𝑓‘(𝑎 + (𝑑‘𝑖)))}
21	18, 20	cima 5688	. . . . . . . 8 class (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))})
22	15, 21	wss 3951	. . . . . . 7 wff ((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))})
23		c1 11156	. . . . . . . 8 class 1
24		vm	. . . . . . . . 9 setvar 𝑚
25	24	cv 1539	. . . . . . . 8 class 𝑚
26		cfz 13547	. . . . . . . 8 class ...
27	23, 25, 26	co 7431	. . . . . . 7 class (1...𝑚)
28	22, 4, 27	wral 3061	. . . . . 6 wff ∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))})
29	4, 27, 19	cmpt 5225	. . . . . . . . 9 class (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))
30	29	crn 5686	. . . . . . . 8 class ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))
31		chash 14369	. . . . . . . 8 class ♯
32	30, 31	cfv 6561	. . . . . . 7 class (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖)))))
33	32, 25	wceq 1540	. . . . . 6 wff (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚
34	28, 33	wa 395	. . . . 5 wff (∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)
35		cn 12266	. . . . . 6 class ℕ
36		cmap 8866	. . . . . 6 class ↑m
37	35, 27, 36	co 7431	. . . . 5 class (ℕ ↑m (1...𝑚))
38	34, 6, 37	wrex 3070	. . . 4 wff ∃𝑑 ∈ (ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)
39	38, 2, 35	wrex 3070	. . 3 wff ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)
40	39, 24, 11, 16	coprab 7432	. 2 class {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)}
41	1, 40	wceq 1540	1 wff PolyAP = {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑‘𝑖))(AP‘𝑘)(𝑑‘𝑖)) ⊆ (◡𝑓 “ {(𝑓‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑‘𝑖))))) = 𝑚)}

This definition is referenced by:  vdwpc  17018