Theorem relco 6138

Description: A composition is a relation. Exercise 24 of [TakeutiZaring] p. 25. (Contributed by NM, 26-Jan-1997.)

Assertion

Ref	Expression
relco	⊢ Rel (𝐴 ∘ 𝐵)

Proof of Theorem relco

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-co 5709	. 2 ⊢ (𝐴 ∘ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ ∃𝑧(𝑥𝐵𝑧 ∧ 𝑧𝐴𝑦)}
2	1	relopabiv 5844	1 ⊢ Rel (𝐴 ∘ 𝐵)

Syntax hints:   ∧ wa 395  ∃wex 1777   class class class wbr 5166   ∘ ccom 5704  Rel wrel 5705

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-opab 5229  df-xp 5706  df-rel 5707  df-co 5709

This theorem is referenced by:  cotrg  6139  cotrgOLD  6140  cotrgOLDOLD  6141  dfco2  6276  resco  6281  coeq0  6286  coiun  6287  cocnvcnv2  6289  cores2  6290  co02  6291  co01  6292  coi1  6293  coass  6296  cossxp  6303  dfpo2  6327  fmptco  7163  cofunexg  7989  dftpos4  8286  ttrcltr  9785  ttrclco  9787  wunco  10802  relexprelg  15087  relexpaddg  15102  imasless  17600  znleval  21596  metustexhalf  24590  fcoinver  32626  fmptcof2  32675  cnvco1  35721  cnvco2  35722  opelco3  35738  txpss3v  35842  sscoid  35877  xrnss3v  38328  cononrel1  43556  cononrel2  43557  coiun1  43614  relexpaddss  43680  brco2f1o  43994  brco3f1o  43995  neicvgnvor  44078  sblpnf  44279