Theorem reldom 8951

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

Syntax hints:  ∃wex 1780  Rel wrel 5681  –1-1→wf1 6540   ≼ cdom 8943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-opab 5211  df-xp 5682  df-rel 5683  df-dom 8947

This theorem is referenced by:  relsdom  8952  brdomg  8958  brdomgOLD  8959  brdomi  8960  brdomiOLD  8961  ctex  8965  domssl  9000  domssr  9001  domtr  9009  undom  9065  undomOLD  9066  xpdom2  9073  xpdom1g  9075  domunsncan  9078  sbth  9099  sbthcl  9101  dom0OLD  9109  fodomr  9134  pwdom  9135  domssex  9144  mapdom1  9148  mapdom2  9154  domtrfil  9201  sbthfi  9208  0sdom1dom  9244  1sdom2dom  9253  fineqv  9269  infsdomnn  9311  infsdomnnOLD  9312  infn0ALT  9314  elharval  9562  harword  9564  domwdom  9575  unxpwdom  9590  infdifsn  9658  infdiffi  9659  ac10ct  10035  djudom2  10184  djuinf  10189  infdju1  10190  pwdjuidm  10192  djulepw  10193  infdjuabs  10207  infunabs  10208  pwdjudom  10217  infpss  10218  infmap2  10219  fictb  10246  infpssALT  10314  fin34  10391  ttukeylem1  10510  fodomb  10527  wdomac  10528  brdom3  10529  iundom2g  10541  iundom  10543  infxpidm  10563  gchdomtri  10630  pwfseq  10665  pwxpndom2  10666  pwxpndom  10667  pwdjundom  10668  gchdjuidm  10669  gchpwdom  10671  gchaclem  10679  reexALT  12975  hashdomi  14347  1stcrestlem  23276  hauspwdom  23325  ufilen  23754  ovoliunnul  25356  ovoliunnfl  36994  voliunnfl  36996  volsupnfl  36997  nnfoctb  44196  rn1st  44437  meadjiun  45641  caragenunicl  45699