Metamath Proof Explorer

Theorem funcrcl

Description: Reverse closure for a functor. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion funcrcl ⊢ F ∈ D Func E → D ∈ Cat ∧ E ∈ Cat

Proof

Step Hyp Ref Expression
1 df-func ⊢ Func = t ∈ Cat , u ∈ Cat ⟼ f g | [˙Base t / b]˙ f : b ⟶ Base u ∧ g ∈ ⨉ z ∈ b × b f ⁡ 1 st ⁡ z Hom ⁡ u f ⁡ 2 nd ⁡ z Hom ⁡ t ⁡ z ∧ ∀ x ∈ b x g x ⁡ Id ⁡ t ⁡ x = Id ⁡ u ⁡ f ⁡ x ∧ ∀ y ∈ b ∀ z ∈ b ∀ m ∈ x Hom ⁡ t y ∀ n ∈ y Hom ⁡ t z x g z ⁡ n x y comp ⁡ t z m = y g z ⁡ n f ⁡ x f ⁡ y comp ⁡ u f ⁡ z x g y ⁡ m
2 1 elmpocl ⊢ F ∈ D Func E → D ∈ Cat ∧ E ∈ Cat