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 ⊢ id func ⁡ C ∈ D Func E → C ∈ Cat

Proof

Step Hyp Ref Expression
1 opex ⊢ I ↾ b z ∈ b × b ⟼ I ↾ Hom ⁡ t ⁡ z ∈ V
2 1 csbex ⊢ ⦋ Base t / b⦌ I ↾ b z ∈ b × b ⟼ I ↾ Hom ⁡ t ⁡ z ∈ V
3 df-idfu ⊢ id func = t ∈ Cat ⟼ ⦋ Base t / b⦌ I ↾ b z ∈ b × b ⟼ I ↾ Hom ⁡ t ⁡ z
4 2 3 dmmpti ⊢ dom ⁡ id func = Cat
5 relfunc ⊢ Rel ⁡ D Func E
6 0nelrel0 ⊢ Rel ⁡ D Func E → ¬ ∅ ∈ D Func E
7 5 6 ax-mp ⊢ ¬ ∅ ∈ D Func E
8 4 7 ndmfvrcl ⊢ id func ⁡ C ∈ D Func E → C ∈ Cat