Theorem reldom 8927

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

Syntax hints:  ∃wex 1779  Rel wrel 5646  –1-1→wf1 6511   ≼ cdom 8919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-opab 5173  df-xp 5647  df-rel 5648  df-dom 8923

This theorem is referenced by:  relsdom  8928  brdomg  8933  brdomi  8934  ctex  8938  domssl  8972  domssr  8973  domtr  8981  undom  9033  undomOLD  9034  xpdom2  9041  xpdom1g  9043  domunsncan  9046  sbth  9067  sbthcl  9069  fodomr  9098  pwdom  9099  domssex  9108  mapdom1  9112  mapdom2  9118  domtrfil  9162  sbthfi  9169  0sdom1dom  9192  1sdom2dom  9201  fineqv  9217  infsdomnn  9256  infsdomnnOLD  9257  infn0ALT  9259  elharval  9521  harword  9523  domwdom  9534  unxpwdom  9549  infdifsn  9617  infdiffi  9618  ac10ct  9994  djudom2  10144  djuinf  10149  infdju1  10150  pwdjuidm  10152  djulepw  10153  infdjuabs  10165  infunabs  10166  pwdjudom  10175  infpss  10176  infmap2  10177  fictb  10204  infpssALT  10273  fin34  10350  ttukeylem1  10469  fodomb  10486  wdomac  10487  brdom3  10488  iundom2g  10500  iundom  10502  infxpidm  10522  gchdomtri  10589  pwfseq  10624  pwxpndom2  10625  pwxpndom  10626  pwdjundom  10627  gchdjuidm  10628  gchpwdom  10630  gchaclem  10638  reexALT  12950  hashdomi  14352  1stcrestlem  23346  hauspwdom  23395  ufilen  23824  ovoliunnul  25415  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  nnfoctb  45049  rn1st  45274  meadjiun  46471  caragenunicl  46529