let R be Relation; :: thesis: ( R is antisymmetric iff R /\ (R ~) c= id (dom R) )
A1: now :: thesis: ( R is antisymmetric implies R /\ (R ~) c= id (dom R) )
assume R is antisymmetric ; :: thesis: R /\ (R ~) c= id (dom R)
then A2: R is_antisymmetric_in field R ;
now :: thesis: for a, b being object st [a,b] in R /\ (R ~) holds
[a,b] in id (dom R)
let a, b be object ; :: thesis: ( [a,b] in R /\ (R ~) implies [a,b] in id (dom R) )
assume A3: [a,b] in R /\ (R ~) ; :: thesis: [a,b] in id (dom R)
then [a,b] in R ~ by XBOOLE_0:def 4;
then A4: [b,a] in R by RELAT_1:def 7;
then A5: b in dom R by XTUPLE_0:def 12;
A6: [a,b] in R by A3, XBOOLE_0:def 4;
then ( a in field R & b in field R ) by RELAT_1:15;
then a = b by A2, A6, A4;
hence [a,b] in id (dom R) by A5, RELAT_1:def 10; :: thesis: verum
end;
hence R /\ (R ~) c= id (dom R) ; :: thesis: verum
end;
now :: thesis: ( R /\ (R ~) c= id (dom R) implies R is antisymmetric )
assume A7: R /\ (R ~) c= id (dom R) ; :: thesis: R is antisymmetric
now :: thesis: for a, b being object st a in field R & b in field R & [a,b] in R & [b,a] in R holds
a = b
let a, b be object ; :: thesis: ( a in field R & b in field R & [a,b] in R & [b,a] in R implies a = b )
assume that
a in field R and
b in field R and
A8: [a,b] in R and
A9: [b,a] in R ; :: thesis: a = b
[a,b] in R ~ by A9, RELAT_1:def 7;
then [a,b] in R /\ (R ~) by A8, XBOOLE_0:def 4;
hence a = b by A7, RELAT_1:def 10; :: thesis: verum
end;
hence R is antisymmetric by Def4; :: thesis: verum
end;
hence ( R is antisymmetric iff R /\ (R ~) c= id (dom R) ) by A1; :: thesis: verum