Theorem reldom 8965

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.

Step	Hyp	Ref	Expression
1		df-dom 8961	. 2 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
2	1	relopabiv 5799	1 ⊢ Rel ≼

Syntax hints:  ∃wex 1779  Rel wrel 5659  –1-1→wf1 6528   ≼ cdom 8957

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-opab 5182  df-xp 5660  df-rel 5661  df-dom 8961

This theorem is referenced by:  relsdom  8966  brdomg  8971  brdomgOLD  8972  brdomi  8973  brdomiOLD  8974  ctex  8978  domssl  9012  domssr  9013  domtr  9021  undom  9073  undomOLD  9074  xpdom2  9081  xpdom1g  9083  domunsncan  9086  sbth  9107  sbthcl  9109  dom0OLD  9117  fodomr  9142  pwdom  9143  domssex  9152  mapdom1  9156  mapdom2  9162  domtrfil  9206  sbthfi  9213  0sdom1dom  9246  1sdom2dom  9255  fineqv  9271  infsdomnn  9310  infsdomnnOLD  9311  infn0ALT  9313  elharval  9575  harword  9577  domwdom  9588  unxpwdom  9603  infdifsn  9671  infdiffi  9672  ac10ct  10048  djudom2  10198  djuinf  10203  infdju1  10204  pwdjuidm  10206  djulepw  10207  infdjuabs  10219  infunabs  10220  pwdjudom  10229  infpss  10230  infmap2  10231  fictb  10258  infpssALT  10327  fin34  10404  ttukeylem1  10523  fodomb  10540  wdomac  10541  brdom3  10542  iundom2g  10554  iundom  10556  infxpidm  10576  gchdomtri  10643  pwfseq  10678  pwxpndom2  10679  pwxpndom  10680  pwdjundom  10681  gchdjuidm  10682  gchpwdom  10684  gchaclem  10692  reexALT  13000  hashdomi  14398  1stcrestlem  23390  hauspwdom  23439  ufilen  23868  ovoliunnul  25460  ovoliunnfl  37686  voliunnfl  37688  volsupnfl  37689  nnfoctb  45072  rn1st  45297  meadjiun  46495  caragenunicl  46553