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