Theorem ltrelnq 7680

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 7668	. 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 4824	. 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 3270	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1398   E.wex 1541   e. wcel 2203   C_ wss 3211   <.cop 3692   class class class wbr 4109   {copab 4170   X. cxp 4747  (class class class)co 6050   [cec 6765   .N cmi 7589   <N clti 7590   ~Q ceq 7594   Q.cnq 7595   <Q cltq 7600

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-in 3217  df-ss 3224  df-opab 4172  df-xp 4755  df-ltnqqs 7668

This theorem is referenced by:  ltanqi  7717  ltmnqi  7718  lt2addnq  7719  lt2mulnq  7720  ltexnqi  7724  ltbtwnnqq  7730  ltbtwnnq  7731  prarloclemarch2  7734  ltrnqi  7736  prcdnql  7799  prcunqu  7800  prnmaxl  7803  prnminu  7804  prloc  7806  prarloclemcalc  7817  genplt2i  7825  genpcdl  7834  genpcuu  7835  genpdisj  7838  addnqprllem  7842  addnqprulem  7843  addlocprlemlt  7846  addlocprlemeq  7848  addlocprlemgt  7849  addlocprlem  7850  nqprdisj  7859  nqprloc  7860  nqprxx  7861  ltnqex  7864  gtnqex  7865  addnqprlemrl  7872  addnqprlemru  7873  addnqprlemfl  7874  addnqprlemfu  7875  appdivnq  7878  prmuloclemcalc  7880  prmuloc  7881  mulnqprlemrl  7888  mulnqprlemru  7889  mulnqprlemfl  7890  mulnqprlemfu  7891  1idprl  7905  1idpru  7906  ltnqpri  7909  ltsopr  7911  ltexprlemopl  7916  ltexprlemopu  7918  ltexprlemdisj  7921  ltexprlemloc  7922  ltexprlemfl  7924  ltexprlemru  7927  recexprlemell  7937  recexprlemelu  7938  recexprlemlol  7941  recexprlemupu  7943  recexprlemdisj  7945  recexprlemloc  7946  recexprlempr  7947  recexprlem1ssl  7948  recexprlem1ssu  7949  recexprlemss1l  7950  recexprlemss1u  7951  cauappcvgprlemm  7960  cauappcvgprlemopl  7961  cauappcvgprlemlol  7962  cauappcvgprlemupu  7964  cauappcvgprlemladdfu  7969  cauappcvgprlemladdfl  7970  caucvgprlemk  7980  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemm  7983  caucvgprlemopl  7984  caucvgprlemlol  7985  caucvgprlemupu  7987  caucvgprlemloc  7990  caucvgprlemladdfu  7992  caucvgprprlemloccalc  7999  caucvgprprlemml  8009  caucvgprprlemopl  8012  caucvgprprlemlol  8013  caucvgprprlemupu  8015  caucvgprprlemloc  8018  suplocexprlemrl  8032  suplocexprlemru  8034