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

Metamath Proof Explorer

Definition df-1p

Description: Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. Definition of Gleason p. 122. (Contributed by NM, 13-Mar-1996) (New usage is discouraged.)

Ref Expression
Assertion df-1p 1P = { 𝑥 ∣ 𝑥 <Q 1Q }

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1p ⊢ 1P
1 vx ⊢ 𝑥
2 1 cv ⊢ 𝑥
3 cltq ⊢ <Q
4 c1q ⊢ 1Q
5 2 4 3 wbr ⊢ 𝑥 <Q 1Q
6 5 1 cab ⊢ { 𝑥 ∣ 𝑥 <Q 1Q }
7 0 6 wceq ⊢ 1P = { 𝑥 ∣ 𝑥 <Q 1Q }