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 ) ) ) ) )