Metamath Proof Explorer

Theorem hashnemnf

Description: The size of a set is never minus infinity. (Contributed by Alexander van der Vekens, 21-Dec-2017)

Ref Expression
Assertion hashnemnf 
|- ( A e. V -> ( # ` A ) =/= -oo )

Proof

Step Hyp Ref Expression
1 hashnn0pnf 
 |-  ( A e. V -> ( ( # ` A ) e. NN0 \/ ( # ` A ) = +oo ) )
2 mnfnre 
 |-  -oo e/ RR
3 df-nel 
 |-  ( -oo e/ RR <-> -. -oo e. RR )
4 nn0re 
 |-  ( -oo e. NN0 -> -oo e. RR )
5 4 con3i 
 |-  ( -. -oo e. RR -> -. -oo e. NN0 )
6 3 5 sylbi 
 |-  ( -oo e/ RR -> -. -oo e. NN0 )
7 2 6 ax-mp 
 |-  -. -oo e. NN0
8 eleq1 
 |-  ( ( # ` A ) = -oo -> ( ( # ` A ) e. NN0 <-> -oo e. NN0 ) )
9 7 8 mtbiri 
 |-  ( ( # ` A ) = -oo -> -. ( # ` A ) e. NN0 )
10 9 necon2ai 
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) =/= -oo )
11 pnfnemnf 
 |-  +oo =/= -oo
12 neeq1 
 |-  ( ( # ` A ) = +oo -> ( ( # ` A ) =/= -oo <-> +oo =/= -oo ) )
13 11 12 mpbiri 
 |-  ( ( # ` A ) = +oo -> ( # ` A ) =/= -oo )
14 10 13 jaoi 
 |-  ( ( ( # ` A ) e. NN0 \/ ( # ` A ) = +oo ) -> ( # ` A ) =/= -oo )
15 1 14 syl 
 |-  ( A e. V -> ( # ` A ) =/= -oo )