Metamath Proof Explorer

Theorem fthepi

Description: A faithful functor reflects epimorphisms. (Contributed by Mario Carneiro, 27-Jan-2017)

Ref Expression
Hypotheses fthmon.b 
|- B = ( Base ` C )
fthmon.h 
|- H = ( Hom ` C )
fthmon.f 
|- ( ph -> F ( C Faith D ) G )
fthmon.x 
|- ( ph -> X e. B )
fthmon.y 
|- ( ph -> Y e. B )
fthmon.r 
|- ( ph -> R e. ( X H Y ) )
fthepi.e 
|- E = ( Epi ` C )
fthepi.p 
|- P = ( Epi ` D )
fthepi.1 
|- ( ph -> ( ( X G Y ) ` R ) e. ( ( F ` X ) P ( F ` Y ) ) )
Assertion fthepi 
|- ( ph -> R e. ( X E Y ) )

Proof

Step Hyp Ref Expression
1 fthmon.b 
 |-  B = ( Base ` C )
2 fthmon.h 
 |-  H = ( Hom ` C )
3 fthmon.f 
 |-  ( ph -> F ( C Faith D ) G )
4 fthmon.x 
 |-  ( ph -> X e. B )
5 fthmon.y 
 |-  ( ph -> Y e. B )
6 fthmon.r 
 |-  ( ph -> R e. ( X H Y ) )
7 fthepi.e 
 |-  E = ( Epi ` C )
8 fthepi.p 
 |-  P = ( Epi ` D )
9 fthepi.1 
 |-  ( ph -> ( ( X G Y ) ` R ) e. ( ( F ` X ) P ( F ` Y ) ) )
10 eqid 
 |-  ( oppCat ` C ) = ( oppCat ` C )
11 10 1 oppcbas 
 |-  B = ( Base ` ( oppCat ` C ) )
12 eqid 
 |-  ( Hom ` ( oppCat ` C ) ) = ( Hom ` ( oppCat ` C ) )
13 eqid 
 |-  ( oppCat ` D ) = ( oppCat ` D )
14 10 13 3 fthoppc 
 |-  ( ph -> F ( ( oppCat ` C ) Faith ( oppCat ` D ) ) tpos G )
15 2 10 oppchom 
 |-  ( Y ( Hom ` ( oppCat ` C ) ) X ) = ( X H Y )
16 6 15 eleqtrrdi 
 |-  ( ph -> R e. ( Y ( Hom ` ( oppCat ` C ) ) X ) )
17 eqid 
 |-  ( Mono ` ( oppCat ` C ) ) = ( Mono ` ( oppCat ` C ) )
18 eqid 
 |-  ( Mono ` ( oppCat ` D ) ) = ( Mono ` ( oppCat ` D ) )
19 ovtpos 
 |-  ( Y tpos G X ) = ( X G Y )
20 19 fveq1i 
 |-  ( ( Y tpos G X ) ` R ) = ( ( X G Y ) ` R )
21 20 9 eqeltrid 
 |-  ( ph -> ( ( Y tpos G X ) ` R ) e. ( ( F ` X ) P ( F ` Y ) ) )
22 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
23 22 ssbri 
 |-  ( F ( C Faith D ) G -> F ( C Func D ) G )
24 3 23 syl 
 |-  ( ph -> F ( C Func D ) G )
25 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
26 24 25 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
27 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
28 26 27 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
29 28 simprd 
 |-  ( ph -> D e. Cat )
30 13 29 18 8 oppcmon 
 |-  ( ph -> ( ( F ` Y ) ( Mono ` ( oppCat ` D ) ) ( F ` X ) ) = ( ( F ` X ) P ( F ` Y ) ) )
31 21 30 eleqtrrd 
 |-  ( ph -> ( ( Y tpos G X ) ` R ) e. ( ( F ` Y ) ( Mono ` ( oppCat ` D ) ) ( F ` X ) ) )
32 11 12 14 5 4 16 17 18 31 fthmon 
 |-  ( ph -> R e. ( Y ( Mono ` ( oppCat ` C ) ) X ) )
33 28 simpld 
 |-  ( ph -> C e. Cat )
34 10 33 17 7 oppcmon 
 |-  ( ph -> ( Y ( Mono ` ( oppCat ` C ) ) X ) = ( X E Y ) )
35 32 34 eleqtrd 
 |-  ( ph -> R e. ( X E Y ) )