This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) )