Theorem ltrelnq 7508

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 7496	. 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 4762	. 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 3229	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1373   E.wex 1516   e. wcel 2177   C_ wss 3170   <.cop 3641   class class class wbr 4054   {copab 4115   X. cxp 4686  (class class class)co 5962   [cec 6636   .N cmi 7417   <N clti 7418   ~Q ceq 7422   Q.cnq 7423   <Q cltq 7428

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-in 3176  df-ss 3183  df-opab 4117  df-xp 4694  df-ltnqqs 7496

This theorem is referenced by:  ltanqi  7545  ltmnqi  7546  lt2addnq  7547  lt2mulnq  7548  ltexnqi  7552  ltbtwnnqq  7558  ltbtwnnq  7559  prarloclemarch2  7562  ltrnqi  7564  prcdnql  7627  prcunqu  7628  prnmaxl  7631  prnminu  7632  prloc  7634  prarloclemcalc  7645  genplt2i  7653  genpcdl  7662  genpcuu  7663  genpdisj  7666  addnqprllem  7670  addnqprulem  7671  addlocprlemlt  7674  addlocprlemeq  7676  addlocprlemgt  7677  addlocprlem  7678  nqprdisj  7687  nqprloc  7688  nqprxx  7689  ltnqex  7692  gtnqex  7693  addnqprlemrl  7700  addnqprlemru  7701  addnqprlemfl  7702  addnqprlemfu  7703  appdivnq  7706  prmuloclemcalc  7708  prmuloc  7709  mulnqprlemrl  7716  mulnqprlemru  7717  mulnqprlemfl  7718  mulnqprlemfu  7719  1idprl  7733  1idpru  7734  ltnqpri  7737  ltsopr  7739  ltexprlemopl  7744  ltexprlemopu  7746  ltexprlemdisj  7749  ltexprlemloc  7750  ltexprlemfl  7752  ltexprlemru  7755  recexprlemell  7765  recexprlemelu  7766  recexprlemlol  7769  recexprlemupu  7771  recexprlemdisj  7773  recexprlemloc  7774  recexprlempr  7775  recexprlem1ssl  7776  recexprlem1ssu  7777  recexprlemss1l  7778  recexprlemss1u  7779  cauappcvgprlemm  7788  cauappcvgprlemopl  7789  cauappcvgprlemlol  7790  cauappcvgprlemupu  7792  cauappcvgprlemladdfu  7797  cauappcvgprlemladdfl  7798  caucvgprlemk  7808  caucvgprlemnkj  7809  caucvgprlemnbj  7810  caucvgprlemm  7811  caucvgprlemopl  7812  caucvgprlemlol  7813  caucvgprlemupu  7815  caucvgprlemloc  7818  caucvgprlemladdfu  7820  caucvgprprlemloccalc  7827  caucvgprprlemml  7837  caucvgprprlemopl  7840  caucvgprprlemlol  7841  caucvgprprlemupu  7843  caucvgprprlemloc  7846  suplocexprlemrl  7860  suplocexprlemru  7862