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 ( ( 𝐴𝐵𝐴𝐵 ) → ¬ 𝐵 ∈ 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 )