Definition df-inftm 29732

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

Step	Hyp	Ref	Expression
1		cinftm 29730	. 2 class <<<
2		vw	. . 3 setvar w
3		cvv 3200	. . 3 class _V
4		vx	. . . . . . . 8 setvar x
5	4	cv 1482	. . . . . . 7 class x
6	2	cv 1482	. . . . . . . 8 class w
7		cbs 15857	. . . . . . . 8 class Base
8	6, 7	cfv 5888	. . . . . . 7 class ( Base ` w )
9	5, 8	wcel 1990	. . . . . 6 wff x e. ( Base ` w )
10		vy	. . . . . . . 8 setvar y
11	10	cv 1482	. . . . . . 7 class y
12	11, 8	wcel 1990	. . . . . 6 wff y e. ( Base ` w )
13	9, 12	wa 384	. . . . 5 wff ( x e. ( Base ` w ) /\ y e. ( Base ` w ) )
14		c0g 16100	. . . . . . . 8 class 0g
15	6, 14	cfv 5888	. . . . . . 7 class ( 0g ` w )
16		cplt 16941	. . . . . . . 8 class lt
17	6, 16	cfv 5888	. . . . . . 7 class ( lt ` w )
18	15, 5, 17	wbr 4653	. . . . . 6 wff ( 0g ` w ) ( lt ` w ) x
19		vn	. . . . . . . . . 10 setvar n
20	19	cv 1482	. . . . . . . . 9 class n
21		cmg 17540	. . . . . . . . . 10 class .g
22	6, 21	cfv 5888	. . . . . . . . 9 class (.g ` w )
23	20, 5, 22	co 6650	. . . . . . . 8 class ( n (.g ` w ) x )
24	23, 11, 17	wbr 4653	. . . . . . 7 wff ( n (.g ` w ) x ) ( lt ` w ) y
25		cn 11020	. . . . . . 7 class NN
26	24, 19, 25	wral 2912	. . . . . 6 wff A. n e. NN ( n (.g ` w ) x ) ( lt ` w ) y
27	18, 26	wa 384	. . . . 5 wff ( ( 0g ` w ) ( lt ` w ) x /\ A. n e. NN ( n (.g ` w ) x ) ( lt ` w ) y )
28	13, 27	wa 384	. . . 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 ) )
29	28, 4, 10	copab 4712	. . 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 ) ) }
30	2, 3, 29	cmpt 4729	. 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 ) ) } )
31	1, 30	wceq 1483	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 ) ) } )

This definition is referenced by:  inftmrel  29734  isinftm  29735