Theorem reldmfunc

Description: The domain of Func is a relation. (Contributed by Zhi Wang, 12-Nov-2025)

	Ref	Expression
Assertion	reldmfunc	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{Func}$$

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	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{Func}$$