Theorem ltrelnq 7739

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

This proof depends on syntax axioms:   ∧ wa 104   = wceq 1402  ∃wex 1545   ∈ wcel 2209   ⊆ wss 3220  ⟨cop 3712   class class class wbr 4131  {copab 4192   × cxp 4774  (class class class)co 6088  [cec 6809   ·_N cmi 7648   <_N clti 7649   ~_Q ceq 7653  Qcnq 7654   <_Q cltq 7659

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-in 3226  df-ss 3233  df-opab 4194  df-xp 4782  df-ltnqqs 7727

This theorem is used by:  ltanqi  7776  ltmnqi  7777  lt2addnq  7778  lt2mulnq  7779  ltexnqi  7783  ltbtwnnqq  7789  ltbtwnnq  7790  prarloclemarch2  7793  ltrnqi  7795  prcdnql  7858  prcunqu  7859  prnmaxl  7862  prnminu  7863  prloc  7865  prarloclemcalc  7876  genplt2i  7884  genpcdl  7893  genpcuu  7894  genpdisj  7897  addnqprllem  7901  addnqprulem  7902  addlocprlemlt  7905  addlocprlemeq  7907  addlocprlemgt  7908  addlocprlem  7909  nqprdisj  7918  nqprloc  7919  nqprxx  7920  ltnqex  7923  gtnqex  7924  addnqprlemrl  7931  addnqprlemru  7932  addnqprlemfl  7933  addnqprlemfu  7934  appdivnq  7937  prmuloclemcalc  7939  prmuloc  7940  mulnqprlemrl  7947  mulnqprlemru  7948  mulnqprlemfl  7949  mulnqprlemfu  7950  1idprl  7964  1idpru  7965  ltnqpri  7968  ltsopr  7970  ltexprlemopl  7975  ltexprlemopu  7977  ltexprlemdisj  7980  ltexprlemloc  7981  ltexprlemfl  7983  ltexprlemru  7986  recexprlemell  7996  recexprlemelu  7997  recexprlemlol  8000  recexprlemupu  8002  recexprlemdisj  8004  recexprlemloc  8005  recexprlempr  8006  recexprlem1ssl  8007  recexprlem1ssu  8008  recexprlemss1l  8009  recexprlemss1u  8010  cauappcvgprlemm  8019  cauappcvgprlemopl  8020  cauappcvgprlemlol  8021  cauappcvgprlemupu  8023  cauappcvgprlemladdfu  8028  cauappcvgprlemladdfl  8029  caucvgprlemk  8039  caucvgprlemnkj  8040  caucvgprlemnbj  8041  caucvgprlemm  8042  caucvgprlemopl  8043  caucvgprlemlol  8044  caucvgprlemupu  8046  caucvgprlemloc  8049  caucvgprlemladdfu  8051  caucvgprprlemloccalc  8058  caucvgprprlemml  8068  caucvgprprlemopl  8071  caucvgprprlemlol  8072  caucvgprprlemupu  8074  caucvgprprlemloc  8077  suplocexprlemrl  8091  suplocexprlemru  8093