This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = x | ∀ y ∈ 𝒫 x y ∈ Fin ∨ x ∖ y ∈ Fin

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfin1a class FinIa
1 vx setvar x
2 vy setvar y
3 1 cv setvar x
4 3 cpw class 𝒫 x
5 2 cv setvar y
6 cfn class Fin
7 5 6 wcel wff y ∈ Fin
8 3 5 cdif class x ∖ y
9 8 6 wcel wff x ∖ y ∈ Fin
10 7 9 wo wff y ∈ Fin ∨ x ∖ y ∈ Fin
11 10 2 4 wral wff ∀ y ∈ 𝒫 x y ∈ Fin ∨ x ∖ y ∈ Fin
12 11 1 cab class x | ∀ y ∈ 𝒫 x y ∈ Fin ∨ x ∖ y ∈ Fin
13 0 12 wceq wff FinIa = x | ∀ y ∈ 𝒫 x y ∈ Fin ∨ x ∖ y ∈ Fin