This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ (A \subset B \land A \approx B) \to \neg B \in Fin$

Step	Hyp	Ref	Expression
1		php3	$⊢ (B \in Fin \land A \subset B) \to A ≺ B$
2	1	ex	$⊢ B \in Fin \to (A \subset B \to A ≺ B)$
3		sdomnen	$⊢ A ≺ B \to \neg A \approx B$
4	2 3	syl6com	$⊢ A \subset B \to (B \in Fin \to \neg A \approx B)$
5	4	con2d	$⊢ A \subset B \to (A \approx B \to \neg B \in Fin)$
6	5	imp	$⊢ (A \subset B \land A \approx B) \to \neg B \in Fin$