Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 nqex ⊢ 𝑸 ∈ V
2 1 pwex ⊢ 𝒫 𝑸 ∈ V
3 pssss ⊢ x ⊂ 𝑸 → x ⊆ 𝑸
4 3 ad2antlr ⊢ ∅ ⊂ x ∧ x ⊂ 𝑸 ∧ ∀ y ∈ x ∀ z z < 𝑸 y → z ∈ x ∧ ∃ z ∈ x y < 𝑸 z → x ⊆ 𝑸
5 4 ss2abi ⊢ x | ∅ ⊂ x ∧ x ⊂ 𝑸 ∧ ∀ y ∈ x ∀ z z < 𝑸 y → z ∈ x ∧ ∃ z ∈ x y < 𝑸 z ⊆ x | x ⊆ 𝑸
6 df-np ⊢ 𝑷 = x | ∅ ⊂ x ∧ x ⊂ 𝑸 ∧ ∀ y ∈ x ∀ z z < 𝑸 y → z ∈ x ∧ ∃ z ∈ x y < 𝑸 z
7 df-pw ⊢ 𝒫 𝑸 = x | x ⊆ 𝑸
8 5 6 7 3sstr4i ⊢ 𝑷 ⊆ 𝒫 𝑸
9 2 8 ssexi ⊢ 𝑷 ∈ V