Theorem initorcl

Description: Reverse closure for an initial object: If a class has an initial object, the class is a category. (Contributed by AV, 4-Apr-2020)

	Ref	Expression
Assertion	initorcl	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		df-inito	⊢ InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
2	1	mptrcl	⊢ ( 𝐼 ∈ ( InitO ‘ 𝐶 ) → 𝐶 ∈ Cat )