Theorem thincmon

Description: In a thin category, all morphisms are monomorphisms. The converse does not hold. See grptcmon . (Contributed by Zhi Wang, 24-Sep-2024)

	Ref	Expression
Hypotheses	thincid.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
	thincid.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	thincid.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	thincid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	thincmon.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
	thincmon.m	⊢ 𝑀 = ( Mono ‘ 𝐶 )
Assertion	thincmon	⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		thincid.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2		thincid.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		thincid.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		thincid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		thincmon.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		thincmon.m	⊢ 𝑀 = ( Mono ‘ 𝐶 )
7		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑧 ∈ 𝐵 )
8	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑋 ∈ 𝐵 )
9		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) )
10		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ℎ ∈ ( 𝑧 𝐻 𝑋 ) )
11	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝐶 ∈ ThinCat )
12	7 8 9 10 2 3 11	thincmo2	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → 𝑔 = ℎ )
13	12	a1d	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∧ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ) ) → ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
14	13	ralrimivvva	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) )
15		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
16	1	thinccd	⊢ ( 𝜑 → 𝐶 ∈ Cat )
17	2 3 15 6 16 4 5	ismon2	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝑀 𝑌 ) ↔ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑧 𝐻 𝑋 ) ∀ ℎ ∈ ( 𝑧 𝐻 𝑋 ) ( ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) 𝑔 ) = ( 𝑓 ( ⟨ 𝑧 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑌 ) ℎ ) → 𝑔 = ℎ ) ) ) )
18	14 17	mpbiran2d	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝑀 𝑌 ) ↔ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )
19	18	eqrdv	⊢ ( 𝜑 → ( 𝑋 𝑀 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )