Theorem pssinf

Description: A set equinumerous to a proper subset of itself is infinite. Corollary 6D(a) of Enderton p. 136. (Contributed by NM, 2-Jun-1998)

	Ref	Expression
Assertion	pssinf	$$⊢\left(A\subset B\wedge A\approx B\right)\to \neg B\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		php3	$$⊢\left(B\in \mathrm{Fin}\wedge A\subset B\right)\to A\prec B$$
2	1	ex	$$⊢B\in \mathrm{Fin}\to \left(A\subset B\to A\prec B\right)$$
3		sdomnen	$$⊢A\prec B\to \neg A\approx B$$
4	2 3	syl6com	$$⊢A\subset B\to \left(B\in \mathrm{Fin}\to \neg A\approx B\right)$$
5	4	con2d	$$⊢A\subset B\to \left(A\approx B\to \neg B\in \mathrm{Fin}\right)$$
6	5	imp	$$⊢\left(A\subset B\wedge A\approx B\right)\to \neg B\in \mathrm{Fin}$$