MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fin1a Structured version   Visualization version   GIF version

Definition df-fin1a 9051
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 7903 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
StepHypRef Expression
1 cfin1a 9044 . 2 class FinIa
2 vy . . . . . . 7 setvar 𝑦
32cv 1479 . . . . . 6 class 𝑦
4 cfn 7899 . . . . . 6 class Fin
53, 4wcel 1987 . . . . 5 wff 𝑦 ∈ Fin
6 vx . . . . . . . 8 setvar 𝑥
76cv 1479 . . . . . . 7 class 𝑥
87, 3cdif 3552 . . . . . 6 class (𝑥𝑦)
98, 4wcel 1987 . . . . 5 wff (𝑥𝑦) ∈ Fin
105, 9wo 383 . . . 4 wff (𝑦 ∈ Fin ∨ (𝑥𝑦) ∈ Fin)
117cpw 4130 . . . 4 class 𝒫 𝑥
1210, 2, 11wral 2907 . . 3 wff 𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥𝑦) ∈ Fin)
1312, 6cab 2607 . 2 class {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥𝑦) ∈ Fin)}
141, 13wceq 1480 1 wff FinIa = {𝑥 ∣ ∀𝑦 ∈ 𝒫 𝑥(𝑦 ∈ Fin ∨ (𝑥𝑦) ∈ Fin)}
Colors of variables: wff setvar class
This definition is referenced by:  isfin1a  9058
  Copyright terms: Public domain W3C validator