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 35105
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 35102 . 2 class Ray
2 vp . . . . . . . 8 setvar 𝑝
32cv 1540 . . . . . . 7 class 𝑝
4 vn . . . . . . . . 9 setvar 𝑛
54cv 1540 . . . . . . . 8 class 𝑛
6 cee 28143 . . . . . . . 8 class 𝔼
75, 6cfv 6543 . . . . . . 7 class (π”Όβ€˜π‘›)
83, 7wcel 2106 . . . . . 6 wff 𝑝 ∈ (π”Όβ€˜π‘›)
9 va . . . . . . . 8 setvar π‘Ž
109cv 1540 . . . . . . 7 class π‘Ž
1110, 7wcel 2106 . . . . . 6 wff π‘Ž ∈ (π”Όβ€˜π‘›)
123, 10wne 2940 . . . . . 6 wff 𝑝 β‰  π‘Ž
138, 11, 12w3a 1087 . . . . 5 wff (𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž)
14 vr . . . . . . 7 setvar π‘Ÿ
1514cv 1540 . . . . . 6 class π‘Ÿ
16 vx . . . . . . . . . 10 setvar π‘₯
1716cv 1540 . . . . . . . . 9 class π‘₯
1810, 17cop 4634 . . . . . . . 8 class βŸ¨π‘Ž, π‘₯⟩
19 coutsideof 35086 . . . . . . . 8 class OutsideOf
203, 18, 19wbr 5148 . . . . . . 7 wff 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩
2120, 16, 7crab 3432 . . . . . 6 class {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩}
2215, 21wceq 1541 . . . . 5 wff π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩}
2313, 22wa 396 . . . 4 wff ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})
24 cn 12211 . . . 4 class β„•
2523, 4, 24wrex 3070 . . 3 wff βˆƒπ‘› ∈ β„• ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})
2625, 2, 9, 14coprab 7409 . 2 class {βŸ¨βŸ¨π‘, π‘ŽβŸ©, π‘ŸβŸ© ∣ βˆƒπ‘› ∈ β„• ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})}
271, 26wceq 1541 1 wff Ray = {βŸ¨βŸ¨π‘, π‘ŽβŸ©, π‘ŸβŸ© ∣ βˆƒπ‘› ∈ β„• ((𝑝 ∈ (π”Όβ€˜π‘›) ∧ π‘Ž ∈ (π”Όβ€˜π‘›) ∧ 𝑝 β‰  π‘Ž) ∧ π‘Ÿ = {π‘₯ ∈ (π”Όβ€˜π‘›) ∣ 𝑝OutsideOfβŸ¨π‘Ž, π‘₯⟩})}
Colors of variables: wff setvar class
This definition is referenced by:  funray  35107  fvray  35108
  Copyright terms: Public domain W3C validator