Metamath Proof Explorer

Theorem setcmon

Description: A monomorphism of sets is an injection. (Contributed by Mario Carneiro, 3-Jan-2017)

Ref Expression
Hypotheses setcmon.c 
|- C = ( SetCat ` U )
setcmon.u 
|- ( ph -> U e. V )
setcmon.x 
|- ( ph -> X e. U )
setcmon.y 
|- ( ph -> Y e. U )
setcmon.h 
|- M = ( Mono ` C )
Assertion setcmon 
|- ( ph -> ( F e. ( X M Y ) <-> F : X -1-1-> Y ) )

Proof

Step Hyp Ref Expression
1 setcmon.c 
 |-  C = ( SetCat ` U )
2 setcmon.u 
 |-  ( ph -> U e. V )
3 setcmon.x 
 |-  ( ph -> X e. U )
4 setcmon.y 
 |-  ( ph -> Y e. U )
5 setcmon.h 
 |-  M = ( Mono ` C )
6 eqid 
 |-  ( Base ` C ) = ( Base ` C )
7 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
8 eqid 
 |-  ( comp ` C ) = ( comp ` C )
9 1 setccat 
 |-  ( U e. V -> C e. Cat )
10 2 9 syl 
 |-  ( ph -> C e. Cat )
11 1 2 setcbas 
 |-  ( ph -> U = ( Base ` C ) )
12 3 11 eleqtrd 
 |-  ( ph -> X e. ( Base ` C ) )
13 4 11 eleqtrd 
 |-  ( ph -> Y e. ( Base ` C ) )
14 6 7 8 5 10 12 13 monhom 
 |-  ( ph -> ( X M Y ) C_ ( X ( Hom ` C ) Y ) )
15 14 sselda 
 |-  ( ( ph /\ F e. ( X M Y ) ) -> F e. ( X ( Hom ` C ) Y ) )
16 1 2 7 3 4 elsetchom 
 |-  ( ph -> ( F e. ( X ( Hom ` C ) Y ) <-> F : X --> Y ) )
17 16 biimpa 
 |-  ( ( ph /\ F e. ( X ( Hom ` C ) Y ) ) -> F : X --> Y )
18 15 17 syldan 
 |-  ( ( ph /\ F e. ( X M Y ) ) -> F : X --> Y )
19 simprr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
20 19 sneqd 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> { ( F ` x ) } = { ( F ` y ) } )
21 20 xpeq2d 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( X X. { ( F ` x ) } ) = ( X X. { ( F ` y ) } ) )
22 18 adantr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> F : X --> Y )
23 22 ffnd 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> F Fn X )
24 simprll 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> x e. X )
25 fcoconst 
 |-  ( ( F Fn X /\ x e. X ) -> ( F o. ( X X. { x } ) ) = ( X X. { ( F ` x ) } ) )
26 23 24 25 syl2anc 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F o. ( X X. { x } ) ) = ( X X. { ( F ` x ) } ) )
27 simprlr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> y e. X )
28 fcoconst 
 |-  ( ( F Fn X /\ y e. X ) -> ( F o. ( X X. { y } ) ) = ( X X. { ( F ` y ) } ) )
29 23 27 28 syl2anc 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F o. ( X X. { y } ) ) = ( X X. { ( F ` y ) } ) )
30 21 26 29 3eqtr4d 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F o. ( X X. { x } ) ) = ( F o. ( X X. { y } ) ) )
31 2 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> U e. V )
32 3 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> X e. U )
33 4 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> Y e. U )
34 fconst6g 
 |-  ( x e. X -> ( X X. { x } ) : X --> X )
35 24 34 syl 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( X X. { x } ) : X --> X )
36 1 31 8 32 32 33 35 22 setcco 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F ( <. X , X >. ( comp ` C ) Y ) ( X X. { x } ) ) = ( F o. ( X X. { x } ) ) )
37 fconst6g 
 |-  ( y e. X -> ( X X. { y } ) : X --> X )
38 27 37 syl 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( X X. { y } ) : X --> X )
39 1 31 8 32 32 33 38 22 setcco 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F ( <. X , X >. ( comp ` C ) Y ) ( X X. { y } ) ) = ( F o. ( X X. { y } ) ) )
40 30 36 39 3eqtr4d 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F ( <. X , X >. ( comp ` C ) Y ) ( X X. { x } ) ) = ( F ( <. X , X >. ( comp ` C ) Y ) ( X X. { y } ) ) )
41 10 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> C e. Cat )
42 12 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> X e. ( Base ` C ) )
43 13 ad2antrr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> Y e. ( Base ` C ) )
44 simplr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> F e. ( X M Y ) )
45 1 31 7 32 32 elsetchom 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( ( X X. { x } ) e. ( X ( Hom ` C ) X ) <-> ( X X. { x } ) : X --> X ) )
46 35 45 mpbird 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( X X. { x } ) e. ( X ( Hom ` C ) X ) )
47 1 31 7 32 32 elsetchom 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( ( X X. { y } ) e. ( X ( Hom ` C ) X ) <-> ( X X. { y } ) : X --> X ) )
48 38 47 mpbird 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( X X. { y } ) e. ( X ( Hom ` C ) X ) )
49 6 7 8 5 41 42 43 42 44 46 48 moni 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( ( F ( <. X , X >. ( comp ` C ) Y ) ( X X. { x } ) ) = ( F ( <. X , X >. ( comp ` C ) Y ) ( X X. { y } ) ) <-> ( X X. { x } ) = ( X X. { y } ) ) )
50 40 49 mpbid 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( X X. { x } ) = ( X X. { y } ) )
51 50 fveq1d 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( ( X X. { x } ) ` x ) = ( ( X X. { y } ) ` x ) )
52 vex 
 |-  x e. _V
53 52 fvconst2 
 |-  ( x e. X -> ( ( X X. { x } ) ` x ) = x )
54 24 53 syl 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( ( X X. { x } ) ` x ) = x )
55 vex 
 |-  y e. _V
56 55 fvconst2 
 |-  ( x e. X -> ( ( X X. { y } ) ` x ) = y )
