Theorem ltrelnq 7432

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

Syntax hints:   ∧ wa 104   = wceq 1364  ∃wex 1506   ∈ wcel 2167   ⊆ wss 3157  ⟨cop 3625   class class class wbr 4033  {copab 4093   × cxp 4661  (class class class)co 5922  [cec 6590   ·_N cmi 7341   <_N clti 7342   ~_Q ceq 7346  Qcnq 7347   <_Q cltq 7352

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 4095  df-xp 4669  df-ltnqqs 7420

This theorem is referenced by:  ltanqi  7469  ltmnqi  7470  lt2addnq  7471  lt2mulnq  7472  ltexnqi  7476  ltbtwnnqq  7482  ltbtwnnq  7483  prarloclemarch2  7486  ltrnqi  7488  prcdnql  7551  prcunqu  7552  prnmaxl  7555  prnminu  7556  prloc  7558  prarloclemcalc  7569  genplt2i  7577  genpcdl  7586  genpcuu  7587  genpdisj  7590  addnqprllem  7594  addnqprulem  7595  addlocprlemlt  7598  addlocprlemeq  7600  addlocprlemgt  7601  addlocprlem  7602  nqprdisj  7611  nqprloc  7612  nqprxx  7613  ltnqex  7616  gtnqex  7617  addnqprlemrl  7624  addnqprlemru  7625  addnqprlemfl  7626  addnqprlemfu  7627  appdivnq  7630  prmuloclemcalc  7632  prmuloc  7633  mulnqprlemrl  7640  mulnqprlemru  7641  mulnqprlemfl  7642  mulnqprlemfu  7643  1idprl  7657  1idpru  7658  ltnqpri  7661  ltsopr  7663  ltexprlemopl  7668  ltexprlemopu  7670  ltexprlemdisj  7673  ltexprlemloc  7674  ltexprlemfl  7676  ltexprlemru  7679  recexprlemell  7689  recexprlemelu  7690  recexprlemlol  7693  recexprlemupu  7695  recexprlemdisj  7697  recexprlemloc  7698  recexprlempr  7699  recexprlem1ssl  7700  recexprlem1ssu  7701  recexprlemss1l  7702  recexprlemss1u  7703  cauappcvgprlemm  7712  cauappcvgprlemopl  7713  cauappcvgprlemlol  7714  cauappcvgprlemupu  7716  cauappcvgprlemladdfu  7721  cauappcvgprlemladdfl  7722  caucvgprlemk  7732  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemm  7735  caucvgprlemopl  7736  caucvgprlemlol  7737  caucvgprlemupu  7739  caucvgprlemloc  7742  caucvgprlemladdfu  7744  caucvgprprlemloccalc  7751  caucvgprprlemml  7761  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemupu  7767  caucvgprprlemloc  7770  suplocexprlemrl  7784  suplocexprlemru  7786