Definition df-fin5

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin5	⊢ FinV
1		vx	⊢ 𝑥
2	1	cv	⊢ 𝑥
3		c0	⊢ ∅
4	2 3	wceq	⊢ 𝑥 = ∅
5		csdm	⊢ ≺
6	2 2	cdju	⊢ ( 𝑥 ⊔ 𝑥 )
7	2 6 5	wbr	⊢ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 )
8	4 7	wo	⊢ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) )
9	8 1	cab	⊢ { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) }
10	0 9	wceq	⊢ FinV = { 𝑥 ∣ ( 𝑥 = ∅ ∨ 𝑥 ≺ ( 𝑥 ⊔ 𝑥 ) ) }