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

Definition df-archi 29861
Description: A structure said to be Archimedean if it has no infinitesimal elements. (Contributed by Thierry Arnoux, 30-Jan-2018.)
Assertion
Ref Expression
df-archi Archi = {𝑤 ∣ (⋘‘𝑤) = ∅}

Detailed syntax breakdown of Definition df-archi
StepHypRef Expression
1 carchi 29859 . 2 class Archi
2 vw . . . . . 6 setvar 𝑤
32cv 1522 . . . . 5 class 𝑤
4 cinftm 29858 . . . . 5 class
53, 4cfv 5926 . . . 4 class (⋘‘𝑤)
6 c0 3948 . . . 4 class
75, 6wceq 1523 . . 3 wff (⋘‘𝑤) = ∅
87, 2cab 2637 . 2 class {𝑤 ∣ (⋘‘𝑤) = ∅}
91, 8wceq 1523 1 wff Archi = {𝑤 ∣ (⋘‘𝑤) = ∅}
Colors of variables: wff setvar class
This definition is referenced by:  isarchi  29864
  Copyright terms: Public domain W3C validator