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
Structured
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