Theorem ltrelnq 7363

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 7351	. 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 4700	. 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 3187	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1353   E.wex 1492   e. wcel 2148   C_ wss 3129   <.cop 3595   class class class wbr 4003   {copab 4063   X. cxp 4624  (class class class)co 5874   [cec 6532   .N cmi 7272   <N clti 7273   ~Q ceq 7277   Q.cnq 7278   <Q cltq 7283

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-in 3135  df-ss 3142  df-opab 4065  df-xp 4632  df-ltnqqs 7351

This theorem is referenced by:  ltanqi  7400  ltmnqi  7401  lt2addnq  7402  lt2mulnq  7403  ltexnqi  7407  ltbtwnnqq  7413  ltbtwnnq  7414  prarloclemarch2  7417  ltrnqi  7419  prcdnql  7482  prcunqu  7483  prnmaxl  7486  prnminu  7487  prloc  7489  prarloclemcalc  7500  genplt2i  7508  genpcdl  7517  genpcuu  7518  genpdisj  7521  addnqprllem  7525  addnqprulem  7526  addlocprlemlt  7529  addlocprlemeq  7531  addlocprlemgt  7532  addlocprlem  7533  nqprdisj  7542  nqprloc  7543  nqprxx  7544  ltnqex  7547  gtnqex  7548  addnqprlemrl  7555  addnqprlemru  7556  addnqprlemfl  7557  addnqprlemfu  7558  appdivnq  7561  prmuloclemcalc  7563  prmuloc  7564  mulnqprlemrl  7571  mulnqprlemru  7572  mulnqprlemfl  7573  mulnqprlemfu  7574  1idprl  7588  1idpru  7589  ltnqpri  7592  ltsopr  7594  ltexprlemopl  7599  ltexprlemopu  7601  ltexprlemdisj  7604  ltexprlemloc  7605  ltexprlemfl  7607  ltexprlemru  7610  recexprlemell  7620  recexprlemelu  7621  recexprlemlol  7624  recexprlemupu  7626  recexprlemdisj  7628  recexprlemloc  7629  recexprlempr  7630  recexprlem1ssl  7631  recexprlem1ssu  7632  recexprlemss1l  7633  recexprlemss1u  7634  cauappcvgprlemm  7643  cauappcvgprlemopl  7644  cauappcvgprlemlol  7645  cauappcvgprlemupu  7647  cauappcvgprlemladdfu  7652  cauappcvgprlemladdfl  7653  caucvgprlemk  7663  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemm  7666  caucvgprlemopl  7667  caucvgprlemlol  7668  caucvgprlemupu  7670  caucvgprlemloc  7673  caucvgprlemladdfu  7675  caucvgprprlemloccalc  7682  caucvgprprlemml  7692  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemupu  7698  caucvgprprlemloc  7701  suplocexprlemrl  7715  suplocexprlemru  7717