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

Definition df-fin 7944
Description: Define the (proper) class of all finite sets. Similar to Definition 10.29 of [TakeutiZaring] p. 91, whose "Fin(a)" corresponds to our "𝑎 ∈ Fin". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 8523. If we accept Infinity, we can also express 𝐴 ∈ Fin by 𝐴 ≺ ω (theorem isfinite 8534.) (Contributed by NM, 22-Aug-2008.)
Assertion
Ref Expression
df-fin Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-fin
StepHypRef Expression
1 cfn 7940 . 2 class Fin
2 vx . . . . . 6 setvar 𝑥
32cv 1480 . . . . 5 class 𝑥
4 vy . . . . . 6 setvar 𝑦
54cv 1480 . . . . 5 class 𝑦
6 cen 7937 . . . . 5 class
73, 5, 6wbr 4644 . . . 4 wff 𝑥𝑦
8 com 7050 . . . 4 class ω
97, 4, 8wrex 2910 . . 3 wff 𝑦 ∈ ω 𝑥𝑦
109, 2cab 2606 . 2 class {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}
111, 10wceq 1481 1 wff Fin = {𝑥 ∣ ∃𝑦 ∈ ω 𝑥𝑦}
Colors of variables: wff setvar class
This definition is referenced by:  isfi  7964  dffin1-5  9195
  Copyright terms: Public domain W3C validator