Theorem isfin7

Description: Definition of a VII-finite set. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	isfin7	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{VII}}\leftrightarrow \neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)A\approx y\right)$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢x=A\to \left(x\approx y\leftrightarrow A\approx y\right)$$
2	1	rexbidv	$$⊢x=A\to \left(\exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y\leftrightarrow \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)A\approx y\right)$$
3	2	notbid	$$⊢x=A\to \left(\neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y\leftrightarrow \neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)A\approx y\right)$$
4		df-fin7	$$⊢{\mathrm{Fin}}^{\mathrm{VII}}=\left\{x|\neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)x\approx y\right\}$$
5	3 4	elab2g	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{VII}}\leftrightarrow \neg \exists y\in \left(\mathrm{On}\setminus \mathrm{\omega }\right)A\approx y\right)$$