hashxrcl

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

		Ref	Expression
	Assertion	hashxrcl	$⊢ A \in V \to \|A\| \in ℝ^{*}$

Step	Hyp	Ref	Expression
1		nn0ssre	$⊢ ℕ_{0} \subseteq ℝ$
2		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
3	1 2	sstri	$⊢ ℕ_{0} \subseteq ℝ^{*}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5		snssi	$⊢ +∞ \in ℝ^{} \to \{+∞\} \subseteq ℝ^{}$
6	4 5	ax-mp	$⊢ \{+∞\} \subseteq ℝ^{*}$
7	3 6	unssi	$⊢ ℕ_{0} \cup \{+∞\} \subseteq ℝ^{*}$
8		elex	$⊢ A \in V \to A \in V$
9		hashf	$⊢ \|.\| : V ⟶ ℕ_{0} \cup \{+∞\}$
10	9	ffvelcdmi	$⊢ A \in V \to \|A\| \in (ℕ_{0} \cup \{+∞\})$
11	8 10	syl	$⊢ A \in V \to \|A\| \in (ℕ_{0} \cup \{+∞\})$
12	7 11	sselid	$⊢ A \in V \to \|A\| \in ℝ^{*}$

Metamath Proof Explorer