This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem termorcl

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

Ref Expression
Assertion termorcl ( 𝑇 ∈ ( TermO ‘ 𝐶 ) → 𝐶 ∈ Cat )

Proof

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