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

Metamath Proof Explorer

Theorem termchommo

Description: All morphisms of a terminal category are identical. (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 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
termchommo.x ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
termchommo.y ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
termchommo.f ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑊 ) )
Assertion termchommo ( 𝜑 → 𝐹 = 𝐺 )

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 termchommo.x ⊢ ( 𝜑 → 𝑍 ∈ 𝐵 )
8 termchommo.y ⊢ ( 𝜑 → 𝑊 ∈ 𝐵 )
9 termchommo.f ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑍 𝐻 𝑊 ) )
10 1 2 3 7 termcbasmo ⊢ ( 𝜑 → 𝑋 = 𝑍 )
11 1 2 4 8 termcbasmo ⊢ ( 𝜑 → 𝑌 = 𝑊 )
12 10 11 oveq12d ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( 𝑍 𝐻 𝑊 ) )
13 9 12 eleqtrrd ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
14 1 termcthind ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
15 3 4 6 13 2 5 14 thincmo2 ⊢ ( 𝜑 → 𝐹 = 𝐺 )