let C be Category; :: thesis: for b, c being Object of C st Hom (b,c) <> {} holds

for f being Morphism of b,c holds

( f opp is epi iff f is monic )

let b, c be Object of C; :: thesis: ( Hom (b,c) <> {} implies for f being Morphism of b,c holds

( f opp is epi iff f is monic ) )

assume A1: Hom (b,c) <> {} ; :: thesis: for f being Morphism of b,c holds

( f opp is epi iff f is monic )

let f be Morphism of b,c; :: thesis: ( f opp is epi iff f is monic )

thus ( f opp is epi implies f is monic ) :: thesis: ( f is monic implies f opp is epi )

A6: Hom (b,c) <> {} and

A7: for a being Object of C st Hom (a,b) <> {} holds

for f1, f2 being Morphism of a,b st f * f1 = f * f2 holds

f1 = f2 ; :: according to CAT_1:def 14 :: thesis: f opp is epi

thus Hom ((c opp),(b opp)) <> {} by A6, Th4; :: according to CAT_1:def 15 :: thesis: for b_{1} being Element of the carrier of (C opp) holds

( Hom ((b opp),b_{1}) = {} or for b_{2}, b_{3} being Morphism of b opp ,b_{1} holds

( not b_{2} * (f opp) = b_{3} * (f opp) or b_{2} = b_{3} ) )

let a be Object of (C opp); :: thesis: ( Hom ((b opp),a) = {} or for b_{1}, b_{2} being Morphism of b opp ,a holds

( not b_{1} * (f opp) = b_{2} * (f opp) or b_{1} = b_{2} ) )

assume A8: Hom ((b opp),a) <> {} ; :: thesis: for b_{1}, b_{2} being Morphism of b opp ,a holds

( not b_{1} * (f opp) = b_{2} * (f opp) or b_{1} = b_{2} )

let g1, g2 be Morphism of b opp ,a; :: thesis: ( not g1 * (f opp) = g2 * (f opp) or g1 = g2 )

assume A9: g1 * (f opp) = g2 * (f opp) ; :: thesis: g1 = g2

Hom ((b opp),a) = Hom ((opp a),(opp (b opp))) by Th5

.= Hom ((opp a),b) ;

then ( opp g1 in Hom ((opp a),b) & opp g2 in Hom ((opp a),b) ) by A8, CAT_1:def 5;

then reconsider f1 = opp g1, f2 = opp g2 as Morphism of opp a,b by CAT_1:def 5;

A10: Hom ((opp a),(opp (b opp))) <> {} by A8, Th5;

f * f1 = (f1 opp) * (f opp) by A6, Lm3, A10

.= g2 * (f opp) by A9, Def6, A10

.= (f2 opp) * (f opp) by Def6, A10

.= f * f2 by A6, Lm3, A10 ;

hence g1 = g2 by A7, A10; :: thesis: verum

for f being Morphism of b,c holds

( f opp is epi iff f is monic )

let b, c be Object of C; :: thesis: ( Hom (b,c) <> {} implies for f being Morphism of b,c holds

( f opp is epi iff f is monic ) )

assume A1: Hom (b,c) <> {} ; :: thesis: for f being Morphism of b,c holds

( f opp is epi iff f is monic )

let f be Morphism of b,c; :: thesis: ( f opp is epi iff f is monic )

thus ( f opp is epi implies f is monic ) :: thesis: ( f is monic implies f opp is epi )

proof

assume that
assume that

Hom ((c opp),(b opp)) <> {} and

A2: for a being Object of (C opp) st Hom ((b opp),a) <> {} holds

for g1, g2 being Morphism of b opp ,a st g1 * (f opp) = g2 * (f opp) holds

g1 = g2 ; :: according to CAT_1:def 15 :: thesis: f is monic

thus Hom (b,c) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b_{1} being Element of the carrier of C holds

( Hom (b_{1},b) = {} or for b_{2}, b_{3} being Morphism of b_{1},b holds

( not f * b_{2} = f * b_{3} or b_{2} = b_{3} ) )

