Theorem idfurcl

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

	Ref	Expression
Assertion	idfurcl	⊢ ( ( idfunc ‘ 𝐶 ) ∈ ( 𝐷 Func 𝐸 ) → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩ ∈ V
2	1	csbex	⊢ ⦋ ( Base ‘ 𝑡 ) / 𝑏 ⦌ ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩ ∈ V
3		df-idfu	⊢ idfunc = ( 𝑡 ∈ Cat ↦ ⦋ ( Base ‘ 𝑡 ) / 𝑏 ⦌ ⟨ ( I ↾ 𝑏 ) , ( 𝑧 ∈ ( 𝑏 × 𝑏 ) ↦ ( I ↾ ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ) ⟩ )
4	2 3	dmmpti	⊢ dom idfunc = Cat
5		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
6		0nelrel0	⊢ ( Rel ( 𝐷 Func 𝐸 ) → ¬ ∅ ∈ ( 𝐷 Func 𝐸 ) )
7	5 6	ax-mp	⊢ ¬ ∅ ∈ ( 𝐷 Func 𝐸 )
8	4 7	ndmfvrcl	⊢ ( ( idfunc ‘ 𝐶 ) ∈ ( 𝐷 Func 𝐸 ) → 𝐶 ∈ Cat )