let A, B be category; ( A,B are_opposite implies for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso ) )
assume A1:
A,B are_opposite
; for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
let a, b be Object of A; ( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso ) )
assume that
A2:
<^a,b^> <> {}
and
A3:
<^b,a^> <> {}
; for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
let a9, b9 be Object of B; ( a9 = a & b9 = b implies for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso ) )
assume that
A4:
a9 = a
and
A5:
b9 = b
; for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
A6:
<^b9,a9^> = <^a,b^>
by A1, A4, A5, Th9;
A7:
<^a9,b9^> = <^b,a^>
by A1, A4, A5, Th9;
now for A, B being category st A,B are_opposite holds
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso let A,
B be
category;
( A,B are_opposite implies for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso )assume A8:
A,
B are_opposite
;
for a, b being Object of A st <^a,b^> <> {} & <^b,a^> <> {} holds
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso let a,
b be
Object of
A;
( <^a,b^> <> {} & <^b,a^> <> {} implies for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso )assume that A9:
<^a,b^> <> {}
and A10:
<^b,a^> <> {}
;
for a9, b9 being Object of B st a9 = a & b9 = b holds
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso let a9,
b9 be
Object of
B;
( a9 = a & b9 = b implies for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso )assume that A11:
a9 = a
and A12:
b9 = b
;
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso let f be
Morphism of
a,
b;
for f9 being Morphism of b9,a9 st f9 = f & f is iso holds
f9 is iso let f9 be
Morphism of
b9,
a9;
( f9 = f & f is iso implies f9 is iso )assume A13:
f9 = f
;
( f is iso implies f9 is iso )assume A14:
f is
iso
;
f9 is iso then A15:
f * (f ") = idm b
;
A16:
(f ") * f = idm a
by A14;
(
f is
retraction &
f is
coretraction )
by A14, ALTCAT_3:5;
then A17:
f9 " = f "
by A8, A9, A10, A11, A12, A13, Th22;
A18:
idm a = idm a9
by A8, A11, Th10;
A19:
idm b = idm b9
by A8, A12, Th10;
A20:
f9 * (f9 ") = idm a9
by A8, A9, A10, A11, A12, A13, A16, A17, A18, Th9;
(f9 ") * f9 = idm b9
by A8, A9, A10, A11, A12, A13, A15, A17, A19, Th9;
hence
f9 is
iso
by A20;
verum end;
hence
for f being Morphism of a,b
for f9 being Morphism of b9,a9 st f9 = f holds
( f is iso iff f9 is iso )
by A1, A2, A3, A4, A5, A6, A7; verum