Theorem reldom 8924

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

Syntax hints:  ∃wex 1779  Rel wrel 5643  –1-1→wf1 6508   ≼ cdom 8916

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-opab 5170  df-xp 5644  df-rel 5645  df-dom 8920

This theorem is referenced by:  relsdom  8925  brdomg  8930  brdomi  8931  ctex  8935  domssl  8969  domssr  8970  domtr  8978  undom  9029  xpdom2  9036  xpdom1g  9038  domunsncan  9041  sbth  9061  sbthcl  9063  fodomr  9092  pwdom  9093  domssex  9102  mapdom1  9106  mapdom2  9112  domtrfil  9156  sbthfi  9163  0sdom1dom  9185  1sdom2dom  9194  fineqv  9210  infsdomnn  9249  infsdomnnOLD  9250  infn0ALT  9252  elharval  9514  harword  9516  domwdom  9527  unxpwdom  9542  infdifsn  9610  infdiffi  9611  ac10ct  9987  djudom2  10137  djuinf  10142  infdju1  10143  pwdjuidm  10145  djulepw  10146  infdjuabs  10158  infunabs  10159  pwdjudom  10168  infpss  10169  infmap2  10170  fictb  10197  infpssALT  10266  fin34  10343  ttukeylem1  10462  fodomb  10479  wdomac  10480  brdom3  10481  iundom2g  10493  iundom  10495  infxpidm  10515  gchdomtri  10582  pwfseq  10617  pwxpndom2  10618  pwxpndom  10619  pwdjundom  10620  gchdjuidm  10621  gchpwdom  10623  gchaclem  10631  reexALT  12943  hashdomi  14345  1stcrestlem  23339  hauspwdom  23388  ufilen  23817  ovoliunnul  25408  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  nnfoctb  45042  rn1st  45267  meadjiun  46464  caragenunicl  46522