Theorem reldom 8963

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

This proof depends on syntax axioms:  ∃wex 1812  Rel wrel 5656  –1-1→wf1 6528   ≼ cdom 8955

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 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-opab 5168  df-xp 5657  df-rel 5658  df-dom 8959

This theorem is used by:  relsdom  8964  brdomg  8969  brdomi  8970  ctex  8974  domssl  9009  domssr  9010  domtr  9018  undom  9068  xpdom2  9075  xpdom1g  9077  domunsncan  9080  sbth  9100  sbthcl  9102  fodomr  9131  pwdom  9132  domssex  9141  mapdom1  9145  mapdom2  9151  domtrfil  9191  sbthfi  9198  0sdom1dom  9221  1sdom2dom  9229  fineqv  9242  infsdomnn  9277  infn0ALT  9279  elharval  9539  harword  9541  domwdom  9552  unxpwdom  9567  infdifsn  9642  infdiffi  9643  ac10ct  10094  djudom2  10243  djuinf  10248  infdju1  10249  pwdjuidm  10251  djulepw  10252  infdjuabs  10264  infunabs  10265  pwdjudom  10274  infpss  10275  infmap2  10276  fictb  10303  infpssALT  10372  fin34  10449  ttukeylem1  10568  fodomb  10586  wdomac  10587  brdom3  10588  iundom2g  10605  iundom  10607  infxpidm  10627  gchdomtri  10695  pwfseq  10730  pwxpndom2  10731  pwxpndom  10732  pwdjundom  10733  gchdjuidm  10734  gchpwdom  10736  gchaclem  10744  reexALT  13093  hashdomi  14504  1stcrestlem  23750  hauspwdom  23800  ufilen  24229  ovoliunnul  25808  karddom  35802  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  nnfoctb  46008  rn1st  46228  meadjiun  47420  caragenunicl  47478