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

Definition df-Cut 25594
Description: Return the cutpoints of a set of points  ( x  u.  y ) where  x and  y are the slices of a Dedekind cut of  ( x  u.  y
). Definition 2 of [AitkenNG] p. 2. (For my private use only. Don't use.) (Contributed by FL, 5-Mar-2016.)
Assertion
Ref Expression
df-Cut  |- Cut  =  ( f  e. Ibg  |->  ( x  e.  ~P (PPoints `  f
) ,  y  e. 
~P (PPoints `  f )  |->  { c  e.  ( x  u.  y )  |  A. u  e.  ( x  u.  y
) A. v  e.  ( x  u.  y
) ( u  e.  ( c (btw `  f ) v )  ->  ( ( u  e.  x  /\  v  e.  x )  \/  (
u  e.  y  /\  v  e.  y )
) ) } ) )
Distinct variable group:    x, f, y, c, u, v

Detailed syntax breakdown of Definition df-Cut
StepHypRef Expression
1 ccut 25593 . 2  class Cut
2 vf . . 3  set  f
3 cibg 25506 . . 3  class Ibg
4 vx . . . 4  set  x
5 vy . . . 4  set  y
62cv 1627 . . . . . 6  class  f
7 cpoints 25455 . . . . . 6  class PPoints
86, 7cfv 5221 . . . . 5  class  (PPoints `  f
)
98cpw 3626 . . . 4  class  ~P (PPoints `  f )
10 vu . . . . . . . . . 10  set  u
1110cv 1627 . . . . . . . . 9  class  u
12 vc . . . . . . . . . . 11  set  c
1312cv 1627 . . . . . . . . . 10  class  c
14 vv . . . . . . . . . . 11  set  v
1514cv 1627 . . . . . . . . . 10  class  v
16 cbtw 25505 . . . . . . . . . . 11  class btw
176, 16cfv 5221 . . . . . . . . . 10  class  (btw `  f )
1813, 15, 17co 5819 . . . . . . . . 9  class  ( c (btw `  f )
v )
1911, 18wcel 1688 . . . . . . . 8  wff  u  e.  ( c (btw `  f ) v )
2010, 4wel 1689 . . . . . . . . . 10  wff  u  e.  x
2114, 4wel 1689 . . . . . . . . . 10  wff  v  e.  x
2220, 21wa 360 . . . . . . . . 9  wff  ( u  e.  x  /\  v  e.  x )
2310, 5wel 1689 . . . . . . . . . 10  wff  u  e.  y
2414, 5wel 1689 . . . . . . . . . 10  wff  v  e.  y
2523, 24wa 360 . . . . . . . . 9  wff  ( u  e.  y  /\  v  e.  y )
2622, 25wo 359 . . . . . . . 8  wff  ( ( u  e.  x  /\  v  e.  x )  \/  ( u  e.  y  /\  v  e.  y ) )
2719, 26wi 6 . . . . . . 7  wff  ( u  e.  ( c (btw
`  f ) v )  ->  ( (
u  e.  x  /\  v  e.  x )  \/  ( u  e.  y  /\  v  e.  y ) ) )
284cv 1627 . . . . . . . 8  class  x
295cv 1627 . . . . . . . 8  class  y
3028, 29cun 3151 . . . . . . 7  class  ( x  u.  y )
3127, 14, 30wral 2544 . . . . . 6  wff  A. v  e.  ( x  u.  y
) ( u  e.  ( c (btw `  f ) v )  ->  ( ( u  e.  x  /\  v  e.  x )  \/  (
u  e.  y  /\  v  e.  y )
) )
3231, 10, 30wral 2544 . . . . 5  wff  A. u  e.  ( x  u.  y
) A. v  e.  ( x  u.  y
) ( u  e.  ( c (btw `  f ) v )  ->  ( ( u  e.  x  /\  v  e.  x )  \/  (
u  e.  y  /\  v  e.  y )
) )
3332, 12, 30crab 2548 . . . 4  class  { c  e.  ( x  u.  y )  |  A. u  e.  ( x  u.  y ) A. v  e.  ( x  u.  y
) ( u  e.  ( c (btw `  f ) v )  ->  ( ( u  e.  x  /\  v  e.  x )  \/  (
u  e.  y  /\  v  e.  y )
) ) }
344, 5, 9, 9, 33cmpt2 5821 . . 3  class  ( x  e.  ~P (PPoints `  f
) ,  y  e. 
~P (PPoints `  f )  |->  { c  e.  ( x  u.  y )  |  A. u  e.  ( x  u.  y
) A. v  e.  ( x  u.  y
) ( u  e.  ( c (btw `  f ) v )  ->  ( ( u  e.  x  /\  v  e.  x )  \/  (
u  e.  y  /\  v  e.  y )
) ) } )
352, 3, 34cmpt 4078 . 2  class  ( f  e. Ibg  |->  ( x  e. 
~P (PPoints `  f ) ,  y  e.  ~P (PPoints `  f )  |->  { c  e.  ( x  u.  y )  | 
A. u  e.  ( x  u.  y ) A. v  e.  ( x  u.  y ) ( u  e.  ( c (btw `  f
) v )  -> 
( ( u  e.  x  /\  v  e.  x )  \/  (
u  e.  y  /\  v  e.  y )
) ) } ) )
361, 35wceq 1628 1  wff Cut  =  ( f  e. Ibg  |->  ( x  e.  ~P (PPoints `  f
) ,  y  e. 
~P (PPoints `  f )  |->  { c  e.  ( x  u.  y )  |  A. u  e.  ( x  u.  y
) A. v  e.  ( x  u.  y
) ( u  e.  ( c (btw `  f ) v )  ->  ( ( u  e.  x  /\  v  e.  x )  \/  (
u  e.  y  /\  v  e.  y )
) ) } ) )
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator