Theorem thincepi

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

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

Proof

Step	Hyp	Ref	Expression
1		thincid.c	⊢ ( 𝜑 → 𝐶 ∈ ThinCat )
2		thincid.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		thincid.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		thincid.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		thincmon.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
6		thincepi.e	⊢ 𝐸 = ( Epi ‘ 𝐶 )
7	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑌 ∈ 𝐵 )
8		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ 𝐵 ∧ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∧ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ) ) → 𝑧 ∈ 𝐵 )
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	isepi2	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐸 𝑌 ) ↔ ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ∧ ∀ 𝑧 ∈ 𝐵 ∀ 𝑔 ∈ ( 𝑌 𝐻 𝑧 ) ∀ ℎ ∈ ( 𝑌 𝐻 𝑧 ) ( ( 𝑔 ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) = ( ℎ ( ⟨ 𝑋 , 𝑌 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) → 𝑔 = ℎ ) ) ) )
18	14 17	mpbiran2d	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐸 𝑌 ) ↔ 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ) )
19	18	eqrdv	⊢ ( 𝜑 → ( 𝑋 𝐸 𝑌 ) = ( 𝑋 𝐻 𝑌 ) )