Description: Define class of positive fractions. 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, 16-Aug-1995) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-nq | |- Q. = { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cnq | |- Q. |
|
| 1 | vx | |- x |
|
| 2 | cnpi | |- N. |
|
| 3 | 2 2 | cxp | |- ( N. X. N. ) |
| 4 | vy | |- y |
|
| 5 | 1 | cv | |- x |
| 6 | ceq | |- ~Q |
|
| 7 | 4 | cv | |- y |
| 8 | 5 7 6 | wbr | |- x ~Q y |
| 9 | c2nd | |- 2nd |
|
| 10 | 7 9 | cfv | |- ( 2nd ` y ) |
| 11 | clti | |- |
|
| 12 | 5 9 | cfv | |- ( 2nd ` x ) |
| 13 | 10 12 11 | wbr | |- ( 2nd ` y ) |
| 14 | 13 | wn | |- -. ( 2nd ` y ) |
| 15 | 8 14 | wi | |- ( x ~Q y -> -. ( 2nd ` y ) |
| 16 | 15 4 3 | wral | |- A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) |
| 17 | 16 1 3 | crab | |- { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) |
| 18 | 0 17 | wceq | |- Q. = { x e. ( N. X. N. ) | A. y e. ( N. X. N. ) ( x ~Q y -> -. ( 2nd ` y ) |