Definition df-fin1a 10041

Description: A set is Ia-finite iff it is not the union of two I-infinite sets. Equivalent to definition Ia of [Levy58] p. 2. A I-infinite Ia-finite set is also known as an amorphous set. This is the second of Levy's eight definitions of finite set. Levy's I-finite is equivalent to our df-fin 8737 and not repeated here. These eight definitions are equivalent with Choice but strictly decreasing in strength in models where Choice fails; conversely, they provide a series of increasingly stronger notions of infiniteness. (Contributed by Stefan O'Rear, 12-Nov-2014.)

Assertion

Ref	Expression
df-fin1a	⊢ FinIa = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-fin1a

Step	Hyp	Ref	Expression
1		cfin1a 10034	. 2 class FinIa
2		vy	. . . . . . 7 setvar 𝑦
3	2	cv 1538	. . . . . 6 class 𝑦
4		cfn 8733	. . . . . 6 class Fin
5	3, 4	wcel 2106	. . . . 5 wff 𝑦 ∈ Fin
6		vx	. . . . . . . 8 setvar 𝑥
7	6	cv 1538	. . . . . . 7 class 𝑥
8	7, 3	cdif 3884	. . . . . 6 class (𝑥 ∖ 𝑦)
9	8, 4	wcel 2106	. . . . 5 wff (𝑥 ∖ 𝑦) ∈ Fin
10	5, 9	wo 844	. . . 4 wff (𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)
11	7	cpw 4533	. . . 4 class 𝒫 𝑥
12	10, 2, 11	wral 3064	. . 3 wff ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)
13	12, 6	cab 2715	. 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)}
14	1, 13	wceq 1539	1 wff FinIa = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥 ∖ 𝑦) ∈ Fin)}

This definition is referenced by:  isfin1a  10048