This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Construction and axiomatization of real and complex numbers Dedekind-cut construction of real and complex numbers elprnq
Description: A positive real is a set of positive fractions. (Contributed by NM , 13-Mar-1996) (Revised by Mario Carneiro , 11-May-2013)
(New usage is discouraged.)
Ref
Expression
Assertion
elprnq ⊢ ( ( 𝐴 ∈ P 𝐵 ∈ 𝐴 ) → 𝐵 ∈ Q
Proof
Step
Hyp
Ref
Expression
1
prpssnq ⊢ ( 𝐴 ∈ P 𝐴 ⊊ Q
2
1
pssssd ⊢ ( 𝐴 ∈ P 𝐴 ⊆ Q
3
2
sselda ⊢ ( ( 𝐴 ∈ P 𝐵 ∈ 𝐴 ) → 𝐵 ∈ Q