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 C. B /\ A ~~ B ) -> -. B e. Fin )

Proof

Step Hyp Ref Expression
1 php3 
 |-  ( ( B e. Fin /\ A C. B ) -> A ~< B )
2 1 ex 
 |-  ( B e. Fin -> ( A C. B -> A ~< B ) )
3 sdomnen 
 |-  ( A ~< B -> -. A ~~ B )
4 2 3 syl6com 
 |-  ( A C. B -> ( B e. Fin -> -. A ~~ B ) )
5 4 con2d 
 |-  ( A C. B -> ( A ~~ B -> -. B e. Fin ) )
6 5 imp 
 |-  ( ( A C. B /\ A ~~ B ) -> -. B e. Fin )