MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-vdwpc Structured version   Visualization version   GIF version

Definition df-vdwpc 15897
Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc 15907 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
StepHypRef Expression
1 cvdwp 15894 . 2 class PolyAP
2 va . . . . . . . . . . 11 setvar 𝑎
32cv 1631 . . . . . . . . . 10 class 𝑎
4 vi . . . . . . . . . . . 12 setvar 𝑖
54cv 1631 . . . . . . . . . . 11 class 𝑖
6 vd . . . . . . . . . . . 12 setvar 𝑑
76cv 1631 . . . . . . . . . . 11 class 𝑑
85, 7cfv 6050 . . . . . . . . . 10 class (𝑑𝑖)
9 caddc 10152 . . . . . . . . . 10 class +
103, 8, 9co 6815 . . . . . . . . 9 class (𝑎 + (𝑑𝑖))
11 vk . . . . . . . . . . 11 setvar 𝑘
1211cv 1631 . . . . . . . . . 10 class 𝑘
13 cvdwa 15892 . . . . . . . . . 10 class AP
1412, 13cfv 6050 . . . . . . . . 9 class (AP‘𝑘)
1510, 8, 14co 6815 . . . . . . . 8 class ((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖))
16 vf . . . . . . . . . . 11 setvar 𝑓
1716cv 1631 . . . . . . . . . 10 class 𝑓
1817ccnv 5266 . . . . . . . . 9 class 𝑓
1910, 17cfv 6050 . . . . . . . . . 10 class (𝑓‘(𝑎 + (𝑑𝑖)))
2019csn 4322 . . . . . . . . 9 class {(𝑓‘(𝑎 + (𝑑𝑖)))}
2118, 20cima 5270 . . . . . . . 8 class (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))})
2215, 21wss 3716 . . . . . . 7 wff ((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖)) ⊆ (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))})
23 c1 10150 . . . . . . . 8 class 1
24 vm . . . . . . . . 9 setvar 𝑚
2524cv 1631 . . . . . . . 8 class 𝑚
26 cfz 12540 . . . . . . . 8 class ...
2723, 25, 26co 6815 . . . . . . 7 class (1...𝑚)
2822, 4, 27wral 3051 . . . . . 6 wff 𝑖 ∈ (1...𝑚)((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖)) ⊆ (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))})
294, 27, 19cmpt 4882 . . . . . . . . 9 class (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))
3029crn 5268 . . . . . . . 8 class ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))
31 chash 13332 . . . . . . . 8 class
3230, 31cfv 6050 . . . . . . 7 class (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖)))))
3332, 25wceq 1632 . . . . . 6 wff (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))) = 𝑚
3428, 33wa 383 . . . . 5 wff (∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖)) ⊆ (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))) = 𝑚)
35 cn 11233 . . . . . 6 class
36 cmap 8026 . . . . . 6 class 𝑚
3735, 27, 36co 6815 . . . . 5 class (ℕ ↑𝑚 (1...𝑚))
3834, 6, 37wrex 3052 . . . 4 wff 𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖)) ⊆ (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))) = 𝑚)
3938, 2, 35wrex 3052 . . 3 wff 𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖)) ⊆ (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))) = 𝑚)
4039, 24, 11, 16coprab 6816 . 2 class {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖)) ⊆ (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))) = 𝑚)}
411, 40wceq 1632 1 wff PolyAP = {⟨⟨𝑚, 𝑘⟩, 𝑓⟩ ∣ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚 (1...𝑚))(∀𝑖 ∈ (1...𝑚)((𝑎 + (𝑑𝑖))(AP‘𝑘)(𝑑𝑖)) ⊆ (𝑓 “ {(𝑓‘(𝑎 + (𝑑𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑚) ↦ (𝑓‘(𝑎 + (𝑑𝑖))))) = 𝑚)}
Colors of variables: wff setvar class
This definition is referenced by:  vdwpc  15907
  Copyright terms: Public domain W3C validator