Theorem reldom 8982

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

This proof depends on syntax axioms:  ∃wex 1811  Rel wrel 5655  –1-1→wf1 6535   ≼ cdom 8974

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-opab 5167  df-xp 5656  df-rel 5657  df-dom 8978

This theorem is used by:  relsdom  8983  brdomg  8988  brdomi  8989  ctex  8993  domssl  9028  domssr  9029  domtr  9037  undom  9087  xpdom2  9094  xpdom1g  9096  domunsncan  9099  sbth  9119  sbthcl  9121  fodomr  9150  pwdom  9151  domssex  9160  mapdom1  9164  mapdom2  9170  domtrfil  9210  sbthfi  9217  0sdom1dom  9240  1sdom2dom  9248  fineqv  9261  infsdomnn  9296  infn0ALT  9298  elharval  9558  harword  9560  domwdom  9571  unxpwdom  9586  infdifsn  9661  infdiffi  9662  ac10ct  10116  djudom2  10265  djuinf  10270  infdju1  10271  pwdjuidm  10273  djulepw  10274  infdjuabs  10286  infunabs  10287  pwdjudom  10296  infpss  10297  infmap2  10298  fictb  10325  infpssALT  10394  fin34  10471  ttukeylem1  10590  fodomb  10608  wdomac  10609  brdom3  10610  iundom2g  10627  iundom  10629  infxpidm  10649  gchdomtri  10717  pwfseq  10752  pwxpndom2  10753  pwxpndom  10754  pwdjundom  10755  gchdjuidm  10756  gchpwdom  10758  gchaclem  10766  reexALT  13115  hashdomi  14527  1stcrestlem  23775  hauspwdom  23825  ufilen  24254  ovoliunnul  25833  weexenwe  35812  karddom  35885  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  nnfoctb  46158  rn1st  46378  meadjiun  47569  caragenunicl  47627