Definition df-fin5 9111

Description: A set is V-finite iff it behaves finitely under +c. Definition V of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)

Assertion

Ref	Expression
df-fin5	|- FinV = { x | ( x = (/) \/ x ~< ( x +c x ) ) }

Detailed syntax breakdown of Definition df-fin5

Step	Hyp	Ref	Expression
1		cfin5 9104	. 2 class FinV
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		c0 3915	. . . . 5 class (/)
5	3, 4	wceq 1483	. . . 4 wff x = (/)
6		ccda 8989	. . . . . 6 class +c
7	3, 3, 6	co 6650	. . . . 5 class ( x +c x )
8		csdm 7954	. . . . 5 class ~<
9	3, 7, 8	wbr 4653	. . . 4 wff x ~< ( x +c x )
10	5, 9	wo 383	. . 3 wff ( x = (/) \/ x ~< ( x +c x ) )
11	10, 2	cab 2608	. 2 class { x | ( x = (/) \/ x ~< ( x +c x ) ) }
12	1, 11	wceq 1483	1 wff FinV = { x | ( x = (/) \/ x ~< ( x +c x ) ) }

This definition is referenced by:  isfin5  9121