Metamath Proof Explorer

Theorem fthmon

Description: A faithful functor reflects monomorphisms. (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 ) )
fthmon.m 
|- M = ( Mono ` C )
fthmon.n 
|- N = ( Mono ` D )
fthmon.1 
|- ( ph -> ( ( X G Y ) ` R ) e. ( ( F ` X ) N ( F ` Y ) ) )
Assertion fthmon 
|- ( ph -> R e. ( X M 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 fthmon.m 
 |-  M = ( Mono ` C )
8 fthmon.n 
 |-  N = ( Mono ` D )
9 fthmon.1 
 |-  ( ph -> ( ( X G Y ) ` R ) e. ( ( F ` X ) N ( F ` Y ) ) )
10 eqid 
 |-  ( Base ` D ) = ( Base ` D )
11 eqid 
 |-  ( Hom ` D ) = ( Hom ` D )
12 eqid 
 |-  ( comp ` D ) = ( comp ` D )
13 fthfunc 
 |-  ( C Faith D ) C_ ( C Func D )
14 13 ssbri 
 |-  ( F ( C Faith D ) G -> F ( C Func D ) G )
15 3 14 syl 
 |-  ( ph -> F ( C Func D ) G )
16 df-br 
 |-  ( F ( C Func D ) G <-> <. F , G >. e. ( C Func D ) )
17 15 16 sylib 
 |-  ( ph -> <. F , G >. e. ( C Func D ) )
18 funcrcl 
 |-  ( <. F , G >. e. ( C Func D ) -> ( C e. Cat /\ D e. Cat ) )
19 17 18 syl 
 |-  ( ph -> ( C e. Cat /\ D e. Cat ) )
20 19 simprd 
 |-  ( ph -> D e. Cat )
21 20 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> D e. Cat )
22 15 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> F ( C Func D ) G )
23 1 10 22 funcf1 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> F : B --> ( Base ` D ) )
24 4 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> X e. B )
25 23 24 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( F ` X ) e. ( Base ` D ) )
26 5 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> Y e. B )
27 23 26 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( F ` Y ) e. ( Base ` D ) )
28 simpr1 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> z e. B )
29 23 28 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( F ` z ) e. ( Base ` D ) )
30 9 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( X G Y ) ` R ) e. ( ( F ` X ) N ( F ` Y ) ) )
31 1 2 11 22 28 24 funcf2 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( z G X ) : ( z H X ) --> ( ( F ` z ) ( Hom ` D ) ( F ` X ) ) )
32 simpr2 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> f e. ( z H X ) )
33 31 32 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( z G X ) ` f ) e. ( ( F ` z ) ( Hom ` D ) ( F ` X ) ) )
34 simpr3 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> g e. ( z H X ) )
35 31 34 ffvelrnd 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( z G X ) ` g ) e. ( ( F ` z ) ( Hom ` D ) ( F ` X ) ) )
36 10 11 12 8 21 25 27 29 30 33 35 moni 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` f ) ) = ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` g ) ) <-> ( ( z G X ) ` f ) = ( ( z G X ) ` g ) ) )
37 eqid 
 |-  ( comp ` C ) = ( comp ` C )
38 6 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> R e. ( X H Y ) )
39 1 2 37 12 22 28 24 26 32 38 funcco 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( z G Y ) ` ( R ( <. z , X >. ( comp ` C ) Y ) f ) ) = ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` f ) ) )
40 1 2 37 12 22 28 24 26 34 38 funcco 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( z G Y ) ` ( R ( <. z , X >. ( comp ` C ) Y ) g ) ) = ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` g ) ) )
41 39 40 eqeq12d 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( ( z G Y ) ` ( R ( <. z , X >. ( comp ` C ) Y ) f ) ) = ( ( z G Y ) ` ( R ( <. z , X >. ( comp ` C ) Y ) g ) ) <-> ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` f ) ) = ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` g ) ) ) )
42 3 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> F ( C Faith D ) G )
43 19 simpld 
 |-  ( ph -> C e. Cat )
44 43 adantr 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> C e. Cat )
45 1 2 37 44 28 24 26 32 38 catcocl 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( R ( <. z , X >. ( comp ` C ) Y ) f ) e. ( z H Y ) )
46 1 2 37 44 28 24 26 34 38 catcocl 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( R ( <. z , X >. ( comp ` C ) Y ) g ) e. ( z H Y ) )
47 1 2 11 42 28 26 45 46 fthi 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( ( z G Y ) ` ( R ( <. z , X >. ( comp ` C ) Y ) f ) ) = ( ( z G Y ) ` ( R ( <. z , X >. ( comp ` C ) Y ) g ) ) <-> ( R ( <. z , X >. ( comp ` C ) Y ) f ) = ( R ( <. z , X >. ( comp ` C ) Y ) g ) ) )
48 41 47 bitr3d 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` f ) ) = ( ( ( X G Y ) ` R ) ( <. ( F ` z ) , ( F ` X ) >. ( comp ` D ) ( F ` Y ) ) ( ( z G X ) ` g ) ) <-> ( R ( <. z , X >. ( comp ` C ) Y ) f ) = ( R ( <. z , X >. ( comp ` C ) Y ) g ) ) )
49 1 2 11 42 28 24 32 34 fthi 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( ( z G X ) ` f ) = ( ( z G X ) ` g ) <-> f = g ) )
50 36 48 49 3bitr3d 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( R ( <. z , X >. ( comp ` C ) Y ) f ) = ( R ( <. z , X >. ( comp ` C ) Y ) g ) <-> f = g ) )
51 50 biimpd 
 |-  ( ( ph /\ ( z e. B /\ f e. ( z H X ) /\ g e. ( z H X ) ) ) -> ( ( R ( <. z , X >. ( comp ` C ) Y ) f ) = ( R ( <. z , X >. ( comp ` C ) Y ) g ) -> f = g ) )
52 51 ralrimivvva 
 |-  ( ph -> A. z e. B A. f e. ( z H X ) A. g e. ( z H X ) ( ( R ( <. z , X >. ( comp ` C ) Y ) f ) = ( R ( <. z , X >. ( comp ` C ) Y ) g ) -> f = g ) )
53 1 2 37 7 43 4 5 ismon2 
 |-  ( ph -> ( R e. ( X M Y ) <-> ( R e. ( X H Y ) /\ A. z e. B A. f e. ( z H X ) A. g e. ( z H X ) ( ( R ( <. z , X >. ( comp ` C ) Y ) f ) = ( R ( <. z , X >. ( comp ` C ) Y ) g ) -> f = g ) ) ) )
54 6 52 53 mpbir2and 
 |-  ( ph -> R e. ( X M Y ) )