Theorem reldom 8896

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

Syntax hints:  ∃wex 1786  Rel wrel 5630  –1-1→wf1 6489   ≼ cdom 8888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-opab 5142  df-xp 5631  df-rel 5632  df-dom 8892

This theorem is referenced by:  relsdom  8897  brdomg  8902  brdomi  8903  ctex  8907  domssl  8942  domssr  8943  domtr  8951  undom  9000  xpdom2  9007  xpdom1g  9009  domunsncan  9012  sbth  9032  sbthcl  9034  fodomr  9063  pwdom  9064  domssex  9073  mapdom1  9077  mapdom2  9083  domtrfil  9123  sbthfi  9130  0sdom1dom  9153  1sdom2dom  9161  fineqv  9174  infsdomnn  9208  infn0ALT  9210  elharval  9473  harword  9475  domwdom  9486  unxpwdom  9501  infdifsn  9576  infdiffi  9577  ac10ct  9954  djudom2  10104  djuinf  10109  infdju1  10110  pwdjuidm  10112  djulepw  10113  infdjuabs  10125  infunabs  10126  pwdjudom  10135  infpss  10136  infmap2  10137  fictb  10164  infpssALT  10233  fin34  10310  ttukeylem1  10429  fodomb  10446  wdomac  10447  brdom3  10448  iundom2g  10460  iundom  10462  infxpidm  10482  gchdomtri  10550  pwfseq  10585  pwxpndom2  10586  pwxpndom  10587  pwdjundom  10588  gchdjuidm  10589  gchpwdom  10591  gchaclem  10599  reexALT  12932  hashdomi  14340  1stcrestlem  23442  hauspwdom  23491  ufilen  23920  ovoliunnul  25499  ovoliunnfl  38036  voliunnfl  38038  volsupnfl  38039  nnfoctb  45503  rn1st  45724  meadjiun  46916  caragenunicl  46974