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 = \{w \| ⋘ (w) = \emptyset\}$

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