Metamath Proof Explorer


Theorem isepi

Description: Definition of an epimorphism in a category. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses isepi.b
|- B = ( Base ` C )
isepi.h
|- H = ( Hom ` C )
isepi.o
|- .x. = ( comp ` C )
isepi.e
|- E = ( Epi ` C )
isepi.c
|- ( ph -> C e. Cat )
isepi.x
|- ( ph -> X e. B )
isepi.y
|- ( ph -> Y e. B )
Assertion isepi
|- ( ph -> ( F e. ( X E Y ) <-> ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isepi.b
 |-  B = ( Base ` C )
2 isepi.h
 |-  H = ( Hom ` C )
3 isepi.o
 |-  .x. = ( comp ` C )
4 isepi.e
 |-  E = ( Epi ` C )
5 isepi.c
 |-  ( ph -> C e. Cat )
6 isepi.x
 |-  ( ph -> X e. B )
7 isepi.y
 |-  ( ph -> Y e. B )
8 eqid
 |-  ( oppCat ` C ) = ( oppCat ` C )
9 8 1 oppcbas
 |-  B = ( Base ` ( oppCat ` C ) )
10 eqid
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
11 eqid
 |-  ( comp ` ( oppCat ` C ) ) = ( comp ` ( oppCat ` C ) )
12 eqid
 |-  ( Mono ` ( oppCat ` C ) ) = ( Mono ` ( oppCat ` C ) )
13 8 oppccat
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
14 5 13 syl
 |-  ( ph -> ( oppCat ` C ) e. Cat )
15 9 10 11 12 14 7 6 ismon
 |-  ( ph -> ( F e. ( Y ( Mono ` ( oppCat ` C ) ) X ) <-> ( F e. ( Y ( Hom ` ( oppCat ` C ) ) X ) /\ A. z e. B Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) ) ) )
16 8 5 12 4 oppcmon
 |-  ( ph -> ( Y ( Mono ` ( oppCat ` C ) ) X ) = ( X E Y ) )
17 16 eleq2d
 |-  ( ph -> ( F e. ( Y ( Mono ` ( oppCat ` C ) ) X ) <-> F e. ( X E Y ) ) )
18 2 8 oppchom
 |-  ( Y ( Hom ` ( oppCat ` C ) ) X ) = ( X H Y )
19 18 a1i
 |-  ( ph -> ( Y ( Hom ` ( oppCat ` C ) ) X ) = ( X H Y ) )
20 19 eleq2d
 |-  ( ph -> ( F e. ( Y ( Hom ` ( oppCat ` C ) ) X ) <-> F e. ( X H Y ) ) )
21 2 8 oppchom
 |-  ( z ( Hom ` ( oppCat ` C ) ) Y ) = ( Y H z )
22 21 a1i
 |-  ( ( ph /\ z e. B ) -> ( z ( Hom ` ( oppCat ` C ) ) Y ) = ( Y H z ) )
23 simpr
 |-  ( ( ph /\ z e. B ) -> z e. B )
24 7 adantr
 |-  ( ( ph /\ z e. B ) -> Y e. B )
25 6 adantr
 |-  ( ( ph /\ z e. B ) -> X e. B )
26 1 3 8 23 24 25 oppcco
 |-  ( ( ph /\ z e. B ) -> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) = ( g ( <. X , Y >. .x. z ) F ) )
27 22 26 mpteq12dv
 |-  ( ( ph /\ z e. B ) -> ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) = ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) )
28 27 cnveqd
 |-  ( ( ph /\ z e. B ) -> `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) = `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) )
29 28 funeqd
 |-  ( ( ph /\ z e. B ) -> ( Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) <-> Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) )
30 29 ralbidva
 |-  ( ph -> ( A. z e. B Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) <-> A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) )
31 20 30 anbi12d
 |-  ( ph -> ( ( F e. ( Y ( Hom ` ( oppCat ` C ) ) X ) /\ A. z e. B Fun `' ( g e. ( z ( Hom ` ( oppCat ` C ) ) Y ) |-> ( F ( <. z , Y >. ( comp ` ( oppCat ` C ) ) X ) g ) ) ) <-> ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) ) )
32 15 17 31 3bitr3d
 |-  ( ph -> ( F e. ( X E Y ) <-> ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) ) )