Definition df-fin5 10367

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 10360	. 2 class FinV
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1569	. . . . 5 class 𝑥
4		c0 4279	. . . . 5 class ∅
5	3, 4	wceq 1570	. . . 4 wff 𝑥 = ∅
6	3, 3	cdju 9979	. . . . 5 class (𝑥 ⊔ 𝑥)
7		csdm 8972	. . . . 5 class ≺
8	3, 6, 7	wbr 5103	. . . 4 wff 𝑥 ≺ (𝑥 ⊔ 𝑥)
9	5, 8	wo 861	. . 3 wff (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 ⊔ 𝑥))
10	9, 2	cab 2739	. 2 class {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 ⊔ 𝑥))}
11	1, 10	wceq 1570	1 wff FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 ⊔ 𝑥))}

This definition is used by:  isfin5  10377