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 8993
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 8986 . 2 class FinIII
2 vx . . . . . 6 setvar 𝑥
32cv 1474 . . . . 5 class 𝑥
43cpw 4108 . . . 4 class 𝒫 𝑥
5 cfin4 8985 . . . 4 class FinIV
64, 5wcel 1977 . . 3 wff 𝒫 𝑥 ∈ FinIV
76, 2cab 2596 . 2 class {𝑥 ∣ 𝒫 𝑥 ∈ FinIV}
81, 7wceq 1475 1 wff FinIII = {𝑥 ∣ 𝒫 𝑥 ∈ FinIV}
Colors of variables: wff setvar class
This definition is referenced by:  isfin3  9001
  Copyright terms: Public domain W3C validator