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 = { w | ( <<< ` w ) = (/) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		carchi	|- Archi
1		vw	|- w
2		cinftm	|- <<<
3	1	cv	|- w
4	3 2	cfv	|- ( <<< ` w )
5		c0	|- (/)
6	4 5	wceq	|- ( <<< ` w ) = (/)
7	6 1	cab	|- { w | ( <<< ` w ) = (/) }
8	0 7	wceq	|- Archi = { w | ( <<< ` w ) = (/) }