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

Metamath Proof Explorer

Theorem indcthing

Description: An indiscrete category, i.e., a category where all hom-sets have exactly one morphism, is thin. (Contributed by Zhi Wang, 11-Nov-2025)

Ref Expression
Hypotheses indcthing.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
indcthing.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
indcthing.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
indcthing.i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑦 ) = { 𝐹 } )
Assertion indcthing ( 𝜑 → 𝐶 ∈ ThinCat )

Proof

Step Hyp Ref Expression
1 indcthing.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 indcthing.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 indcthing.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 indcthing.i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑦 ) = { 𝐹 } )
5 eqid ⊢ { 𝐹 } = { 𝐹 }
6 mosn ⊢ ( { 𝐹 } = { 𝐹 } → ∃* 𝑓 𝑓 ∈ { 𝐹 } )
7 5 6 ax-mp ⊢ ∃* 𝑓 𝑓 ∈ { 𝐹 }
8 4 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑓 ∈ { 𝐹 } ) )
9 8 mobidv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∃* 𝑓 𝑓 ∈ { 𝐹 } ) )
10 7 9 mpbiri ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑓 𝑓 ∈ ( 𝑥 𝐻 𝑦 ) )
11 1 2 10 3 isthincd ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )