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 )