Theorem ltrelnq 7451

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 7439	. 2 ⊢ <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2		opabssxp 4738	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ Q ∧ 𝑦 ∈ Q) ∧ ∃𝑧∃𝑤∃𝑣∃𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q ∧ 𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q)
3	1, 2	eqsstri 3216	1 ⊢ <Q ⊆ (Q × Q)

Syntax hints:   ∧ wa 104   = wceq 1364  ∃wex 1506   ∈ wcel 2167   ⊆ wss 3157  ⟨cop 3626   class class class wbr 4034  {copab 4094   × cxp 4662  (class class class)co 5925  [cec 6599   ·_N cmi 7360   <_N clti 7361   ~_Q ceq 7365  Qcnq 7366   <_Q cltq 7371

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 7439

This theorem is referenced by:  ltanqi  7488  ltmnqi  7489  lt2addnq  7490  lt2mulnq  7491  ltexnqi  7495  ltbtwnnqq  7501  ltbtwnnq  7502  prarloclemarch2  7505  ltrnqi  7507  prcdnql  7570  prcunqu  7571  prnmaxl  7574  prnminu  7575  prloc  7577  prarloclemcalc  7588  genplt2i  7596  genpcdl  7605  genpcuu  7606  genpdisj  7609  addnqprllem  7613  addnqprulem  7614  addlocprlemlt  7617  addlocprlemeq  7619  addlocprlemgt  7620  addlocprlem  7621  nqprdisj  7630  nqprloc  7631  nqprxx  7632  ltnqex  7635  gtnqex  7636  addnqprlemrl  7643  addnqprlemru  7644  addnqprlemfl  7645  addnqprlemfu  7646  appdivnq  7649  prmuloclemcalc  7651  prmuloc  7652  mulnqprlemrl  7659  mulnqprlemru  7660  mulnqprlemfl  7661  mulnqprlemfu  7662  1idprl  7676  1idpru  7677  ltnqpri  7680  ltsopr  7682  ltexprlemopl  7687  ltexprlemopu  7689  ltexprlemdisj  7692  ltexprlemloc  7693  ltexprlemfl  7695  ltexprlemru  7698  recexprlemell  7708  recexprlemelu  7709  recexprlemlol  7712  recexprlemupu  7714  recexprlemdisj  7716  recexprlemloc  7717  recexprlempr  7718  recexprlem1ssl  7719  recexprlem1ssu  7720  recexprlemss1l  7721  recexprlemss1u  7722  cauappcvgprlemm  7731  cauappcvgprlemopl  7732  cauappcvgprlemlol  7733  cauappcvgprlemupu  7735  cauappcvgprlemladdfu  7740  cauappcvgprlemladdfl  7741  caucvgprlemk  7751  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemupu  7758  caucvgprlemloc  7761  caucvgprlemladdfu  7763  caucvgprprlemloccalc  7770  caucvgprprlemml  7780  caucvgprprlemopl  7783  caucvgprprlemlol  7784  caucvgprprlemupu  7786  caucvgprprlemloc  7789  suplocexprlemrl  7803  suplocexprlemru  7805