Metamath Proof Explorer

Theorem epii

Description: Property of an epimorphism. (Contributed by Mario Carneiro, 3-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 )
epii.z 
|- ( ph -> Z e. B )
epii.f 
|- ( ph -> F e. ( X E Y ) )
epii.g 
|- ( ph -> G e. ( Y H Z ) )
epii.k 
|- ( ph -> K e. ( Y H Z ) )
Assertion epii 
|- ( ph -> ( ( G ( <. X , Y >. .x. Z ) F ) = ( K ( <. X , Y >. .x. Z ) F ) <-> G = K ) )

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 epii.z 
 |-  ( ph -> Z e. B )
9 epii.f 
 |-  ( ph -> F e. ( X E Y ) )
10 epii.g 
 |-  ( ph -> G e. ( Y H Z ) )
11 epii.k 
 |-  ( ph -> K e. ( Y H Z ) )
12 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
13 1 3 12 8 7 6 oppcco 
 |-  ( ph -> ( F ( <. Z , Y >. ( comp ` ( oppCat ` C ) ) X ) G ) = ( G ( <. X , Y >. .x. Z ) F ) )
14 1 3 12 8 7 6 oppcco 
 |-  ( ph -> ( F ( <. Z , Y >. ( comp ` ( oppCat ` C ) ) X ) K ) = ( K ( <. X , Y >. .x. Z ) F ) )
15 13 14 eqeq12d 
 |-  ( ph -> ( ( F ( <. Z , Y >. ( comp ` ( oppCat ` C ) ) X ) G ) = ( F ( <. Z , Y >. ( comp ` ( oppCat ` C ) ) X ) K ) <-> ( G ( <. X , Y >. .x. Z ) F ) = ( K ( <. X , Y >. .x. Z ) F ) ) )
16 12 1 oppcbas 
 |-  B = ( Base ` ( oppCat ` C ) )
17 eqid 
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
18 eqid 
 |-  ( comp ` ( oppCat ` C ) ) = ( comp ` ( oppCat ` C ) )
19 eqid 
 |-  ( Mono ` ( oppCat ` C ) ) = ( Mono ` ( oppCat ` C ) )
20 12 oppccat 
 |-  ( C e. Cat -> ( oppCat ` C ) e. Cat )
21 5 20 syl 
 |-  ( ph -> ( oppCat ` C ) e. Cat )
22 12 5 19 4 oppcmon 
 |-  ( ph -> ( Y ( Mono ` ( oppCat ` C ) ) X ) = ( X E Y ) )
23 9 22 eleqtrrd 
 |-  ( ph -> F e. ( Y ( Mono ` ( oppCat ` C ) ) X ) )
24 2 12 oppchom 
 |-  ( Z ( Hom ` ( oppCat ` C ) ) Y ) = ( Y H Z )
25 10 24 eleqtrrdi 
 |-  ( ph -> G e. ( Z ( Hom ` ( oppCat ` C ) ) Y ) )
26 11 24 eleqtrrdi 
 |-  ( ph -> K e. ( Z ( Hom ` ( oppCat ` C ) ) Y ) )
27 16 17 18 19 21 7 6 8 23 25 26 moni 
 |-  ( ph -> ( ( F ( <. Z , Y >. ( comp ` ( oppCat ` C ) ) X ) G ) = ( F ( <. Z , Y >. ( comp ` ( oppCat ` C ) ) X ) K ) <-> G = K ) )
28 15 27 bitr3d 
 |-  ( ph -> ( ( G ( <. X , Y >. .x. Z ) F ) = ( K ( <. X , Y >. .x. Z ) F ) <-> G = K ) )