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 No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
thincid.b ⊢B=BaseC
thincid.h ⊢H=Hom⁡C
thincid.x ⊢φ→X∈B
thincmon.y ⊢φ→Y∈B
thincepi.e ⊢E=Epi⁡C
Assertion thincepi ⊢φ→XEY=XHY

Proof

Step Hyp Ref Expression
1 thincid.c Could not format ( ph -> C e. ThinCat ) : No typesetting found for |- ( ph -> C e. ThinCat ) with typecode |-
2 thincid.b ⊢B=BaseC
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∈YHz∧h∈YHz→Y∈B
8 simpr1 ⊢φ∧z∈B∧g∈YHz∧h∈YHz→z∈B
9 simpr2 ⊢φ∧z∈B∧g∈YHz∧h∈YHz→g∈YHz
10 simpr3 ⊢φ∧z∈B∧g∈YHz∧h∈YHz→h∈YHz
11 1 adantr Could not format ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> C e. ThinCat ) : No typesetting found for |- ( ( ph /\ ( z e. B /\ g e. ( Y H z ) /\ h e. ( Y H z ) ) ) -> C e. ThinCat ) with typecode |-
12 7 8 9 10 2 3 11 thincmo2 ⊢φ∧z∈B∧g∈YHz∧h∈YHz→g=h
13 12 a1d ⊢φ∧z∈B∧g∈YHz∧h∈YHz→gXYcomp⁡Czf=hXYcomp⁡Czf→g=h
14 13 ralrimivvva ⊢φ→∀z∈B∀g∈YHz∀h∈YHzgXYcomp⁡Czf=hXYcomp⁡Czf→g=h
15 eqid ⊢comp⁡C=comp⁡C
16 1 thinccd ⊢φ→C∈Cat
17 2 3 15 6 16 4 5 isepi2 ⊢φ→f∈XEY↔f∈XHY∧∀z∈B∀g∈YHz∀h∈YHzgXYcomp⁡Czf=hXYcomp⁡Czf→g=h
18 14 17 mpbiran2d ⊢φ→f∈XEY↔f∈XHY
19 18 eqrdv ⊢φ→XEY=XHY