Metamath Proof Explorer

Definition df-1nq

Description: Define positive fraction 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. From Proposition 9-2.2 of Gleason p. 117. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.)

Ref Expression
Assertion df-1nq 
|- 1Q = <. 1o , 1o >.

Detailed syntax breakdown

Step Hyp Ref Expression
0 c1q 
 |-  1Q
1 c1o 
 |-  1o
2 1 1 cop 
 |-  <. 1o , 1o >.
3 0 2 wceq 
 |-  1Q = <. 1o , 1o >.