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 prpssnq
Description: A positive real is a subset of the positive fractions. (Contributed by NM , 29-Feb-1996) (Revised by Mario Carneiro , 11-May-2013)
(New usage is discouraged.)
Ref
Expression
Assertion
prpssnq ⊢ ( 𝐴 ∈ P 𝐴 ⊊ Q
Proof
Step
Hyp
Ref
Expression
1
elnpi ⊢ ( 𝐴 ∈ P 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )
2
simpl3 ⊢ ( ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) → 𝐴 ⊊ Q
3
1 2
sylbi ⊢ ( 𝐴 ∈ P 𝐴 ⊊ Q