Theorem reldom 8942

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

Syntax hints:  ∃wex 1782  Rel wrel 5681  –1-1→wf1 6538   ≼ cdom 8934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683  df-dom 8938

This theorem is referenced by:  relsdom  8943  brdomg  8949  brdomgOLD  8950  brdomi  8951  brdomiOLD  8952  ctex  8956  domssl  8991  domssr  8992  domtr  9000  undom  9056  undomOLD  9057  xpdom2  9064  xpdom1g  9066  domunsncan  9069  sbth  9090  sbthcl  9092  dom0OLD  9100  fodomr  9125  pwdom  9126  domssex  9135  mapdom1  9139  mapdom2  9145  domtrfil  9192  sbthfi  9199  0sdom1dom  9235  1sdom2dom  9244  fineqv  9260  infsdomnn  9302  infsdomnnOLD  9303  infn0ALT  9305  elharval  9553  harword  9555  domwdom  9566  unxpwdom  9581  infdifsn  9649  infdiffi  9650  ac10ct  10026  djudom2  10175  djuinf  10180  infdju1  10181  pwdjuidm  10183  djulepw  10184  infdjuabs  10198  infunabs  10199  pwdjudom  10208  infpss  10209  infmap2  10210  fictb  10237  infpssALT  10305  fin34  10382  ttukeylem1  10501  fodomb  10518  wdomac  10519  brdom3  10520  iundom2g  10532  iundom  10534  infxpidm  10554  gchdomtri  10621  pwfseq  10656  pwxpndom2  10657  pwxpndom  10658  pwdjundom  10659  gchdjuidm  10660  gchpwdom  10662  gchaclem  10670  reexALT  12965  hashdomi  14337  1stcrestlem  22948  hauspwdom  22997  ufilen  23426  ovoliunnul  25016  ovoliunnfl  36519  voliunnfl  36521  volsupnfl  36522  nnfoctb  43720  rn1st  43965  meadjiun  45169  caragenunicl  45227