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

Metamath Proof Explorer

Theorem thincid

Description: In a thin category, a morphism from an object to itself is an identity morphism. (Contributed by Zhi Wang, 24-Sep-2024)

Ref Expression
Hypotheses thincid.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
thincid.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
thincid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
thincid.i ⊢ 1 = ( Id ‘ 𝐶 )
thincid.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑋 ) )
Assertion thincid ( 𝜑 → 𝐹 = ( 1 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 thincid.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2 thincid.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 thincid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
4 thincid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5 thincid.i ⊢ 1 = ( Id ‘ 𝐶 )
6 thincid.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑋 ) )
7 1 thinccd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
8 2 3 5 7 4 catidcl ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
9 4 4 6 8 2 3 1 thincmo2 ⊢ ( 𝜑 → 𝐹 = ( 1 ‘ 𝑋 ) )