Definition df-fin6 8995

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

Assertion

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

Detailed syntax breakdown of Definition df-fin6

Step	Hyp	Ref	Expression
1		cfin6 8988	. 2 class FinVI
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1474	. . . . 5 class 𝑥
4		c2o 7441	. . . . 5 class 2𝑜
5		csdm 7840	. . . . 5 class ≺
6	3, 4, 5	wbr 4583	. . . 4 wff 𝑥 ≺ 2𝑜
7	3, 3	cxp 5036	. . . . 5 class (𝑥 × 𝑥)
8	3, 7, 5	wbr 4583	. . . 4 wff 𝑥 ≺ (𝑥 × 𝑥)
9	6, 8	wo 382	. . 3 wff (𝑥 ≺ 2𝑜 ∨ 𝑥 ≺ (𝑥 × 𝑥))
10	9, 2	cab 2596	. 2 class {𝑥 ∣ (𝑥 ≺ 2𝑜 ∨ 𝑥 ≺ (𝑥 × 𝑥))}
11	1, 10	wceq 1475	1 wff FinVI = {𝑥 ∣ (𝑥 ≺ 2𝑜 ∨ 𝑥 ≺ (𝑥 × 𝑥))}

This definition is referenced by:  isfin6  9005