Theorem ltrelnq 7366

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 7354	. 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 4702	. 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 3189	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1353   E.wex 1492   e. wcel 2148   C_ wss 3131   <.cop 3597   class class class wbr 4005   {copab 4065   X. cxp 4626  (class class class)co 5877   [cec 6535   .N cmi 7275   <N clti 7276   ~Q ceq 7280   Q.cnq 7281   <Q cltq 7286

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 3137  df-ss 3144  df-opab 4067  df-xp 4634  df-ltnqqs 7354

This theorem is referenced by:  ltanqi  7403  ltmnqi  7404  lt2addnq  7405  lt2mulnq  7406  ltexnqi  7410  ltbtwnnqq  7416  ltbtwnnq  7417  prarloclemarch2  7420  ltrnqi  7422  prcdnql  7485  prcunqu  7486  prnmaxl  7489  prnminu  7490  prloc  7492  prarloclemcalc  7503  genplt2i  7511  genpcdl  7520  genpcuu  7521  genpdisj  7524  addnqprllem  7528  addnqprulem  7529  addlocprlemlt  7532  addlocprlemeq  7534  addlocprlemgt  7535  addlocprlem  7536  nqprdisj  7545  nqprloc  7546  nqprxx  7547  ltnqex  7550  gtnqex  7551  addnqprlemrl  7558  addnqprlemru  7559  addnqprlemfl  7560  addnqprlemfu  7561  appdivnq  7564  prmuloclemcalc  7566  prmuloc  7567  mulnqprlemrl  7574  mulnqprlemru  7575  mulnqprlemfl  7576  mulnqprlemfu  7577  1idprl  7591  1idpru  7592  ltnqpri  7595  ltsopr  7597  ltexprlemopl  7602  ltexprlemopu  7604  ltexprlemdisj  7607  ltexprlemloc  7608  ltexprlemfl  7610  ltexprlemru  7613  recexprlemell  7623  recexprlemelu  7624  recexprlemlol  7627  recexprlemupu  7629  recexprlemdisj  7631  recexprlemloc  7632  recexprlempr  7633  recexprlem1ssl  7634  recexprlem1ssu  7635  recexprlemss1l  7636  recexprlemss1u  7637  cauappcvgprlemm  7646  cauappcvgprlemopl  7647  cauappcvgprlemlol  7648  cauappcvgprlemupu  7650  cauappcvgprlemladdfu  7655  cauappcvgprlemladdfl  7656  caucvgprlemk  7666  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemupu  7673  caucvgprlemloc  7676  caucvgprlemladdfu  7678  caucvgprprlemloccalc  7685  caucvgprprlemml  7695  caucvgprprlemopl  7698  caucvgprprlemlol  7699  caucvgprprlemupu  7701  caucvgprprlemloc  7704  suplocexprlemrl  7718  suplocexprlemru  7720