Metamath Proof Explorer


Theorem hashclb

Description: Reverse closure of the # function. (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Assertion hashclb
|- ( A e. V -> ( A e. Fin <-> ( # ` A ) e. NN0 ) )

Proof

Step Hyp Ref Expression
1 hashcl
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
2 nn0re
 |-  ( ( # ` A ) e. NN0 -> ( # ` A ) e. RR )
3 pnfnre
 |-  +oo e/ RR
4 3 neli
 |-  -. +oo e. RR
5 hashinf
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( # ` A ) = +oo )
6 5 eleq1d
 |-  ( ( A e. V /\ -. A e. Fin ) -> ( ( # ` A ) e. RR <-> +oo e. RR ) )
7 4 6 mtbiri
 |-  ( ( A e. V /\ -. A e. Fin ) -> -. ( # ` A ) e. RR )
8 7 ex
 |-  ( A e. V -> ( -. A e. Fin -> -. ( # ` A ) e. RR ) )
9 8 con4d
 |-  ( A e. V -> ( ( # ` A ) e. RR -> A e. Fin ) )
10 2 9 syl5
 |-  ( A e. V -> ( ( # ` A ) e. NN0 -> A e. Fin ) )
11 1 10 impbid2
 |-  ( A e. V -> ( A e. Fin <-> ( # ` A ) e. NN0 ) )