Theorem isfin4

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

	Ref	Expression
Assertion	isfin4	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \exists y\left(y\subset A\wedge y\approx A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		psseq2	$$⊢x=A\to \left(y\subset x\leftrightarrow y\subset A\right)$$
2		breq2	$$⊢x=A\to \left(y\approx x\leftrightarrow y\approx A\right)$$
3	1 2	anbi12d	$$⊢x=A\to \left(\left(y\subset x\wedge y\approx x\right)\leftrightarrow \left(y\subset A\wedge y\approx A\right)\right)$$
4	3	exbidv	$$⊢x=A\to \left(\exists y\left(y\subset x\wedge y\approx x\right)\leftrightarrow \exists y\left(y\subset A\wedge y\approx A\right)\right)$$
5	4	notbid	$$⊢x=A\to \left(\neg \exists y\left(y\subset x\wedge y\approx x\right)\leftrightarrow \neg \exists y\left(y\subset A\wedge y\approx A\right)\right)$$
6		df-fin4	$$⊢{\mathrm{Fin}}^{\mathrm{IV}}=\left\{x|\neg \exists y\left(y\subset x\wedge y\approx x\right)\right\}$$
7	5 6	elab2g	$$⊢A\in V\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \exists y\left(y\subset A\wedge y\approx A\right)\right)$$