Theorem funcrcl3

Description: Reverse closure for a functor. (Contributed by Zhi Wang, 17-Sep-2025)

	Ref	Expression
Hypothesis	funcrcl2.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
Assertion	funcrcl3	⊢ ( 𝜑 → 𝐸 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		funcrcl2.f	⊢ ( 𝜑 → 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 )
2		df-br	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 ↔ ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
3	2	biimpi	⊢ ( 𝐹 ( 𝐷 Func 𝐸 ) 𝐺 → ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) )
4		funcrcl	⊢ ( ⟨ 𝐹 , 𝐺 ⟩ ∈ ( 𝐷 Func 𝐸 ) → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
5	1 3 4	3syl	⊢ ( 𝜑 → ( 𝐷 ∈ Cat ∧ 𝐸 ∈ Cat ) )
6	5	simprd	⊢ ( 𝜑 → 𝐸 ∈ Cat )