Theorem 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	$$⊢A\in 𝑷\to A\subset 𝑸$$

Proof

Step	Hyp	Ref	Expression
1		elnpi	$$⊢A\in 𝑷\leftrightarrow \left(\left(A\in \mathrm{V}\wedge \varnothing \subset A\wedge A\subset 𝑸\right)\wedge \forall x\in A\left(\forall y\left(y{<}_{𝑸}x\to y\in A\right)\wedge \exists y\in Ax{<}_{𝑸}y\right)\right)$$
2		simpl3	$$⊢\left(\left(A\in \mathrm{V}\wedge \varnothing \subset A\wedge A\subset 𝑸\right)\wedge \forall x\in A\left(\forall y\left(y{<}_{𝑸}x\to y\in A\right)\wedge \exists y\in Ax{<}_{𝑸}y\right)\right)\to A\subset 𝑸$$
3	1 2	sylbi	$$⊢A\in 𝑷\to A\subset 𝑸$$