Definition df-fin4 9974

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 9967	. 2 class FinIV
2		vy	. . . . . . . 8 setvar 𝑦
3	2	cv 1538	. . . . . . 7 class 𝑦
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1538	. . . . . . 7 class 𝑥
6	3, 5	wpss 3884	. . . . . 6 wff 𝑦 ⊊ 𝑥
7		cen 8688	. . . . . . 7 class ≈
8	3, 5, 7	wbr 5070	. . . . . 6 wff 𝑦 ≈ 𝑥
9	6, 8	wa 395	. . . . 5 wff (𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)
10	9, 2	wex 1783	. . . 4 wff ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)
11	10	wn 3	. . 3 wff ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)
12	11, 4	cab 2715	. 2 class {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)}
13	1, 12	wceq 1539	1 wff FinIV = {𝑥 ∣ ¬ ∃𝑦(𝑦 ⊊ 𝑥 ∧ 𝑦 ≈ 𝑥)}

This definition is referenced by:  isfin4  9984