Definition df-ray 32245

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.)

Assertion

Ref	Expression
df-ray	|- Ray = { <. <. p , a >. , r >. | E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | pOutsideOf <. a , x >. } ) }

Distinct variable group:   p, a, r, n, x

Detailed syntax breakdown of Definition df-ray

Step	Hyp	Ref	Expression
1		cray 32242	. 2 class Ray
2		vp	. . . . . . . 8 setvar p
3	2	cv 1482	. . . . . . 7 class p
4		vn	. . . . . . . . 9 setvar n
5	4	cv 1482	. . . . . . . 8 class n
6		cee 25768	. . . . . . . 8 class EE
7	5, 6	cfv 5888	. . . . . . 7 class ( EE ` n )
8	3, 7	wcel 1990	. . . . . 6 wff p e. ( EE ` n )
9		va	. . . . . . . 8 setvar a
10	9	cv 1482	. . . . . . 7 class a
11	10, 7	wcel 1990	. . . . . 6 wff a e. ( EE ` n )
12	3, 10	wne 2794	. . . . . 6 wff p =/= a
13	8, 11, 12	w3a 1037	. . . . 5 wff ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a )
14		vr	. . . . . . 7 setvar r
15	14	cv 1482	. . . . . 6 class r
16		vx	. . . . . . . . . 10 setvar x
17	16	cv 1482	. . . . . . . . 9 class x
18	10, 17	cop 4183	. . . . . . . 8 class <. a , x >.
19		coutsideof 32226	. . . . . . . 8 class OutsideOf
20	3, 18, 19	wbr 4653	. . . . . . 7 wff pOutsideOf <. a , x >.
21	20, 16, 7	crab 2916	. . . . . 6 class { x e. ( EE ` n ) | pOutsideOf <. a , x >. }
22	15, 21	wceq 1483	. . . . 5 wff r = { x e. ( EE ` n ) | pOutsideOf <. a , x >. }
23	13, 22	wa 384	. . . 4 wff ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | pOutsideOf <. a , x >. } )
24		cn 11020	. . . 4 class NN
25	23, 4, 24	wrex 2913	. . 3 wff E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | pOutsideOf <. a , x >. } )
26	25, 2, 9, 14	coprab 6651	. 2 class { <. <. p , a >. , r >. | E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | pOutsideOf <. a , x >. } ) }
27	1, 26	wceq 1483	1 wff Ray = { <. <. p , a >. , r >. | E. n e. NN ( ( p e. ( EE ` n ) /\ a e. ( EE ` n ) /\ p =/= a ) /\ r = { x e. ( EE ` n ) | pOutsideOf <. a , x >. } ) }

This definition is referenced by:  funray  32247  fvray  32248