Theorem prn0

Description: A positive real is not empty. (Contributed by NM, 15-May-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	prn0	$$⊢A\in 𝑷\to A\ne \varnothing$$

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		simpl2	$$⊢\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 \varnothing \subset A$$
3	1 2	sylbi	$$⊢A\in 𝑷\to \varnothing \subset A$$
4		0pss	$$⊢\varnothing \subset A\leftrightarrow A\ne \varnothing$$
5	3 4	sylib	$$⊢A\in 𝑷\to A\ne \varnothing$$