57 24 56 syl 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( ( X X. { y } ) ` x ) = y )
58 51 54 57 3eqtr3d 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( ( x e. X /\ y e. X ) /\ ( F ` x ) = ( F ` y ) ) ) -> x = y )
59 58 expr 
 |-  ( ( ( ph /\ F e. ( X M Y ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
60 59 ralrimivva 
 |-  ( ( ph /\ F e. ( X M Y ) ) -> A. x e. X A. y e. X ( ( F ` x ) = ( F ` y ) -> x = y ) )
61 dff13 
 |-  ( F : X -1-1-> Y <-> ( F : X --> Y /\ A. x e. X A. y e. X ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
62 18 60 61 sylanbrc 
 |-  ( ( ph /\ F e. ( X M Y ) ) -> F : X -1-1-> Y )
63 f1f 
 |-  ( F : X -1-1-> Y -> F : X --> Y )
64 16 biimpar 
 |-  ( ( ph /\ F : X --> Y ) -> F e. ( X ( Hom ` C ) Y ) )
65 63 64 sylan2 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> F e. ( X ( Hom ` C ) Y ) )
66 11 adantr 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> U = ( Base ` C ) )
67 66 eleq2d 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> ( z e. U <-> z e. ( Base ` C ) ) )
68 2 ad2antrr 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> U e. V )
69 simprl 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> z e. U )
70 3 ad2antrr 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> X e. U )
71 4 ad2antrr 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> Y e. U )
72 simprrl 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> g e. ( z ( Hom ` C ) X ) )
73 1 68 7 69 70 elsetchom 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( g e. ( z ( Hom ` C ) X ) <-> g : z --> X ) )
74 72 73 mpbid 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> g : z --> X )
75 63 ad2antlr 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> F : X --> Y )
76 1 68 8 69 70 71 74 75 setcco 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F o. g ) )
77 simprrr 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> h e. ( z ( Hom ` C ) X ) )
78 1 68 7 69 70 elsetchom 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( h e. ( z ( Hom ` C ) X ) <-> h : z --> X ) )
79 77 78 mpbid 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> h : z --> X )
80 1 68 8 69 70 71 79 75 setcco 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( F ( <. z , X >. ( comp ` C ) Y ) h ) = ( F o. h ) )
81 76 80 eqeq12d 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) <-> ( F o. g ) = ( F o. h ) ) )
82 simplr 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> F : X -1-1-> Y )
83 cocan1 
 |-  ( ( F : X -1-1-> Y /\ g : z --> X /\ h : z --> X ) -> ( ( F o. g ) = ( F o. h ) <-> g = h ) )
84 82 74 79 83 syl3anc 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( ( F o. g ) = ( F o. h ) <-> g = h ) )
85 84 biimpd 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( ( F o. g ) = ( F o. h ) -> g = h ) )
86 81 85 sylbid 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ ( z e. U /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) ) -> ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
87 86 anassrs 
 |-  ( ( ( ( ph /\ F : X -1-1-> Y ) /\ z e. U ) /\ ( g e. ( z ( Hom ` C ) X ) /\ h e. ( z ( Hom ` C ) X ) ) ) -> ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
88 87 ralrimivva 
 |-  ( ( ( ph /\ F : X -1-1-> Y ) /\ z e. U ) -> A. g e. ( z ( Hom ` C ) X ) A. h e. ( z ( Hom ` C ) X ) ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
89 88 ex 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> ( z e. U -> A. g e. ( z ( Hom ` C ) X ) A. h e. ( z ( Hom ` C ) X ) ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) ) )
90 67 89 sylbird 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> ( z e. ( Base ` C ) -> A. g e. ( z ( Hom ` C ) X ) A. h e. ( z ( Hom ` C ) X ) ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) ) )
91 90 ralrimiv 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> A. z e. ( Base ` C ) A. g e. ( z ( Hom ` C ) X ) A. h e. ( z ( Hom ` C ) X ) ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) )
92 6 7 8 5 10 12 13 ismon2 
 |-  ( ph -> ( F e. ( X M Y ) <-> ( F e. ( X ( Hom ` C ) Y ) /\ A. z e. ( Base ` C ) A. g e. ( z ( Hom ` C ) X ) A. h e. ( z ( Hom ` C ) X ) ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) ) ) )
93 92 adantr 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> ( F e. ( X M Y ) <-> ( F e. ( X ( Hom ` C ) Y ) /\ A. z e. ( Base ` C ) A. g e. ( z ( Hom ` C ) X ) A. h e. ( z ( Hom ` C ) X ) ( ( F ( <. z , X >. ( comp ` C ) Y ) g ) = ( F ( <. z , X >. ( comp ` C ) Y ) h ) -> g = h ) ) ) )
94 65 91 93 mpbir2and 
 |-  ( ( ph /\ F : X -1-1-> Y ) -> F e. ( X M Y ) )
95 62 94 impbida 
 |-  ( ph -> ( F e. ( X M Y ) <-> F : X -1-1-> Y ) )