Metamath Proof Explorer


Definition df-fin

Description: Define the (proper) class of all finite sets. Similar to Definition 10.29 of TakeutiZaring p. 91, whose "Fin(a)" corresponds to our " a e. Fin ". This definition is meaningful whether or not we accept the Axiom of Infinity ax-inf2 . If we accept Infinity, we can also express A e. Fin by A ~< _om (Theorem isfinite .) (Contributed by NM, 22-Aug-2008)

Ref Expression
Assertion df-fin Fin = { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑥𝑦 }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfn Fin
1 vx 𝑥
2 vy 𝑦
3 com ω
4 1 cv 𝑥
5 cen
6 2 cv 𝑦
7 4 6 5 wbr 𝑥𝑦
8 7 2 3 wrex 𝑦 ∈ ω 𝑥𝑦
9 8 1 cab { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑥𝑦 }
10 0 9 wceq Fin = { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑥𝑦 }