Metamath Proof Explorer

Theorem hashxrcl

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

Ref Expression
Assertion hashxrcl 
|- ( A e. V -> ( # ` A ) e. RR* )

Proof

Step Hyp Ref Expression
1 nn0ssre 
 |-  NN0 C_ RR
2 ressxr 
 |-  RR C_ RR*
3 1 2 sstri 
 |-  NN0 C_ RR*
4 pnfxr 
 |-  +oo e. RR*
5 snssi 
 |-  ( +oo e. RR* -> { +oo } C_ RR* )
6 4 5 ax-mp 
 |-  { +oo } C_ RR*
7 3 6 unssi 
 |-  ( NN0 u. { +oo } ) C_ RR*
8 elex 
 |-  ( A e. V -> A e. _V )
9 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
10 9 ffvelcdmi 
 |-  ( A e. _V -> ( # ` A ) e. ( NN0 u. { +oo } ) )
11 8 10 syl 
 |-  ( A e. V -> ( # ` A ) e. ( NN0 u. { +oo } ) )
12 7 11 sselid 
 |-  ( A e. V -> ( # ` A ) e. RR* )