Theorem ltrelnq 7427

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 7415	. 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 4734	. 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 3212	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1364   E.wex 1503   e. wcel 2164   C_ wss 3154   <.cop 3622   class class class wbr 4030   {copab 4090   X. cxp 4658  (class class class)co 5919   [cec 6587   .N cmi 7336   <N clti 7337   ~Q ceq 7341   Q.cnq 7342   <Q cltq 7347

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-in 3160  df-ss 3167  df-opab 4092  df-xp 4666  df-ltnqqs 7415

This theorem is referenced by:  ltanqi  7464  ltmnqi  7465  lt2addnq  7466  lt2mulnq  7467  ltexnqi  7471  ltbtwnnqq  7477  ltbtwnnq  7478  prarloclemarch2  7481  ltrnqi  7483  prcdnql  7546  prcunqu  7547  prnmaxl  7550  prnminu  7551  prloc  7553  prarloclemcalc  7564  genplt2i  7572  genpcdl  7581  genpcuu  7582  genpdisj  7585  addnqprllem  7589  addnqprulem  7590  addlocprlemlt  7593  addlocprlemeq  7595  addlocprlemgt  7596  addlocprlem  7597  nqprdisj  7606  nqprloc  7607  nqprxx  7608  ltnqex  7611  gtnqex  7612  addnqprlemrl  7619  addnqprlemru  7620  addnqprlemfl  7621  addnqprlemfu  7622  appdivnq  7625  prmuloclemcalc  7627  prmuloc  7628  mulnqprlemrl  7635  mulnqprlemru  7636  mulnqprlemfl  7637  mulnqprlemfu  7638  1idprl  7652  1idpru  7653  ltnqpri  7656  ltsopr  7658  ltexprlemopl  7663  ltexprlemopu  7665  ltexprlemdisj  7668  ltexprlemloc  7669  ltexprlemfl  7671  ltexprlemru  7674  recexprlemell  7684  recexprlemelu  7685  recexprlemlol  7688  recexprlemupu  7690  recexprlemdisj  7692  recexprlemloc  7693  recexprlempr  7694  recexprlem1ssl  7695  recexprlem1ssu  7696  recexprlemss1l  7697  recexprlemss1u  7698  cauappcvgprlemm  7707  cauappcvgprlemopl  7708  cauappcvgprlemlol  7709  cauappcvgprlemupu  7711  cauappcvgprlemladdfu  7716  cauappcvgprlemladdfl  7717  caucvgprlemk  7727  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemupu  7734  caucvgprlemloc  7737  caucvgprlemladdfu  7739  caucvgprprlemloccalc  7746  caucvgprprlemml  7756  caucvgprprlemopl  7759  caucvgprprlemlol  7760  caucvgprprlemupu  7762  caucvgprprlemloc  7765  suplocexprlemrl  7779  suplocexprlemru  7781