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

Metamath Proof Explorer

Theorem termchomn0

Description: All hom-sets of a terminal category are non-empty. (Contributed by Zhi Wang, 17-Oct-2025)

Ref Expression
Hypotheses termcbas.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
termcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
termcbasmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
termcbasmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
termcid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion termchomn0 ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )

Proof

Step Hyp Ref Expression
1 termcbas.c ⊢ ( 𝜑 → 𝐶 ∈ TermCat )
2 termcbas.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 termcbasmo.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
4 termcbasmo.y ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
5 termcid.h ⊢ 𝐻 = ( Hom ‘ 𝐶 )
6 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
7 1 termccd ⊢ ( 𝜑 → 𝐶 ∈ Cat )
8 2 5 6 7 3 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑋 ) )
9 1 2 3 4 termcbasmo ⊢ ( 𝜑 → 𝑋 = 𝑌 )
10 9 oveq2d ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑋 ) = ( 𝑋 𝐻 𝑌 ) )
11 8 10 eleqtrd ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑌 ) )
12 n0i ⊢ ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 𝐻 𝑌 ) → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )
13 11 12 syl ⊢ ( 𝜑 → ¬ ( 𝑋 𝐻 𝑌 ) = ∅ )