Definition df-fin1a

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfin1a	⊢ FinIa
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	3	cpw	⊢ 𝒫 𝑥
5	2	cv	⊢ 𝑦
6		cfn	⊢ Fin
7	5 6	wcel	⊢ 𝑦 ∈ Fin
8	3 5	cdif	⊢ ( 𝑥 ∖ 𝑦 )
9	8 6	wcel	⊢ ( 𝑥 ∖ 𝑦 ) ∈ Fin
10	7 9	wo	⊢ ( 𝑦 ∈ Fin ∨ ( 𝑥 ∖ 𝑦 ) ∈ Fin )
11	10 2 4	wral	⊢ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ∈ Fin ∨ ( 𝑥 ∖ 𝑦 ) ∈ Fin )
12	11 1	cab	⊢ { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ∈ Fin ∨ ( 𝑥 ∖ 𝑦 ) ∈ Fin ) }
13	0 12	wceq	⊢ FinIa = { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ∈ Fin ∨ ( 𝑥 ∖ 𝑦 ) ∈ Fin ) }