Theorem ltrelnq 7359

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 7347	. 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 4698	. 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 3187	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1353   E.wex 1492   e. wcel 2148   C_ wss 3129   <.cop 3595   class class class wbr 4001   {copab 4061   X. cxp 4622  (class class class)co 5870   [cec 6528   .N cmi 7268   <N clti 7269   ~Q ceq 7273   Q.cnq 7274   <Q cltq 7279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-in 3135  df-ss 3142  df-opab 4063  df-xp 4630  df-ltnqqs 7347

This theorem is referenced by:  ltanqi  7396  ltmnqi  7397  lt2addnq  7398  lt2mulnq  7399  ltexnqi  7403  ltbtwnnqq  7409  ltbtwnnq  7410  prarloclemarch2  7413  ltrnqi  7415  prcdnql  7478  prcunqu  7479  prnmaxl  7482  prnminu  7483  prloc  7485  prarloclemcalc  7496  genplt2i  7504  genpcdl  7513  genpcuu  7514  genpdisj  7517  addnqprllem  7521  addnqprulem  7522  addlocprlemlt  7525  addlocprlemeq  7527  addlocprlemgt  7528  addlocprlem  7529  nqprdisj  7538  nqprloc  7539  nqprxx  7540  ltnqex  7543  gtnqex  7544  addnqprlemrl  7551  addnqprlemru  7552  addnqprlemfl  7553  addnqprlemfu  7554  appdivnq  7557  prmuloclemcalc  7559  prmuloc  7560  mulnqprlemrl  7567  mulnqprlemru  7568  mulnqprlemfl  7569  mulnqprlemfu  7570  1idprl  7584  1idpru  7585  ltnqpri  7588  ltsopr  7590  ltexprlemopl  7595  ltexprlemopu  7597  ltexprlemdisj  7600  ltexprlemloc  7601  ltexprlemfl  7603  ltexprlemru  7606  recexprlemell  7616  recexprlemelu  7617  recexprlemlol  7620  recexprlemupu  7622  recexprlemdisj  7624  recexprlemloc  7625  recexprlempr  7626  recexprlem1ssl  7627  recexprlem1ssu  7628  recexprlemss1l  7629  recexprlemss1u  7630  cauappcvgprlemm  7639  cauappcvgprlemopl  7640  cauappcvgprlemlol  7641  cauappcvgprlemupu  7643  cauappcvgprlemladdfu  7648  cauappcvgprlemladdfl  7649  caucvgprlemk  7659  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemm  7662  caucvgprlemopl  7663  caucvgprlemlol  7664  caucvgprlemupu  7666  caucvgprlemloc  7669  caucvgprlemladdfu  7671  caucvgprprlemloccalc  7678  caucvgprprlemml  7688  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemupu  7694  caucvgprprlemloc  7697  suplocexprlemrl  7711  suplocexprlemru  7713