ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ltrelnq GIF version

Theorem ltrelnq 6868
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.
StepHypRef Expression
1 df-ltnqqs 6856 . 2 <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2 opabssxp 4480 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q)
31, 2eqsstri 3045 1 <Q ⊆ (Q × Q)
Colors of variables: wff set class
Syntax hints:  wa 102   = wceq 1287  wex 1424  wcel 1436  wss 2988  cop 3434   class class class wbr 3820  {copab 3873   × cxp 4409  (class class class)co 5613  [cec 6242   ·N cmi 6777   <N clti 6778   ~Q ceq 6782  Qcnq 6783   <Q cltq 6788
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-in 2994  df-ss 3001  df-opab 3875  df-xp 4417  df-ltnqqs 6856
This theorem is referenced by:  ltanqi  6905  ltmnqi  6906  lt2addnq  6907  lt2mulnq  6908  ltexnqi  6912  ltbtwnnqq  6918  ltbtwnnq  6919  prarloclemarch2  6922  ltrnqi  6924  prcdnql  6987  prcunqu  6988  prnmaxl  6991  prnminu  6992  prloc  6994  prarloclemcalc  7005  genplt2i  7013  genpcdl  7022  genpcuu  7023  genpdisj  7026  addnqprllem  7030  addnqprulem  7031  addlocprlemlt  7034  addlocprlemeq  7036  addlocprlemgt  7037  addlocprlem  7038  nqprdisj  7047  nqprloc  7048  nqprxx  7049  ltnqex  7052  gtnqex  7053  addnqprlemrl  7060  addnqprlemru  7061  addnqprlemfl  7062  addnqprlemfu  7063  appdivnq  7066  prmuloclemcalc  7068  prmuloc  7069  mulnqprlemrl  7076  mulnqprlemru  7077  mulnqprlemfl  7078  mulnqprlemfu  7079  1idprl  7093  1idpru  7094  ltnqpri  7097  ltsopr  7099  ltexprlemopl  7104  ltexprlemopu  7106  ltexprlemdisj  7109  ltexprlemloc  7110  ltexprlemfl  7112  ltexprlemru  7115  recexprlemell  7125  recexprlemelu  7126  recexprlemlol  7129  recexprlemupu  7131  recexprlemdisj  7133  recexprlemloc  7134  recexprlempr  7135  recexprlem1ssl  7136  recexprlem1ssu  7137  recexprlemss1l  7138  recexprlemss1u  7139  cauappcvgprlemm  7148  cauappcvgprlemopl  7149  cauappcvgprlemlol  7150  cauappcvgprlemupu  7152  cauappcvgprlemladdfu  7157  cauappcvgprlemladdfl  7158  caucvgprlemk  7168  caucvgprlemnkj  7169  caucvgprlemnbj  7170  caucvgprlemm  7171  caucvgprlemopl  7172  caucvgprlemlol  7173  caucvgprlemupu  7175  caucvgprlemloc  7178  caucvgprlemladdfu  7180  caucvgprprlemloccalc  7187  caucvgprprlemml  7197  caucvgprprlemopl  7200  caucvgprprlemlol  7201  caucvgprprlemupu  7203  caucvgprprlemloc  7206
  Copyright terms: Public domain W3C validator