Theorem idfurcl

Description: Reverse closure for an identity functor. (Contributed by Zhi Wang, 10-Nov-2025)

	Ref	Expression
Assertion	idfurcl	$$⊢{id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)\to C\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩\in \mathrm{V}$$
2	1	csbex	$$⊢⦋{\mathrm{Base}}_t/b⦌⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩\in \mathrm{V}$$
3		df-idfu	$$⊢{id}_{\mathrm{func}}=\left(t\in \mathrm{Cat}⟼⦋{\mathrm{Base}}_t/b⦌⟨{\mathrm{I}\upharpoonright }_b,\left(z\in \left(b\times b\right)⟼{\mathrm{I}\upharpoonright }_{\mathrm{Hom}\left(t\right)\left(z\right)}\right)⟩\right)$$
4	2 3	dmmpti	$$⊢\mathrm{dom}{id}_{\mathrm{func}}=\mathrm{Cat}$$
5		relfunc	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)$$
6		0nelrel0	$$⊢\mathrm{Rel}\left(D\mathrm{Func}E\right)\to \neg \varnothing \in \left(D\mathrm{Func}E\right)$$
7	5 6	ax-mp	$$⊢\neg \varnothing \in \left(D\mathrm{Func}E\right)$$
8	4 7	ndmfvrcl	$$⊢{id}_{\mathrm{func}}\left(C\right)\in \left(D\mathrm{Func}E\right)\to C\in \mathrm{Cat}$$