This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V ⟼ x y | x ∈ Base w ∧ y ∈ Base w ∧ 0 w < w x ∧ ∀ n ∈ ℕ n ⋅ w x < w y

Detailed syntax breakdown

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 ∈ Base w
10 4 cv setvar y
11 10 8 wcel wff y ∈ Base w
12 9 11 wa wff x ∈ Base w ∧ y ∈ 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 ⋅ w
23 20 5 22 co class n ⋅ w x
24 23 10 16 wbr wff n ⋅ w x < w y
25 24 18 19 wral wff ∀ n ∈ ℕ n ⋅ w x < w y
26 17 25 wa wff 0 w < w x ∧ ∀ n ∈ ℕ n ⋅ w x < w y
27 12 26 wa wff x ∈ Base w ∧ y ∈ Base w ∧ 0 w < w x ∧ ∀ n ∈ ℕ n ⋅ w x < w y
28 27 3 4 copab class x y | x ∈ Base w ∧ y ∈ Base w ∧ 0 w < w x ∧ ∀ n ∈ ℕ n ⋅ w x < w y
29 1 2 28 cmpt class w ∈ V ⟼ x y | x ∈ Base w ∧ y ∈ Base w ∧ 0 w < w x ∧ ∀ n ∈ ℕ n ⋅ w x < w y
30 0 29 wceq wff ⋘ = w ∈ V ⟼ x y | x ∈ Base w ∧ y ∈ Base w ∧ 0 w < w x ∧ ∀ n ∈ ℕ n ⋅ w x < w y