let X be non empty with_non-empty_elements set ; :: thesis: for o1, o2 being object of (EnsCat X) st <^o1,o2^> <> {} holds
for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let o1, o2 be object of (EnsCat X); :: thesis: ( <^o1,o2^> <> {} implies for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto ) )
assume A1: <^o1,o2^> <> {} ; :: thesis: for A being Morphism of o1,o2
for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let A be Morphism of o1,o2; :: thesis: for F being Function of o1,o2 st F = A holds
( A is epi iff F is onto )
let F be Function of o1,o2; :: thesis: ( F = A implies ( A is epi iff F is onto ) )
assume A2: F = A ; :: thesis: ( A is epi iff F is onto )
per cases ( for x being set st x in X holds
x is trivial or ex x being set st
( x in X & not x is trivial ) ) ;
suppose A3: for x being set st x in X holds
x is trivial ; :: thesis: ( A is epi iff F is onto )
thus ( A is epi implies F is onto ) :: thesis: ( F is onto implies A is epi )thus ( F is onto implies A is epi ) :: thesis: verum
proof
assume A10: F is onto ; :: thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def 8 :: thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A11: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
then A12: <^o1,o^> <> {} by A1, ALTCAT_1:def 4;
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
A13: <^o2,o^> = Funcs o2,o by ALTCAT_1:def 16;
then consider B1 being Function such that
A14: B1 = B and
A15: dom B1 = o2 and
rng B1 c= o by A11, FUNCT_2:def 2;
consider C1 being Function such that
A16: C1 = C and
A17: dom C1 = o2 and
rng C1 c= o by A11, A13, FUNCT_2:def 2;
assume B * A = C * A ; :: thesis: B = C
then A18: B1 * F = C * A by A1, A2, A11, A14, A12, ALTCAT_1:18
.= C1 * F by A1, A2, A11, A16, A12, ALTCAT_1:18 ;
now
assume B1 <> C1 ; :: thesis: contradiction
then consider z being set such that
A19: z in o2 and
A20: B1 . z <> C1 . z by A15, A17, FUNCT_1:9;
z in rng F by A10, A19, FUNCT_2:def 3;
then consider x being set such that
A21: x in dom F and
A22: F . x = z by FUNCT_1:def 5;
B1 . (F . x) = (B1 * F) . x by A21, FUNCT_1:23;
hence contradiction by A18, A20, A21, A22, FUNCT_1:23; :: thesis: verum
end;
hence B = C by A14, A16; :: thesis: verum
end;
end;
suppose A23: ex x being set st
( x in X & not x is trivial ) ; :: thesis: ( A is epi iff F is onto )
now
per cases ( o2 <> {} or o2 = {} ) ;
suppose A24: o2 <> {} ; :: thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) )
consider o being set such that
A25: o in X and
A26: not o is trivial by A23;
reconsider o = o as object of (EnsCat X) by A25, ALTCAT_1:def 16;
A27: dom F = o1 by A24, FUNCT_2:def 1;
thus ( A is epi implies F is onto ) :: thesis: ( F is onto implies A is epi )
proof
consider k being Element of o;
A28: rng F c= o2 by RELAT_1:def 19;
reconsider ok = o \ {k} as non empty set by A26, REALSET1:4;
assume that
A29: A is epi and
A30: not F is onto ; :: thesis: contradiction
rng F <> o2 by A30, FUNCT_2:def 3;
then not o2 c= rng F by A28, XBOOLE_0:def 10;
then consider y being set such that
A31: y in o2 and
A32: not y in rng F by TARSKI:def 3;
set C = o2 --> k;
A33: dom (o2 --> k) = o2 by FUNCOP_1:19;
A34: o <> {} by A25;
then A35: k in o ;
rng (o2 --> k) c= o
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (o2 --> k) or y in o )
assume y in rng (o2 --> k) ; :: thesis: y in o
then ex x being set st
( x in dom (o2 --> k) & (o2 --> k) . x = y ) by FUNCT_1:def 5;
hence y in o by A35, A33, FUNCOP_1:13; :: thesis: verum
end;
then o2 --> k in Funcs o2,o by A33, FUNCT_2:def 2;
then reconsider C1 = o2 --> k as Morphism of o2,o by ALTCAT_1:def 16;
consider l being Element of ok;
A36: not l in {k} by XBOOLE_0:def 5;
reconsider l = l as Element of o by XBOOLE_0:def 5;
A37: k <> l by A36, TARSKI:def 1;
deffunc H1( set ) -> Element of o = IFEQ $1,y,l,k;
consider B being Function such that
A38: dom B = o2 and
A39: for x being set st x in o2 holds
B . x = H1(x) from FUNCT_1:sch 3();
 A40: dom (B * F) = o1 by A27, A28, A38, RELAT_1:46;
