Theorem reldom 8901

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

Syntax hints:  ∃wex 1781  Rel wrel 5637  –1-1→wf1 6497   ≼ cdom 8893

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 3444  df-ss 3920  df-opab 5163  df-xp 5638  df-rel 5639  df-dom 8897

This theorem is referenced by:  relsdom  8902  brdomg  8907  brdomi  8908  ctex  8912  domssl  8947  domssr  8948  domtr  8956  undom  9005  xpdom2  9012  xpdom1g  9014  domunsncan  9017  sbth  9037  sbthcl  9039  fodomr  9068  pwdom  9069  domssex  9078  mapdom1  9082  mapdom2  9088  domtrfil  9128  sbthfi  9135  0sdom1dom  9158  1sdom2dom  9166  fineqv  9179  infsdomnn  9213  infn0ALT  9215  elharval  9478  harword  9480  domwdom  9491  unxpwdom  9506  infdifsn  9578  infdiffi  9579  ac10ct  9956  djudom2  10106  djuinf  10111  infdju1  10112  pwdjuidm  10114  djulepw  10115  infdjuabs  10127  infunabs  10128  pwdjudom  10137  infpss  10138  infmap2  10139  fictb  10166  infpssALT  10235  fin34  10312  ttukeylem1  10431  fodomb  10448  wdomac  10449  brdom3  10450  iundom2g  10462  iundom  10464  infxpidm  10484  gchdomtri  10552  pwfseq  10587  pwxpndom2  10588  pwxpndom  10589  pwdjundom  10590  gchdjuidm  10591  gchpwdom  10593  gchaclem  10601  reexALT  12909  hashdomi  14315  1stcrestlem  23408  hauspwdom  23457  ufilen  23886  ovoliunnul  25476  ovoliunnfl  37907  voliunnfl  37909  volsupnfl  37910  nnfoctb  45402  rn1st  45625  meadjiun  46818  caragenunicl  46876