Metamath Proof Explorer

Definition df-inftm

Description: Define the relation " x is infinitesimal with respect to y " for a structure w . (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Assertion 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 ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cinftm 
 |-  <<<
1 vw 
 |-  w
2 cvv 
 |-  _V
3 vx 
 |-  x
4 vy 
 |-  y
5 3 cv 
 |-  x
6 cbs 
 |-  Base
7 1 cv 
 |-  w
8 7 6 cfv 
 |-  ( Base ` w )
9 5 8 wcel 
 |-  x e. ( Base ` w )
10 4 cv 
 |-  y
11 10 8 wcel 
 |-  y e. ( Base ` w )
12 9 11 wa 
 |-  ( x e. ( Base ` w ) /\ y e. ( Base ` w ) )
13 c0g 
 |-  0g
14 7 13 cfv 
 |-  ( 0g ` w )
15 cplt 
 |-  lt
16 7 15 cfv 
 |-  ( lt ` w )
17 14 5 16 wbr 
 |-  ( 0g ` w ) ( lt ` w ) x
18 vn 
 |-  n
19 cn 
 |-  NN
20 18 cv 
 |-  n
21 cmg 
 |-  .g
22 7 21 cfv 
 |-  ( .g ` w )
23 20 5 22 co 
 |-  ( n ( .g ` w ) x )
24 23 10 16 wbr 
 |-  ( n ( .g ` w ) x ) ( lt ` w ) y
25 24 18 19 wral 
 |-  A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y
26 17 25 wa 
 |-  ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y )
27 12 26 wa 
 |-  ( ( x e. ( Base ` w ) /\ y e. ( Base ` w ) ) /\ ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n ( .g ` w ) x ) ( lt ` w ) y ) )
28 27 3 4 copab 
 |-  { <. 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 ) ) }
29 1 2 28 cmpt 
 |-  ( 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 ) ) } )
30 0 29 wceq 
 |-  <<< = ( 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 ) ) } )