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

Definition df-fin3 8970
Description: A set is III-finite (weakly Dedekind finite) iff its power set is Dedekind finite. Definition III of [Levy58] p. 2. (Contributed by Stefan O'Rear, 12-Nov-2014.)
Assertion
Ref Expression
df-fin3 FinIII = {𝑥 ∣ 𝒫 𝑥 ∈ FinIV}

Detailed syntax breakdown of Definition df-fin3
StepHypRef Expression
1 cfin3 8963 . 2 class FinIII
2 vx . . . . . 6 setvar 𝑥
32cv 1473 . . . . 5 class 𝑥
43cpw 4107 . . . 4 class 𝒫 𝑥
5 cfin4 8962 . . . 4 class FinIV
64, 5wcel 1976 . . 3 wff 𝒫 𝑥 ∈ FinIV
76, 2cab 2595 . 2 class {𝑥 ∣ 𝒫 𝑥 ∈ FinIV}
81, 7wceq 1474 1 wff FinIII = {𝑥 ∣ 𝒫 𝑥 ∈ FinIV}
Colors of variables: wff setvar class
This definition is referenced by:  isfin3  8978
  Copyright terms: Public domain W3C validator