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

Definition df-seg2 25463
Description: Definition of the segment xy degenerated or not. Definition 8 of [AitkenIBG] p. 4. (For my private use only. Don't use.) (Contributed by FL, 28-Feb-2016.)
Assertion
Ref Expression
df-seg2  |-  seg  =  ( f  e. Ibg  |->  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  { z  e.  (PPoints `  f
)  |  ( z  e.  ( x (btw
`  f ) y )  \/  z  =  x  \/  z  =  y ) } ,  { x } ) ) )
Distinct variable group:    x, f, y, z

Detailed syntax breakdown of Definition df-seg2
StepHypRef Expression
1 cseg 25462 . 2  class  seg
2 vf . . 3  set  f
3 cibg 25439 . . 3  class Ibg
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1618 . . . . 5  class  f
7 cpoints 25388 . . . . 5  class PPoints
86, 7cfv 4638 . . . 4  class  (PPoints `  f
)
94cv 1618 . . . . . 6  class  x
105cv 1618 . . . . . 6  class  y
119, 10wne 2419 . . . . 5  wff  x  =/=  y
12 vz . . . . . . . . 9  set  z
1312cv 1618 . . . . . . . 8  class  z
14 cbtw 25438 . . . . . . . . . 10  class btw
156, 14cfv 4638 . . . . . . . . 9  class  (btw `  f )
169, 10, 15co 5757 . . . . . . . 8  class  ( x (btw `  f )
y )
1713, 16wcel 1621 . . . . . . 7  wff  z  e.  ( x (btw `  f ) y )
1812, 4weq 1620 . . . . . . 7  wff  z  =  x
1912, 5weq 1620 . . . . . . 7  wff  z  =  y
2017, 18, 19w3o 938 . . . . . 6  wff  ( z  e.  ( x (btw
`  f ) y )  \/  z  =  x  \/  z  =  y )
2120, 12, 8crab 2519 . . . . 5  class  { z  e.  (PPoints `  f
)  |  ( z  e.  ( x (btw
`  f ) y )  \/  z  =  x  \/  z  =  y ) }
229csn 3581 . . . . 5  class  { x }
2311, 21, 22cif 3506 . . . 4  class  if ( x  =/=  y ,  { z  e.  (PPoints `  f )  |  ( z  e.  ( x (btw `  f )
y )  \/  z  =  x  \/  z  =  y ) } ,  { x }
)
244, 5, 8, 8, 23cmpt2 5759 . . 3  class  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  { z  e.  (PPoints `  f
)  |  ( z  e.  ( x (btw
`  f ) y )  \/  z  =  x  \/  z  =  y ) } ,  { x } ) )
252, 3, 24cmpt 4017 . 2  class  ( f  e. Ibg  |->  ( x  e.  (PPoints `  f ) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  { z  e.  (PPoints `  f )  |  ( z  e.  ( x (btw `  f )
y )  \/  z  =  x  \/  z  =  y ) } ,  { x }
) ) )
261, 25wceq 1619 1  wff  seg  =  ( f  e. Ibg  |->  ( x  e.  (PPoints `  f
) ,  y  e.  (PPoints `  f )  |->  if ( x  =/=  y ,  { z  e.  (PPoints `  f
)  |  ( z  e.  ( x (btw
`  f ) y )  \/  z  =  x  \/  z  =  y ) } ,  { x } ) ) )
Colors of variables: wff set class
This definition is referenced by:  sgplpte21  25464  sgplpte22  25470
  Copyright terms: Public domain W3C validator