Metamath Proof Explorer

Theorem subcrcl

Description: Reverse closure for the subcategory predicate. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion subcrcl ⊢ H ∈ Subcat ⁡ C → C ∈ Cat

Proof

Step Hyp Ref Expression
1 df-subc ⊢ Subcat = c ∈ Cat ⟼ h | h ⊆ cat Hom 𝑓 ⁡ c ∧ [˙ dom ⁡ dom ⁡ h / s]˙ ∀ x ∈ s Id ⁡ c ⁡ x ∈ x h x ∧ ∀ y ∈ s ∀ z ∈ s ∀ f ∈ x h y ∀ g ∈ y h z g x y comp ⁡ c z f ∈ x h z
2 1 mptrcl ⊢ H ∈ Subcat ⁡ C → C ∈ Cat