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

Metamath Proof Explorer

Theorem thincmo2

Description: Morphisms in the same hom-set are identical. (Contributed by Zhi Wang, 17-Sep-2024)

Ref Expression
Hypotheses isthincd2lem1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
isthincd2lem1.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
isthincd2lem1.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
isthincd2lem1.4 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
thincmo2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
thincmo2.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
thincmo2.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
Assertion thincmo2 ( 𝜑 → 𝐹 = 𝐺 )

Proof

Step Hyp Ref Expression
1 isthincd2lem1.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
2 isthincd2lem1.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
3 isthincd2lem1.3 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑋 𝐻 𝑌 ) )
4 isthincd2lem1.4 ⊢ ( 𝜑 → 𝐺 ∈ ( 𝑋 𝐻 𝑌 ) )
5 thincmo2.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
6 thincmo2.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
7 thincmo2.c ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
8 5 6 isthinc ⊢ ( 𝐶 ∈ ThinCat ↔ ( 𝐶 ∈ Cat ∧ ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ) )
9 8 simprbi ⊢ ( 𝐶 ∈ ThinCat → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
10 7 9 syl ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
11 1 2 3 4 10 isthincd2lem1 ⊢ ( 𝜑 → 𝐹 = 𝐺 )