Metamath Proof Explorer


Theorem hashxrcl

Description: Extended real closure of the # function. (Contributed by Mario Carneiro, 22-Apr-2015)

Ref Expression
Assertion hashxrcl AVA*

Proof

Step Hyp Ref Expression
1 nn0ssre 0
2 ressxr *
3 1 2 sstri 0*
4 pnfxr +∞*
5 snssi +∞*+∞*
6 4 5 ax-mp +∞*
7 3 6 unssi 0+∞*
8 elex AVAV
9 hashf .:V0+∞
10 9 ffvelrni AVA0+∞
11 8 10 syl AVA0+∞
12 7 11 sselid AVA*