Database
REAL AND COMPLEX NUMBERS
Elementary integer functions
The ` # ` (set size) function
hashxrcl
Next ⟩
hashclb
Metamath Proof Explorer
Ascii
Unicode
Theorem
hashxrcl
Description:
Extended real closure of the
#
function.
(Contributed by
Mario Carneiro
, 22-Apr-2015)
Ref
Expression
Assertion
hashxrcl
⊢
A
∈
V
→
A
∈
ℝ
*
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
⊢
A
∈
V
→
A
∈
V
9
hashf
⊢
.
:
V
⟶
ℕ
0
∪
+∞
10
9
ffvelcdmi
⊢
A
∈
V
→
A
∈
ℕ
0
∪
+∞
11
8
10
syl
⊢
A
∈
V
→
A
∈
ℕ
0
∪
+∞
12
7
11
sselid
⊢
A
∈
V
→
A
∈
ℝ
*