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 \in V ⟼ \{⟨x, y⟩ \| ((x \in {Base}_{w} \land y \in {Base}_{w}) \land (0_{w} <_{w} x \land \forall n \in ℕ (n \cdot_{w} x) <_{w} y))\})$

Step	Hyp	Ref	Expression
0		cinftm	$class ⋘$
1		vw	$setvar w$
2		cvv	$class V$
3		vx	$setvar x$
4		vy	$setvar y$
5	3	cv	$setvar x$
6		cbs	$class Base$
7	1	cv	$setvar w$
8	7 6	cfv	$class {Base}_{w}$
9	5 8	wcel	$wff x \in {Base}_{w}$
10	4	cv	$setvar y$
11	10 8	wcel	$wff y \in {Base}_{w}$
12	9 11	wa	$wff (x \in {Base}_{w} \land y \in {Base}_{w})$
13		c0g	$class 0_{𝑔}$
14	7 13	cfv	$class 0_{w}$
15		cplt	$class lt$
16	7 15	cfv	$class <_{w}$
17	14 5 16	wbr	$wff 0_{w} <_{w} x$
18		vn	$setvar n$
19		cn	$class ℕ$
20	18	cv	$setvar n$
21		cmg	$class ⋅_{𝑔}$
22	7 21	cfv	$class \cdot_{w}$
23	20 5 22	co	$class (n \cdot_{w} x)$
24	23 10 16	wbr	$wff (n \cdot_{w} x) <_{w} y$
25	24 18 19	wral	$wff \forall n \in ℕ (n \cdot_{w} x) <_{w} y$
26	17 25	wa	$wff (0_{w} <_{w} x \land \forall n \in ℕ (n \cdot_{w} x) <_{w} y)$
27	12 26	wa	$wff ((x \in {Base}_{w} \land y \in {Base}_{w}) \land (0_{w} <_{w} x \land \forall n \in ℕ (n \cdot_{w} x) <_{w} y))$
28	27 3 4	copab	$class \{⟨x, y⟩ \| ((x \in {Base}_{w} \land y \in {Base}_{w}) \land (0_{w} <_{w} x \land \forall n \in ℕ (n \cdot_{w} x) <_{w} y))\}$
29	1 2 28	cmpt	$class (w \in V ⟼ \{⟨x, y⟩ \| ((x \in {Base}_{w} \land y \in {Base}_{w}) \land (0_{w} <_{w} x \land \forall n \in ℕ (n \cdot_{w} x) <_{w} y))\})$
30	0 29	wceq	$wff ⋘ = (w \in V ⟼ \{⟨x, y⟩ \| ((x \in {Base}_{w} \land y \in {Base}_{w}) \land (0_{w} <_{w} x \land \forall n \in ℕ (n \cdot_{w} x) <_{w} y))\})$

Metamath Proof Explorer