Theorem ltrelnq 7563

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 7551	. 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 4793	. 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 3256	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1395   E.wex 1538   e. wcel 2200   C_ wss 3197   <.cop 3669   class class class wbr 4083   {copab 4144   X. cxp 4717  (class class class)co 6007   [cec 6686   .N cmi 7472   <N clti 7473   ~Q ceq 7477   Q.cnq 7478   <Q cltq 7483

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-in 3203  df-ss 3210  df-opab 4146  df-xp 4725  df-ltnqqs 7551

This theorem is referenced by:  ltanqi  7600  ltmnqi  7601  lt2addnq  7602  lt2mulnq  7603  ltexnqi  7607  ltbtwnnqq  7613  ltbtwnnq  7614  prarloclemarch2  7617  ltrnqi  7619  prcdnql  7682  prcunqu  7683  prnmaxl  7686  prnminu  7687  prloc  7689  prarloclemcalc  7700  genplt2i  7708  genpcdl  7717  genpcuu  7718  genpdisj  7721  addnqprllem  7725  addnqprulem  7726  addlocprlemlt  7729  addlocprlemeq  7731  addlocprlemgt  7732  addlocprlem  7733  nqprdisj  7742  nqprloc  7743  nqprxx  7744  ltnqex  7747  gtnqex  7748  addnqprlemrl  7755  addnqprlemru  7756  addnqprlemfl  7757  addnqprlemfu  7758  appdivnq  7761  prmuloclemcalc  7763  prmuloc  7764  mulnqprlemrl  7771  mulnqprlemru  7772  mulnqprlemfl  7773  mulnqprlemfu  7774  1idprl  7788  1idpru  7789  ltnqpri  7792  ltsopr  7794  ltexprlemopl  7799  ltexprlemopu  7801  ltexprlemdisj  7804  ltexprlemloc  7805  ltexprlemfl  7807  ltexprlemru  7810  recexprlemell  7820  recexprlemelu  7821  recexprlemlol  7824  recexprlemupu  7826  recexprlemdisj  7828  recexprlemloc  7829  recexprlempr  7830  recexprlem1ssl  7831  recexprlem1ssu  7832  recexprlemss1l  7833  recexprlemss1u  7834  cauappcvgprlemm  7843  cauappcvgprlemopl  7844  cauappcvgprlemlol  7845  cauappcvgprlemupu  7847  cauappcvgprlemladdfu  7852  cauappcvgprlemladdfl  7853  caucvgprlemk  7863  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemupu  7870  caucvgprlemloc  7873  caucvgprlemladdfu  7875  caucvgprprlemloccalc  7882  caucvgprprlemml  7892  caucvgprprlemopl  7895  caucvgprprlemlol  7896  caucvgprprlemupu  7898  caucvgprprlemloc  7901  suplocexprlemrl  7915  suplocexprlemru  7917