This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = { 𝑥 ∣ ∃ 𝑦 ∈ ω 𝑥 ≈ 𝑦 }