# Metamath Proof Explorer

## Theorem epii

Description: Property of an epimorphism. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses isepi.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
isepi.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
isepi.o
isepi.e ${⊢}{E}=\mathrm{Epi}\left({C}\right)$
isepi.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
isepi.x ${⊢}{\phi }\to {X}\in {B}$
isepi.y ${⊢}{\phi }\to {Y}\in {B}$
epii.z ${⊢}{\phi }\to {Z}\in {B}$
epii.f ${⊢}{\phi }\to {F}\in \left({X}{E}{Y}\right)$
epii.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
epii.k ${⊢}{\phi }\to {K}\in \left({Y}{H}{Z}\right)$
Assertion epii

### Proof

Step Hyp Ref Expression
1 isepi.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
2 isepi.h ${⊢}{H}=\mathrm{Hom}\left({C}\right)$
3 isepi.o
4 isepi.e ${⊢}{E}=\mathrm{Epi}\left({C}\right)$
5 isepi.c ${⊢}{\phi }\to {C}\in \mathrm{Cat}$
6 isepi.x ${⊢}{\phi }\to {X}\in {B}$
7 isepi.y ${⊢}{\phi }\to {Y}\in {B}$
8 epii.z ${⊢}{\phi }\to {Z}\in {B}$
9 epii.f ${⊢}{\phi }\to {F}\in \left({X}{E}{Y}\right)$
10 epii.g ${⊢}{\phi }\to {G}\in \left({Y}{H}{Z}\right)$
11 epii.k ${⊢}{\phi }\to {K}\in \left({Y}{H}{Z}\right)$
12 eqid ${⊢}\mathrm{oppCat}\left({C}\right)=\mathrm{oppCat}\left({C}\right)$
13 1 3 12 8 7 6 oppcco
14 1 3 12 8 7 6 oppcco
15 13 14 eqeq12d
16 12 1 oppcbas ${⊢}{B}={\mathrm{Base}}_{\mathrm{oppCat}\left({C}\right)}$
17 eqid ${⊢}\mathrm{Hom}\left(\mathrm{oppCat}\left({C}\right)\right)=\mathrm{Hom}\left(\mathrm{oppCat}\left({C}\right)\right)$
18 eqid ${⊢}\mathrm{comp}\left(\mathrm{oppCat}\left({C}\right)\right)=\mathrm{comp}\left(\mathrm{oppCat}\left({C}\right)\right)$
19 eqid ${⊢}\mathrm{Mono}\left(\mathrm{oppCat}\left({C}\right)\right)=\mathrm{Mono}\left(\mathrm{oppCat}\left({C}\right)\right)$
20 12 oppccat ${⊢}{C}\in \mathrm{Cat}\to \mathrm{oppCat}\left({C}\right)\in \mathrm{Cat}$
21 5 20 syl ${⊢}{\phi }\to \mathrm{oppCat}\left({C}\right)\in \mathrm{Cat}$
22 12 5 19 4 oppcmon ${⊢}{\phi }\to {Y}\mathrm{Mono}\left(\mathrm{oppCat}\left({C}\right)\right){X}={X}{E}{Y}$
23 9 22 eleqtrrd ${⊢}{\phi }\to {F}\in \left({Y}\mathrm{Mono}\left(\mathrm{oppCat}\left({C}\right)\right){X}\right)$
24 2 12 oppchom ${⊢}{Z}\mathrm{Hom}\left(\mathrm{oppCat}\left({C}\right)\right){Y}={Y}{H}{Z}$
25 10 24 eleqtrrdi ${⊢}{\phi }\to {G}\in \left({Z}\mathrm{Hom}\left(\mathrm{oppCat}\left({C}\right)\right){Y}\right)$
26 11 24 eleqtrrdi ${⊢}{\phi }\to {K}\in \left({Z}\mathrm{Hom}\left(\mathrm{oppCat}\left({C}\right)\right){Y}\right)$
27 16 17 18 19 21 7 6 8 23 25 26 moni ${⊢}{\phi }\to \left({F}\left(⟨{Z},{Y}⟩\mathrm{comp}\left(\mathrm{oppCat}\left({C}\right)\right){X}\right){G}={F}\left(⟨{Z},{Y}⟩\mathrm{comp}\left(\mathrm{oppCat}\left({C}\right)\right){X}\right){K}↔{G}={K}\right)$
28 15 27 bitr3d