let X, Y be set ; :: thesis: ( id (X \/ Y) = (id X) \/ (id Y) & id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
thus id (X \/ Y) = (id X) \/ (id Y) :: thesis: ( id (X /\ Y) = (id X) /\ (id Y) & id (X \ Y) = (id X) \ (id Y) )
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in id (X \/ Y) or [x,y] in (id X) \/ (id Y) ) & ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) ) )
thus ( [x,y] in id (X \/ Y) implies [x,y] in (id X) \/ (id Y) ) :: thesis: ( not [x,y] in (id X) \/ (id Y) or [x,y] in id (X \/ Y) )
proof
assume A1: [x,y] in id (X \/ Y) ; :: thesis: [x,y] in (id X) \/ (id Y)
then x in X \/ Y by RELAT_1:def 10;
then A2: ( x in X or x in Y ) by XBOOLE_0:def 3;
x = y by A1, RELAT_1:def 10;
then ( [x,y] in id X or [x,y] in id Y ) by A2, RELAT_1:def 10;
hence [x,y] in (id X) \/ (id Y) by XBOOLE_0:def 3; :: thesis: verum
end;
assume [x,y] in (id X) \/ (id Y) ; :: thesis: [x,y] in id (X \/ Y)
then A3: ( [x,y] in id X or [x,y] in id Y ) by XBOOLE_0:def 3;
then ( x in X or x in Y ) by RELAT_1:def 10;
then A4: x in X \/ Y by XBOOLE_0:def 3;
x = y by A3, RELAT_1:def 10;
hence [x,y] in id (X \/ Y) by A4, RELAT_1:def 10; :: thesis: verum
end;
thus id (X /\ Y) = (id X) /\ (id Y) :: thesis: id (X \ Y) = (id X) \ (id Y)
proof
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in id (X /\ Y) or [x,y] in (id X) /\ (id Y) ) & ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) ) )
thus ( [x,y] in id (X /\ Y) implies [x,y] in (id X) /\ (id Y) ) :: thesis: ( not [x,y] in (id X) /\ (id Y) or [x,y] in id (X /\ Y) )
proof
assume A5: [x,y] in id (X /\ Y) ; :: thesis: [x,y] in (id X) /\ (id Y)
then A6: x in X /\ Y by RELAT_1:def 10;
A7: x = y by A5, RELAT_1:def 10;
x in Y by A6, XBOOLE_0:def 4;
then A8: [x,y] in id Y by A7, RELAT_1:def 10;
x in X by A6, XBOOLE_0:def 4;
then [x,y] in id X by A7, RELAT_1:def 10;
hence [x,y] in (id X) /\ (id Y) by A8, XBOOLE_0:def 4; :: thesis: verum
end;
assume A9: [x,y] in (id X) /\ (id Y) ; :: thesis: [x,y] in id (X /\ Y)
then A10: [x,y] in id X by XBOOLE_0:def 4;
then A11: x = y by RELAT_1:def 10;
[x,y] in id Y by A9, XBOOLE_0:def 4;
then A12: x in Y by RELAT_1:def 10;
x in X by A10, RELAT_1:def 10;
then x in X /\ Y by A12, XBOOLE_0:def 4;
hence [x,y] in id (X /\ Y) by A11, RELAT_1:def 10; :: thesis: verum
end;
let x, y be object ; :: according to RELAT_1:def 2 :: thesis: ( ( not [x,y] in id (X \ Y) or [x,y] in (id X) \ (id Y) ) & ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) ) )
thus ( [x,y] in id (X \ Y) implies [x,y] in (id X) \ (id Y) ) :: thesis: ( not [x,y] in (id X) \ (id Y) or [x,y] in id (X \ Y) )
proof
assume A13: [x,y] in id (X \ Y) ; :: thesis: [x,y] in (id X) \ (id Y)
then A14: x in X \ Y by RELAT_1:def 10;
then not x in Y by XBOOLE_0:def 5;
then A15: not [x,y] in id Y by RELAT_1:def 10;
x = y by A13, RELAT_1:def 10;
then [x,y] in id X by A14, RELAT_1:def 10;
hence [x,y] in (id X) \ (id Y) by A15, XBOOLE_0:def 5; :: thesis: verum
end;
assume A16: [x,y] in (id X) \ (id Y) ; :: thesis: [x,y] in id (X \ Y)
then A17: x = y by RELAT_1:def 10;
not [x,y] in id Y by A16, XBOOLE_0:def 5;
then A18: ( not x in Y or not x = y ) by RELAT_1:def 10;
x in X by A16, RELAT_1:def 10;
then x in X \ Y by A16, A18, RELAT_1:def 10, XBOOLE_0:def 5;
hence [x,y] in id (X \ Y) by A17, RELAT_1:def 10; :: thesis: verum