Theorem reldom 9010

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 9006	. 2 ⊢ ≼ = {⟨𝑥, 𝑦⟩ ∣ ∃𝑓 𝑓:𝑥⟶1-1𝑦}
2	1	relopabi 5806	1 ⊢ Rel ≼

This proof depends on syntax axioms:  ∃wex 1812  Rel wrel 5661  ⟶1-1wf1 6558   ≼ cdom 9002

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5172  df-xp 5662  df-rel 5663  df-dom 9006

This theorem is used by:  relsdom  9011  brdomg  9016  brdomi  9017  ctex  9021  domssl  9056  domssr  9057  domtr  9065  undom  9115  xpdom2  9122  xpdom1g  9124  domunsncan  9127  sbth  9147  sbthcl  9149  fodomr  9178  pwdom  9179  domssex  9188  mapdom1  9192  mapdom2  9198  domtrfil  9238  sbthfi  9245  0sdom1dom  9268  1sdom2dom  9276  fineqv  9289  infsdomnn  9324  infn0ALT  9326  elharval  9585  harword  9587  domwdom  9598  unxpwdom  9613  infdifsn  9688  infdiffi  9689  ac10ct  10143  djudom2  10292  djuinf  10297  infdju1  10298  pwdjuidm  10300  djulepw  10301  infdjuabs  10313  infunabs  10314  pwdjudom  10323  infpss  10324  infmap2  10325  fictb  10352  infpssALT  10421  fin34  10498  ttukeylem1  10617  fodomb  10635  wdomac  10636  brdom3  10637  iundom2g  10654  iundom  10656  infxpidm  10676  gchdomtri  10744  pwfseq  10779  pwxpndom2  10780  pwxpndom  10781  pwdjundom  10782  gchdjuidm  10783  gchpwdom  10785  gchaclem  10793  reexALT  13142  hashdomi  14554  1stcrestlem  23803  hauspwdom  23853  ufilen  24282  ovoliunnul  25861  weexenwe  35861  karddom  35942  ovoliunnfl  38785  voliunnfl  38787  volsupnfl  38788  nnfoctb  46281  rn1st  46500  meadjiun  47691  caragenunicl  47749