Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reldom Structured version   Visualization version   GIF version

Theorem reldom 8538
 Description: Dominance is a relation. (Contributed by NM, 28-Mar-1998.)
Assertion
Ref Expression
reldom Rel ≼

Proof of Theorem reldom
Dummy variables 𝑥 𝑦 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-dom 8534 . 2 ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥1-1𝑦}
21relopabiv 5666 1 Rel ≼
 Colors of variables: wff setvar class Syntax hints:  ∃wex 1781  Rel wrel 5532  –1-1→wf1 6336   ≼ cdom 8530 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729 This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-opab 5098  df-xp 5533  df-rel 5534  df-dom 8534 This theorem is referenced by:  relsdom  8539  brdomg  8542  brdomi  8543  ctex  8547  domtr  8585  undom  8631  xpdom2  8638  xpdom1g  8640  domunsncan  8643  sbth  8664  sbthcl  8666  dom0  8672  fodomr  8695  pwdom  8696  domssex  8705  mapdom1  8709  mapdom2  8715  fineqv  8776  infsdomnn  8817  infn0  8818  elharval  9063  harword  9065  domwdom  9076  unxpwdom  9091  infdifsn  9158  infdiffi  9159  ac10ct  9499  djudom2  9648  djuinf  9653  infdju1  9654  pwdjuidm  9656  djulepw  9657  infdjuabs  9671  infunabs  9672  pwdjudom  9681  infpss  9682  infmap2  9683  fictb  9710  infpssALT  9778  fin34  9855  ttukeylem1  9974  fodomb  9991  wdomac  9992  brdom3  9993  iundom2g  10005  iundom  10007  infxpidm  10027  gchdomtri  10094  pwfseq  10129  pwxpndom2  10130  pwxpndom  10131  pwdjundom  10132  gchdjuidm  10133  gchpwdom  10135  gchaclem  10143  reexALT  12429  hashdomi  13796  1stcrestlem  22157  hauspwdom  22206  ufilen  22635  ovoliunnul  24212  ovoliunnfl  35405  voliunnfl  35407  volsupnfl  35408  nnfoctb  42082  meadjiun  43499  caragenunicl  43557
 Copyright terms: Public domain W3C validator