Definition df-fin5

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

	Ref	Expression
Assertion	df-fin5	|- Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin5	|- Fin5
1		vx	|- x
2	1	cv	|- x
3		c0	|- (/)
4	2 3	wceq	|- x = (/)
5		csdm	|- ~<
6	2 2	cdju	|- ( x |_| x )
7	2 6 5	wbr	|- x ~< ( x |_| x )
8	4 7	wo	|- ( x = (/) \/ x ~< ( x |_| x ) )
9	8 1	cab	|- { x | ( x = (/) \/ x ~< ( x |_| x ) ) }
10	0 9	wceq	|- Fin5 = { x | ( x = (/) \/ x ~< ( x |_| x ) ) }