Theorem 0npq 5115

Description: The empty set is not a positive fraction.

Assertion

Ref	Expression
0npq	|- -. (/) e. Q.

Proof of Theorem 0npq

Step	Hyp	Ref	Expression
1		dmenq 5110	. . 3 |- dom ~Q = (N. X. N.)
2	1	0nelqs 4359	. 2 |- -. (/) e. ((N. X. N.)/. ~Q )
3		df-nq 5103	. . 3 |- Q. = ((N. X. N.)/. ~Q )
4	3	eleq2i 1585	. 2 |- ((/) e. Q. <-> (/) e. ((N. X. N.)/. ~Q ))
5	2, 4	mtbir 199	1 |- -. (/) e. Q.

Syntax hints:  -. wn 2   e. wcel 999  (/)c0 2331   X. cxp 3225  /.cqs 4318  N.cnpi 5037   ~Q ceq 5043  Q.cnq 5044

This theorem is referenced by:  dmaddpq 5124  dmmulpq 5126  addasspq 5128  mulasspq 5130  distrpq 5132  recmulpq 5135  recclpq 5137  ltapq 5141  ltmpq 5142  ltexpq 5145  ltexpq2 5146  nsmallpq 5148  ltbtwnpq 5149  ltaddpr 5205  ltexprlem2 5208  ltexprlem3 5209  ltexprlem4 5210  ltexprlem6 5212  ltexprlem7 5213  reclem1pr 5221  reclem2pr 5222

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-nul 2765  ax-pow 2798  ax-pr 2835  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-3or 788  df-3an 789  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-sbc 1989  df-csb 2052  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-if 2414  df-pw 2454  df-sn 2464  df-pr 2465  df-tp 2467  df-op 2468  df-uni 2558  df-int 2588  df-iun 2622  df-br 2675  df-opab 2722  df-tr 2736  df-eprel 2888  df-id 2891  df-po 2896  df-so 2906  df-fr 2974  df-we 2991  df-ord 3008  df-on 3009  df-lim 3010  df-suc 3011  df-om 3189  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255  df-rdg 3990  df-opr 4023  df-oprab 4024  df-1st 4137  df-2nd 4138  df-oadd 4193  df-omul 4194  df-ec 4321  df-qs 4324  df-ni 5065  df-mi 5067  df-enq 5102  df-nq 5103

Copyright terms: Public domain