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⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (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 \in 𝔼 (n)$
11	2	cv	$setvar a$
12	11 9	wcel	$wff a \in 𝔼 (n)$
13	6 11	wne	$wff p \neq a$
14	10 12 13	w3a	$wff (p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq 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 \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}$
22	15 21	wceq	$wff r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\}$
23	14 22	wa	$wff ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})$
24	23 4 5	wrex	$wff \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})$
25	24 1 2 3	coprab	$class \{⟨⟨p, a⟩, r⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})\}$
26	0 25	wceq	$wff Ray = \{⟨⟨p, a⟩, r⟩ \| \exists n \in ℕ ((p \in 𝔼 (n) \land a \in 𝔼 (n) \land p \neq a) \land r = \{x \in 𝔼 (n) \| p OutsideOf ⟨a, x⟩\})\}$

Metamath Proof Explorer

Definition df-ray

Detailed syntax breakdown