Metamath Proof Explorer

Theorem isepi2

Description: Write out the epimorphism property directly. (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 isepi2 
|- ( ph -> ( F e. ( X E Y ) <-> ( F e. ( X H Y ) /\ A. z e. B A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) ) )

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 1 2 3 4 5 6 7 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 ) ) ) ) )
9 5 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( Y H z ) ) ) -> C e. Cat )
10 6 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( Y H z ) ) ) -> X e. B )
11 7 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( Y H z ) ) ) -> Y e. B )
12 simprl 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( Y H z ) ) ) -> z e. B )
13 simplr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( Y H z ) ) ) -> F e. ( X H Y ) )
14 simprr 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( Y H z ) ) ) -> g e. ( Y H z ) )
15 1 2 3 9 10 11 12 13 14 catcocl 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ ( z e. B /\ g e. ( Y H z ) ) ) -> ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) )
16 15 anassrs 
 |-  ( ( ( ( ph /\ F e. ( X H Y ) ) /\ z e. B ) /\ g e. ( Y H z ) ) -> ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) )
17 16 ralrimiva 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ z e. B ) -> A. g e. ( Y H z ) ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) )
18 eqid 
 |-  ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) = ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) )
19 18 fmpt 
 |-  ( A. g e. ( Y H z ) ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) <-> ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) --> ( X H z ) )
20 df-f1 
 |-  ( ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) -1-1-> ( X H z ) <-> ( ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) --> ( X H z ) /\ Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) )
21 20 baib 
 |-  ( ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) --> ( X H z ) -> ( ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) -1-1-> ( X H z ) <-> Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) )
22 19 21 sylbi 
 |-  ( A. g e. ( Y H z ) ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) -> ( ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) -1-1-> ( X H z ) <-> Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) )
23 oveq1 
 |-  ( g = h -> ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) )
24 18 23 f1mpt 
 |-  ( ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) -1-1-> ( X H z ) <-> ( A. g e. ( Y H z ) ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) /\ A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) )
25 24 baib 
 |-  ( A. g e. ( Y H z ) ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) -> ( ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) : ( Y H z ) -1-1-> ( X H z ) <-> A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) )
26 22 25 bitr3d 
 |-  ( A. g e. ( Y H z ) ( g ( <. X , Y >. .x. z ) F ) e. ( X H z ) -> ( Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) <-> A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) )
27 17 26 syl 
 |-  ( ( ( ph /\ F e. ( X H Y ) ) /\ z e. B ) -> ( Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) <-> A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) )
28 27 ralbidva 
 |-  ( ( ph /\ F e. ( X H Y ) ) -> ( A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) <-> A. z e. B A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) )
29 28 pm5.32da 
 |-  ( ph -> ( ( F e. ( X H Y ) /\ A. z e. B Fun `' ( g e. ( Y H z ) |-> ( g ( <. X , Y >. .x. z ) F ) ) ) <-> ( F e. ( X H Y ) /\ A. z e. B A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) ) )
30 8 29 bitrd 
 |-  ( ph -> ( F e. ( X E Y ) <-> ( F e. ( X H Y ) /\ A. z e. B A. g e. ( Y H z ) A. h e. ( Y H z ) ( ( g ( <. X , Y >. .x. z ) F ) = ( h ( <. X , Y >. .x. z ) F ) -> g = h ) ) ) )