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 16903
Description: Define the "contains a polychromatic collection of APs" predicate. See vdwpc 16913 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
StepHypRef Expression
1 cvdwp 16900 . 2 class PolyAP
2 va . . . . . . . . . . 11 setvar π‘Ž
32cv 1541 . . . . . . . . . 10 class π‘Ž
4 vi . . . . . . . . . . . 12 setvar 𝑖
54cv 1541 . . . . . . . . . . 11 class 𝑖
6 vd . . . . . . . . . . . 12 setvar 𝑑
76cv 1541 . . . . . . . . . . 11 class 𝑑
85, 7cfv 6544 . . . . . . . . . 10 class (π‘‘β€˜π‘–)
9 caddc 11113 . . . . . . . . . 10 class +
103, 8, 9co 7409 . . . . . . . . 9 class (π‘Ž + (π‘‘β€˜π‘–))
11 vk . . . . . . . . . . 11 setvar π‘˜
1211cv 1541 . . . . . . . . . 10 class π‘˜
13 cvdwa 16898 . . . . . . . . . 10 class AP
1412, 13cfv 6544 . . . . . . . . 9 class (APβ€˜π‘˜)
1510, 8, 14co 7409 . . . . . . . 8 class ((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–))
16 vf . . . . . . . . . . 11 setvar 𝑓
1716cv 1541 . . . . . . . . . 10 class 𝑓
1817ccnv 5676 . . . . . . . . 9 class ◑𝑓
1910, 17cfv 6544 . . . . . . . . . 10 class (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))
2019csn 4629 . . . . . . . . 9 class {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))}
2118, 20cima 5680 . . . . . . . 8 class (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))})
2215, 21wss 3949 . . . . . . 7 wff ((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–)) βŠ† (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))})
23 c1 11111 . . . . . . . 8 class 1
24 vm . . . . . . . . 9 setvar π‘š
2524cv 1541 . . . . . . . 8 class π‘š
26 cfz 13484 . . . . . . . 8 class ...
2723, 25, 26co 7409 . . . . . . 7 class (1...π‘š)
2822, 4, 27wral 3062 . . . . . 6 wff βˆ€π‘– ∈ (1...π‘š)((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–)) βŠ† (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))})
294, 27, 19cmpt 5232 . . . . . . . . 9 class (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))
3029crn 5678 . . . . . . . 8 class ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))
31 chash 14290 . . . . . . . 8 class β™―
3230, 31cfv 6544 . . . . . . 7 class (β™―β€˜ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))))
3332, 25wceq 1542 . . . . . 6 wff (β™―β€˜ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))) = π‘š
3428, 33wa 397 . . . . 5 wff (βˆ€π‘– ∈ (1...π‘š)((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–)) βŠ† (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))}) ∧ (β™―β€˜ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))) = π‘š)
35 cn 12212 . . . . . 6 class β„•
36 cmap 8820 . . . . . 6 class ↑m
3735, 27, 36co 7409 . . . . 5 class (β„• ↑m (1...π‘š))
3834, 6, 37wrex 3071 . . . 4 wff βˆƒπ‘‘ ∈ (β„• ↑m (1...π‘š))(βˆ€π‘– ∈ (1...π‘š)((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–)) βŠ† (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))}) ∧ (β™―β€˜ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))) = π‘š)
3938, 2, 35wrex 3071 . . 3 wff βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ (β„• ↑m (1...π‘š))(βˆ€π‘– ∈ (1...π‘š)((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–)) βŠ† (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))}) ∧ (β™―β€˜ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))) = π‘š)
4039, 24, 11, 16coprab 7410 . 2 class {βŸ¨βŸ¨π‘š, π‘˜βŸ©, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ (β„• ↑m (1...π‘š))(βˆ€π‘– ∈ (1...π‘š)((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–)) βŠ† (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))}) ∧ (β™―β€˜ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))) = π‘š)}
411, 40wceq 1542 1 wff PolyAP = {βŸ¨βŸ¨π‘š, π‘˜βŸ©, π‘“βŸ© ∣ βˆƒπ‘Ž ∈ β„• βˆƒπ‘‘ ∈ (β„• ↑m (1...π‘š))(βˆ€π‘– ∈ (1...π‘š)((π‘Ž + (π‘‘β€˜π‘–))(APβ€˜π‘˜)(π‘‘β€˜π‘–)) βŠ† (◑𝑓 β€œ {(π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–)))}) ∧ (β™―β€˜ran (𝑖 ∈ (1...π‘š) ↦ (π‘“β€˜(π‘Ž + (π‘‘β€˜π‘–))))) = π‘š)}
Colors of variables: wff setvar class
This definition is referenced by:  vdwpc  16913
  Copyright terms: Public domain W3C validator