Theorem reldom 8889

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

Syntax hints:  ∃wex 1780  Rel wrel 5629  –1-1→wf1 6489   ≼ cdom 8881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-ss 3918  df-opab 5161  df-xp 5630  df-rel 5631  df-dom 8885

This theorem is referenced by:  relsdom  8890  brdomg  8895  brdomi  8896  ctex  8900  domssl  8935  domssr  8936  domtr  8944  undom  8993  xpdom2  9000  xpdom1g  9002  domunsncan  9005  sbth  9025  sbthcl  9027  fodomr  9056  pwdom  9057  domssex  9066  mapdom1  9070  mapdom2  9076  domtrfil  9116  sbthfi  9123  0sdom1dom  9146  1sdom2dom  9154  fineqv  9167  infsdomnn  9201  infn0ALT  9203  elharval  9466  harword  9468  domwdom  9479  unxpwdom  9494  infdifsn  9566  infdiffi  9567  ac10ct  9944  djudom2  10094  djuinf  10099  infdju1  10100  pwdjuidm  10102  djulepw  10103  infdjuabs  10115  infunabs  10116  pwdjudom  10125  infpss  10126  infmap2  10127  fictb  10154  infpssALT  10223  fin34  10300  ttukeylem1  10419  fodomb  10436  wdomac  10437  brdom3  10438  iundom2g  10450  iundom  10452  infxpidm  10472  gchdomtri  10540  pwfseq  10575  pwxpndom2  10576  pwxpndom  10577  pwdjundom  10578  gchdjuidm  10579  gchpwdom  10581  gchaclem  10589  reexALT  12897  hashdomi  14303  1stcrestlem  23396  hauspwdom  23445  ufilen  23874  ovoliunnul  25464  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  nnfoctb  45289  rn1st  45513  meadjiun  46706  caragenunicl  46764