Theorem reldom 8958

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

This proof depends on syntax axioms:  ∃wex 1812  Rel wrel 5671  –1-1→wf1 6540   ≼ cdom 8950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-opab 5179  df-xp 5672  df-rel 5673  df-dom 8954

This theorem is used by:  relsdom  8959  brdomg  8964  brdomi  8965  ctex  8969  domssl  9004  domssr  9005  domtr  9013  undom  9063  xpdom2  9070  xpdom1g  9072  domunsncan  9075  sbth  9095  sbthcl  9097  fodomr  9126  pwdom  9127  domssex  9136  mapdom1  9140  mapdom2  9146  domtrfil  9186  sbthfi  9193  0sdom1dom  9216  1sdom2dom  9224  fineqv  9237  infsdomnn  9271  infn0ALT  9273  elharval  9533  harword  9535  domwdom  9546  unxpwdom  9561  infdifsn  9636  infdiffi  9637  ac10ct  10037  djudom2  10186  djuinf  10191  infdju1  10192  pwdjuidm  10194  djulepw  10195  infdjuabs  10207  infunabs  10208  pwdjudom  10217  infpss  10218  infmap2  10219  fictb  10246  infpssALT  10315  fin34  10392  ttukeylem1  10511  fodomb  10528  wdomac  10529  brdom3  10530  iundom2g  10542  iundom  10544  infxpidm  10564  gchdomtri  10632  pwfseq  10667  pwxpndom2  10668  pwxpndom  10669  pwdjundom  10670  gchdjuidm  10671  gchpwdom  10673  gchaclem  10681  reexALT  13026  hashdomi  14436  1stcrestlem  23646  hauspwdom  23695  ufilen  24124  ovoliunnul  25703  karddom  35598  ovoliunnfl  38354  voliunnfl  38356  volsupnfl  38357  nnfoctb  45809  rn1st  46029  meadjiun  47221  caragenunicl  47279