Theorem reldom 8990

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 8986	. 2 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥–1-1→𝑦}
2	1	relopabiv 5833	1 ⊢ Rel ≼

Syntax hints:  ∃wex 1776  Rel wrel 5694  –1-1→wf1 6560   ≼ cdom 8982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-opab 5211  df-xp 5695  df-rel 5696  df-dom 8986

This theorem is referenced by:  relsdom  8991  brdomg  8996  brdomgOLD  8997  brdomi  8998  brdomiOLD  8999  ctex  9003  domssl  9037  domssr  9038  domtr  9046  undom  9098  undomOLD  9099  xpdom2  9106  xpdom1g  9108  domunsncan  9111  sbth  9132  sbthcl  9134  dom0OLD  9142  fodomr  9167  pwdom  9168  domssex  9177  mapdom1  9181  mapdom2  9187  domtrfil  9230  sbthfi  9237  0sdom1dom  9272  1sdom2dom  9281  fineqv  9297  infsdomnn  9336  infsdomnnOLD  9337  infn0ALT  9339  elharval  9599  harword  9601  domwdom  9612  unxpwdom  9627  infdifsn  9695  infdiffi  9696  ac10ct  10072  djudom2  10222  djuinf  10227  infdju1  10228  pwdjuidm  10230  djulepw  10231  infdjuabs  10243  infunabs  10244  pwdjudom  10253  infpss  10254  infmap2  10255  fictb  10282  infpssALT  10351  fin34  10428  ttukeylem1  10547  fodomb  10564  wdomac  10565  brdom3  10566  iundom2g  10578  iundom  10580  infxpidm  10600  gchdomtri  10667  pwfseq  10702  pwxpndom2  10703  pwxpndom  10704  pwdjundom  10705  gchdjuidm  10706  gchpwdom  10708  gchaclem  10716  reexALT  13024  hashdomi  14416  1stcrestlem  23476  hauspwdom  23525  ufilen  23954  ovoliunnul  25556  ovoliunnfl  37649  voliunnfl  37651  volsupnfl  37652  nnfoctb  44987  rn1st  45219  meadjiun  46422  caragenunicl  46480