Metamath Proof Explorer

Theorem hashnnn0genn0

Description: If the size of a set is not a nonnegative integer, it is greater than or equal to any nonnegative integer. (Contributed by Alexander van der Vekens, 6-Dec-2017)

Ref Expression
Assertion hashnnn0genn0 
|- ( ( M e. V /\ ( # ` M ) e/ NN0 /\ N e. NN0 ) -> N <_ ( # ` M ) )

Proof

Step Hyp Ref Expression
1 df-nel 
 |-  ( ( # ` M ) e/ NN0 <-> -. ( # ` M ) e. NN0 )
2 pm2.21 
 |-  ( -. ( # ` M ) e. NN0 -> ( ( # ` M ) e. NN0 -> N <_ ( # ` M ) ) )
3 1 2 sylbi 
 |-  ( ( # ` M ) e/ NN0 -> ( ( # ` M ) e. NN0 -> N <_ ( # ` M ) ) )
4 3 3ad2ant2 
 |-  ( ( M e. V /\ ( # ` M ) e/ NN0 /\ N e. NN0 ) -> ( ( # ` M ) e. NN0 -> N <_ ( # ` M ) ) )
5 nn0re 
 |-  ( N e. NN0 -> N e. RR )
6 5 ltpnfd 
 |-  ( N e. NN0 -> N < +oo )
7 5 rexrd 
 |-  ( N e. NN0 -> N e. RR* )
8 pnfxr 
 |-  +oo e. RR*
9 xrltle 
 |-  ( ( N e. RR* /\ +oo e. RR* ) -> ( N < +oo -> N <_ +oo ) )
10 7 8 9 sylancl 
 |-  ( N e. NN0 -> ( N < +oo -> N <_ +oo ) )
11 6 10 mpd 
 |-  ( N e. NN0 -> N <_ +oo )
12 breq2 
 |-  ( ( # ` M ) = +oo -> ( N <_ ( # ` M ) <-> N <_ +oo ) )
13 11 12 syl5ibrcom 
 |-  ( N e. NN0 -> ( ( # ` M ) = +oo -> N <_ ( # ` M ) ) )
14 13 3ad2ant3 
 |-  ( ( M e. V /\ ( # ` M ) e/ NN0 /\ N e. NN0 ) -> ( ( # ` M ) = +oo -> N <_ ( # ` M ) ) )
15 hashnn0pnf 
 |-  ( M e. V -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) )
16 15 3ad2ant1 
 |-  ( ( M e. V /\ ( # ` M ) e/ NN0 /\ N e. NN0 ) -> ( ( # ` M ) e. NN0 \/ ( # ` M ) = +oo ) )
17 4 14 16 mpjaod 
 |-  ( ( M e. V /\ ( # ` M ) e/ NN0 /\ N e. NN0 ) -> N <_ ( # ` M ) )