Theorem reldom 9009

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

Syntax hints:  ∃wex 1777  Rel wrel 5705  –1-1→wf1 6570   ≼ cdom 9001

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707  df-dom 9005

This theorem is referenced by:  relsdom  9010  brdomg  9016  brdomgOLD  9017  brdomi  9018  brdomiOLD  9019  ctex  9023  domssl  9058  domssr  9059  domtr  9067  undom  9125  undomOLD  9126  xpdom2  9133  xpdom1g  9135  domunsncan  9138  sbth  9159  sbthcl  9161  dom0OLD  9169  fodomr  9194  pwdom  9195  domssex  9204  mapdom1  9208  mapdom2  9214  domtrfil  9258  sbthfi  9265  0sdom1dom  9301  1sdom2dom  9310  fineqv  9326  infsdomnn  9366  infsdomnnOLD  9367  infn0ALT  9369  elharval  9630  harword  9632  domwdom  9643  unxpwdom  9658  infdifsn  9726  infdiffi  9727  ac10ct  10103  djudom2  10253  djuinf  10258  infdju1  10259  pwdjuidm  10261  djulepw  10262  infdjuabs  10274  infunabs  10275  pwdjudom  10284  infpss  10285  infmap2  10286  fictb  10313  infpssALT  10382  fin34  10459  ttukeylem1  10578  fodomb  10595  wdomac  10596  brdom3  10597  iundom2g  10609  iundom  10611  infxpidm  10631  gchdomtri  10698  pwfseq  10733  pwxpndom2  10734  pwxpndom  10735  pwdjundom  10736  gchdjuidm  10737  gchpwdom  10739  gchaclem  10747  reexALT  13049  hashdomi  14429  1stcrestlem  23481  hauspwdom  23530  ufilen  23959  ovoliunnul  25561  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  nnfoctb  44949  rn1st  45183  meadjiun  46387  caragenunicl  46445