Metamath Proof Explorer

Theorem natrcl

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

Ref Expression
Hypothesis natrcl.1 ⊢ N = C Nat D
Assertion natrcl ⊢ A ∈ F N G → F ∈ C Func D ∧ G ∈ C Func D

Proof

Step Hyp Ref Expression
1 natrcl.1 ⊢ N = C Nat D
2 eqid ⊢ Base C = Base C
3 eqid ⊢ Hom ⁡ C = Hom ⁡ C
4 eqid ⊢ Hom ⁡ D = Hom ⁡ D
5 eqid ⊢ comp ⁡ D = comp ⁡ D
6 1 2 3 4 5 natfval ⊢ N = f ∈ C Func D , g ∈ C Func D ⟼ ⦋ 1 st ⁡ f / r⦌ ⦋ 1 st ⁡ g / s⦌ a ∈ ⨉ x ∈ Base C r ⁡ x Hom ⁡ D s ⁡ x | ∀ x ∈ Base C ∀ y ∈ Base C ∀ h ∈ x Hom ⁡ C y a ⁡ y r ⁡ x r ⁡ y comp ⁡ D s ⁡ y x 2 nd ⁡ f y ⁡ h = x 2 nd ⁡ g y ⁡ h r ⁡ x s ⁡ x comp ⁡ D s ⁡ y a ⁡ x
7 6 elmpocl ⊢ A ∈ F N G → F ∈ C Func D ∧ G ∈ C Func D