Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Ordering on real numbers - Real and complex numbers basic operations
rpex
Next ⟩
xrge0ge0
Metamath Proof Explorer
Ascii
Unicode
Theorem
rpex
Description:
The positive reals form a set.
(Contributed by
Glauco Siliprandi
, 11-Oct-2020)
Ref
Expression
Assertion
rpex
⊢
ℝ
+
∈
V
Proof
Step
Hyp
Ref
Expression
1
reex
⊢
ℝ
∈
V
2
rpssre
⊢
ℝ
+
⊆
ℝ
3
1
2
ssexi
⊢
ℝ
+
∈
V