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

Metamath Proof Explorer

Theorem discthing

Description: A discrete category, i.e., a category where all morphisms are identity morphisms, is thin. Example 3.26(1) of Adamek p. 33. (Contributed by Zhi Wang, 11-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 indcthing.b ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝐶 ) )
2 indcthing.h ⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝐶 ) )
3 indcthing.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
4 discthing.i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 𝐻 𝑦 ) = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) )
5 eleq2w2 ⊢ ( { 𝐼 } = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( 𝑖 ∈ { 𝐼 } ↔ 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
6 5 mobidv ⊢ ( { 𝐼 } = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( ∃* 𝑖 𝑖 ∈ { 𝐼 } ↔ ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
7 eleq2w2 ⊢ ( ∅ = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( 𝑖 ∈ ∅ ↔ 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
8 7 mobidv ⊢ ( ∅ = if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) → ( ∃* 𝑖 𝑖 ∈ ∅ ↔ ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
9 eqid ⊢ { 𝐼 } = { 𝐼 }
10 mosn ⊢ ( { 𝐼 } = { 𝐼 } → ∃* 𝑖 𝑖 ∈ { 𝐼 } )
11 9 10 mp1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ 𝑥 = 𝑦 ) → ∃* 𝑖 𝑖 ∈ { 𝐼 } )
12 eqid ⊢ ∅ = ∅
13 mo0 ⊢ ( ∅ = ∅ → ∃* 𝑖 𝑖 ∈ ∅ )
14 12 13 mp1i ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) ∧ ¬ 𝑥 = 𝑦 ) → ∃* 𝑖 𝑖 ∈ ∅ )
15 6 8 11 14 ifbothda ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) )
16 4 eleq2d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ↔ 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
17 16 mobidv ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ∃* 𝑖 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) ↔ ∃* 𝑖 𝑖 ∈ if ( 𝑥 = 𝑦 , { 𝐼 } , ∅ ) ) )
18 15 17 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ∃* 𝑖 𝑖 ∈ ( 𝑥 𝐻 𝑦 ) )
19 1 2 18 3 isthincd ⊢ ( 𝜑 → 𝐶 ∈ ThinCat )