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

Metamath Proof Explorer

Definition df-archi

Description: A structure said to be Archimedean if it has no infinitesimal elements. (Contributed by Thierry Arnoux, 30-Jan-2018)

Ref Expression
Assertion df-archi Archi = { 𝑤 ∣ ( ⋘ ‘ 𝑤 ) = ∅ }

Detailed syntax breakdown

Step Hyp Ref Expression
0 carchi ⊢ Archi
1 vw ⊢ 𝑤
2 cinftm ⊢ ⋘
3 1 cv ⊢ 𝑤
4 3 2 cfv ⊢ ( ⋘ ‘ 𝑤 )
5 c0 ⊢ ∅
6 4 5 wceq ⊢ ( ⋘ ‘ 𝑤 ) = ∅
7 6 1 cab ⊢ { 𝑤 ∣ ( ⋘ ‘ 𝑤 ) = ∅ }
8 0 7 wceq ⊢ Archi = { 𝑤 ∣ ( ⋘ ‘ 𝑤 ) = ∅ }