Definition df-inftm 33185

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 33183	. 2 class ⋘
2		vw	. . 3 setvar 𝑤
3		cvv 3480	. . 3 class V
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1539	. . . . . . 7 class 𝑥
6	2	cv 1539	. . . . . . . 8 class 𝑤
7		cbs 17247	. . . . . . . 8 class Base
8	6, 7	cfv 6561	. . . . . . 7 class (Base‘𝑤)
9	5, 8	wcel 2108	. . . . . 6 wff 𝑥 ∈ (Base‘𝑤)
10		vy	. . . . . . . 8 setvar 𝑦
11	10	cv 1539	. . . . . . 7 class 𝑦
12	11, 8	wcel 2108	. . . . . 6 wff 𝑦 ∈ (Base‘𝑤)
13	9, 12	wa 395	. . . . 5 wff (𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤))
14		c0g 17484	. . . . . . . 8 class 0g
15	6, 14	cfv 6561	. . . . . . 7 class (0g‘𝑤)
16		cplt 18354	. . . . . . . 8 class lt
17	6, 16	cfv 6561	. . . . . . 7 class (lt‘𝑤)
18	15, 5, 17	wbr 5143	. . . . . 6 wff (0g‘𝑤)(lt‘𝑤)𝑥
19		vn	. . . . . . . . . 10 setvar 𝑛
20	19	cv 1539	. . . . . . . . 9 class 𝑛
21		cmg 19085	. . . . . . . . . 10 class .g
22	6, 21	cfv 6561	. . . . . . . . 9 class (.g‘𝑤)
23	20, 5, 22	co 7431	. . . . . . . 8 class (𝑛(.g‘𝑤)𝑥)
24	23, 11, 17	wbr 5143	. . . . . . 7 wff (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦
25		cn 12266	. . . . . . 7 class ℕ
26	24, 19, 25	wral 3061	. . . . . 6 wff ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦
27	18, 26	wa 395	. . . . 5 wff ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦)
28	13, 27	wa 395	. . . 4 wff ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))
29	28, 4, 10	copab 5205	. . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))}
30	2, 3, 29	cmpt 5225	. 2 class (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))})
31	1, 30	wceq 1540	1 wff ⋘ = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))})

This definition is referenced by:  inftmrel  33187  isinftm  33188