Metamath Proof Explorer

Theorem funcrcl3

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

Ref Expression
Hypothesis funcrcl2.f ⊢ φ → F D Func E G
Assertion funcrcl3 ⊢ φ → E ∈ Cat

Proof

Step Hyp Ref Expression
1 funcrcl2.f ⊢ φ → F D Func E G
2 df-br ⊢ F D Func E G ↔ F G ∈ D Func E
3 2 biimpi ⊢ F D Func E G → F G ∈ D Func E
4 funcrcl ⊢ F G ∈ D Func E → D ∈ Cat ∧ E ∈ Cat
5 1 3 4 3syl ⊢ φ → D ∈ Cat ∧ E ∈ Cat
6 5 simprd ⊢ φ → E ∈ Cat