Theorem ltrelnq 7478

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 7466	. 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 4749	. 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 3225	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1373   E.wex 1515   e. wcel 2176   C_ wss 3166   <.cop 3636   class class class wbr 4044   {copab 4104   X. cxp 4673  (class class class)co 5944   [cec 6618   .N cmi 7387   <N clti 7388   ~Q ceq 7392   Q.cnq 7393   <Q cltq 7398

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-in 3172  df-ss 3179  df-opab 4106  df-xp 4681  df-ltnqqs 7466

This theorem is referenced by:  ltanqi  7515  ltmnqi  7516  lt2addnq  7517  lt2mulnq  7518  ltexnqi  7522  ltbtwnnqq  7528  ltbtwnnq  7529  prarloclemarch2  7532  ltrnqi  7534  prcdnql  7597  prcunqu  7598  prnmaxl  7601  prnminu  7602  prloc  7604  prarloclemcalc  7615  genplt2i  7623  genpcdl  7632  genpcuu  7633  genpdisj  7636  addnqprllem  7640  addnqprulem  7641  addlocprlemlt  7644  addlocprlemeq  7646  addlocprlemgt  7647  addlocprlem  7648  nqprdisj  7657  nqprloc  7658  nqprxx  7659  ltnqex  7662  gtnqex  7663  addnqprlemrl  7670  addnqprlemru  7671  addnqprlemfl  7672  addnqprlemfu  7673  appdivnq  7676  prmuloclemcalc  7678  prmuloc  7679  mulnqprlemrl  7686  mulnqprlemru  7687  mulnqprlemfl  7688  mulnqprlemfu  7689  1idprl  7703  1idpru  7704  ltnqpri  7707  ltsopr  7709  ltexprlemopl  7714  ltexprlemopu  7716  ltexprlemdisj  7719  ltexprlemloc  7720  ltexprlemfl  7722  ltexprlemru  7725  recexprlemell  7735  recexprlemelu  7736  recexprlemlol  7739  recexprlemupu  7741  recexprlemdisj  7743  recexprlemloc  7744  recexprlempr  7745  recexprlem1ssl  7746  recexprlem1ssu  7747  recexprlemss1l  7748  recexprlemss1u  7749  cauappcvgprlemm  7758  cauappcvgprlemopl  7759  cauappcvgprlemlol  7760  cauappcvgprlemupu  7762  cauappcvgprlemladdfu  7767  cauappcvgprlemladdfl  7768  caucvgprlemk  7778  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemupu  7785  caucvgprlemloc  7788  caucvgprlemladdfu  7790  caucvgprprlemloccalc  7797  caucvgprprlemml  7807  caucvgprprlemopl  7810  caucvgprprlemlol  7811  caucvgprprlemupu  7813  caucvgprprlemloc  7816  suplocexprlemrl  7830  suplocexprlemru  7832