Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-inftm Structured version   Unicode version

Definition df-inftm 26360
Description: Define the relation " x is infinitesimal with respect to  y " for a structure  w. (Contributed by Thierry Arnoux, 30-Jan-2018.)
Assertion
Ref Expression
df-inftm  |- <<<  =  (
w  e.  _V  |->  {
<. x ,  y >.  |  ( ( x  e.  ( Base `  w
)  /\  y  e.  ( Base `  w )
)  /\  ( ( 0g `  w ) ( lt `  w ) x  /\  A. n  e.  NN  ( n (.g `  w ) x ) ( lt `  w
) y ) ) } )
Distinct variable group:    w, n, x, y

Detailed syntax breakdown of Definition df-inftm
StepHypRef Expression
1 cinftm 26358 . 2  class <<<
2 vw . . 3  setvar  w
3 cvv 3078 . . 3  class  _V
4 vx . . . . . . . 8  setvar  x
54cv 1369 . . . . . . 7  class  x
62cv 1369 . . . . . . . 8  class  w
7 cbs 14295 . . . . . . . 8  class  Base
86, 7cfv 5529 . . . . . . 7  class  ( Base `  w )
95, 8wcel 1758 . . . . . 6  wff  x  e.  ( Base `  w
)
10 vy . . . . . . . 8  setvar  y
1110cv 1369 . . . . . . 7  class  y
1211, 8wcel 1758 . . . . . 6  wff  y  e.  ( Base `  w
)
139, 12wa 369 . . . . 5  wff  ( x  e.  ( Base `  w
)  /\  y  e.  ( Base `  w )
)
14 c0g 14500 . . . . . . . 8  class  0g
156, 14cfv 5529 . . . . . . 7  class  ( 0g
`  w )
16 cplt 15233 . . . . . . . 8  class  lt
176, 16cfv 5529 . . . . . . 7  class  ( lt
`  w )
1815, 5, 17wbr 4403 . . . . . 6  wff  ( 0g
`  w ) ( lt `  w ) x
19 vn . . . . . . . . . 10  setvar  n
2019cv 1369 . . . . . . . . 9  class  n
21 cmg 15536 . . . . . . . . . 10  class .g
226, 21cfv 5529 . . . . . . . . 9  class  (.g `  w
)
2320, 5, 22co 6203 . . . . . . . 8  class  ( n (.g `  w ) x )
2423, 11, 17wbr 4403 . . . . . . 7  wff  ( n (.g `  w ) x ) ( lt `  w ) y
25 cn 10436 . . . . . . 7  class  NN
2624, 19, 25wral 2799 . . . . . 6  wff  A. n  e.  NN  ( n (.g `  w ) x ) ( lt `  w
) y
2718, 26wa 369 . . . . 5  wff  ( ( 0g `  w ) ( lt `  w
) x  /\  A. n  e.  NN  (
n (.g `  w ) x ) ( lt `  w ) y )
2813, 27wa 369 . . . 4  wff  ( ( x  e.  ( Base `  w )  /\  y  e.  ( Base `  w
) )  /\  (
( 0g `  w
) ( lt `  w ) x  /\  A. n  e.  NN  (
n (.g `  w ) x ) ( lt `  w ) y ) )
2928, 4, 10copab 4460 . . 3  class  { <. x ,  y >.  |  ( ( x  e.  (
Base `  w )  /\  y  e.  ( Base `  w ) )  /\  ( ( 0g
`  w ) ( lt `  w ) x  /\  A. n  e.  NN  ( n (.g `  w ) x ) ( lt `  w
) y ) ) }
302, 3, 29cmpt 4461 . 2  class  ( w  e.  _V  |->  { <. x ,  y >.  |  ( ( x  e.  (
Base `  w )  /\  y  e.  ( Base `  w ) )  /\  ( ( 0g
`  w ) ( lt `  w ) x  /\  A. n  e.  NN  ( n (.g `  w ) x ) ( lt `  w
) y ) ) } )
311, 30wceq 1370 1  wff <<<  =  (
w  e.  _V  |->  {
<. x ,  y >.  |  ( ( x  e.  ( Base `  w
)  /\  y  e.  ( Base `  w )
)  /\  ( ( 0g `  w ) ( lt `  w ) x  /\  A. n  e.  NN  ( n (.g `  w ) x ) ( lt `  w
) y ) ) } )
Colors of variables: wff setvar class
This definition is referenced by:  inftmrel  26362  isinftm  26363
  Copyright terms: Public domain W3C validator