This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )