Theorem reldom 8892

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-opab 5149  df-xp 5630  df-rel 5631  df-dom 8888

This theorem is referenced by:  relsdom  8893  brdomg  8898  brdomi  8899  ctex  8903  domssl  8938  domssr  8939  domtr  8947  undom  8996  xpdom2  9003  xpdom1g  9005  domunsncan  9008  sbth  9028  sbthcl  9030  fodomr  9059  pwdom  9060  domssex  9069  mapdom1  9073  mapdom2  9079  domtrfil  9119  sbthfi  9126  0sdom1dom  9149  1sdom2dom  9157  fineqv  9170  infsdomnn  9204  infn0ALT  9206  elharval  9469  harword  9471  domwdom  9482  unxpwdom  9497  infdifsn  9569  infdiffi  9570  ac10ct  9947  djudom2  10097  djuinf  10102  infdju1  10103  pwdjuidm  10105  djulepw  10106  infdjuabs  10118  infunabs  10119  pwdjudom  10128  infpss  10129  infmap2  10130  fictb  10157  infpssALT  10226  fin34  10303  ttukeylem1  10422  fodomb  10439  wdomac  10440  brdom3  10441  iundom2g  10453  iundom  10455  infxpidm  10475  gchdomtri  10543  pwfseq  10578  pwxpndom2  10579  pwxpndom  10580  pwdjundom  10581  gchdjuidm  10582  gchpwdom  10584  gchaclem  10592  reexALT  12925  hashdomi  14333  1stcrestlem  23427  hauspwdom  23476  ufilen  23905  ovoliunnul  25484  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  nnfoctb  45497  rn1st  45720  meadjiun  46912  caragenunicl  46970