Theorem fin4i

Description: Infer that a set is IV-infinite. (Contributed by Stefan O'Rear, 16-May-2015)

	Ref	Expression
Assertion	fin4i	$$⊢\left(X\subset A\wedge X\approx A\right)\to \neg A\in {\mathrm{Fin}}^{\mathrm{IV}}$$

Proof

Step	Hyp	Ref	Expression
1		isfin4	$$⊢A\in {\mathrm{Fin}}^{\mathrm{IV}}\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \exists x\left(x\subset A\wedge x\approx A\right)\right)$$
2	1	ibi	$$⊢A\in {\mathrm{Fin}}^{\mathrm{IV}}\to \neg \exists x\left(x\subset A\wedge x\approx A\right)$$
3		relen	$$⊢\mathrm{Rel}\approx$$
4	3	brrelex1i	$$⊢X\approx A\to X\in \mathrm{V}$$
5	4	adantl	$$⊢\left(X\subset A\wedge X\approx A\right)\to X\in \mathrm{V}$$
6		psseq1	$$⊢x=X\to \left(x\subset A\leftrightarrow X\subset A\right)$$
7		breq1	$$⊢x=X\to \left(x\approx A\leftrightarrow X\approx A\right)$$
8	6 7	anbi12d	$$⊢x=X\to \left(\left(x\subset A\wedge x\approx A\right)\leftrightarrow \left(X\subset A\wedge X\approx A\right)\right)$$
9	8	spcegv	$$⊢X\in \mathrm{V}\to \left(\left(X\subset A\wedge X\approx A\right)\to \exists x\left(x\subset A\wedge x\approx A\right)\right)$$
10	5 9	mpcom	$$⊢\left(X\subset A\wedge X\approx A\right)\to \exists x\left(x\subset A\wedge x\approx A\right)$$
11	2 10	nsyl3	$$⊢\left(X\subset A\wedge X\approx A\right)\to \neg A\in {\mathrm{Fin}}^{\mathrm{IV}}$$