Theorem ltrelnq 7435

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 7423	. 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 4738	. 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 3216	1 |- <Q C_ ( Q. X. Q. )

Syntax hints:   /\ wa 104   = wceq 1364   E.wex 1506   e. wcel 2167   C_ wss 3157   <.cop 3626   class class class wbr 4034   {copab 4094   X. cxp 4662  (class class class)co 5923   [cec 6592   .N cmi 7344   <N clti 7345   ~Q ceq 7349   Q.cnq 7350   <Q cltq 7355

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-in 3163  df-ss 3170  df-opab 4096  df-xp 4670  df-ltnqqs 7423

This theorem is referenced by:  ltanqi  7472  ltmnqi  7473  lt2addnq  7474  lt2mulnq  7475  ltexnqi  7479  ltbtwnnqq  7485  ltbtwnnq  7486  prarloclemarch2  7489  ltrnqi  7491  prcdnql  7554  prcunqu  7555  prnmaxl  7558  prnminu  7559  prloc  7561  prarloclemcalc  7572  genplt2i  7580  genpcdl  7589  genpcuu  7590  genpdisj  7593  addnqprllem  7597  addnqprulem  7598  addlocprlemlt  7601  addlocprlemeq  7603  addlocprlemgt  7604  addlocprlem  7605  nqprdisj  7614  nqprloc  7615  nqprxx  7616  ltnqex  7619  gtnqex  7620  addnqprlemrl  7627  addnqprlemru  7628  addnqprlemfl  7629  addnqprlemfu  7630  appdivnq  7633  prmuloclemcalc  7635  prmuloc  7636  mulnqprlemrl  7643  mulnqprlemru  7644  mulnqprlemfl  7645  mulnqprlemfu  7646  1idprl  7660  1idpru  7661  ltnqpri  7664  ltsopr  7666  ltexprlemopl  7671  ltexprlemopu  7673  ltexprlemdisj  7676  ltexprlemloc  7677  ltexprlemfl  7679  ltexprlemru  7682  recexprlemell  7692  recexprlemelu  7693  recexprlemlol  7696  recexprlemupu  7698  recexprlemdisj  7700  recexprlemloc  7701  recexprlempr  7702  recexprlem1ssl  7703  recexprlem1ssu  7704  recexprlemss1l  7705  recexprlemss1u  7706  cauappcvgprlemm  7715  cauappcvgprlemopl  7716  cauappcvgprlemlol  7717  cauappcvgprlemupu  7719  cauappcvgprlemladdfu  7724  cauappcvgprlemladdfl  7725  caucvgprlemk  7735  caucvgprlemnkj  7736  caucvgprlemnbj  7737  caucvgprlemm  7738  caucvgprlemopl  7739  caucvgprlemlol  7740  caucvgprlemupu  7742  caucvgprlemloc  7745  caucvgprlemladdfu  7747  caucvgprprlemloccalc  7754  caucvgprprlemml  7764  caucvgprprlemopl  7767  caucvgprprlemlol  7768  caucvgprprlemupu  7770  caucvgprprlemloc  7773  suplocexprlemrl  7787  suplocexprlemru  7789