Definition df-fin4 8992

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

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-fin4

Step	Hyp	Ref	Expression
1		cfin4 8985	. 2 class FinIV
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1474	. . . . . . 7 class 𝑦
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1474	. . . . . . 7 class 𝑥
6	3, 5	wpss 3541	. . . . . 6 wff 𝑦 ⊊ 𝑥
7		cen 7838	. . . . . . 7 class ≈
8	3, 5, 7	wbr 4583	. . . . . 6 wff 𝑦 ≈ 𝑥
9	6, 8	wa 383	. . . . 5 wff (𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)
10	9, 2	wex 1695	. . . 4 wff ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)
11	10	wn 3	. . 3 wff ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)
12	11, 4	cab 2596	. 2 class {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)}
13	1, 12	wceq 1475	1 wff FinIV = {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)}

This definition is referenced by:  isfin4  9002