set F = Yoneda A;
for x1, x2 being object st x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) & (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 implies x1 = x2 )
assume that
A1: ( x1 in dom (Obj (Yoneda A)) & x2 in dom (Obj (Yoneda A)) ) and
A2: (Obj (Yoneda A)) . x1 = (Obj (Yoneda A)) . x2 ; :: thesis: x1 = x2
reconsider c = x1, c1 = x2 as Object of A by A1, FUNCT_2:def 1;
reconsider f = id c1 as Morphism of c1,c1 ;
<|c1,?> in Funct (A,(EnsHom A)) by CAT_2:def 2;
then reconsider d1 = <|c1,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def 17;
<|c,?> in Funct (A,(EnsHom A)) by CAT_2:def 2;
then reconsider d = <|c,?> as Object of (Functors (A,(EnsHom A))) by NATTRA_1:def 17;
(Yoneda A) . (id c1) = id d1
proof
set X = dom <|(id c1),?>;
A3: for y being object st y in dom <|(id c1),?> holds
<|(id c1),?> . y = (id <|c1,?>) . y
proof
let y be object ; :: thesis: ( y in dom <|(id c1),?> implies <|(id c1),?> . y = (id <|c1,?>) . y )
assume y in dom <|(id c1),?> ; :: thesis: <|(id c1),?> . y = (id <|c1,?>) . y
then reconsider z = y as Object of A by FUNCT_2:def 1;
reconsider zz = id z as Morphism of z,z ;
A4: Hom (z,z) <> {} ;
<|(id c1),?> . z = [[(Hom ((cod (id c1)),z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))] by Def3
.= [[(Hom (c1,z)),(Hom ((dom (id c1)),z))],(hom ((id c1),(id z)))]
.= [[(Hom (c1,z)),(Hom (c1,z))],(hom ((id c1),(id z)))]
.= [[(Hom (c1,z)),(Hom (c1,z))],(hom (c1,(id z)))] by ENS_1:53
.= [[(Hom (c1,z)),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))]
.= [[(Hom (c1,(dom (id z)))),(Hom (c1,(cod (id z))))],(hom (c1,(id z)))]
.= <|c1,?> . (id z) by ENS_1:def 21
.= <|c1,?> /. zz by A4, CAT_3:def 10
.= id (<|c1,?> . z) by NATTRA_1:15
.= (id <|c1,?>) . z by NATTRA_1:20
.= (id <|c1,?>) . z by NATTRA_1:def 5 ;
hence <|(id c1),?> . y = (id <|c1,?>) . y by NATTRA_1:def 5; :: thesis: verum
end;
dom <|(id c1),?> = the carrier of A by FUNCT_2:def 1
.= dom (id <|c1,?>) by FUNCT_2:def 1 ;
then A5: <|(id c1),?> = id <|c1,?> by A3, FUNCT_1:2;
(Yoneda A) . (id c1) = [[<|(cod (id c1)),?>,<|(dom (id c1)),?>],<|(id c1),?>] by Def4
.= [[<|c1,?>,<|(dom (id c1)),?>],<|(id c1),?>]
.= [[<|c1,?>,<|c1,?>],(id <|c1,?>)] by A5
.= id d1 by NATTRA_1:def 17 ;
hence (Yoneda A) . (id c1) = id d1 ; :: thesis: verum
end;
then A6: (Obj (Yoneda A)) . c1 = d1 by OPPCAT_1:30;
(Yoneda A) . (id c) = id d
proof
set X = dom <|(id c),?>;
A7: for y being object st y in dom <|(id c),?> holds
<|(id c),?> . y = (id <|c,?>) . y
proof
let y be object ; :: thesis: ( y in dom <|(id c),?> implies <|(id c),?> . y = (id <|c,?>) . y )
assume y in dom <|(id c),?> ; :: thesis: <|(id c),?> . y = (id <|c,?>) . y
then reconsider z = y as Object of A by FUNCT_2:def 1;
reconsider zz = id z as Morphism of z,z ;
A8: Hom (z,z) <> {} ;
<|(id c),?> . z = [[(Hom ((cod (id c)),z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))] by Def3
.= [[(Hom (c,z)),(Hom ((dom (id c)),z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom ((id c),(id z)))]
.= [[(Hom (c,z)),(Hom (c,z))],(hom (c,(id z)))] by ENS_1:53
.= [[(Hom (c,z)),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= [[(Hom (c,(dom (id z)))),(Hom (c,(cod (id z))))],(hom (c,(id z)))]
.= <|c,?> . (id z) by ENS_1:def 21
.= <|c,?> /. zz by A8, CAT_3:def 10
.= id (<|c,?> . z) by NATTRA_1:15
.= (id <|c,?>) . z by NATTRA_1:20
.= (id <|c,?>) . z by NATTRA_1:def 5 ;
hence <|(id c),?> . y = (id <|c,?>) . y by NATTRA_1:def 5; :: thesis: verum
end;
dom <|(id c),?> = the carrier of A by FUNCT_2:def 1
.= dom (id <|c,?>) by FUNCT_2:def 1 ;
then A9: <|(id c),?> = id <|c,?> by A7, FUNCT_1:2;
(Yoneda A) . (id c) = [[<|(cod (id c)),?>,<|(dom (id c)),?>],<|(id c),?>] by Def4
.= [[<|c,?>,<|(dom (id c)),?>],<|(id c),?>]
.= [[<|c,?>,<|c,?>],(id <|c,?>)] by A9
.= id d by NATTRA_1:def 17 ;
hence (Yoneda A) . (id c) = id d ; :: thesis: verum
end;
then (Obj (Yoneda A)) . c = d by OPPCAT_1:30;
then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = (hom?- c1) . f by A2, A6, ENS_1:def 21;
then [[(Hom (c,(dom f))),(Hom (c,(cod f)))],(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] by ENS_1:def 21;
then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [[(Hom (c1,(dom f))),(Hom (c1,(cod f)))],(hom (c1,f))] ;
then [(Hom (c,(dom f))),(Hom (c,(cod f))),(hom (c,f))] = [(Hom (c1,(dom f))),(Hom (c1,(cod f))),(hom (c1,f))] ;
then Hom (c,(dom f)) = Hom (c1,(dom f)) by XTUPLE_0:3;
then Hom (c,(dom f)) = Hom (c1,c1) ;
then A10: Hom (c,c1) = Hom (c1,c1) ;
id c1 in Hom (c1,c1) by CAT_1:27;
then reconsider h = id c1 as Morphism of c,c1 by A10, CAT_1:def 5;
dom h = c by A10, CAT_1:5;
hence x1 = x2 ; :: thesis: verum
end;
then Obj (Yoneda A) is one-to-one by FUNCT_1:def 4;
hence Yoneda A is one-to-one by Th5; :: thesis: verum