Theorem reldom 8538

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

Syntax hints:  ∃wex 1781  Rel wrel 5532  –1-1→wf1 6336   ≼ cdom 8530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-v 3411  df-in 3867  df-ss 3877  df-opab 5098  df-xp 5533  df-rel 5534  df-dom 8534

This theorem is referenced by:  relsdom  8539  brdomg  8542  brdomi  8543  ctex  8547  domtr  8585  undom  8631  xpdom2  8638  xpdom1g  8640  domunsncan  8643  sbth  8664  sbthcl  8666  dom0  8672  fodomr  8695  pwdom  8696  domssex  8705  mapdom1  8709  mapdom2  8715  fineqv  8776  infsdomnn  8817  infn0  8818  elharval  9063  harword  9065  domwdom  9076  unxpwdom  9091  infdifsn  9158  infdiffi  9159  ac10ct  9499  djudom2  9648  djuinf  9653  infdju1  9654  pwdjuidm  9656  djulepw  9657  infdjuabs  9671  infunabs  9672  pwdjudom  9681  infpss  9682  infmap2  9683  fictb  9710  infpssALT  9778  fin34  9855  ttukeylem1  9974  fodomb  9991  wdomac  9992  brdom3  9993  iundom2g  10005  iundom  10007  infxpidm  10027  gchdomtri  10094  pwfseq  10129  pwxpndom2  10130  pwxpndom  10131  pwdjundom  10132  gchdjuidm  10133  gchpwdom  10135  gchaclem  10143  reexALT  12429  hashdomi  13796  1stcrestlem  22157  hauspwdom  22206  ufilen  22635  ovoliunnul  24212  ovoliunnfl  35405  voliunnfl  35407  volsupnfl  35408  nnfoctb  42082  meadjiun  43499  caragenunicl  43557