Theorem reldom 8929

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

Syntax hints:  ∃wex 1798  Rel wrel 5650  –1-1→wf1 6514   ≼ cdom 8921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-opab 5162  df-xp 5651  df-rel 5652  df-dom 8925

This theorem is referenced by:  relsdom  8930  brdomg  8935  brdomi  8936  ctex  8940  domssl  8975  domssr  8976  domtr  8984  undom  9033  xpdom2  9040  xpdom1g  9042  domunsncan  9045  sbth  9065  sbthcl  9067  fodomr  9096  pwdom  9097  domssex  9106  mapdom1  9110  mapdom2  9116  domtrfil  9156  sbthfi  9163  0sdom1dom  9186  1sdom2dom  9194  fineqv  9207  infsdomnn  9241  infn0ALT  9243  elharval  9506  harword  9508  domwdom  9519  unxpwdom  9534  infdifsn  9609  infdiffi  9610  ac10ct  9987  djudom2  10137  djuinf  10142  infdju1  10143  pwdjuidm  10145  djulepw  10146  infdjuabs  10158  infunabs  10159  pwdjudom  10168  infpss  10169  infmap2  10170  fictb  10197  infpssALT  10267  fin34  10344  ttukeylem1  10463  fodomb  10480  wdomac  10481  brdom3  10482  iundom2g  10494  iundom  10496  infxpidm  10516  gchdomtri  10584  pwfseq  10619  pwxpndom2  10620  pwxpndom  10621  pwdjundom  10622  gchdjuidm  10623  gchpwdom  10625  gchaclem  10633  reexALT  12982  hashdomi  14390  1stcrestlem  23492  hauspwdom  23541  ufilen  23970  ovoliunnul  25549  ovoliunnfl  38125  voliunnfl  38127  volsupnfl  38128  nnfoctb  45592  rn1st  45812  meadjiun  47004  caragenunicl  47062