Definition df-inftm 31105

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

Assertion

Ref	Expression
df-inftm	⊢ ⋘ = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))})

Distinct variable group:   𝑤,𝑛,𝑥,𝑦

Detailed syntax breakdown of Definition df-inftm

Step	Hyp	Ref	Expression
1		cinftm 31103	. 2 class ⋘
2		vw	. . 3 setvar 𝑤
3		cvv 3398	. . 3 class V
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1542	. . . . . . 7 class 𝑥
6	2	cv 1542	. . . . . . . 8 class 𝑤
7		cbs 16666	. . . . . . . 8 class Base
8	6, 7	cfv 6358	. . . . . . 7 class (Base‘𝑤)
9	5, 8	wcel 2112	. . . . . 6 wff 𝑥 ∈ (Base‘𝑤)
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1542	. . . . . . 7 class 𝑦
12	11, 8	wcel 2112	. . . . . 6 wff 𝑦 ∈ (Base‘𝑤)
13	9, 12	wa 399	. . . . 5 wff (𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤))
14		c0g 16898	. . . . . . . 8 class 0g
15	6, 14	cfv 6358	. . . . . . 7 class (0g‘𝑤)
16		cplt 17769	. . . . . . . 8 class lt
17	6, 16	cfv 6358	. . . . . . 7 class (lt‘𝑤)
18	15, 5, 17	wbr 5039	. . . . . 6 wff (0g‘𝑤)(lt‘𝑤)𝑥
19		vn	. . . . . . . . . 10 setvar 𝑛
20	19	cv 1542	. . . . . . . . 9 class 𝑛
21		cmg 18442	. . . . . . . . . 10 class .g
22	6, 21	cfv 6358	. . . . . . . . 9 class (.g‘𝑤)
23	20, 5, 22	co 7191	. . . . . . . 8 class (𝑛(.g‘𝑤)𝑥)
24	23, 11, 17	wbr 5039	. . . . . . 7 wff (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦
25		cn 11795	. . . . . . 7 class ℕ
26	24, 19, 25	wral 3051	. . . . . 6 wff ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦
27	18, 26	wa 399	. . . . 5 wff ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦)
28	13, 27	wa 399	. . . 4 wff ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))
29	28, 4, 10	copab 5101	. . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))}
30	2, 3, 29	cmpt 5120	. 2 class (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))})
31	1, 30	wceq 1543	1 wff ⋘ = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))})

This definition is referenced by:  inftmrel  31107  isinftm  31108