Theorem infpssALT

Description: Alternate proof of infpss , shorter but requiring Replacement ( ax-rep ). (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	infpssALT	$$⊢\mathrm{\omega }\preccurlyeq A\to \exists x\left(x\subset A\wedge x\approx A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ominf4	$$⊢\neg \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}$$
2		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
3	2	brrelex2i	$$⊢\mathrm{\omega }\preccurlyeq A\to A\in \mathrm{V}$$
4		isfin4	$$⊢A\in \mathrm{V}\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \exists x\left(x\subset A\wedge x\approx A\right)\right)$$
5	3 4	syl	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\leftrightarrow \neg \exists x\left(x\subset A\wedge x\approx A\right)\right)$$
6		domfin4	$$⊢\left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\wedge \mathrm{\omega }\preccurlyeq A\right)\to \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}$$
7	6	expcom	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(A\in {\mathrm{Fin}}^{\mathrm{IV}}\to \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}\right)$$
8	5 7	sylbird	$$⊢\mathrm{\omega }\preccurlyeq A\to \left(\neg \exists x\left(x\subset A\wedge x\approx A\right)\to \mathrm{\omega }\in {\mathrm{Fin}}^{\mathrm{IV}}\right)$$
9	1 8	mt3i	$$⊢\mathrm{\omega }\preccurlyeq A\to \exists x\left(x\subset A\wedge x\approx A\right)$$