Theorem reldom 8885

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

Syntax hints:  ∃wex 1779  Rel wrel 5628  –1-1→wf1 6483   ≼ cdom 8877

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-opab 5158  df-xp 5629  df-rel 5630  df-dom 8881

This theorem is referenced by:  relsdom  8886  brdomg  8891  brdomi  8892  ctex  8896  domssl  8930  domssr  8931  domtr  8939  undom  8989  xpdom2  8996  xpdom1g  8998  domunsncan  9001  sbth  9021  sbthcl  9023  fodomr  9052  pwdom  9053  domssex  9062  mapdom1  9066  mapdom2  9072  domtrfil  9116  sbthfi  9123  0sdom1dom  9145  1sdom2dom  9153  fineqv  9168  infsdomnn  9207  infsdomnnOLD  9208  infn0ALT  9210  elharval  9472  harword  9474  domwdom  9485  unxpwdom  9500  infdifsn  9572  infdiffi  9573  ac10ct  9947  djudom2  10097  djuinf  10102  infdju1  10103  pwdjuidm  10105  djulepw  10106  infdjuabs  10118  infunabs  10119  pwdjudom  10128  infpss  10129  infmap2  10130  fictb  10157  infpssALT  10226  fin34  10303  ttukeylem1  10422  fodomb  10439  wdomac  10440  brdom3  10441  iundom2g  10453  iundom  10455  infxpidm  10475  gchdomtri  10542  pwfseq  10577  pwxpndom2  10578  pwxpndom  10579  pwdjundom  10580  gchdjuidm  10581  gchpwdom  10583  gchaclem  10591  reexALT  12903  hashdomi  14305  1stcrestlem  23355  hauspwdom  23404  ufilen  23833  ovoliunnul  25424  ovoliunnfl  37641  voliunnfl  37643  volsupnfl  37644  nnfoctb  45026  rn1st  45251  meadjiun  46448  caragenunicl  46506