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 = { 𝑤 ∣ ( ⋘ ‘ 𝑤 ) = ∅ }