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	$$⊢\mathrm{Archi}=\left\{w|⋘\left(w\right)=\varnothing \right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carchi	$$class\mathrm{Archi}$$
1		vw	$$setvarw$$
2		cinftm	$$class⋘$$
3	1	cv	$$setvarw$$
4	3 2	cfv	$$class⋘\left(w\right)$$
5		c0	$$class\varnothing$$
6	4 5	wceq	$$wff⋘\left(w\right)=\varnothing$$
7	6 1	cab	$$class\left\{w|⋘\left(w\right)=\varnothing \right\}$$
8	0 7	wceq	$$wff\mathrm{Archi}=\left\{w|⋘\left(w\right)=\varnothing \right\}$$