Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ray Structured version   Visualization version   GIF version

Definition df-ray 34776
Description: Define the Ray function. This function generates the set of all points that lie on the ray starting at 𝑝 and passing through π‘Ž. Definition 6.8 of [Schwabhauser] p. 44. (Contributed by Scott Fenton, 21-Oct-2013.)
Assertion
Ref Expression
df-ray Ray = {βŸ¨βŸ¨π‘, π‘ŽβŸ©, π‘ŸβŸ© ∣ βˆƒπ‘› ∈ β„• ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})}
Distinct variable group:   𝑝,π‘Ž,π‘Ÿ,𝑛,π‘₯

Detailed syntax breakdown of Definition df-ray
StepHypRef Expression
1 cray 34773 . 2 class Ray
2 vp . . . . . . . 8 setvar 𝑝
32cv 1541 . . . . . . 7 class 𝑝
4 vn . . . . . . . . 9 setvar 𝑛
54cv 1541 . . . . . . . 8 class 𝑛
6 cee 27886 . . . . . . . 8 class 𝔼
75, 6cfv 6500 . . . . . . 7 class (π”Όβ€˜π‘›)
83, 7wcel 2107 . . . . . 6 wff 𝑝 ∈ (π”Όβ€˜π‘›)
9 va . . . . . . . 8 setvar π‘Ž
109cv 1541 . . . . . . 7 class π‘Ž
1110, 7wcel 2107 . . . . . 6 wff π‘Ž ∈ (π”Όβ€˜π‘›)
123, 10wne 2940 . . . . . 6 wff 𝑝 β‰  π‘Ž
138, 11, 12w3a 1088 . . . . 5 wff (𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž)
14 vr . . . . . . 7 setvar π‘Ÿ
1514cv 1541 . . . . . 6 class π‘Ÿ
16 vx . . . . . . . . . 10 setvar π‘₯
1716cv 1541 . . . . . . . . 9 class π‘₯
1810, 17cop 4596 . . . . . . . 8 class βŸ¨π‘Ž, π‘₯⟩
19 coutsideof 34757 . . . . . . . 8 class OutsideOf
203, 18, 19wbr 5109 . . . . . . 7 wff 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩
2120, 16, 7crab 3406 . . . . . 6 class {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩}
2215, 21wceq 1542 . . . . 5 wff π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩}
2313, 22wa 397 . . . 4 wff ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})
24 cn 12161 . . . 4 class β„•
2523, 4, 24wrex 3070 . . 3 wff βˆƒπ‘› ∈ β„• ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})
2625, 2, 9, 14coprab 7362 . 2 class {βŸ¨βŸ¨π‘, π‘ŽβŸ©, π‘ŸβŸ© ∣ βˆƒπ‘› ∈ β„• ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})}
271, 26wceq 1542 1 wff Ray = {βŸ¨βŸ¨π‘, π‘ŽβŸ©, π‘ŸβŸ© ∣ βˆƒπ‘› ∈ β„• ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})}
Colors of variables: wff setvar class
This definition is referenced by:  funray  34778  fvray  34779
  Copyright terms: Public domain W3C validator