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 31887
 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 31884 . 2 class Ray
2 vp . . . . . . . 8 setvar 𝑝
32cv 1479 . . . . . . 7 class 𝑝
4 vn . . . . . . . . 9 setvar 𝑛
54cv 1479 . . . . . . . 8 class 𝑛
6 cee 25668 . . . . . . . 8 class 𝔼
75, 6cfv 5847 . . . . . . 7 class (𝔼‘𝑛)
83, 7wcel 1987 . . . . . 6 wff 𝑝 ∈ (𝔼‘𝑛)
9 va . . . . . . . 8 setvar 𝑎
109cv 1479 . . . . . . 7 class 𝑎
1110, 7wcel 1987 . . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
123, 10wne 2790 . . . . . 6 wff 𝑝𝑎
138, 11, 12w3a 1036 . . . . 5 wff (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎)
14 vr . . . . . . 7 setvar 𝑟
1514cv 1479 . . . . . 6 class 𝑟
16 vx . . . . . . . . . 10 setvar 𝑥
1716cv 1479 . . . . . . . . 9 class 𝑥
1810, 17cop 4154 . . . . . . . 8 class 𝑎, 𝑥
19 coutsideof 31868 . . . . . . . 8 class OutsideOf
203, 18, 19wbr 4613 . . . . . . 7 wff 𝑝OutsideOf⟨𝑎, 𝑥
2120, 16, 7crab 2911 . . . . . 6 class {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩}
2215, 21wceq 1480 . . . . 5 wff 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩}
2313, 22wa 384 . . . 4 wff ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})
24 cn 10964 . . . 4 class
2523, 4, 24wrex 2908 . . 3 wff 𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})
2625, 2, 9, 14coprab 6605 . 2 class {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})}
271, 26wceq 1480 1 wff Ray = {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})}
 Colors of variables: wff setvar class This definition is referenced by:  funray  31889  fvray  31890
 Copyright terms: Public domain W3C validator