Theorem reldom 8962

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

This proof depends on syntax axioms:  ∃wex 1812  Rel wrel 5664  –1-1→wf1 6534   ≼ cdom 8954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-opab 5172  df-xp 5665  df-rel 5666  df-dom 8958

This theorem is used by:  relsdom  8963  brdomg  8968  brdomi  8969  ctex  8973  domssl  9008  domssr  9009  domtr  9017  undom  9067  xpdom2  9074  xpdom1g  9076  domunsncan  9079  sbth  9099  sbthcl  9101  fodomr  9130  pwdom  9131  domssex  9140  mapdom1  9144  mapdom2  9150  domtrfil  9190  sbthfi  9197  0sdom1dom  9220  1sdom2dom  9228  fineqv  9241  infsdomnn  9275  infn0ALT  9277  elharval  9537  harword  9539  domwdom  9550  unxpwdom  9565  infdifsn  9640  infdiffi  9641  ac10ct  10041  djudom2  10190  djuinf  10195  infdju1  10196  pwdjuidm  10198  djulepw  10199  infdjuabs  10211  infunabs  10212  pwdjudom  10221  infpss  10222  infmap2  10223  fictb  10250  infpssALT  10319  fin34  10396  ttukeylem1  10515  fodomb  10533  wdomac  10534  brdom3  10535  iundom2g  10552  iundom  10554  infxpidm  10574  gchdomtri  10642  pwfseq  10677  pwxpndom2  10678  pwxpndom  10679  pwdjundom  10680  gchdjuidm  10681  gchpwdom  10683  gchaclem  10691  reexALT  13038  hashdomi  14448  1stcrestlem  23683  hauspwdom  23733  ufilen  24162  ovoliunnul  25741  karddom  35695  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  nnfoctb  45890  rn1st  46110  meadjiun  47302  caragenunicl  47360