Metamath Proof Explorer


Theorem funcrcl

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

Ref Expression
Assertion funcrcl ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )

Proof

Step Hyp Ref Expression
1 df-func Func = ( 𝑡 ∈ Cat , 𝑢 ∈ Cat ↦ { ⟨ 𝑓 , 𝑔 ⟩ ∣ [ ( Base ‘ 𝑡 ) / 𝑏 ] ( 𝑓 : 𝑏 ⟶ ( Base ‘ 𝑢 ) ∧ 𝑔X 𝑧 ∈ ( 𝑏 × 𝑏 ) ( ( ( 𝑓 ‘ ( 1st𝑧 ) ) ( Hom ‘ 𝑢 ) ( 𝑓 ‘ ( 2nd𝑧 ) ) ) ↑m ( ( Hom ‘ 𝑡 ) ‘ 𝑧 ) ) ∧ ∀ 𝑥𝑏 ( ( ( 𝑥 𝑔 𝑥 ) ‘ ( ( Id ‘ 𝑡 ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝑢 ) ‘ ( 𝑓𝑥 ) ) ∧ ∀ 𝑦𝑏𝑧𝑏𝑚 ∈ ( 𝑥 ( Hom ‘ 𝑡 ) 𝑦 ) ∀ 𝑛 ∈ ( 𝑦 ( Hom ‘ 𝑡 ) 𝑧 ) ( ( 𝑥 𝑔 𝑧 ) ‘ ( 𝑛 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑡 ) 𝑧 ) 𝑚 ) ) = ( ( ( 𝑦 𝑔 𝑧 ) ‘ 𝑛 ) ( ⟨ ( 𝑓𝑥 ) , ( 𝑓𝑦 ) ⟩ ( comp ‘ 𝑢 ) ( 𝑓𝑧 ) ) ( ( 𝑥 𝑔 𝑦 ) ‘ 𝑚 ) ) ) ) } )
2 1 elmpocl ( 𝐹 ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )