let A be Category; :: thesis: for F being Contravariant_Functor of A, Functors A,(EnsHom A) st Obj F is one-to-one & F is faithful holds
F is one-to-one
let F be Contravariant_Functor of A, Functors A,(EnsHom A); :: thesis: ( Obj F is one-to-one & F is faithful implies F is one-to-one )
assume A1:
Obj F is one-to-one
; :: thesis: ( not F is faithful or F is one-to-one )
assume A2:
F is faithful
; :: thesis: F is one-to-one
for x1, x2 being set st x1 in dom F & x2 in dom F & F . x1 = F . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom F & x2 in dom F & F . x1 = F . x2 implies x1 = x2 )
assume A3:
(
x1 in dom F &
x2 in dom F &
F . x1 = F . x2 )
;
:: thesis: x1 = x2
then reconsider m1 =
x1,
m2 =
x2 as
Morphism of
A by FUNCT_2:def 1;
A4:
m1 is
Morphism of
dom m1,
cod m1
by CAT_1:22;
set o1 =
dom m1;
set o2 =
cod m1;
A5:
m2 is
Morphism of
dom m2,
cod m2
by CAT_1:22;
set o3 =
dom m2;
set o4 =
cod m2;
reconsider m2' =
m2 as
Morphism of
dom m2,
cod m2 by CAT_1:22;
A6:
Hom (dom m1),
(cod m1) <> {}
by CAT_1:19;
(Obj F) . (dom m1) =
cod (F . m2')
by A3, OPPCAT_1:33
.=
(Obj F) . (dom m2)
by OPPCAT_1:33
;
then A7:
dom m1 = dom m2
by A1, FUNCT_2:25;
(Obj F) . (cod m1) =
dom (F . m2')
by A3, OPPCAT_1:33
.=
(Obj F) . (cod m2)
by OPPCAT_1:33
;
then
m2 is
Morphism of
dom m1,
cod m1
by A1, A5, A7, FUNCT_2:25;
hence
x1 = x2
by A2, A3, A4, A6, Def6;
:: thesis: verum
end;
hence
F is one-to-one
by FUNCT_1:def 8; :: thesis: verum