Theorem ltrelnq 7733

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 7721	. 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 4849	. 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 4130   {copab 4191   X. cxp 4772  (class class class)co 6085   [cec 6805   .N cmi 7642   <N clti 7643   ~Q ceq 7647   Q.cnq 7648   <Q cltq 7653

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 4193  df-xp 4780  df-ltnqqs 7721

This theorem is used by:  ltanqi  7770  ltmnqi  7771  lt2addnq  7772  lt2mulnq  7773  ltexnqi  7777  ltbtwnnqq  7783  ltbtwnnq  7784  prarloclemarch2  7787  ltrnqi  7789  prcdnql  7852  prcunqu  7853  prnmaxl  7856  prnminu  7857  prloc  7859  prarloclemcalc  7870  genplt2i  7878  genpcdl  7887  genpcuu  7888  genpdisj  7891  addnqprllem  7895  addnqprulem  7896  addlocprlemlt  7899  addlocprlemeq  7901  addlocprlemgt  7902  addlocprlem  7903  nqprdisj  7912  nqprloc  7913  nqprxx  7914  ltnqex  7917  gtnqex  7918  addnqprlemrl  7925  addnqprlemru  7926  addnqprlemfl  7927  addnqprlemfu  7928  appdivnq  7931  prmuloclemcalc  7933  prmuloc  7934  mulnqprlemrl  7941  mulnqprlemru  7942  mulnqprlemfl  7943  mulnqprlemfu  7944  1idprl  7958  1idpru  7959  ltnqpri  7962  ltsopr  7964  ltexprlemopl  7969  ltexprlemopu  7971  ltexprlemdisj  7974  ltexprlemloc  7975  ltexprlemfl  7977  ltexprlemru  7980  recexprlemell  7990  recexprlemelu  7991  recexprlemlol  7994  recexprlemupu  7996  recexprlemdisj  7998  recexprlemloc  7999  recexprlempr  8000  recexprlem1ssl  8001  recexprlem1ssu  8002  recexprlemss1l  8003  recexprlemss1u  8004  cauappcvgprlemm  8013  cauappcvgprlemopl  8014  cauappcvgprlemlol  8015  cauappcvgprlemupu  8017  cauappcvgprlemladdfu  8022  cauappcvgprlemladdfl  8023  caucvgprlemk  8033  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemupu  8040  caucvgprlemloc  8043  caucvgprlemladdfu  8045  caucvgprprlemloccalc  8052  caucvgprprlemml  8062  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemupu  8068  caucvgprprlemloc  8071  suplocexprlemrl  8085  suplocexprlemru  8087