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

Definition df-slices 26193
Description: Return the slices generated by the Dedekind cut of a set of points. Definition 1 of [AitkenNG] p. 2. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-slices  |- slices  =  ( f  e. Ibg  |->  ( x  e.  ~P (PPoints `  f
)  |->  { <. a ,  b >.  |  ( ( ( a  u.  b )  =  x  /\  ( a  i^i  b )  =  (/) )  /\  ( a  =/=  (/)  /\  b  =/=  (/) )  /\  ( a  e.  (convex `  f )  /\  b  e.  (convex `  f )
) ) } ) )
Distinct variable group:    x, f, a, b

Detailed syntax breakdown of Definition df-slices
StepHypRef Expression
1 cslices 26192 . 2  class slices
2 vf . . 3  set  f
3 cibg 26107 . . 3  class Ibg
4 vx . . . 4  set  x
52cv 1622 . . . . . 6  class  f
6 cpoints 26056 . . . . . 6  class PPoints
75, 6cfv 5255 . . . . 5  class  (PPoints `  f
)
87cpw 3625 . . . 4  class  ~P (PPoints `  f )
9 va . . . . . . . . . 10  set  a
109cv 1622 . . . . . . . . 9  class  a
11 vb . . . . . . . . . 10  set  b
1211cv 1622 . . . . . . . . 9  class  b
1310, 12cun 3150 . . . . . . . 8  class  ( a  u.  b )
144cv 1622 . . . . . . . 8  class  x
1513, 14wceq 1623 . . . . . . 7  wff  ( a  u.  b )  =  x
1610, 12cin 3151 . . . . . . . 8  class  ( a  i^i  b )
17 c0 3455 . . . . . . . 8  class  (/)
1816, 17wceq 1623 . . . . . . 7  wff  ( a  i^i  b )  =  (/)
1915, 18wa 358 . . . . . 6  wff  ( ( a  u.  b )  =  x  /\  (
a  i^i  b )  =  (/) )
2010, 17wne 2446 . . . . . . 7  wff  a  =/=  (/)
2112, 17wne 2446 . . . . . . 7  wff  b  =/=  (/)
2220, 21wa 358 . . . . . 6  wff  ( a  =/=  (/)  /\  b  =/=  (/) )
23 cconvex 26178 . . . . . . . . 9  class convex
245, 23cfv 5255 . . . . . . . 8  class  (convex `  f )
2510, 24wcel 1684 . . . . . . 7  wff  a  e.  (convex `  f )
2612, 24wcel 1684 . . . . . . 7  wff  b  e.  (convex `  f )
2725, 26wa 358 . . . . . 6  wff  ( a  e.  (convex `  f
)  /\  b  e.  (convex `  f ) )
2819, 22, 27w3a 934 . . . . 5  wff  ( ( ( a  u.  b
)  =  x  /\  ( a  i^i  b
)  =  (/) )  /\  ( a  =/=  (/)  /\  b  =/=  (/) )  /\  (
a  e.  (convex `  f )  /\  b  e.  (convex `  f )
) )
2928, 9, 11copab 4076 . . . 4  class  { <. a ,  b >.  |  ( ( ( a  u.  b )  =  x  /\  ( a  i^i  b )  =  (/) )  /\  ( a  =/=  (/)  /\  b  =/=  (/) )  /\  ( a  e.  (convex `  f )  /\  b  e.  (convex `  f )
) ) }
304, 8, 29cmpt 4077 . . 3  class  ( x  e.  ~P (PPoints `  f
)  |->  { <. a ,  b >.  |  ( ( ( a  u.  b )  =  x  /\  ( a  i^i  b )  =  (/) )  /\  ( a  =/=  (/)  /\  b  =/=  (/) )  /\  ( a  e.  (convex `  f )  /\  b  e.  (convex `  f )
) ) } )
312, 3, 30cmpt 4077 . 2  class  ( f  e. Ibg  |->  ( x  e. 
~P (PPoints `  f )  |->  { <. a ,  b
>.  |  ( (
( a  u.  b
)  =  x  /\  ( a  i^i  b
)  =  (/) )  /\  ( a  =/=  (/)  /\  b  =/=  (/) )  /\  (
a  e.  (convex `  f )  /\  b  e.  (convex `  f )
) ) } ) )
321, 31wceq 1623 1  wff slices  =  ( f  e. Ibg  |->  ( x  e.  ~P (PPoints `  f
)  |->  { <. a ,  b >.  |  ( ( ( a  u.  b )  =  x  /\  ( a  i^i  b )  =  (/) )  /\  ( a  =/=  (/)  /\  b  =/=  (/) )  /\  ( a  e.  (convex `  f )  /\  b  e.  (convex `  f )
) ) } ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator