Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Real intervals
ioofun
Next ⟩
icomnfinre
Metamath Proof Explorer
Ascii
Unicode
Theorem
ioofun
Description:
(,)
is a function.
(Contributed by
Glauco Siliprandi
, 26-Jun-2021)
Ref
Expression
Assertion
ioofun
⊢
Fun
⁡
.
Proof
Step
Hyp
Ref
Expression
1
ioof
⊢
.
:
ℝ
*
×
ℝ
*
⟶
𝒫
ℝ
2
ffun
⊢
.
:
ℝ
*
×
ℝ
*
⟶
𝒫
ℝ
→
Fun
⁡
.
3
1
2
ax-mp
⊢
Fun
⁡
.