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

Theorem ltrelnq 6491
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 6479 . 2 <Q = {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))}
2 opabssxp 4439 . 2 {⟨𝑥, 𝑦⟩ ∣ ((𝑥Q𝑦Q) ∧ ∃𝑧𝑤𝑣𝑢((𝑥 = [⟨𝑧, 𝑤⟩] ~Q𝑦 = [⟨𝑣, 𝑢⟩] ~Q ) ∧ (𝑧 ·N 𝑢) <N (𝑤 ·N 𝑣)))} ⊆ (Q × Q)
31, 2eqsstri 3000 1 <Q ⊆ (Q × Q)
Colors of variables: wff set class
Syntax hints:  wa 101   = wceq 1257  wex 1395  wcel 1407  wss 2942  cop 3403   class class class wbr 3789  {copab 3842   × cxp 4368  (class class class)co 5537  [cec 6132   ·N cmi 6400   <N clti 6401   ~Q ceq 6405  Qcnq 6406   <Q cltq 6411
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036
This theorem depends on definitions:  df-bi 114  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-in 2949  df-ss 2956  df-opab 3844  df-xp 4376  df-ltnqqs 6479
This theorem is referenced by:  ltanqi  6528  ltmnqi  6529  lt2addnq  6530  lt2mulnq  6531  ltexnqi  6535  ltbtwnnqq  6541  ltbtwnnq  6542  prarloclemarch2  6545  ltrnqi  6547  prcdnql  6610  prcunqu  6611  prnmaxl  6614  prnminu  6615  prloc  6617  prarloclemcalc  6628  genplt2i  6636  genpcdl  6645  genpcuu  6646  genpdisj  6649  addnqprllem  6653  addnqprulem  6654  addlocprlemlt  6657  addlocprlemeq  6659  addlocprlemgt  6660  addlocprlem  6661  nqprdisj  6670  nqprloc  6671  nqprxx  6672  ltnqex  6675  gtnqex  6676  addnqprlemrl  6683  addnqprlemru  6684  addnqprlemfl  6685  addnqprlemfu  6686  appdivnq  6689  prmuloclemcalc  6691  prmuloc  6692  mulnqprlemrl  6699  mulnqprlemru  6700  mulnqprlemfl  6701  mulnqprlemfu  6702  1idprl  6716  1idpru  6717  ltnqpri  6720  ltsopr  6722  ltexprlemopl  6727  ltexprlemopu  6729  ltexprlemdisj  6732  ltexprlemloc  6733  ltexprlemfl  6735  ltexprlemru  6738  recexprlemell  6748  recexprlemelu  6749  recexprlemlol  6752  recexprlemupu  6754  recexprlemdisj  6756  recexprlemloc  6757  recexprlempr  6758  recexprlem1ssl  6759  recexprlem1ssu  6760  recexprlemss1l  6761  recexprlemss1u  6762  cauappcvgprlemm  6771  cauappcvgprlemopl  6772  cauappcvgprlemlol  6773  cauappcvgprlemupu  6775  cauappcvgprlemladdfu  6780  cauappcvgprlemladdfl  6781  caucvgprlemk  6791  caucvgprlemnkj  6792  caucvgprlemnbj  6793  caucvgprlemm  6794  caucvgprlemopl  6795  caucvgprlemlol  6796  caucvgprlemupu  6798  caucvgprlemloc  6801  caucvgprlemladdfu  6803  caucvgprprlemloccalc  6810  caucvgprprlemml  6820  caucvgprprlemopl  6823  caucvgprprlemlol  6824  caucvgprprlemupu  6826  caucvgprprlemloc  6829
  Copyright terms: Public domain W3C validator