Theorem reldom 8945

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

Syntax hints:  ∃wex 1782  Rel wrel 5682  –1-1→wf1 6541   ≼ cdom 8937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966  df-opab 5212  df-xp 5683  df-rel 5684  df-dom 8941

This theorem is referenced by:  relsdom  8946  brdomg  8952  brdomgOLD  8953  brdomi  8954  brdomiOLD  8955  ctex  8959  domssl  8994  domssr  8995  domtr  9003  undom  9059  undomOLD  9060  xpdom2  9067  xpdom1g  9069  domunsncan  9072  sbth  9093  sbthcl  9095  dom0OLD  9103  fodomr  9128  pwdom  9129  domssex  9138  mapdom1  9142  mapdom2  9148  domtrfil  9195  sbthfi  9202  0sdom1dom  9238  1sdom2dom  9247  fineqv  9263  infsdomnn  9305  infsdomnnOLD  9306  infn0ALT  9308  elharval  9556  harword  9558  domwdom  9569  unxpwdom  9584  infdifsn  9652  infdiffi  9653  ac10ct  10029  djudom2  10178  djuinf  10183  infdju1  10184  pwdjuidm  10186  djulepw  10187  infdjuabs  10201  infunabs  10202  pwdjudom  10211  infpss  10212  infmap2  10213  fictb  10240  infpssALT  10308  fin34  10385  ttukeylem1  10504  fodomb  10521  wdomac  10522  brdom3  10523  iundom2g  10535  iundom  10537  infxpidm  10557  gchdomtri  10624  pwfseq  10659  pwxpndom2  10660  pwxpndom  10661  pwdjundom  10662  gchdjuidm  10663  gchpwdom  10665  gchaclem  10673  reexALT  12968  hashdomi  14340  1stcrestlem  22956  hauspwdom  23005  ufilen  23434  ovoliunnul  25024  ovoliunnfl  36578  voliunnfl  36580  volsupnfl  36581  nnfoctb  43782  rn1st  44026  meadjiun  45230  caragenunicl  45288