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