Metamath Proof Explorer


Theorem subcrcl

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

Ref Expression
Assertion subcrcl ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )

Proof

Step Hyp Ref Expression
1 df-subc Subcat = ( 𝑐 ∈ Cat ↦ { ∣ ( cat ( Homf𝑐 ) ∧ [ dom dom / 𝑠 ]𝑥𝑠 ( ( ( Id ‘ 𝑐 ) ‘ 𝑥 ) ∈ ( 𝑥 𝑥 ) ∧ ∀ 𝑦𝑠𝑧𝑠𝑓 ∈ ( 𝑥 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝑐 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝑧 ) ) ) } )
2 1 mptrcl ( 𝐻 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )