Theorem isfi

Description: Express " A is finite." Definition 10.29 of TakeutiZaring p. 91 (whose " Fin " is a predicate instead of a class). (Contributed by NM, 22-Aug-2008)

	Ref	Expression
Assertion	isfi	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$

Proof

Step	Hyp	Ref	Expression
1		df-fin	$$⊢\mathrm{Fin}=\left\{y|\exists x\in \mathrm{\omega }y\approx x\right\}$$
2	1	eleq2i	$$⊢A\in \mathrm{Fin}\leftrightarrow A\in \left\{y|\exists x\in \mathrm{\omega }y\approx x\right\}$$
3		relen	$$⊢\mathrm{Rel}\approx$$
4	3	brrelex1i	$$⊢A\approx x\to A\in \mathrm{V}$$
5	4	rexlimivw	$$⊢\exists x\in \mathrm{\omega }A\approx x\to A\in \mathrm{V}$$
6		breq1	$$⊢y=A\to \left(y\approx x\leftrightarrow A\approx x\right)$$
7	6	rexbidv	$$⊢y=A\to \left(\exists x\in \mathrm{\omega }y\approx x\leftrightarrow \exists x\in \mathrm{\omega }A\approx x\right)$$
8	5 7	elab3	$$⊢A\in \left\{y|\exists x\in \mathrm{\omega }y\approx x\right\}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$
9	2 8	bitri	$$⊢A\in \mathrm{Fin}\leftrightarrow \exists x\in \mathrm{\omega }A\approx x$$