Description: The empty set is not a positive fraction. (Contributed by NM, 24-Aug-1995) (Revised by Mario Carneiro, 27-Apr-2013) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0nnq | |- -. (/) e. Q. |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0nelxp | |- -. (/) e. ( N. X. N. ) |
|
| 2 | df-nq | |- Q. = { y e. ( N. X. N. ) | A. x e. ( N. X. N. ) ( y ~Q x -> -. ( 2nd ` x ) |
|
| 3 | 2 | ssrab3 | |- Q. C_ ( N. X. N. ) |
| 4 | 3 | sseli | |- ( (/) e. Q. -> (/) e. ( N. X. N. ) ) |
| 5 | 1 4 | mto | |- -. (/) e. Q. |