Definition df-fin4

Description: A set is IV-finite (Dedekind finite) iff it has no equinumerous proper subset. Definition IV of Levy58 p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014)

	Ref	Expression
Assertion	df-fin4	⊢ FinIV = { 𝑥 ∣ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin4	⊢ FinIV
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	2	cv	⊢ 𝑦
4	1	cv	⊢ 𝑥
5	3 4	wpss	⊢ 𝑦 ⊊ 𝑥
6		cen	⊢ ≈
7	3 4 6	wbr	⊢ 𝑦 ≈ 𝑥
8	5 7	wa	⊢ ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 )
9	8 2	wex	⊢ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 )
10	9	wn	⊢ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 )
11	10 1	cab	⊢ { 𝑥 ∣ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) }
12	0 11	wceq	⊢ FinIV = { 𝑥 ∣ ¬ ∃ 𝑦 ( 𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥 ) }