Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  npex Structured version   Visualization version   GIF version

Theorem npex 10415
 Description: The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
Assertion
Ref Expression
npex P ∈ V

Proof of Theorem npex
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nqex 10352 . . 3 Q ∈ V
21pwex 5250 . 2 𝒫 Q ∈ V
3 pssss 4026 . . . . 5 (𝑥Q𝑥Q)
43ad2antlr 726 . . . 4 (((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧)) → 𝑥Q)
54ss2abi 3996 . . 3 {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))} ⊆ {𝑥𝑥Q}
6 df-np 10410 . . 3 P = {𝑥 ∣ ((∅ ⊊ 𝑥𝑥Q) ∧ ∀𝑦𝑥 (∀𝑧(𝑧 <Q 𝑦𝑧𝑥) ∧ ∃𝑧𝑥 𝑦 <Q 𝑧))}
7 df-pw 4502 . . 3 𝒫 Q = {𝑥𝑥Q}
85, 6, 73sstr4i 3960 . 2 P ⊆ 𝒫 Q
92, 8ssexi 5194 1 P ∈ V
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107  Vcvv 3442   ⊆ wss 3883   ⊊ wpss 3884  ∅c0 4246  𝒫 cpw 4500   class class class wbr 5034  Qcnq 10281
 Copyright terms: Public domain W3C validator