This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 1pr

Description: The positive real number 'one'. (Contributed by NM, 13-Mar-1996) (Revised by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion 1pr 1P ∈ P

Proof

Step Hyp Ref Expression
1 df-1p ⊢ 1P = { 𝑥 ∣ 𝑥 <Q 1Q }
2 1nq ⊢ 1Q ∈ Q
3 nqpr ⊢ ( 1Q ∈ Q → { 𝑥 ∣ 𝑥 <Q 1Q } ∈ P )
4 2 3 ax-mp ⊢ { 𝑥 ∣ 𝑥 <Q 1Q } ∈ P
5 1 4 eqeltri ⊢ 1P ∈ P