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

Definition df-fin5 8994
 Description: A set is V-finite iff it behaves finitely under +𝑐. Definition V of [Levy58] p. 3. (Contributed by Stefan O'Rear, 12-Nov-2014.)
Assertion
Ref Expression
df-fin5 FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))}

Detailed syntax breakdown of Definition df-fin5
StepHypRef Expression
1 cfin5 8987 . 2 class FinV
2 vx . . . . . 6 setvar 𝑥
32cv 1474 . . . . 5 class 𝑥
4 c0 3874 . . . . 5 class
53, 4wceq 1475 . . . 4 wff 𝑥 = ∅
6 ccda 8872 . . . . . 6 class +𝑐
73, 3, 6co 6549 . . . . 5 class (𝑥 +𝑐 𝑥)
8 csdm 7840 . . . . 5 class
93, 7, 8wbr 4583 . . . 4 wff 𝑥 ≺ (𝑥 +𝑐 𝑥)
105, 9wo 382 . . 3 wff (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))
1110, 2cab 2596 . 2 class {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))}
121, 11wceq 1475 1 wff FinV = {𝑥 ∣ (𝑥 = ∅ ∨ 𝑥 ≺ (𝑥 +𝑐 𝑥))}
 Colors of variables: wff setvar class This definition is referenced by:  isfin5  9004
 Copyright terms: Public domain W3C validator