Metamath Proof Explorer

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 ⊢ φ → C ∈ ThinCat
thincid.b ⊢ B = Base C
thincid.h ⊢ H = Hom ⁡ C
thincid.x ⊢ φ → X ∈ B
thincmon.y ⊢ φ → Y ∈ B
thincepi.e ⊢ E = Epi ⁡ C
Assertion thincepi ⊢ φ → X E Y = X H Y

Proof

Step Hyp Ref Expression
1 thincid.c ⊢ φ → C ∈ ThinCat
2 thincid.b ⊢ B = Base C
3 thincid.h ⊢ H = Hom ⁡ C
4 thincid.x ⊢ φ → X ∈ B
5 thincmon.y ⊢ φ → Y ∈ B
6 thincepi.e ⊢ E = Epi ⁡ C
7 5 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ Y H z ∧ h ∈ Y H z → Y ∈ B
8 simpr1 ⊢ φ ∧ z ∈ B ∧ g ∈ Y H z ∧ h ∈ Y H z → z ∈ B
9 simpr2 ⊢ φ ∧ z ∈ B ∧ g ∈ Y H z ∧ h ∈ Y H z → g ∈ Y H z
10 simpr3 ⊢ φ ∧ z ∈ B ∧ g ∈ Y H z ∧ h ∈ Y H z → h ∈ Y H z
11 1 adantr ⊢ φ ∧ z ∈ B ∧ g ∈ Y H z ∧ h ∈ Y H z → C ∈ ThinCat
12 7 8 9 10 2 3 11 thincmo2 ⊢ φ ∧ z ∈ B ∧ g ∈ Y H z ∧ h ∈ Y H z → g = h
13 12 a1d ⊢ φ ∧ z ∈ B ∧ g ∈ Y H z ∧ h ∈ Y H z → g X Y comp ⁡ C z f = h X Y comp ⁡ C z f → g = h
14 13 ralrimivvva ⊢ φ → ∀ z ∈ B ∀ g ∈ Y H z ∀ h ∈ Y H z g X Y comp ⁡ C z f = h X Y comp ⁡ C z f → g = h
15 eqid ⊢ comp ⁡ C = comp ⁡ C
16 1 thinccatd ⊢ φ → C ∈ Cat
17 2 3 15 6 16 4 5 isepi2 ⊢ φ → f ∈ X E Y ↔ f ∈ X H Y ∧ ∀ z ∈ B ∀ g ∈ Y H z ∀ h ∈ Y H z g X Y comp ⁡ C z f = h X Y comp ⁡ C z f → g = h
18 14 17 mpbiran2d ⊢ φ → f ∈ X E Y ↔ f ∈ X H Y
19 18 eqrdv ⊢ φ → X E Y = X H Y