Theorem ltrelnq 7738

Description: Positive fraction 'less than' is a relation on positive fractions. (Contributed by NM, 14-Feb-1996.) (Revised by Mario Carneiro, 27-Apr-2013.)

Assertion

Ref	Expression
ltrelnq	|- <Q C_ ( Q. X. Q. )

Proof of Theorem ltrelnq

Dummy variables x y z w u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ltnqqs 7726	. 2 |- <Q = { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) ) }
2		opabssxp 4851	. 2 |- { <. x , y >. | ( ( x e. Q. /\ y e. Q. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~Q /\ y = [ <. v , u >. ] ~Q ) /\ ( z .N u ) <N ( w .N v ) ) ) } C_ ( Q. X. Q. )
3	1, 2	eqsstri 3280	1 |- <Q C_ ( Q. X. Q. )

This proof depends on syntax axioms:   /\ wa 104   = wceq 1402   E.wex 1545   e. wcel 2209   C_ wss 3220   <.cop 3712   class class class wbr 4131   {copab 4192   X. cxp 4774  (class class class)co 6088   [cec 6809   .N cmi 7647   <N clti 7648   ~Q ceq 7652   Q.cnq 7653   <Q cltq 7658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-in 3226  df-ss 3233  df-opab 4194  df-xp 4782  df-ltnqqs 7726

This theorem is used by:  ltanqi  7775  ltmnqi  7776  lt2addnq  7777  lt2mulnq  7778  ltexnqi  7782  ltbtwnnqq  7788  ltbtwnnq  7789  prarloclemarch2  7792  ltrnqi  7794  prcdnql  7857  prcunqu  7858  prnmaxl  7861  prnminu  7862  prloc  7864  prarloclemcalc  7875  genplt2i  7883  genpcdl  7892  genpcuu  7893  genpdisj  7896  addnqprllem  7900  addnqprulem  7901  addlocprlemlt  7904  addlocprlemeq  7906  addlocprlemgt  7907  addlocprlem  7908  nqprdisj  7917  nqprloc  7918  nqprxx  7919  ltnqex  7922  gtnqex  7923  addnqprlemrl  7930  addnqprlemru  7931  addnqprlemfl  7932  addnqprlemfu  7933  appdivnq  7936  prmuloclemcalc  7938  prmuloc  7939  mulnqprlemrl  7946  mulnqprlemru  7947  mulnqprlemfl  7948  mulnqprlemfu  7949  1idprl  7963  1idpru  7964  ltnqpri  7967  ltsopr  7969  ltexprlemopl  7974  ltexprlemopu  7976  ltexprlemdisj  7979  ltexprlemloc  7980  ltexprlemfl  7982  ltexprlemru  7985  recexprlemell  7995  recexprlemelu  7996  recexprlemlol  7999  recexprlemupu  8001  recexprlemdisj  8003  recexprlemloc  8004  recexprlempr  8005  recexprlem1ssl  8006  recexprlem1ssu  8007  recexprlemss1l  8008  recexprlemss1u  8009  cauappcvgprlemm  8018  cauappcvgprlemopl  8019  cauappcvgprlemlol  8020  cauappcvgprlemupu  8022  cauappcvgprlemladdfu  8027  cauappcvgprlemladdfl  8028  caucvgprlemk  8038  caucvgprlemnkj  8039  caucvgprlemnbj  8040  caucvgprlemm  8041  caucvgprlemopl  8042  caucvgprlemlol  8043  caucvgprlemupu  8045  caucvgprlemloc  8048  caucvgprlemladdfu  8050  caucvgprprlemloccalc  8057  caucvgprprlemml  8067  caucvgprprlemopl  8070  caucvgprprlemlol  8071  caucvgprprlemupu  8073  caucvgprprlemloc  8076  suplocexprlemrl  8090  suplocexprlemru  8092