let x1, x2 be set ; for C being Category
for c being Object of C
for i1, i2 being Morphism of C st x1 <> x2 holds
( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )
let C be Category; for c being Object of C
for i1, i2 being Morphism of C st x1 <> x2 holds
( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )
let c be Object of C; for i1, i2 being Morphism of C st x1 <> x2 holds
( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )
let i1, i2 be Morphism of C; ( x1 <> x2 implies ( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) ) )
set F = (x1,x2) --> (i1,i2);
set I = {x1,x2};
assume A1:
x1 <> x2
; ( c is_a_coproduct_wrt i1,i2 iff c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )
thus
( c is_a_coproduct_wrt i1,i2 implies c is_a_coproduct_wrt (x1,x2) --> (i1,i2) )
( c is_a_coproduct_wrt (x1,x2) --> (i1,i2) implies c is_a_coproduct_wrt i1,i2 )proof
assume A2:
c is_a_coproduct_wrt i1,
i2
;
c is_a_coproduct_wrt (x1,x2) --> (i1,i2)
then
(
cod i1 = c &
cod i2 = c )
;
hence
(
x1,
x2)
--> (
i1,
i2) is
Injections_family of
c,
{x1,x2}
by Th65;
CAT_3:def 17 for d being Object of C
for F9 being Injections_family of d,{x1,x2} st doms ((x1,x2) --> (i1,i2)) = doms F9 holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )
let b be
Object of
C;
for F9 being Injections_family of b,{x1,x2} st doms ((x1,x2) --> (i1,i2)) = doms F9 holds
ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )let F9 be
Injections_family of
b,
{x1,x2};
( doms ((x1,x2) --> (i1,i2)) = doms F9 implies ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) ) )
assume A3:
doms ((x1,x2) --> (i1,i2)) = doms F9
;
ex h being Morphism of C st
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )
set f =
F9 /. x1;
set g =
F9 /. x2;
A4:
x1 in {x1,x2}
by TARSKI:def 2;
then
(doms ((x1,x2) --> (i1,i2))) /. x1 = dom (((x1,x2) --> (i1,i2)) /. x1)
by Def1;
then
dom (F9 /. x1) = dom (((x1,x2) --> (i1,i2)) /. x1)
by A3, A4, Def1;
then A5:
dom (F9 /. x1) = dom i1
by A1, Th3;
A6:
x2 in {x1,x2}
by TARSKI:def 2;
then
(doms ((x1,x2) --> (i1,i2))) /. x2 = dom (((x1,x2) --> (i1,i2)) /. x2)
by Def1;
then
dom (F9 /. x2) = dom (((x1,x2) --> (i1,i2)) /. x2)
by A3, A6, Def1;
then A7:
dom (F9 /. x2) = dom i2
by A1, Th3;
cod (F9 /. x2) = b
by A6, Th62;
then A8:
F9 /. x2 in Hom (
(dom i2),
b)
by A7;
cod (F9 /. x1) = b
by A4, Th62;
then
F9 /. x1 in Hom (
(dom i1),
b)
by A5;
then consider h being
Morphism of
C such that A9:
h in Hom (
c,
b)
and A10:
for
k being
Morphism of
C st
k in Hom (
c,
b) holds
( (
k (*) i1 = F9 /. x1 &
k (*) i2 = F9 /. x2 ) iff
h = k )
by A2, A8;
take
h
;
( h in Hom (c,b) & ( for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) ) )
thus
h in Hom (
c,
b)
by A9;
for k being Morphism of C st k in Hom (c,b) holds
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k )
let k be
Morphism of
C;
( k in Hom (c,b) implies ( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k ) )
assume A11:
k in Hom (
c,
b)
;
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k )
thus
( ( for
x being
set st
x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) implies
h = k )
( h = k implies for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )proof
assume A12:
for
x being
set st
x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x
;
h = k
then
k (*) (((x1,x2) --> (i1,i2)) /. x2) = F9 /. x2
by A6;
then A13:
k (*) i2 = F9 /. x2
by A1, Th3;
k (*) (((x1,x2) --> (i1,i2)) /. x1) = F9 /. x1
by A4, A12;
then
k (*) i1 = F9 /. x1
by A1, Th3;
hence
h = k
by A10, A11, A13;
verum
end;
assume
h = k
;
for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x
then A14:
(
k (*) i1 = F9 /. x1 &
k (*) i2 = F9 /. x2 )
by A10, A11;
let x be
set ;
( x in {x1,x2} implies k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )
assume
x in {x1,x2}
;
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x
then
(
x = x1 or
x = x2 )
by TARSKI:def 2;
hence
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x
by A1, A14, Th3;
verum
end;
assume A15:
c is_a_coproduct_wrt (x1,x2) --> (i1,i2)
; c is_a_coproduct_wrt i1,i2
then A16:
(x1,x2) --> (i1,i2) is Injections_family of c,{x1,x2}
;
x2 in {x1,x2}
by TARSKI:def 2;
then A17:
cod (((x1,x2) --> (i1,i2)) /. x2) = c
by A16, Th62;
x1 in {x1,x2}
by TARSKI:def 2;
then
cod (((x1,x2) --> (i1,i2)) /. x1) = c
by A16, Th62;
hence
( cod i1 = c & cod i2 = c )
by A1, A17, Th3; CAT_3:def 18 for d being Object of C
for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) )
let d be Object of C; for f, g being Morphism of C st f in Hom ((dom i1),d) & g in Hom ((dom i2),d) holds
ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) )
let f, g be Morphism of C; ( f in Hom ((dom i1),d) & g in Hom ((dom i2),d) implies ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) ) )
assume that
A18:
f in Hom ((dom i1),d)
and
A19:
g in Hom ((dom i2),d)
; ex h being Morphism of C st
( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) )
( cod f = d & cod g = d )
by A18, A19, CAT_1:1;
then reconsider F9 = (x1,x2) --> (f,g) as Injections_family of d,{x1,x2} by Th65;
doms ((x1,x2) --> (i1,i2)) =
(x1,x2) --> ((dom i1),(dom i2))
by Th6
.=
(x1,x2) --> ((dom f),(dom i2))
by A18, CAT_1:1
.=
(x1,x2) --> ((dom f),(dom g))
by A19, CAT_1:1
.=
doms F9
by Th6
;
then consider h being Morphism of C such that
A20:
h in Hom (c,d)
and
A21:
for k being Morphism of C st k in Hom (c,d) holds
( ( for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x ) iff h = k )
by A15;
take
h
; ( h in Hom (c,d) & ( for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) ) )
thus
h in Hom (c,d)
by A20; for k being Morphism of C st k in Hom (c,d) holds
( ( k (*) i1 = f & k (*) i2 = g ) iff h = k )
let k be Morphism of C; ( k in Hom (c,d) implies ( ( k (*) i1 = f & k (*) i2 = g ) iff h = k ) )
assume A22:
k in Hom (c,d)
; ( ( k (*) i1 = f & k (*) i2 = g ) iff h = k )
thus
( k (*) i1 = f & k (*) i2 = g implies h = k )
( h = k implies ( k (*) i1 = f & k (*) i2 = g ) )proof
assume A23:
(
k (*) i1 = f &
k (*) i2 = g )
;
h = k
now for x being set st x in {x1,x2} holds
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. xlet x be
set ;
( x in {x1,x2} implies k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x )assume
x in {x1,x2}
;
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. xthen
(
x = x1 or
x = x2 )
by TARSKI:def 2;
then
( (
((x1,x2) --> (i1,i2)) /. x = i1 &
F9 /. x = f ) or (
((x1,x2) --> (i1,i2)) /. x = i2 &
F9 /. x = g ) )
by A1, Th3;
hence
k (*) (((x1,x2) --> (i1,i2)) /. x) = F9 /. x
by A23;
verum end;
hence
h = k
by A21, A22;
verum
end;
assume A24:
h = k
; ( k (*) i1 = f & k (*) i2 = g )
x2 in {x1,x2}
by TARSKI:def 2;
then
k (*) (((x1,x2) --> (i1,i2)) /. x2) = F9 /. x2
by A21, A22, A24;
then A25:
k (*) (((x1,x2) --> (i1,i2)) /. x2) = g
by A1, Th3;
x1 in {x1,x2}
by TARSKI:def 2;
then
k (*) (((x1,x2) --> (i1,i2)) /. x1) = F9 /. x1
by A21, A22, A24;
then
k (*) (((x1,x2) --> (i1,i2)) /. x1) = f
by A1, Th3;
hence
( k (*) i1 = f & k (*) i2 = g )
by A1, A25, Th3; verum