Metamath Proof Explorer


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