Theorem reldom 8899

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

Syntax hints:  ∃wex 1781  Rel wrel 5636  –1-1→wf1 6495   ≼ cdom 8891

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-opab 5148  df-xp 5637  df-rel 5638  df-dom 8895

This theorem is referenced by:  relsdom  8900  brdomg  8905  brdomi  8906  ctex  8910  domssl  8945  domssr  8946  domtr  8954  undom  9003  xpdom2  9010  xpdom1g  9012  domunsncan  9015  sbth  9035  sbthcl  9037  fodomr  9066  pwdom  9067  domssex  9076  mapdom1  9080  mapdom2  9086  domtrfil  9126  sbthfi  9133  0sdom1dom  9156  1sdom2dom  9164  fineqv  9177  infsdomnn  9211  infn0ALT  9213  elharval  9476  harword  9478  domwdom  9489  unxpwdom  9504  infdifsn  9578  infdiffi  9579  ac10ct  9956  djudom2  10106  djuinf  10111  infdju1  10112  pwdjuidm  10114  djulepw  10115  infdjuabs  10127  infunabs  10128  pwdjudom  10137  infpss  10138  infmap2  10139  fictb  10166  infpssALT  10235  fin34  10312  ttukeylem1  10431  fodomb  10448  wdomac  10449  brdom3  10450  iundom2g  10462  iundom  10464  infxpidm  10484  gchdomtri  10552  pwfseq  10587  pwxpndom2  10588  pwxpndom  10589  pwdjundom  10590  gchdjuidm  10591  gchpwdom  10593  gchaclem  10601  reexALT  12934  hashdomi  14342  1stcrestlem  23417  hauspwdom  23466  ufilen  23895  ovoliunnul  25474  ovoliunnfl  37983  voliunnfl  37985  volsupnfl  37986  nnfoctb  45479  rn1st  45702  meadjiun  46894  caragenunicl  46952