Definition df-fin5 9426

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.)

Assertion

Ref	Expression
df-fin5	⊢ FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))}

Detailed syntax breakdown of Definition df-fin5

Step	Hyp	Ref	Expression
1		cfin5 9419	. 2 class FinV
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1657	. . . . 5 class 𝑥
4		c0 4144	. . . . 5 class ∅
5	3, 4	wceq 1658	. . . 4 wff 𝑥 = ∅
6		ccda 9304	. . . . . 6 class +𝑐
7	3, 3, 6	co 6905	. . . . 5 class (𝑥 +𝑐 𝑥)
8		csdm 8221	. . . . 5 class ≺
9	3, 7, 8	wbr 4873	. . . 4 wff 𝑥 ≺ (𝑥 +𝑐 𝑥)
10	5, 9	wo 880	. . 3 wff (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))
11	10, 2	cab 2811	. 2 class {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))}
12	1, 11	wceq 1658	1 wff FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))}

This definition is referenced by:  isfin5  9436