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 = { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cray	⊢ Ray
1		vp	⊢ 𝑝
2		va	⊢ 𝑎
3		vr	⊢ 𝑟
4		vn	⊢ 𝑛
5		cn	⊢ ℕ
6	1	cv	⊢ 𝑝
7		cee	⊢ 𝔼
8	4	cv	⊢ 𝑛
9	8 7	cfv	⊢ ( 𝔼 ‘ 𝑛 )
10	6 9	wcel	⊢ 𝑝 ∈ ( 𝔼 ‘ 𝑛 )
11	2	cv	⊢ 𝑎
12	11 9	wcel	⊢ 𝑎 ∈ ( 𝔼 ‘ 𝑛 )
13	6 11	wne	⊢ 𝑝 ≠ 𝑎
14	10 12 13	w3a	⊢ ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 )
15	3	cv	⊢ 𝑟
16		vx	⊢ 𝑥
17		coutsideof	⊢ OutsideOf
18	16	cv	⊢ 𝑥
19	11 18	cop	⊢ ⟨ 𝑎 , 𝑥 ⟩
20	6 19 17	wbr	⊢ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩
21	20 16 9	crab	⊢ { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ }
22	15 21	wceq	⊢ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ }
23	14 22	wa	⊢ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } )
24	23 4 5	wrex	⊢ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } )
25	24 1 2 3	coprab	⊢ { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) }
26	0 25	wceq	⊢ Ray = { ⟨ ⟨ 𝑝 , 𝑎 ⟩ , 𝑟 ⟩ ∣ ∃ 𝑛 ∈ ℕ ( ( 𝑝 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑎 ∈ ( 𝔼 ‘ 𝑛 ) ∧ 𝑝 ≠ 𝑎 ) ∧ 𝑟 = { 𝑥 ∈ ( 𝔼 ‘ 𝑛 ) ∣ 𝑝 OutsideOf ⟨ 𝑎 , 𝑥 ⟩ } ) }