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	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		php3	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ⊊ 𝐵 ) → 𝐴 ≺ 𝐵 )
2	1	ex	⊢ ( 𝐵 ∈ Fin → ( 𝐴 ⊊ 𝐵 → 𝐴 ≺ 𝐵 ) )
3		sdomnen	⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
4	2 3	syl6com	⊢ ( 𝐴 ⊊ 𝐵 → ( 𝐵 ∈ Fin → ¬ 𝐴 ≈ 𝐵 ) )
5	4	con2d	⊢ ( 𝐴 ⊊ 𝐵 → ( 𝐴 ≈ 𝐵 → ¬ 𝐵 ∈ Fin ) )
6	5	imp	⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ∈ Fin )