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

Metamath Proof Explorer

Theorem termcid2

Description: The morphism of a terminal category is an identity morphism. (Contributed by Zhi Wang, 16-Oct-2025)

Ref Expression
Hypotheses termcbas.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
termcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
termcbasmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
termcbasmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
termcid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
termcid.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
termcid.i ⊢ 1 = ( Id ‘ 𝐶 )
Assertion termcid2 ( 𝜑 → 𝐹 = ( 1 ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 termcbas.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2 termcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 termcbasmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 termcbasmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 termcid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
6 termcid.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
7 termcid.i ⊢ 1 = ( Id ‘ 𝐶 )
8 1 2 3 4 5 6 7 termcid ⊢ ( 𝜑 → 𝐹 = ( 1 ‘ 𝑋 ) )
9 1 2 3 4 termcbasmo ⊢ ( 𝜑 → 𝑋 = 𝑌 )
10 9 fveq2d ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( 1 ‘ 𝑌 ) )
11 8 10 eqtrd ⊢ ( 𝜑 → 𝐹 = ( 1 ‘ 𝑌 ) )