:: The Operation of Addition of Relational Structures
:: by Katarzyna Romanowicz and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ORDERS_2, PARTFUN1, STRUCT_0, FINSEQ_1, RELAT_1,
TARSKI, RELAT_2, SUBSET_1, XXREAL_0, LATTICE3, WAYBEL_0, EQREL_1,
LATTICES;
notations XBOOLE_0, TARSKI, SUBSET_1, RELSET_1, RELAT_2, STRUCT_0, ORDERS_2,
YELLOW_0, WAYBEL_0, LATTICE3;
constructors LATTICE3, WAYBEL_0, RELSET_1;
registrations XBOOLE_0, RELSET_1, STRUCT_0, WAYBEL_0;
requirements SUBSET, BOOLE;
definitions RELAT_2;
expansions RELAT_2;
theorems ZFMISC_1, RELAT_1, RELSET_1, ORDERS_2, XBOOLE_0, XBOOLE_1, WAYBEL_0,
YELLOW_0, YELLOW_5;
begin
theorem
for x, y, A, B being set st x in A \/ B & y in A \/ B holds x in A \ B
& y in A \ B or x in B & y in B or x in A \ B & y in B or x in B & y in A \ B
proof
let x, y, A, B be set;
assume
A1: x in A \/ B & y in A \/ B;
A \/ B = (A \ B) \/ B by XBOOLE_1:39;
hence thesis by A1,XBOOLE_0:def 3;
end;
definition
let R, S be RelStr;
pred R tolerates S means
for x, y being set st x in (the carrier of R
) /\ (the carrier of S) & y in (the carrier of R) /\ (the carrier of S) holds [
x, y] in the InternalRel of R iff [x,y] in the InternalRel of S;
end;
begin
definition
let R, S be RelStr; :: Wronski Sum Operation
func R [*] S -> strict RelStr means
:Def2:
the carrier of it = (the carrier
of R) \/ (the carrier of S) & the InternalRel of it = (the InternalRel of R) \/
(the InternalRel of S) \/ ((the InternalRel of R) * the InternalRel of S);
existence
proof
set X = (the carrier of R) \/ (the carrier of S);
the carrier of R c= X & the carrier of S c= X by XBOOLE_1:7;
then reconsider
G = (the InternalRel of R) * the InternalRel of S as Relation
of X by RELSET_1:7;
the carrier of R c= X & the carrier of S c= X by XBOOLE_1:7;
then reconsider IR = the InternalRel of R, IS = the InternalRel of S as
Relation of X by RELSET_1:7;
set F = IR \/ IS \/ G;
reconsider F as Relation of X;
take RelStr (# X, F #);
thus thesis;
end;
uniqueness;
end;
registration
let R be RelStr, S be non empty RelStr;
cluster R [*] S -> non empty;
coherence
proof
(the carrier of R) \/ (the carrier of S) <> {};
hence thesis by Def2;
end;
end;
registration
let R be non empty RelStr, S be RelStr;
cluster R [*] S -> non empty;
coherence
proof
(the carrier of R) \/ (the carrier of S) <> {};
hence thesis by Def2;
end;
end;
theorem Th2:
for R, S being RelStr holds the InternalRel of R c= the
InternalRel of R [*] S & the InternalRel of S c= the InternalRel of R [*] S
proof
let R, S be RelStr;
the InternalRel of R c= (the InternalRel of R) \/ (the InternalRel of S)
& ( the InternalRel of R) \/ (the InternalRel of S) c= (the InternalRel of R)
\/ ( the InternalRel of S) \/ ((the InternalRel of R) * the InternalRel of S)
by XBOOLE_1:7;
then
the InternalRel of R c= (the InternalRel of R) \/ (the InternalRel of S)
\/ ((the InternalRel of R) * the InternalRel of S) by XBOOLE_1:1;
hence the InternalRel of R c= the InternalRel of R [*] S by Def2;
the InternalRel of S c= (the InternalRel of R) \/ (the InternalRel of S)
& ( the InternalRel of R) \/ (the InternalRel of S) c= (the InternalRel of R)
\/ ( the InternalRel of S) \/ ((the InternalRel of R) * the InternalRel of S)
by XBOOLE_1:7;
then
the InternalRel of S c= (the InternalRel of R) \/ (the InternalRel of S)
\/ ((the InternalRel of R) * the InternalRel of S) by XBOOLE_1:1;
hence thesis by Def2;
end;
theorem Th3:
for R, S being RelStr st R is reflexive & S is reflexive holds R
[*] S is reflexive
proof
let R, S be RelStr;
assume R is reflexive & S is reflexive;
then
A1: the InternalRel of R is_reflexive_in the carrier of R & the InternalRel
of S is_reflexive_in the carrier of S by ORDERS_2:def 2;
A2: the InternalRel of R c= the InternalRel of R [*] S & the InternalRel of
S c= the InternalRel of R [*] S by Th2;
the InternalRel of R [*] S is_reflexive_in the carrier of R [*] S
proof
let x be object;
assume x in the carrier of R [*] S;
then x in (the carrier of R) \/ (the carrier of S) by Def2;
then x in the carrier of R or x in the carrier of S by XBOOLE_0:def 3;
then
[x,x] in the InternalRel of R or [x,x] in the InternalRel of S by A1;
hence thesis by A2;
end;
hence thesis by ORDERS_2:def 2;
end;
begin
theorem Th4: :: theorem 3.1 (vii)
for R, S being RelStr, a, b being set st [a,b] in the InternalRel
of R [*] S & a in the carrier of R & b in the carrier of R & R tolerates S & R
is transitive holds [a,b] in the InternalRel of R
proof
let R, S be RelStr, a, b be set;
assume that
A1: [a,b] in the InternalRel of R [*] S and
A2: a in the carrier of R and
A3: b in the carrier of R and
A4: R tolerates S and
A5: R is transitive;
[a,b] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by A1,Def2;
then
A6: [a,b] in (the InternalRel of R) \/ (the InternalRel of S) or [a,b] in ((
the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
assume
A7: not [a,b] in the InternalRel of R;
per cases by A7,A6,XBOOLE_0:def 3;
suppose
A8: [a,b] in the InternalRel of S;
then b in the carrier of S by ZFMISC_1:87;
then
A9: b in (the carrier of R) /\ (the carrier of S) by A3,XBOOLE_0:def 4;
a in the carrier of S by A8,ZFMISC_1:87;
then a in (the carrier of R) /\ (the carrier of S) by A2,XBOOLE_0:def 4;
hence thesis by A4,A7,A8,A9;
end;
suppose
A10: [a,b] in ((the InternalRel of R) * the InternalRel of S);
then b in the carrier of S by ZFMISC_1:87;
then
A11: b in (the carrier of R) /\ (the carrier of S) by A3,XBOOLE_0:def 4;
A12: the InternalRel of R is_transitive_in the carrier of R by A5,
ORDERS_2:def 3;
consider z being object such that
A13: [a,z] in the InternalRel of R and
A14: [z,b] in the InternalRel of S by A10,RELAT_1:def 8;
A15: z in the carrier of R by A13,ZFMISC_1:87;
z in the carrier of S by A14,ZFMISC_1:87;
then z in (the carrier of R) /\ (the carrier of S) by A15,XBOOLE_0:def 4;
then [z,b] in the InternalRel of R by A4,A11,A14;
hence thesis by A2,A3,A7,A13,A15,A12;
end;
end;
theorem Th5: :: theorem 3.1 (viii)
for R, S being RelStr, a, b being set st [a,b] in the InternalRel
of R [*] S & a in the carrier of S & b in the carrier of S & R tolerates S & S
is transitive holds [a,b] in the InternalRel of S
proof
let R, S be RelStr, a, b be set;
assume that
A1: [a,b] in the InternalRel of R [*] S and
A2: a in the carrier of S and
A3: b in the carrier of S and
A4: R tolerates S and
A5: S is transitive;
[a,b] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by A1,Def2;
then
A6: [a,b] in (the InternalRel of R) \/ (the InternalRel of S) or [a,b] in ((
the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
assume
A7: not [a,b] in the InternalRel of S;
per cases by A7,A6,XBOOLE_0:def 3;
suppose
A8: [a,b] in the InternalRel of R;
then b in the carrier of R by ZFMISC_1:87;
then
A9: b in (the carrier of R) /\ (the carrier of S) by A3,XBOOLE_0:def 4;
a in the carrier of R by A8,ZFMISC_1:87;
then a in (the carrier of R) /\ (the carrier of S) by A2,XBOOLE_0:def 4;
hence thesis by A4,A7,A8,A9;
end;
suppose
A10: [a,b] in ((the InternalRel of R) * the InternalRel of S);
then a in the carrier of R by ZFMISC_1:87;
then
A11: a in (the carrier of R) /\ (the carrier of S) by A2,XBOOLE_0:def 4;
A12: the InternalRel of S is_transitive_in the carrier of S by A5,
ORDERS_2:def 3;
consider z being object such that
A13: [a,z] in the InternalRel of R and
A14: [z,b] in the InternalRel of S by A10,RELAT_1:def 8;
A15: z in the carrier of S by A14,ZFMISC_1:87;
z in the carrier of R by A13,ZFMISC_1:87;
then z in (the carrier of R) /\ (the carrier of S) by A15,XBOOLE_0:def 4;
then [a,z] in the InternalRel of S by A4,A11,A13;
hence thesis by A2,A3,A7,A14,A15,A12;
end;
end;
theorem Th6: :: a version of 3.1 (vii, viii - left to right)
for R, S being RelStr, a, b being object holds ([a,b] in the
InternalRel of R implies [a,b] in the InternalRel of R [*] S) & ([a,b] in the
InternalRel of S implies [a,b] in the InternalRel of R [*] S)
proof
let R, S be RelStr, a, b be object;
thus [a,b] in the InternalRel of R implies [a,b] in the InternalRel of R [*]
S
proof
assume [a,b] in the InternalRel of R;
then [a,b] in (the InternalRel of R) \/ (the InternalRel of S) by
XBOOLE_0:def 3;
then [a,b] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
assume [a,b] in the InternalRel of S;
then [a,b] in (the InternalRel of R) \/ (the InternalRel of S) by
XBOOLE_0:def 3;
then [a,b] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
theorem
for R, S being non empty RelStr, x being Element of R [*] S holds x in
the carrier of R or x in (the carrier of S) \ (the carrier of R)
proof
let R, S be non empty RelStr, x be Element of R [*] S;
x in the carrier of R [*] S;
then x in (the carrier of S) \/ (the carrier of R) by Def2;
then
x in (the carrier of R) \/ ((the carrier of S) \ (the carrier of R)) by
XBOOLE_1:39;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th8: :: theorem 3.1 (vii)
for R, S being non empty RelStr for x, y being Element of R, a, b
being Element of R [*] S st x = a & y = b & R tolerates S & R is transitive
holds x <= y iff a <= b
proof
let R, S be non empty RelStr, x, y be Element of R, a, b be Element of R [*]
S;
assume
A1: x = a & y = b;
assume
A2: R tolerates S & R is transitive;
hereby
assume x <= y;
then [x,y] in the InternalRel of R by ORDERS_2:def 5;
then [a,b] in the InternalRel of R [*] S by A1,Th6;
hence a <= b by ORDERS_2:def 5;
end;
assume a <= b;
then [a,b] in the InternalRel of R [*] S by ORDERS_2:def 5;
then [x,y] in the InternalRel of R by A1,A2,Th4;
hence thesis by ORDERS_2:def 5;
end;
theorem Th9: :: theorem 3.1 (viii)
for R, S being non empty RelStr, a, b being Element of R [*] S, c
, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
a <= b iff c <= d
proof
let R, S be non empty RelStr, a, b be Element of R [*] S, c, d be Element of
S;
assume that
A1: a = c & b = d and
A2: R tolerates S & S is transitive;
hereby
assume a <= b;
then [a,b] in the InternalRel of R [*] S by ORDERS_2:def 5;
then [c,d] in the InternalRel of S by A1,A2,Th5;
hence c <= d by ORDERS_2:def 5;
end;
assume c <= d;
then [c,d] in the InternalRel of S by ORDERS_2:def 5;
then [a,b] in the InternalRel of R [*] S by A1,Th6;
hence thesis by ORDERS_2:def 5;
end;
theorem Th10:
for R, S being antisymmetric reflexive transitive with_suprema
non empty RelStr for x being set st x in the carrier of R holds x is Element
of R [*] S
proof
let R, S be antisymmetric reflexive transitive with_suprema non empty
RelStr;
let x be set;
assume x in the carrier of R;
then x in (the carrier of R) \/ (the carrier of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
theorem
for R, S being antisymmetric reflexive transitive with_suprema non
empty RelStr for x being set st x in the carrier of S holds x is Element of R
[*] S
proof
let R, S be antisymmetric reflexive transitive with_suprema non empty
RelStr;
let x be set;
assume x in the carrier of S;
then x in (the carrier of R) \/ (the carrier of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
theorem Th12:
for R, S being non empty RelStr for x being set st x in (the
carrier of R) /\ (the carrier of S) holds x is Element of R
proof
let R, S be non empty RelStr;
let x be set;
assume
A1: x in (the carrier of R) /\ (the carrier of S);
(the carrier of R) /\ (the carrier of S) c= the carrier of R by XBOOLE_1:17;
hence thesis by A1;
end;
theorem Th13:
for R, S being non empty RelStr for x being set st x in (the
carrier of R) /\ (the carrier of S) holds x is Element of S
proof
let R, S be non empty RelStr;
let x be set;
assume
A1: x in (the carrier of R) /\ (the carrier of S);
(the carrier of R) /\ (the carrier of S) c= the carrier of S by XBOOLE_1:17;
hence thesis by A1;
end;
theorem
for R, S being antisymmetric reflexive transitive with_suprema non
empty RelStr for x, y being Element of R [*] S st x in the carrier of R & y in
the carrier of S & R tolerates S holds x <= y iff (ex a being Element of R [*]
S st a in (the carrier of R) /\ (the carrier of S) & x <= a & a <= y)
proof
let R, S be antisymmetric reflexive transitive with_suprema non empty
RelStr, x, y be Element of R [*] S;
assume that
A1: x in the carrier of R and
A2: y in the carrier of S and
A3: R tolerates S;
per cases;
suppose
A4: [x,y] in the InternalRel of R;
hereby
assume
A5: x <= y;
take a = y;
y in the carrier of R by A4,ZFMISC_1:87;
hence a in (the carrier of R) /\ (the carrier of S) by A2,XBOOLE_0:def 4;
R [*] S is reflexive by Th3;
hence x <= a & a <= y by A5,ORDERS_2:1;
end;
[x,y] in the InternalRel of R [*] S by A4,Th6;
hence thesis by ORDERS_2:def 5;
end;
suppose
A6: [x,y] in the InternalRel of S;
hereby
assume
A7: x <= y;
take a = x;
x in the carrier of S by A6,ZFMISC_1:87;
hence a in (the carrier of R) /\ (the carrier of S) by A1,XBOOLE_0:def 4;
R [*] S is reflexive by Th3;
hence x <= a & a <= y by A7,ORDERS_2:1;
end;
[x,y] in the InternalRel of R [*] S by A6,Th6;
hence thesis by ORDERS_2:def 5;
end;
suppose that
A8: ( not [x,y] in the InternalRel of R)& not [x,y] in the InternalRel of S;
hereby
assume x <= y;
then [x,y] in the InternalRel of R [*] S by ORDERS_2:def 5;
then [x,y] in (the InternalRel of R) \/ (the InternalRel of S) \/ (the
InternalRel of R) * the InternalRel of S by Def2;
then [x,y] in (the InternalRel of R) \/ (the InternalRel of S) or [x,y]
in (the InternalRel of R) * the InternalRel of S by XBOOLE_0:def 3;
then consider z being object such that
A9: [x,z] in the InternalRel of R and
A10: [z,y] in the InternalRel of S by A8,RELAT_1:def 8,XBOOLE_0:def 3;
A11: z in the carrier of R by A9,ZFMISC_1:87;
A12: z in the carrier of S by A10,ZFMISC_1:87;
then z in (the carrier of R) \/ (the carrier of S) by XBOOLE_0:def 3;
then reconsider z as Element of R [*] S by Def2;
take z;
thus z in (the carrier of R) /\ (the carrier of S) by A11,A12,
XBOOLE_0:def 4;
[x,z] in the InternalRel of R [*] S by A9,Th6;
hence x <= z by ORDERS_2:def 5;
[z,y] in the InternalRel of R [*] S by A10,Th6;
hence z <= y by ORDERS_2:def 5;
end;
given a being Element of R [*] S such that
A13: a in (the carrier of R) /\ (the carrier of S) and
A14: x <= a and
A15: a <= y;
reconsider y9 = y, a1 = a as Element of S by A2,A13,Th13;
a1 <= y9 by A3,A15,Th9;
then
A16: [a,y] in the InternalRel of S by ORDERS_2:def 5;
reconsider x9 = x, a9 = a as Element of R by A1,A13,Th12;
x9 <= a9 by A3,A14,Th8;
then [x,a] in the InternalRel of R by ORDERS_2:def 5;
then [x,y] in (the InternalRel of R) * the InternalRel of S by A16,
RELAT_1:def 8;
then [x,y] in (the InternalRel of R) \/ (the InternalRel of S) \/ (the
InternalRel of R) * the InternalRel of S by XBOOLE_0:def 3;
then [x,y] in the InternalRel of R [*] S by Def2;
hence thesis by ORDERS_2:def 5;
end;
end;
theorem Th15:
for R, S being non empty RelStr, a, b being Element of R, c, d
being Element of S st a = c & b = d & R tolerates S & R is transitive & S is
transitive holds a <= b iff c <= d
proof
let R, S be non empty RelStr, a, b be Element of R, c, d be Element of S;
assume that
A1: a = c & b = d and
A2: R tolerates S and
A3: R is transitive and
A4: S is transitive;
a in (the carrier of R) \/ the carrier of S & b in (the carrier of R) \/
the carrier of S by XBOOLE_0:def 3;
then reconsider a9 = a, b9 = b as Element of R [*] S by Def2;
hereby
assume a <= b;
then a9 <= b9 by A2,A3,Th8;
hence c <= d by A1,A2,A4,Th9;
end;
assume c <= d;
then a9 <= b9 by A1,A2,A4,Th9;
hence thesis by A2,A3,Th8;
end;
theorem Th16:
for R being antisymmetric reflexive transitive with_suprema non
empty RelStr, D being lower directed Subset of R for x, y being Element of R
st x in D & y in D holds x "\/" y in D
proof
let R be antisymmetric reflexive transitive with_suprema non empty RelStr,
D be lower directed Subset of R;
let x, y be Element of R;
assume x in D & y in D;
then consider z being Element of R such that
A1: z in D and
A2: x <= z & y <= z by WAYBEL_0:def 1;
x "\/" y <= z by A2,YELLOW_0:22;
hence thesis by A1,WAYBEL_0:def 19;
end;
theorem Th17:
for R, S being RelStr, a, b being set st (the carrier of R) /\ (
the carrier of S) is upper Subset of R & [a,b] in the InternalRel of R [*] S &
a in the carrier of S holds b in the carrier of S
proof
let R, S be RelStr, a, b be set;
set X = (the carrier of R) /\ (the carrier of S);
reconsider X as Subset of R by XBOOLE_1:17;
assume that
A1: (the carrier of R) /\ (the carrier of S) is upper Subset of R and
A2: [a,b] in the InternalRel of R [*] S and
A3: a in the carrier of S;
[a,b] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by A2,Def2;
then
A4: [a,b] in (the InternalRel of R) \/ (the InternalRel of S) or [a,b] in ((
the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
assume
A5: not b in the carrier of S;
per cases by A4,XBOOLE_0:def 3;
suppose
A6: [a,b] in the InternalRel of R;
then reconsider a9 = a, b9 = b as Element of R by ZFMISC_1:87;
a in the carrier of R by A6,ZFMISC_1:87;
then
A7: a in (the carrier of R) /\ the carrier of S by A3,XBOOLE_0:def 4;
a9 <= b9 by A6,ORDERS_2:def 5;
then X c= the carrier of S & b in X by A1,A7,WAYBEL_0:def 20,XBOOLE_1:17;
hence thesis by A5;
end;
suppose
[a,b] in the InternalRel of S;
hence thesis by A5,ZFMISC_1:87;
end;
suppose
[a,b] in (the InternalRel of R) * the InternalRel of S;
hence thesis by A5,ZFMISC_1:87;
end;
end;
theorem Th18: :: theorem 3.1 (xi)
for R, S being RelStr, a, b being Element of R [*] S st (the
carrier of R) /\ (the carrier of S) is upper Subset of R & a <= b & a in the
carrier of S holds b in the carrier of S
proof
let R, S be RelStr, a, b be Element of R [*] S;
assume that
A1: (the carrier of R) /\ (the carrier of S) is upper Subset of R and
A2: a <= b and
A3: a in the carrier of S;
[a,b] in the InternalRel of R [*] S by A2,ORDERS_2:def 5;
hence thesis by A1,A3,Th17;
end;
theorem :: theorem 3.1 (vi)
for R, S being antisymmetric reflexive transitive with_suprema non
empty RelStr for x, y being Element of R, a, b being Element of S st (the
carrier of R) /\ (the carrier of S) is lower directed Subset of S & (the
carrier of R) /\ (the carrier of S) is upper Subset of R & R tolerates S & x =
a & y = b holds x "\/" y = a "\/" b
proof
let R, S be antisymmetric reflexive transitive with_suprema non empty
RelStr;
let x, y be Element of R;
let a, b be Element of S;
assume that
A1: (the carrier of R) /\ (the carrier of S) is lower directed Subset of S and
A2: (the carrier of R) /\ (the carrier of S) is upper Subset of R and
A3: R tolerates S and
A4: x = a and
A5: y = b;
a in (the carrier of R) /\ (the carrier of S) & b in (the carrier of R)
/\ ( the carrier of S) by A4,A5,XBOOLE_0:def 4;
then reconsider xy = a "\/" b as Element of R by A1,Th13,Th16;
a "\/" b >= b by YELLOW_0:22;
then
A6: xy >= y by A3,A5,Th15;
A7: for d being Element of R st d >= x & d >= y holds xy <= d
proof
let d be Element of R;
reconsider X = x, D = d as Element of R [*] S by Th10;
assume that
A8: d >= x and
A9: d >= y;
X <= D by A3,A8,Th8;
then reconsider dd = d as Element of S by A2,A4,Th18;
dd >= a & b <= dd by A3,A4,A5,A8,A9,Th15;
then a "\/" b <= dd by YELLOW_5:9;
hence thesis by A3,Th15;
end;
a "\/" b >= a by YELLOW_0:22;
then xy >= x by A3,A4,Th15;
hence thesis by A6,A7,YELLOW_0:22;
end;
theorem
for R, S being lower-bounded antisymmetric reflexive transitive
with_suprema non empty RelStr st (the carrier of R) /\ (the carrier of S) is
non empty lower directed Subset of S holds Bottom S in the carrier of R
proof
let R, S be lower-bounded antisymmetric reflexive transitive with_suprema
non empty RelStr;
assume
A1: (the carrier of R) /\ (the carrier of S) is non empty lower directed
Subset of S;
then consider x being object such that
A2: x in (the carrier of R) /\ (the carrier of S) by XBOOLE_0:def 1;
reconsider x as Element of S by A2,Th13;
Bottom S <= x by YELLOW_0:44;
then Bottom S in (the carrier of R) /\ (the carrier of S) by A1,A2,
WAYBEL_0:def 19;
hence thesis by XBOOLE_0:def 4;
end;
theorem Th21:
for R, S being RelStr, a, b being set st (the carrier of R) /\ (
the carrier of S) is lower Subset of S & [a,b] in the InternalRel of R [*] S &
b in the carrier of R holds a in the carrier of R
proof
let R, S be RelStr, a, b be set;
set X = (the carrier of R) /\ (the carrier of S);
reconsider X as Subset of R by XBOOLE_1:17;
assume that
A1: (the carrier of R) /\ (the carrier of S) is lower Subset of S and
A2: [a,b] in the InternalRel of R [*] S and
A3: b in the carrier of R;
[a,b] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by A2,Def2;
then
A4: [a,b] in (the InternalRel of R) \/ (the InternalRel of S) or [a,b] in ((
the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
assume
A5: not a in the carrier of R;
per cases by A4,XBOOLE_0:def 3;
suppose
A6: [a,b] in the InternalRel of S;
then reconsider a9 = a, b9 = b as Element of S by ZFMISC_1:87;
b in the carrier of S by A6,ZFMISC_1:87;
then
A7: b in (the carrier of R) /\ the carrier of S by A3,XBOOLE_0:def 4;
a9 <= b9 by A6,ORDERS_2:def 5;
then a in X by A1,A7,WAYBEL_0:def 19;
hence thesis by A5;
end;
suppose
[a,b] in the InternalRel of R;
hence thesis by A5,ZFMISC_1:87;
end;
suppose
[a,b] in (the InternalRel of R) * the InternalRel of S;
hence thesis by A5,ZFMISC_1:87;
end;
end;
theorem :: theorem 1 (ix)
for x, y being set, R, S being RelStr st [x,y] in the InternalRel of R
[*] S & (the carrier of R) /\ (the carrier of S) is upper Subset of R holds x
in the carrier of R & y in the carrier of R or x in the carrier of S & y in the
carrier of S or x in (the carrier of R) \ (the carrier of S) & y in (the
carrier of S) \ (the carrier of R)
proof
let x, y be set, R, S be RelStr;
assume that
A1: [x,y] in the InternalRel of R [*] S and
A2: (the carrier of R) /\ (the carrier of S) is upper Subset of R;
x in the carrier of R [*] S by A1,ZFMISC_1:87;
then
A3: x in (the carrier of R) \/ (the carrier of S) by Def2;
y in the carrier of R [*] S by A1,ZFMISC_1:87;
then
A4: y in (the carrier of R) \/ (the carrier of S) by Def2;
per cases by A3,A4,XBOOLE_0:def 3;
suppose
x in the carrier of R & y in the carrier of R;
hence thesis;
end;
suppose
x in the carrier of S & y in the carrier of S;
hence thesis;
end;
suppose
x in the carrier of R & y in the carrier of S;
hence thesis by XBOOLE_0:def 5;
end;
suppose
x in the carrier of S & y in the carrier of R;
hence thesis by A1,A2,Th17;
end;
end;
theorem :: theorem 3.1 (x)
for R, S being RelStr, a, b being Element of R [*] S st (the carrier
of R) /\ (the carrier of S) is lower Subset of S & a <= b & b in the carrier of
R holds a in the carrier of R
proof
let R, S be RelStr, a, b be Element of R [*] S;
assume that
A1: (the carrier of R) /\ (the carrier of S) is lower Subset of S and
A2: a <= b and
A3: b in the carrier of R;
[a,b] in the InternalRel of R [*] S by A2,ORDERS_2:def 5;
hence thesis by A1,A3,Th21;
end;
theorem :: theorem 3.1 (xii)
for R, S being RelStr st R tolerates S & (the carrier of R) /\ (the
carrier of S) is upper Subset of R & (the carrier of R) /\ (the carrier of S)
is lower Subset of S & R is transitive antisymmetric & S is transitive
antisymmetric holds R [*] S is antisymmetric
proof
let R, S be RelStr;
set X = the carrier of R [*] S, F = the InternalRel of R [*] S;
assume that
A1: R tolerates S and
A2: (the carrier of R) /\ (the carrier of S) is upper Subset of R and
A3: (the carrier of R) /\ (the carrier of S) is lower Subset of S and
A4: R is transitive antisymmetric and
A5: S is transitive antisymmetric;
A6: the InternalRel of S is_antisymmetric_in the carrier of S by A5,
ORDERS_2:def 4;
A7: the InternalRel of R is_antisymmetric_in the carrier of R by A4,
ORDERS_2:def 4;
F is_antisymmetric_in X
proof
let x, y be object;
assume that
A8: x in X & y in X and
A9: [x,y] in F and
A10: [y,x] in F;
A11: x in (the carrier of R) \/ (the carrier of S) & y in (the carrier of
R) \/ ( the carrier of S) by A8,Def2;
per cases by A11,XBOOLE_0:def 3;
suppose
A12: x in the carrier of R & y in the carrier of R;
then
[x,y] in the InternalRel of R & [y,x] in the InternalRel of R by A1,A4,A9
,A10,Th4;
hence thesis by A7,A12;
end;
suppose
A13: x in the carrier of R & y in the carrier of S;
then
A14: y in the carrier of R by A3,A10,Th21;
then
[x,y] in the InternalRel of R & [y,x] in the InternalRel of R by A1,A4,A9
,A10,A13,Th4;
hence thesis by A7,A13,A14;
end;
suppose
A15: x in the carrier of S & y in the carrier of R;
then
A16: y in the carrier of S by A2,A9,Th17;
then
[x,y] in the InternalRel of S & [y,x] in the InternalRel of S by A1,A5,A9
,A10,A15,Th5;
hence thesis by A6,A15,A16;
end;
suppose
A17: x in the carrier of S & y in the carrier of S;
then
[x,y] in the InternalRel of S & [y,x] in the InternalRel of S by A1,A5,A9
,A10,Th5;
hence thesis by A6,A17;
end;
end;
hence thesis by ORDERS_2:def 4;
end;
theorem :: theorem 3.1 (xiii)
for R, S being RelStr st (the carrier of R) /\ (the carrier of S) is
upper Subset of R & (the carrier of R) /\ (the carrier of S) is lower Subset of
S & R tolerates S & R is transitive & S is transitive holds R [*] S is
transitive
proof
let R, S be RelStr;
set X = the carrier of R [*] S, F = the InternalRel of R [*] S;
assume that
A1: (the carrier of R) /\ (the carrier of S) is upper Subset of R and
A2: (the carrier of R) /\ (the carrier of S) is lower Subset of S and
A3: R tolerates S and
A4: R is transitive and
A5: S is transitive;
A6: the InternalRel of S is_transitive_in the carrier of S by A5,ORDERS_2:def 3
;
A7: the InternalRel of R is_transitive_in the carrier of R by A4,ORDERS_2:def 3
;
F is_transitive_in X
proof
let x, y, z be object;
assume that
A8: x in X & y in X and
A9: z in X and
A10: [x,y] in F and
A11: [y,z] in F;
A12: x in (the carrier of R) \/ (the carrier of S) & y in (the carrier of
R) \/ ( the carrier of S) by A8,Def2;
A13: z in (the carrier of R) \/ (the carrier of S) by A9,Def2;
per cases by A12,A13,XBOOLE_0:def 3;
suppose
A14: x in the carrier of R & y in the carrier of R & z in the carrier of R;
then
[x,y] in the InternalRel of R & [y,z] in the InternalRel of R by A3,A4
,A10,A11,Th4;
then [x,z] in the InternalRel of R by A7,A14;
hence thesis by Th6;
end;
suppose
A15: x in the carrier of R & y in the carrier of R & z in the carrier of S;
then
A16: [x,y] in the InternalRel of R by A3,A4,A10,Th4;
[y,z] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by A11,Def2;
then
A17: [y,z] in (the InternalRel of R) \/ (the InternalRel of S) or [y,z]
in ((the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
now
per cases by A17,XBOOLE_0:def 3;
suppose
A18: [y,z] in the InternalRel of R;
then z in the carrier of R by ZFMISC_1:87;
then [x,z] in the InternalRel of R by A7,A15,A16,A18;
hence thesis by Th6;
end;
suppose
[y,z] in the InternalRel of S;
then
[x,z] in ((the InternalRel of R) * the InternalRel of S) by A16,
RELAT_1:def 8;
then
[x,z] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((
the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
suppose
[y,z] in ((the InternalRel of R) * the InternalRel of S);
then consider a being object such that
A19: [y,a] in the InternalRel of R and
A20: [a,z] in the InternalRel of S by RELAT_1:def 8;
a in the carrier of R by A19,ZFMISC_1:87;
then [x,a] in the InternalRel of R by A7,A15,A16,A19;
then
[x,z] in ((the InternalRel of R) * the InternalRel of S) by A20,
RELAT_1:def 8;
then [x,z] in ((the InternalRel of R) \/ (the InternalRel of S)) \/
((the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
end;
hence thesis;
end;
suppose
A21: x in the carrier of R & y in the carrier of S & z in the carrier of R;
then
A22: y in the carrier of R by A2,A11,Th21;
then
[x,y] in the InternalRel of R & [y,z] in the InternalRel of R by A3,A4
,A10,A11,A21,Th4;
then [x,z] in the InternalRel of R by A7,A21,A22;
hence thesis by Th6;
end;
suppose
A23: x in the carrier of S & y in the carrier of R & z in the carrier of R;
then
A24: [y,z] in the InternalRel of R by A3,A4,A11,Th4;
A25: x in the carrier of R by A2,A10,A23,Th21;
then [x,y] in the InternalRel of R by A3,A4,A10,A23,Th4;
then [x,z] in the InternalRel of R by A7,A23,A25,A24;
hence thesis by Th6;
end;
suppose
A26: x in the carrier of S & y in the carrier of S & z in the carrier of R;
then
A27: [x,y] in the InternalRel of S by A3,A5,A10,Th5;
A28: z in the carrier of S by A1,A11,A26,Th17;
then [y,z] in the InternalRel of S by A3,A5,A11,A26,Th5;
then [x,z] in the InternalRel of S by A6,A26,A27,A28;
hence thesis by Th6;
end;
suppose
A29: x in the carrier of S & y in the carrier of S & z in the carrier of S;
then
[x,y] in the InternalRel of S & [y,z] in the InternalRel of S by A3,A5
,A10,A11,Th5;
then [x,z] in the InternalRel of S by A6,A29;
hence thesis by Th6;
end;
suppose
A30: x in the carrier of R & y in the carrier of S & z in the carrier of S;
then
A31: [y,z] in the InternalRel of S by A3,A5,A11,Th5;
[x,y] in (the InternalRel of R) \/ (the InternalRel of S) \/ ((the
InternalRel of R) * the InternalRel of S) by A10,Def2;
then
A32: [x,y] in (the InternalRel of R) \/ (the InternalRel of S) or [x,y]
in ((the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
now
per cases by A32,XBOOLE_0:def 3;
suppose
[x,y] in the InternalRel of R;
then
[x,z] in ((the InternalRel of R) * the InternalRel of S) by A31,
RELAT_1:def 8;
then [x,z] in ((the InternalRel of R) \/ (the InternalRel of S)) \/
((the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
suppose
A33: [x,y] in the InternalRel of S;
then x in the carrier of S by ZFMISC_1:87;
then [x,z] in the InternalRel of S by A6,A30,A31,A33;
hence thesis by Th6;
end;
suppose
[x,y] in ((the InternalRel of R) * the InternalRel of S);
then consider a being object such that
A34: [x,a] in the InternalRel of R and
A35: [a,y] in the InternalRel of S by RELAT_1:def 8;
a in the carrier of S by A35,ZFMISC_1:87;
then [a,z] in the InternalRel of S by A6,A30,A31,A35;
then
[x,z] in ((the InternalRel of R) * the InternalRel of S) by A34,
RELAT_1:def 8;
then [x,z] in ((the InternalRel of R) \/ (the InternalRel of S)) \/
((the InternalRel of R) * the InternalRel of S) by XBOOLE_0:def 3;
hence thesis by Def2;
end;
end;
hence thesis;
end;
suppose
A36: x in the carrier of S & y in the carrier of R & z in the carrier of S;
then
A37: y in the carrier of S by A1,A10,Th17;
then
[x,y] in the InternalRel of S & [y,z] in the InternalRel of S by A3,A5
,A10,A11,A36,Th5;
then [x,z] in the InternalRel of S by A6,A36,A37;
hence thesis by Th6;
end;
end;
hence thesis by ORDERS_2:def 3;
end;