Theorem hashf2

Description: Lemma for hasheuni . (Contributed by Thierry Arnoux, 19-Nov-2016)

	Ref	Expression
Assertion	hashf2	|- # : _V --> ( 0 [,] +oo )

Proof

Step	Hyp	Ref	Expression
1		hashf	|- # : _V --> ( NN0 u. { +oo } )
2		nn0z	|- ( x e. NN0 -> x e. ZZ )
3		zre	|- ( x e. ZZ -> x e. RR )
4		rexr	|- ( x e. RR -> x e. RR* )
5	2 3 4	3syl	|- ( x e. NN0 -> x e. RR* )
6		nn0ge0	|- ( x e. NN0 -> 0 <_ x )
7		elxrge0	|- ( x e. ( 0 [,] +oo ) <-> ( x e. RR* /\ 0 <_ x ) )
8	5 6 7	sylanbrc	|- ( x e. NN0 -> x e. ( 0 [,] +oo ) )
9	8	ssriv	|- NN0 C_ ( 0 [,] +oo )
10		0xr	|- 0 e. RR*
11		pnfxr	|- +oo e. RR*
12		0lepnf	|- 0 <_ +oo
13		ubicc2	|- ( ( 0 e. RR* /\ +oo e. RR* /\ 0 <_ +oo ) -> +oo e. ( 0 [,] +oo ) )
14	10 11 12 13	mp3an	|- +oo e. ( 0 [,] +oo )
15		snssi	|- ( +oo e. ( 0 [,] +oo ) -> { +oo } C_ ( 0 [,] +oo ) )
16	14 15	ax-mp	|- { +oo } C_ ( 0 [,] +oo )
17	9 16	unssi	|- ( NN0 u. { +oo } ) C_ ( 0 [,] +oo )
18		fss	|- ( ( # : _V --> ( NN0 u. { +oo } ) /\ ( NN0 u. { +oo } ) C_ ( 0 [,] +oo ) ) -> # : _V --> ( 0 [,] +oo ) )
19	1 17 18	mp2an	|- # : _V --> ( 0 [,] +oo )