Theorem ltrelnq 7314

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 ⊆ (Q × Q)

Proof of Theorem ltrelnq

Dummy variables 𝑥 𝑦 𝑧 𝑤 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ltnqqs 7302	. 2 ⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2		opabssxp 4683	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q)
3	1, 2	eqsstri 3179	1 ⊢ <Q ⊆ (Q × Q)

Syntax hints:   ∧ wa 103   = wceq 1348  ∃wex 1485   ∈ wcel 2141   ⊆ wss 3121  ⟨cop 3584   class class class wbr 3987  {copab 4047   × cxp 4607  (class class class)co 5850  [cec 6507   ·_N cmi 7223   <_N clti 7224   ~_Q ceq 7228  Qcnq 7229   <_Q cltq 7234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-in 3127  df-ss 3134  df-opab 4049  df-xp 4615  df-ltnqqs 7302

This theorem is referenced by:  ltanqi  7351  ltmnqi  7352  lt2addnq  7353  lt2mulnq  7354  ltexnqi  7358  ltbtwnnqq  7364  ltbtwnnq  7365  prarloclemarch2  7368  ltrnqi  7370  prcdnql  7433  prcunqu  7434  prnmaxl  7437  prnminu  7438  prloc  7440  prarloclemcalc  7451  genplt2i  7459  genpcdl  7468  genpcuu  7469  genpdisj  7472  addnqprllem  7476  addnqprulem  7477  addlocprlemlt  7480  addlocprlemeq  7482  addlocprlemgt  7483  addlocprlem  7484  nqprdisj  7493  nqprloc  7494  nqprxx  7495  ltnqex  7498  gtnqex  7499  addnqprlemrl  7506  addnqprlemru  7507  addnqprlemfl  7508  addnqprlemfu  7509  appdivnq  7512  prmuloclemcalc  7514  prmuloc  7515  mulnqprlemrl  7522  mulnqprlemru  7523  mulnqprlemfl  7524  mulnqprlemfu  7525  1idprl  7539  1idpru  7540  ltnqpri  7543  ltsopr  7545  ltexprlemopl  7550  ltexprlemopu  7552  ltexprlemdisj  7555  ltexprlemloc  7556  ltexprlemfl  7558  ltexprlemru  7561  recexprlemell  7571  recexprlemelu  7572  recexprlemlol  7575  recexprlemupu  7577  recexprlemdisj  7579  recexprlemloc  7580  recexprlempr  7581  recexprlem1ssl  7582  recexprlem1ssu  7583  recexprlemss1l  7584  recexprlemss1u  7585  cauappcvgprlemm  7594  cauappcvgprlemopl  7595  cauappcvgprlemlol  7596  cauappcvgprlemupu  7598  cauappcvgprlemladdfu  7603  cauappcvgprlemladdfl  7604  caucvgprlemk  7614  caucvgprlemnkj  7615  caucvgprlemnbj  7616  caucvgprlemm  7617  caucvgprlemopl  7618  caucvgprlemlol  7619  caucvgprlemupu  7621  caucvgprlemloc  7624  caucvgprlemladdfu  7626  caucvgprprlemloccalc  7633  caucvgprprlemml  7643  caucvgprprlemopl  7646  caucvgprprlemlol  7647  caucvgprprlemupu  7649  caucvgprprlemloc  7652  suplocexprlemrl  7666  suplocexprlemru  7668