Definition df-fin6

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)

	Ref	Expression
Assertion	df-fin6	⊢ FinVI = { 𝑥 ∣ ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin6	⊢ FinVI
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3		csdm	⊢ ≺
4		c2o	⊢ 2o
5	2 4 3	wbr	⊢ 𝑥 ≺ 2o
6	2 2	cxp	⊢ ( 𝑥 × 𝑥 )
7	2 6 3	wbr	⊢ 𝑥 ≺ ( 𝑥 × 𝑥 )
8	5 7	wo	⊢ ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) )
9	8 1	cab	⊢ { 𝑥 ∣ ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) ) }
10	0 9	wceq	⊢ FinVI = { 𝑥 ∣ ( 𝑥 ≺ 2o ∨ 𝑥 ≺ ( 𝑥 × 𝑥 ) ) }