Definition df-fin6 9112

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

Assertion

Ref	Expression
df-fin6	|- FinVI = { x | ( x ~< 2o \/ x ~< ( x X. x ) ) }

Detailed syntax breakdown of Definition df-fin6

Step	Hyp	Ref	Expression
1		cfin6 9105	. 2 class FinVI
2		vx	. . . . . 6 setvar x
3	2	cv 1482	. . . . 5 class x
4		c2o 7554	. . . . 5 class 2o
5		csdm 7954	. . . . 5 class ~<
6	3, 4, 5	wbr 4653	. . . 4 wff x ~< 2o
7	3, 3	cxp 5112	. . . . 5 class ( x X. x )
8	3, 7, 5	wbr 4653	. . . 4 wff x ~< ( x X. x )
9	6, 8	wo 383	. . 3 wff ( x ~< 2o \/ x ~< ( x X. x ) )
10	9, 2	cab 2608	. 2 class { x | ( x ~< 2o \/ x ~< ( x X. x ) ) }
11	1, 10	wceq 1483	1 wff FinVI = { x | ( x ~< 2o \/ x ~< ( x X. x ) ) }

This definition is referenced by:  isfin6  9122