Theorem reldom 8973

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

Syntax hints:  ∃wex 1778  Rel wrel 5670  –1-1→wf1 6538   ≼ cdom 8965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-ss 3948  df-opab 5186  df-xp 5671  df-rel 5672  df-dom 8969

This theorem is referenced by:  relsdom  8974  brdomg  8979  brdomgOLD  8980  brdomi  8981  brdomiOLD  8982  ctex  8986  domssl  9020  domssr  9021  domtr  9029  undom  9081  undomOLD  9082  xpdom2  9089  xpdom1g  9091  domunsncan  9094  sbth  9115  sbthcl  9117  dom0OLD  9125  fodomr  9150  pwdom  9151  domssex  9160  mapdom1  9164  mapdom2  9170  domtrfil  9214  sbthfi  9221  0sdom1dom  9256  1sdom2dom  9265  fineqv  9281  infsdomnn  9320  infsdomnnOLD  9321  infn0ALT  9323  elharval  9583  harword  9585  domwdom  9596  unxpwdom  9611  infdifsn  9679  infdiffi  9680  ac10ct  10056  djudom2  10206  djuinf  10211  infdju1  10212  pwdjuidm  10214  djulepw  10215  infdjuabs  10227  infunabs  10228  pwdjudom  10237  infpss  10238  infmap2  10239  fictb  10266  infpssALT  10335  fin34  10412  ttukeylem1  10531  fodomb  10548  wdomac  10549  brdom3  10550  iundom2g  10562  iundom  10564  infxpidm  10584  gchdomtri  10651  pwfseq  10686  pwxpndom2  10687  pwxpndom  10688  pwdjundom  10689  gchdjuidm  10690  gchpwdom  10692  gchaclem  10700  reexALT  13008  hashdomi  14401  1stcrestlem  23406  hauspwdom  23455  ufilen  23884  ovoliunnul  25478  ovoliunnfl  37628  voliunnfl  37630  volsupnfl  37631  nnfoctb  45010  rn1st  45237  meadjiun  46438  caragenunicl  46496