Theorem reldom 8893

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

Syntax hints:  ∃wex 1781  Rel wrel 5630  –1-1→wf1 6490   ≼ cdom 8885

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 3443  df-ss 3919  df-opab 5162  df-xp 5631  df-rel 5632  df-dom 8889

This theorem is referenced by:  relsdom  8894  brdomg  8899  brdomi  8900  ctex  8904  domssl  8939  domssr  8940  domtr  8948  undom  8997  xpdom2  9004  xpdom1g  9006  domunsncan  9009  sbth  9029  sbthcl  9031  fodomr  9060  pwdom  9061  domssex  9070  mapdom1  9074  mapdom2  9080  domtrfil  9120  sbthfi  9127  0sdom1dom  9150  1sdom2dom  9158  fineqv  9171  infsdomnn  9205  infn0ALT  9207  elharval  9470  harword  9472  domwdom  9483  unxpwdom  9498  infdifsn  9570  infdiffi  9571  ac10ct  9948  djudom2  10098  djuinf  10103  infdju1  10104  pwdjuidm  10106  djulepw  10107  infdjuabs  10119  infunabs  10120  pwdjudom  10129  infpss  10130  infmap2  10131  fictb  10158  infpssALT  10227  fin34  10304  ttukeylem1  10423  fodomb  10440  wdomac  10441  brdom3  10442  iundom2g  10454  iundom  10456  infxpidm  10476  gchdomtri  10544  pwfseq  10579  pwxpndom2  10580  pwxpndom  10581  pwdjundom  10582  gchdjuidm  10583  gchpwdom  10585  gchaclem  10593  reexALT  12901  hashdomi  14307  1stcrestlem  23400  hauspwdom  23449  ufilen  23878  ovoliunnul  25468  ovoliunnfl  37834  voliunnfl  37836  volsupnfl  37837  nnfoctb  45329  rn1st  45553  meadjiun  46746  caragenunicl  46804