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 = { 𝑥 ∣ ∀ 𝑦 ∈ 𝒫 𝑥 ( 𝑦 ∈ 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 ) }