Theorem ltrelnq 7477

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 7465	. 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 4748	. 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 3224	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1372   E.wex 1514   e. wcel 2175   C_ wss 3165   <.cop 3635   class class class wbr 4043   {copab 4103   X. cxp 4672  (class class class)co 5943   [cec 6617   .N cmi 7386   <N clti 7387   ~Q ceq 7391   Q.cnq 7392   <Q cltq 7397

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-in 3171  df-ss 3178  df-opab 4105  df-xp 4680  df-ltnqqs 7465

This theorem is referenced by:  ltanqi  7514  ltmnqi  7515  lt2addnq  7516  lt2mulnq  7517  ltexnqi  7521  ltbtwnnqq  7527  ltbtwnnq  7528  prarloclemarch2  7531  ltrnqi  7533  prcdnql  7596  prcunqu  7597  prnmaxl  7600  prnminu  7601  prloc  7603  prarloclemcalc  7614  genplt2i  7622  genpcdl  7631  genpcuu  7632  genpdisj  7635  addnqprllem  7639  addnqprulem  7640  addlocprlemlt  7643  addlocprlemeq  7645  addlocprlemgt  7646  addlocprlem  7647  nqprdisj  7656  nqprloc  7657  nqprxx  7658  ltnqex  7661  gtnqex  7662  addnqprlemrl  7669  addnqprlemru  7670  addnqprlemfl  7671  addnqprlemfu  7672  appdivnq  7675  prmuloclemcalc  7677  prmuloc  7678  mulnqprlemrl  7685  mulnqprlemru  7686  mulnqprlemfl  7687  mulnqprlemfu  7688  1idprl  7702  1idpru  7703  ltnqpri  7706  ltsopr  7708  ltexprlemopl  7713  ltexprlemopu  7715  ltexprlemdisj  7718  ltexprlemloc  7719  ltexprlemfl  7721  ltexprlemru  7724  recexprlemell  7734  recexprlemelu  7735  recexprlemlol  7738  recexprlemupu  7740  recexprlemdisj  7742  recexprlemloc  7743  recexprlempr  7744  recexprlem1ssl  7745  recexprlem1ssu  7746  recexprlemss1l  7747  recexprlemss1u  7748  cauappcvgprlemm  7757  cauappcvgprlemopl  7758  cauappcvgprlemlol  7759  cauappcvgprlemupu  7761  cauappcvgprlemladdfu  7766  cauappcvgprlemladdfl  7767  caucvgprlemk  7777  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemm  7780  caucvgprlemopl  7781  caucvgprlemlol  7782  caucvgprlemupu  7784  caucvgprlemloc  7787  caucvgprlemladdfu  7789  caucvgprprlemloccalc  7796  caucvgprprlemml  7806  caucvgprprlemopl  7809  caucvgprprlemlol  7810  caucvgprprlemupu  7812  caucvgprprlemloc  7815  suplocexprlemrl  7829  suplocexprlemru  7831