let a be Object of C; :: thesis: ( Hom (a,b) = {} or for b_{1}, b_{2} being Morphism of a,b holds

( not f * b_{1} = f * b_{2} or b_{1} = b_{2} ) )

assume A3: Hom (a,b) <> {} ; :: thesis: for b_{1}, b_{2} being Morphism of a,b holds

( not f * b_{1} = f * b_{2} or b_{1} = b_{2} )

let f1, f2 be Morphism of a,b; :: thesis: ( not f * f1 = f * f2 or f1 = f2 )

assume A4: f * f1 = f * f2 ; :: thesis: f1 = f2

reconsider g1 = f1 opp , g2 = f2 opp as Morphism of b opp ,a opp ;

A5: Hom ((b opp),(a opp)) <> {} by A3, Th4;

g1 * (f opp) = f * f1 by Lm3, A1, A3

.= g2 * (f opp) by Lm3, A1, A3, A4 ;

then g1 = g2 by A2, A5;

hence f1 = g2 by Def6, A3

.= f2 by Def6, A3 ;

:: thesis: verum

end;Hom ((c opp),(b opp)) <> {} and

A2: for a being Object of (C opp) st Hom ((b opp),a) <> {} holds

for g1, g2 being Morphism of b opp ,a st g1 * (f opp) = g2 * (f opp) holds

g1 = g2 ; :: according to CAT_1:def 15 :: thesis: f is monic

thus Hom (b,c) <> {} by A1; :: according to CAT_1:def 14 :: thesis: for b

( Hom (b

( not f * b

let a be Object of C; :: thesis: ( Hom (a,b) = {} or for b

( not f * b

assume A3: Hom (a,b) <> {} ; :: thesis: for b

( not f * b

let f1, f2 be Morphism of a,b; :: thesis: ( not f * f1 = f * f2 or f1 = f2 )

assume A4: f * f1 = f * f2 ; :: thesis: f1 = f2

reconsider g1 = f1 opp , g2 = f2 opp as Morphism of b opp ,a opp ;

A5: Hom ((b opp),(a opp)) <> {} by A3, Th4;

g1 * (f opp) = f * f1 by Lm3, A1, A3

.= g2 * (f opp) by Lm3, A1, A3, A4 ;

then g1 = g2 by A2, A5;

hence f1 = g2 by Def6, A3

.= f2 by Def6, A3 ;

:: thesis: verum

A6: Hom (b,c) <> {} and

A7: for a being Object of C st Hom (a,b) <> {} holds

for f1, f2 being Morphism of a,b st f * f1 = f * f2 holds

f1 = f2 ; :: according to CAT_1:def 14 :: thesis: f opp is epi

thus Hom ((c opp),(b opp)) <> {} by A6, Th4; :: according to CAT_1:def 15 :: thesis: for b

( Hom ((b opp),b

( not b

let a be Object of (C opp); :: thesis: ( Hom ((b opp),a) = {} or for b

( not b

assume A8: Hom ((b opp),a) <> {} ; :: thesis: for b

( not b

let g1, g2 be Morphism of b opp ,a; :: thesis: ( not g1 * (f opp) = g2 * (f opp) or g1 = g2 )

assume A9: g1 * (f opp) = g2 * (f opp) ; :: thesis: g1 = g2

Hom ((b opp),a) = Hom ((opp a),(opp (b opp))) by Th5

.= Hom ((opp a),b) ;

then ( opp g1 in Hom ((opp a),b) & opp g2 in Hom ((opp a),b) ) by A8, CAT_1:def 5;

then reconsider f1 = opp g1, f2 = opp g2 as Morphism of opp a,b by CAT_1:def 5;

A10: Hom ((opp a),(opp (b opp))) <> {} by A8, Th5;

f * f1 = (f1 opp) * (f opp) by A6, Lm3, A10

.= g2 * (f opp) by A9, Def6, A10

.= (f2 opp) * (f opp) by Def6, A10

.= f * f2 by A6, Lm3, A10 ;

hence g1 = g2 by A7, A10; :: thesis: verum