Metamath Proof Explorer


Theorem hashnfinnn0

Description: The size of an infinite set is not a nonnegative integer. (Contributed by Alexander van der Vekens, 21-Dec-2017) (Proof shortened by Alexander van der Vekens, 18-Jan-2018)

Ref Expression
Assertion hashnfinnn0
|- ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) e/ NN0 )

Proof

Step Hyp Ref Expression
1 nnel
 |-  ( -. ( # ` A ) e/ NN0 <-> ( # ` A ) e. NN0 )
2 hashclb
 |-  ( A e. V -> ( A e. Fin <-> ( # ` A ) e. NN0 ) )
3 2 biimprd
 |-  ( A e. V -> ( ( # ` A ) e. NN0 -> A e. Fin ) )
4 1 3 syl5bi
 |-  ( A e. V -> ( -. ( # ` A ) e/ NN0 -> A e. Fin ) )
5 4 con1d
 |-  ( A e. V -> ( -. A e. Fin -> ( # ` A ) e/ NN0 ) )
6 5 imp
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) e/ NN0 )