Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-inftm Structured version   Visualization version   GIF version

Definition df-inftm 30860
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
StepHypRef Expression
1 cinftm 30858 . 2 class
2 vw . . 3 setvar 𝑤
3 cvv 3444 . . 3 class V
4 vx . . . . . . . 8 setvar 𝑥
54cv 1537 . . . . . . 7 class 𝑥
62cv 1537 . . . . . . . 8 class 𝑤
7 cbs 16478 . . . . . . . 8 class Base
86, 7cfv 6328 . . . . . . 7 class (Base‘𝑤)
95, 8wcel 2112 . . . . . 6 wff 𝑥 ∈ (Base‘𝑤)
10 vy . . . . . . . 8 setvar 𝑦
1110cv 1537 . . . . . . 7 class 𝑦
1211, 8wcel 2112 . . . . . 6 wff 𝑦 ∈ (Base‘𝑤)
139, 12wa 399 . . . . 5 wff (𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤))
14 c0g 16708 . . . . . . . 8 class 0g
156, 14cfv 6328 . . . . . . 7 class (0g𝑤)
16 cplt 17546 . . . . . . . 8 class lt
176, 16cfv 6328 . . . . . . 7 class (lt‘𝑤)
1815, 5, 17wbr 5033 . . . . . 6 wff (0g𝑤)(lt‘𝑤)𝑥
19 vn . . . . . . . . . 10 setvar 𝑛
2019cv 1537 . . . . . . . . 9 class 𝑛
21 cmg 18219 . . . . . . . . . 10 class .g
226, 21cfv 6328 . . . . . . . . 9 class (.g𝑤)
2320, 5, 22co 7139 . . . . . . . 8 class (𝑛(.g𝑤)𝑥)
2423, 11, 17wbr 5033 . . . . . . 7 wff (𝑛(.g𝑤)𝑥)(lt‘𝑤)𝑦
25 cn 11629 . . . . . . 7 class
2624, 19, 25wral 3109 . . . . . 6 wff 𝑛 ∈ ℕ (𝑛(.g𝑤)𝑥)(lt‘𝑤)𝑦
2718, 26wa 399 . . . . 5 wff ((0g𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g𝑤)𝑥)(lt‘𝑤)𝑦)
2813, 27wa 399 . . . 4 wff ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g𝑤)𝑥)(lt‘𝑤)𝑦))
2928, 4, 10copab 5095 . . 3 class {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g𝑤)𝑥)(lt‘𝑤)𝑦))}
302, 3, 29cmpt 5113 . 2 class (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g𝑤)𝑥)(lt‘𝑤)𝑦))})
311, 30wceq 1538 1 wff ⋘ = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g𝑤)𝑥)(lt‘𝑤)𝑦))})
Colors of variables: wff setvar class
This definition is referenced by:  inftmrel  30862  isinftm  30863
  Copyright terms: Public domain W3C validator