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	⊢ P ∈ V

Proof

Step	Hyp	Ref	Expression
1		nqex	⊢ Q ∈ V
2	1	pwex	⊢ 𝒫 Q ∈ V
3		pssss	⊢ ( 𝑥 ⊊ Q → 𝑥 ⊆ Q )
4	3	ad2antlr	⊢ ( ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) → 𝑥 ⊆ Q )
5	4	ss2abi	⊢ { 𝑥 ∣ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) } ⊆ { 𝑥 ∣ 𝑥 ⊆ Q }
6		df-np	⊢ P = { 𝑥 ∣ ( ( ∅ ⊊ 𝑥 ∧ 𝑥 ⊊ Q ) ∧ ∀ 𝑦 ∈ 𝑥 ( ∀ 𝑧 ( 𝑧 <Q 𝑦 → 𝑧 ∈ 𝑥 ) ∧ ∃ 𝑧 ∈ 𝑥 𝑦 <Q 𝑧 ) ) }
7		df-pw	⊢ 𝒫 Q = { 𝑥 ∣ 𝑥 ⊆ Q }
8	5 6 7	3sstr4i	⊢ P ⊆ 𝒫 Q
9	2 8	ssexi	⊢ P ∈ V