Theorem npex

Description: The class of positive reals is a set. (Contributed by NM, 31-Oct-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	npex	$$⊢𝑷\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		nqex	$$⊢𝑸\in \mathrm{V}$$
2	1	pwex	$$⊢𝒫𝑸\in \mathrm{V}$$
3		pssss	$$⊢x\subset 𝑸\to x\subseteq 𝑸$$
4	3	ad2antlr	$$⊢\left(\left(\varnothing \subset x\wedge x\subset 𝑸\right)\wedge \forall y\in x\left(\forall z\left(z{<}_{𝑸}y\to z\in x\right)\wedge \exists z\in xy{<}_{𝑸}z\right)\right)\to x\subseteq 𝑸$$
5	4	ss2abi	$$⊢\left\{x|\left(\left(\varnothing \subset x\wedge x\subset 𝑸\right)\wedge \forall y\in x\left(\forall z\left(z{<}_{𝑸}y\to z\in x\right)\wedge \exists z\in xy{<}_{𝑸}z\right)\right)\right\}\subseteq \left\{x|x\subseteq 𝑸\right\}$$
6		df-np	$$⊢𝑷=\left\{x|\left(\left(\varnothing \subset x\wedge x\subset 𝑸\right)\wedge \forall y\in x\left(\forall z\left(z{<}_{𝑸}y\to z\in x\right)\wedge \exists z\in xy{<}_{𝑸}z\right)\right)\right\}$$
7		df-pw	$$⊢𝒫𝑸=\left\{x|x\subseteq 𝑸\right\}$$
8	5 6 7	3sstr4i	$$⊢𝑷\subseteq 𝒫𝑸$$
9	2 8	ssexi	$$⊢𝑷\in \mathrm{V}$$