Theorem reldom 8991

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

Syntax hints:  ∃wex 1779  Rel wrel 5690  –1-1→wf1 6558   ≼ cdom 8983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-opab 5206  df-xp 5691  df-rel 5692  df-dom 8987

This theorem is referenced by:  relsdom  8992  brdomg  8997  brdomgOLD  8998  brdomi  8999  brdomiOLD  9000  ctex  9004  domssl  9038  domssr  9039  domtr  9047  undom  9099  undomOLD  9100  xpdom2  9107  xpdom1g  9109  domunsncan  9112  sbth  9133  sbthcl  9135  dom0OLD  9143  fodomr  9168  pwdom  9169  domssex  9178  mapdom1  9182  mapdom2  9188  domtrfil  9232  sbthfi  9239  0sdom1dom  9274  1sdom2dom  9283  fineqv  9299  infsdomnn  9338  infsdomnnOLD  9339  infn0ALT  9341  elharval  9601  harword  9603  domwdom  9614  unxpwdom  9629  infdifsn  9697  infdiffi  9698  ac10ct  10074  djudom2  10224  djuinf  10229  infdju1  10230  pwdjuidm  10232  djulepw  10233  infdjuabs  10245  infunabs  10246  pwdjudom  10255  infpss  10256  infmap2  10257  fictb  10284  infpssALT  10353  fin34  10430  ttukeylem1  10549  fodomb  10566  wdomac  10567  brdom3  10568  iundom2g  10580  iundom  10582  infxpidm  10602  gchdomtri  10669  pwfseq  10704  pwxpndom2  10705  pwxpndom  10706  pwdjundom  10707  gchdjuidm  10708  gchpwdom  10710  gchaclem  10718  reexALT  13026  hashdomi  14419  1stcrestlem  23460  hauspwdom  23509  ufilen  23938  ovoliunnul  25542  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  nnfoctb  45053  rn1st  45280  meadjiun  46481  caragenunicl  46539