A41: rng B c= o
proof
let y1 be set ; :: according to TARSKI:def 3 :: thesis: ( not y1 in rng B or y1 in o )
assume y1 in rng B ; :: thesis: y1 in o
then consider x being set such that
A42: ( x in dom B & B . x = y1 ) by FUNCT_1:def 5;
per cases ( x = y or x <> y ) ;
suppose A43: x = y ; :: thesis: y1 in o
y1 = IFEQ x,y,l,k by A38, A39, A42
.= l by A43, FUNCOP_1:def 8 ;
hence y1 in o by A34; :: thesis: verum
end;
suppose A44: x <> y ; :: thesis: y1 in o
y1 = IFEQ x,y,l,k by A38, A39, A42
.= k by A44, FUNCOP_1:def 8 ;
hence y1 in o by A34; :: thesis: verum
end;
end;
end;
then A45: B in Funcs o2,o by A38, FUNCT_2:def 2;
then A46: B in <^o2,o^> by ALTCAT_1:def 16;
reconsider B1 = B as Morphism of o2,o by A45, ALTCAT_1:def 16;
for z being set st z in rng (B * F) holds
z in rng B by FUNCT_1:25;
then rng (B * F) c= rng B by TARSKI:def 3;
then rng (B * F) c= o by A41, XBOOLE_1:1;
then B * F in Funcs o1,o by A40, FUNCT_2:def 2;
then A47: B * F in <^o1,o^> by ALTCAT_1:def 16;
B . y = IFEQ y,y,l,k by A31, A39
.= l by FUNCOP_1:def 8 ;
then A48: not B = o2 --> k by A31, A37, FUNCOP_1:13;
A49: dom ((o2 --> k) * F) = o1 by A27, A28, A33, RELAT_1:46;
now
let z be set ; :: thesis: ( z in o1 implies (B * F) . z = ((o2 --> k) * F) . z )
assume A50: z in o1 ; :: thesis: (B * F) . z = ((o2 --> k) * F) . z
then A51: F . z in rng F by A27, FUNCT_1:def 5;
then A52: B . (F . z) = IFEQ (F . z),y,l,k by A28, A39
.= k by A32, A51, FUNCOP_1:def 8 ;
thus (B * F) . z = B . (F . z) by A40, A50, FUNCT_1:22
.= (o2 --> k) . (F . z) by A28, A51, A52, FUNCOP_1:13
.= ((o2 --> k) * F) . z by A49, A50, FUNCT_1:22 ; :: thesis: verum
end;
then B * F = (o2 --> k) * F by A40, A49, FUNCT_1:9;
then B1 * A = (o2 --> k) * F by A1, A2, A46, A47, ALTCAT_1:18
.= C1 * A by A1, A2, A46, A47, ALTCAT_1:18 ;
hence contradiction by A29, A48, A46, Def8; :: thesis: verum
end;
thus ( F is onto implies A is epi ) :: thesis: verum
proof
assume A53: F is onto ; :: thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def 8 :: thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A54: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
then A55: <^o1,o^> <> {} by A1, ALTCAT_1:def 4;
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
A56: <^o2,o^> = Funcs o2,o by ALTCAT_1:def 16;
then consider B1 being Function such that
A57: B1 = B and
A58: dom B1 = o2 and
rng B1 c= o by A54, FUNCT_2:def 2;
consider C1 being Function such that
A59: C1 = C and
A60: dom C1 = o2 and
rng C1 c= o by A54, A56, FUNCT_2:def 2;
assume B * A = C * A ; :: thesis: B = C
then A61: B1 * F = C * A by A1, A2, A54, A57, A55, ALTCAT_1:18
.= C1 * F by A1, A2, A54, A59, A55, ALTCAT_1:18 ;
now
assume B1 <> C1 ; :: thesis: contradiction
then consider z being set such that
A62: z in o2 and
A63: B1 . z <> C1 . z by A58, A60, FUNCT_1:9;
z in rng F by A53, A62, FUNCT_2:def 3;
then consider x being set such that
A64: x in dom F and
A65: F . x = z by FUNCT_1:def 5;
B1 . (F . x) = (B1 * F) . x by A64, FUNCT_1:23;
hence contradiction by A61, A63, A64, A65, FUNCT_1:23; :: thesis: verum
end;
hence B = C by A57, A59; :: thesis: verum
end;
end;
suppose A66: o2 = {} ; :: thesis: ( ( A is epi implies F is onto ) & ( F is onto implies A is epi ) )
then F = {} ;
hence ( A is epi implies F is onto ) by A66, FUNCT_2:def 3, RELAT_1:60; :: thesis: ( F is onto implies A is epi )
thus ( F is onto implies A is epi ) :: thesis: verum
proof
assume F is onto ; :: thesis: A is epi
let o be object of (EnsCat X); :: according to ALTCAT_3:def 8 :: thesis: ( <^o2,o^> <> {} implies for B, C being Morphism of o2,o st B * A = C * A holds
B = C )
assume A67: <^o2,o^> <> {} ; :: thesis: for B, C being Morphism of o2,o st B * A = C * A holds
B = C
let B, C be Morphism of o2,o; :: thesis: ( B * A = C * A implies B = C )
A68: <^o2,o^> = Funcs o2,o by ALTCAT_1:def 16;
then consider B1 being Function such that
A69: B1 = B and
A70: dom B1 = o2 and
rng B1 c= o by A67, FUNCT_2:def 2;
A71: ex C1 being Function st
( C1 = C & dom C1 = o2 & rng C1 c= o ) by A67, A68, FUNCT_2:def 2;
assume B * A = C * A ; :: thesis: B = C
B1 = {} by A66, A70, RELAT_1:64;
hence B = C by A66, A69, A71, RELAT_1:64; :: thesis: verum
end;
end;
end;
end;
hence ( A is epi iff F is onto ) ; :: thesis: verum
end;
end;