Theorem hashxrcl

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

	Ref	Expression
Assertion	hashxrcl	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )

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	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ V )
9		hashf	⊢ ♯ : V ⟶ ( ℕ0 ∪ { +∞ } )
10	9	ffvelrni	⊢ ( 𝐴 ∈ V → ( ♯ ‘ 𝐴 ) ∈ ( ℕ0 ∪ { +∞ } ) )
11	8 10	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ( ℕ0 ∪ { +∞ } ) )
12	7 11	sselid	⊢ ( 𝐴 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) ∈ ℝ* )