Theorem relfunc

Description: The set of functors is a relation. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Assertion	relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-func	$$⊢\mathrm{Func}=\left(t\in \mathrm{Cat},u\in \mathrm{Cat}⟼\left\{⟨f,g⟩|\underset{\dot{}}{[}{\mathrm{Base}}_t/b\underset{\dot{}}{]}\left(f:b⟶{\mathrm{Base}}_u\wedge g\in \underset{z\in b\times b}{⨉}\left({\left(f\left(1^{st}\left(z\right)\right)\mathrm{Hom}\left(u\right)f\left(2^{nd}\left(z\right)\right)\right)}^{\mathrm{Hom}\left(t\right)\left(z\right)}\right)\wedge \forall x\in b\left(\left(xgx\right)\left(\mathrm{Id}\left(t\right)\left(x\right)\right)=\mathrm{Id}\left(u\right)\left(f\left(x\right)\right)\wedge \forall y\in b\forall z\in b\forall m\in \left(x\mathrm{Hom}\left(t\right)y\right)\forall n\in \left(y\mathrm{Hom}\left(t\right)z\right)\left(xgz\right)\left(n\left(⟨x,y⟩\mathrm{comp}\left(t\right)z\right)m\right)=\left(ygz\right)\left(n\right)\left(⟨f\left(x\right),f\left(y\right)⟩\mathrm{comp}\left(u\right)f\left(z\right)\right)\left(xgy\right)\left(m\right)\right)\right)\right\}\right)$$
2	1	relmpoopab	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$