Theorem ltrelnq 7548

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 7536	. 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 4792	. 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 4082   {copab 4143   X. cxp 4716  (class class class)co 6000   [cec 6676   .N cmi 7457   <N clti 7458   ~Q ceq 7462   Q.cnq 7463   <Q cltq 7468

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 4145  df-xp 4724  df-ltnqqs 7536

This theorem is referenced by:  ltanqi  7585  ltmnqi  7586  lt2addnq  7587  lt2mulnq  7588  ltexnqi  7592  ltbtwnnqq  7598  ltbtwnnq  7599  prarloclemarch2  7602  ltrnqi  7604  prcdnql  7667  prcunqu  7668  prnmaxl  7671  prnminu  7672  prloc  7674  prarloclemcalc  7685  genplt2i  7693  genpcdl  7702  genpcuu  7703  genpdisj  7706  addnqprllem  7710  addnqprulem  7711  addlocprlemlt  7714  addlocprlemeq  7716  addlocprlemgt  7717  addlocprlem  7718  nqprdisj  7727  nqprloc  7728  nqprxx  7729  ltnqex  7732  gtnqex  7733  addnqprlemrl  7740  addnqprlemru  7741  addnqprlemfl  7742  addnqprlemfu  7743  appdivnq  7746  prmuloclemcalc  7748  prmuloc  7749  mulnqprlemrl  7756  mulnqprlemru  7757  mulnqprlemfl  7758  mulnqprlemfu  7759  1idprl  7773  1idpru  7774  ltnqpri  7777  ltsopr  7779  ltexprlemopl  7784  ltexprlemopu  7786  ltexprlemdisj  7789  ltexprlemloc  7790  ltexprlemfl  7792  ltexprlemru  7795  recexprlemell  7805  recexprlemelu  7806  recexprlemlol  7809  recexprlemupu  7811  recexprlemdisj  7813  recexprlemloc  7814  recexprlempr  7815  recexprlem1ssl  7816  recexprlem1ssu  7817  recexprlemss1l  7818  recexprlemss1u  7819  cauappcvgprlemm  7828  cauappcvgprlemopl  7829  cauappcvgprlemlol  7830  cauappcvgprlemupu  7832  cauappcvgprlemladdfu  7837  cauappcvgprlemladdfl  7838  caucvgprlemk  7848  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemm  7851  caucvgprlemopl  7852  caucvgprlemlol  7853  caucvgprlemupu  7855  caucvgprlemloc  7858  caucvgprlemladdfu  7860  caucvgprprlemloccalc  7867  caucvgprprlemml  7877  caucvgprprlemopl  7880  caucvgprprlemlol  7881  caucvgprprlemupu  7883  caucvgprprlemloc  7886  suplocexprlemrl  7900  suplocexprlemru  7902