Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ray Unicode version

Definition df-ray 24101
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
StepHypRef Expression
1 cray 24098 . 2  class Ray
2 vp . . . . . . . 8  set  p
32cv 1618 . . . . . . 7  class  p
4 vn . . . . . . . . 9  set  n
54cv 1618 . . . . . . . 8  class  n
6 cee 23856 . . . . . . . 8  class  EE
75, 6cfv 4638 . . . . . . 7  class  ( EE
`  n )
83, 7wcel 1621 . . . . . 6  wff  p  e.  ( EE `  n
)
9 va . . . . . . . 8  set  a
109cv 1618 . . . . . . 7  class  a
1110, 7wcel 1621 . . . . . 6  wff  a  e.  ( EE `  n
)
123, 10wne 2419 . . . . . 6  wff  p  =/=  a
138, 11, 12w3a 939 . . . . 5  wff  ( p  e.  ( EE `  n )  /\  a  e.  ( EE `  n
)  /\  p  =/=  a )
14 vr . . . . . . 7  set  r
1514cv 1618 . . . . . 6  class  r
16 vx . . . . . . . . . 10  set  x
1716cv 1618 . . . . . . . . 9  class  x
1810, 17cop 3584 . . . . . . . 8  class  <. a ,  x >.
19 coutsideof 24082 . . . . . . . 8  class OutsideOf
203, 18, 19wbr 3963 . . . . . . 7  wff  pOutsideOf <. a ,  x >.
2120, 16, 7crab 2519 . . . . . 6  class  { x  e.  ( EE `  n
)  |  pOutsideOf <. a ,  x >. }
2215, 21wceq 1619 . . . . 5  wff  r  =  { x  e.  ( EE `  n )  |  pOutsideOf <. a ,  x >. }
2313, 22wa 360 . . . 4  wff  ( ( p  e.  ( EE
`  n )  /\  a  e.  ( EE `  n )  /\  p  =/=  a )  /\  r  =  { x  e.  ( EE `  n )  |  pOutsideOf <. a ,  x >. } )
24 cn 9679 . . . 4  class  NN
2523, 4, 24wrex 2517 . . 3  wff  E. n  e.  NN  ( ( p  e.  ( EE `  n )  /\  a  e.  ( EE `  n
)  /\  p  =/=  a )  /\  r  =  { x  e.  ( EE `  n )  |  pOutsideOf <. a ,  x >. } )
2625, 2, 9, 14coprab 5758 . 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 >. } ) }
271, 26wceq 1619 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 >. } ) }
Colors of variables: wff set class
This definition is referenced by:  funray  24103  fvray  24104
  Copyright terms: Public domain W3C validator