Definition df-ray 31415

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

Step	Hyp	Ref	Expression
1		cray 31412	. 2 class Ray
2		vp	. . . . . . . 8 setvar 𝑝
3	2	cv 1474	. . . . . . 7 class 𝑝
4		vn	. . . . . . . . 9 setvar 𝑛
5	4	cv 1474	. . . . . . . 8 class 𝑛
6		cee 25568	. . . . . . . 8 class 𝔼
7	5, 6	cfv 5804	. . . . . . 7 class (𝔼‘𝑛)
8	3, 7	wcel 1977	. . . . . 6 wff 𝑝 ∈ (𝔼‘𝑛)
9		va	. . . . . . . 8 setvar 𝑎
10	9	cv 1474	. . . . . . 7 class 𝑎
11	10, 7	wcel 1977	. . . . . 6 wff 𝑎 ∈ (𝔼‘𝑛)
12	3, 10	wne 2780	. . . . . 6 wff 𝑝 ≠ 𝑎
13	8, 11, 12	w3a 1031	. . . . 5 wff (𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎)
14		vr	. . . . . . 7 setvar 𝑟
15	14	cv 1474	. . . . . 6 class 𝑟
16		vx	. . . . . . . . . 10 setvar 𝑥
17	16	cv 1474	. . . . . . . . 9 class 𝑥
18	10, 17	cop 4131	. . . . . . . 8 class ⟨𝑎, 𝑥⟩
19		coutsideof 31396	. . . . . . . 8 class OutsideOf
20	3, 18, 19	wbr 4583	. . . . . . 7 wff 𝑝OutsideOf⟨𝑎, 𝑥⟩
21	20, 16, 7	crab 2900	. . . . . 6 class {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩}
22	15, 21	wceq 1475	. . . . 5 wff 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩}
23	13, 22	wa 383	. . . 4 wff ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})
24		cn 10897	. . . 4 class ℕ
25	23, 4, 24	wrex 2897	. . 3 wff ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})
26	25, 2, 9, 14	coprab 6550	. 2 class {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})}
27	1, 26	wceq 1475	1 wff Ray = {⟨⟨𝑝, 𝑎⟩, 𝑟⟩ ∣ ∃𝑛 ∈ ℕ ((𝑝 ∈ (𝔼‘𝑛) ∧ 𝑎 ∈ (𝔼‘𝑛) ∧ 𝑝 ≠ 𝑎) ∧ 𝑟 = {𝑥 ∈ (𝔼‘𝑛) ∣ 𝑝OutsideOf⟨𝑎, 𝑥⟩})}

This definition is referenced by:  funray  31417  fvray  31418