Theorem reldom 8979

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

This proof depends on syntax axioms:  ∃wex 1811  Rel wrel 5655  –1-1→wf1 6535   ≼ cdom 8971

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656  df-rel 5657  df-dom 8975

This theorem is used by:  relsdom  8980  brdomg  8985  brdomi  8986  ctex  8990  domssl  9025  domssr  9026  domtr  9034  undom  9084  xpdom2  9091  xpdom1g  9093  domunsncan  9096  sbth  9116  sbthcl  9118  fodomr  9147  pwdom  9148  domssex  9157  mapdom1  9161  mapdom2  9167  domtrfil  9207  sbthfi  9214  0sdom1dom  9237  1sdom2dom  9245  fineqv  9258  infsdomnn  9293  infn0ALT  9295  elharval  9555  harword  9557  domwdom  9568  unxpwdom  9583  infdifsn  9658  infdiffi  9659  ac10ct  10113  djudom2  10262  djuinf  10267  infdju1  10268  pwdjuidm  10270  djulepw  10271  infdjuabs  10283  infunabs  10284  pwdjudom  10293  infpss  10294  infmap2  10295  fictb  10322  infpssALT  10391  fin34  10468  ttukeylem1  10587  fodomb  10605  wdomac  10606  brdom3  10607  iundom2g  10624  iundom  10626  infxpidm  10646  gchdomtri  10714  pwfseq  10749  pwxpndom2  10750  pwxpndom  10751  pwdjundom  10752  gchdjuidm  10753  gchpwdom  10755  gchaclem  10763  reexALT  13112  hashdomi  14524  1stcrestlem  23770  hauspwdom  23820  ufilen  24249  ovoliunnul  25828  weexenwe  35798  karddom  35871  ovoliunnfl  38623  voliunnfl  38625  volsupnfl  38626  nnfoctb  46107  rn1st  46327  meadjiun  47518  caragenunicl  47576