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 V$

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

Metamath Proof Explorer