Metamath Proof Explorer


Theorem 0nnq

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.

Proof

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.