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 28489
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 28487 . 2  class <<<
2 vw . . 3  setvar  w
3 cvv 3081 . . 3  class  _V
4 vx . . . . . . . 8  setvar  x
54cv 1436 . . . . . . 7  class  x
62cv 1436 . . . . . . . 8  class  w
7 cbs 15108 . . . . . . . 8  class  Base
86, 7cfv 5597 . . . . . . 7  class  ( Base `  w )
95, 8wcel 1868 . . . . . 6  wff  x  e.  ( Base `  w
)
10 vy . . . . . . . 8  setvar  y
1110cv 1436 . . . . . . 7  class  y
1211, 8wcel 1868 . . . . . 6  wff  y  e.  ( Base `  w
)
139, 12wa 370 . . . . 5  wff  ( x  e.  ( Base `  w
)  /\  y  e.  ( Base `  w )
)
14 c0g 15325 . . . . . . . 8  class  0g
156, 14cfv 5597 . . . . . . 7  class  ( 0g
`  w )
16 cplt 16173 . . . . . . . 8  class  lt
176, 16cfv 5597 . . . . . . 7  class  ( lt
`  w )
1815, 5, 17wbr 4420 . . . . . 6  wff  ( 0g
`  w ) ( lt `  w ) x
19 vn . . . . . . . . . 10  setvar  n
2019cv 1436 . . . . . . . . 9  class  n
21 cmg 16659 . . . . . . . . . 10  class .g
226, 21cfv 5597 . . . . . . . . 9  class  (.g `  w
)
2320, 5, 22co 6301 . . . . . . . 8  class  ( n (.g `  w ) x )
2423, 11, 17wbr 4420 . . . . . . 7  wff  ( n (.g `  w ) x ) ( lt `  w ) y
25 cn 10609 . . . . . . 7  class  NN
2624, 19, 25wral 2775 . . . . . 6  wff  A. n  e.  NN  ( n (.g `  w ) x ) ( lt `  w
) y
2718, 26wa 370 . . . . 5  wff  ( ( 0g `  w ) ( lt `  w
) x  /\  A. n  e.  NN  (
n (.g `  w ) x ) ( lt `  w ) y )
2813, 27wa 370 . . . 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 4478 . . 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 4479 . 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 1437 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  28491  isinftm  28492
  Copyright terms: Public domain W3C validator