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

Metamath Proof Explorer

Definition df-fin7

Description: A set is VII-finite iff it cannot be infinitely well-ordered. Equivalent to definition VII of Levy58 p. 4. (Contributed by Stefan O'Rear, 12-Nov-2014)

		Ref	Expression
	Assertion	df-fin7	$⊢ {Fin}^{VII} = \{x \| \neg \exists y \in (On ∖ ω) x \approx y\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin7	$class {Fin}^{VII}$
1		vx	$setvar x$
2		vy	$setvar y$
3		con0	$class On$
4		com	$class ω$
5	3 4	cdif	$class (On ∖ ω)$
6	1	cv	$setvar x$
7		cen	$class \approx$
8	2	cv	$setvar y$
9	6 8 7	wbr	$wff x \approx y$
10	9 2 5	wrex	$wff \exists y \in (On ∖ ω) x \approx y$
11	10	wn	$wff \neg \exists y \in (On ∖ ω) x \approx y$
12	11 1	cab	$class \{x \| \neg \exists y \in (On ∖ ω) x \approx y\}$
13	0 12	wceq	$wff {Fin}^{VII} = \{x \| \neg \exists y \in (On ∖ ω) x \approx y\}$