Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ray2 Unicode version

Definition df-ray2 26152
Description: Definition of the ray xy degenerated or not. Definition 11 of [AitkenIBG] p. 4. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-ray2  |- ray  =  ( f  e. Ibg  |->  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( ( x ( seg `  f
) y )  u. 
{ z  e.  (PPoints `  f )  |  y  e.  ( x (btw
`  f ) z ) } ) ,  { x } ) ) )
Distinct variable group:    x, f, y, z

Detailed syntax breakdown of Definition df-ray2
StepHypRef Expression
1 cray2 26151 . 2  class ray
2 vf . . 3  set  f
3 cibg 26107 . . 3  class Ibg
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1622 . . . . 5  class  f
7 cpoints 26056 . . . . 5  class PPoints
86, 7cfv 5255 . . . 4  class  (PPoints `  f
)
94cv 1622 . . . . . 6  class  x
105cv 1622 . . . . . 6  class  y
119, 10wne 2446 . . . . 5  wff  x  =/=  y
12 cseg 26130 . . . . . . . 8  class  seg
136, 12cfv 5255 . . . . . . 7  class  ( seg `  f )
149, 10, 13co 5858 . . . . . 6  class  ( x ( seg `  f
) y )
15 vz . . . . . . . . . 10  set  z
1615cv 1622 . . . . . . . . 9  class  z
17 cbtw 26106 . . . . . . . . . 10  class btw
186, 17cfv 5255 . . . . . . . . 9  class  (btw `  f )
199, 16, 18co 5858 . . . . . . . 8  class  ( x (btw `  f )
z )
2010, 19wcel 1684 . . . . . . 7  wff  y  e.  ( x (btw `  f ) z )
2120, 15, 8crab 2547 . . . . . 6  class  { z  e.  (PPoints `  f
)  |  y  e.  ( x (btw `  f ) z ) }
2214, 21cun 3150 . . . . 5  class  ( ( x ( seg `  f
) y )  u. 
{ z  e.  (PPoints `  f )  |  y  e.  ( x (btw
`  f ) z ) } )
239csn 3640 . . . . 5  class  { x }
2411, 22, 23cif 3565 . . . 4  class  if ( x  =/=  y ,  ( ( x ( seg `  f ) y )  u.  {
z  e.  (PPoints `  f
)  |  y  e.  ( x (btw `  f ) z ) } ) ,  {
x } )
254, 5, 8, 8, 24cmpt2 5860 . . 3  class  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( ( x ( seg `  f
) y )  u. 
{ z  e.  (PPoints `  f )  |  y  e.  ( x (btw
`  f ) z ) } ) ,  { x } ) )
262, 3, 25cmpt 4077 . 2  class  ( f  e. Ibg  |->  ( x  e.  (PPoints `  f ) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( ( x ( seg `  f ) y )  u.  {
z  e.  (PPoints `  f
)  |  y  e.  ( x (btw `  f ) z ) } ) ,  {
x } ) ) )
271, 26wceq 1623 1  wff ray  =  ( f  e. Ibg  |->  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  ( ( x ( seg `  f
) y )  u. 
{ z  e.  (PPoints `  f )  |  y  e.  ( x (btw
`  f ) z ) } ) ,  { x } ) ) )
Colors of variables: wff set class
This definition is referenced by:  isray2  26153  isray  26154
  Copyright terms: Public domain W3C validator