Metamath Proof Explorer

Definition df-ray

Description: Define the Ray function. This function generates the set of all points that lie on the ray starting at p and passing through a . Definition 6.8 of Schwabhauser p. 44. (Contributed by Scott Fenton, 21-Oct-2013)

Ref Expression
Assertion df-ray ⊢ Ray = p a r | ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n ∧ a ∈ 𝔼 ⁡ n ∧ p ≠ a ∧ r = x ∈ 𝔼 ⁡ n | p OutsideOf a x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cray class Ray
1 vp setvar p
2 va setvar a
3 vr setvar r
4 vn setvar n
5 cn class ℕ
6 1 cv setvar p
7 cee class 𝔼
8 4 cv setvar n
9 8 7 cfv class 𝔼 ⁡ n
10 6 9 wcel wff p ∈ 𝔼 ⁡ n
11 2 cv setvar a
12 11 9 wcel wff a ∈ 𝔼 ⁡ n
13 6 11 wne wff p ≠ a
14 10 12 13 w3a wff p ∈ 𝔼 ⁡ n ∧ a ∈ 𝔼 ⁡ n ∧ p ≠ a
15 3 cv setvar r
16 vx setvar x
17 coutsideof class OutsideOf
18 16 cv setvar x
19 11 18 cop class a x
20 6 19 17 wbr wff p OutsideOf a x
21 20 16 9 crab class x ∈ 𝔼 ⁡ n | p OutsideOf a x
22 15 21 wceq wff r = x ∈ 𝔼 ⁡ n | p OutsideOf a x
23 14 22 wa wff p ∈ 𝔼 ⁡ n ∧ a ∈ 𝔼 ⁡ n ∧ p ≠ a ∧ r = x ∈ 𝔼 ⁡ n | p OutsideOf a x
24 23 4 5 wrex wff ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n ∧ a ∈ 𝔼 ⁡ n ∧ p ≠ a ∧ r = x ∈ 𝔼 ⁡ n | p OutsideOf a x
25 24 1 2 3 coprab class p a r | ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n ∧ a ∈ 𝔼 ⁡ n ∧ p ≠ a ∧ r = x ∈ 𝔼 ⁡ n | p OutsideOf a x
26 0 25 wceq wff Ray = p a r | ∃ n ∈ ℕ p ∈ 𝔼 ⁡ n ∧ a ∈ 𝔼 ⁡ n ∧ p ≠ a ∧ r = x ∈ 𝔼 ⁡ n | p OutsideOf a x