:: Cartesian Products of Relations and Relational Structures
:: by Artur Korni{\l}owicz
::
:: Received September 25, 1996
:: Copyright (c) 1996-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, SUBSET_1, TARSKI, ORDERS_2, WAYBEL_0, XXREAL_0,
ZFMISC_1, RELAT_1, MCART_1, LATTICE3, RELAT_2, LATTICES, YELLOW_0,
EQREL_1, REWRITE1, ORDINAL2, FUNCT_1, STRUCT_0, YELLOW_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1, RELAT_2,
RELSET_1, MCART_1, DOMAIN_1, FUNCT_2, BINOP_1, STRUCT_0, ORDERS_2,
LATTICE3, YELLOW_0, WAYBEL_0;
constructors DOMAIN_1, LATTICE3, ORDERS_3, WAYBEL_0, RELSET_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0,
WAYBEL_0, RELAT_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions LATTICE3, RELAT_2, TARSKI, WAYBEL_0, ORDERS_2;
expansions LATTICE3, RELAT_2, WAYBEL_0, ORDERS_2;
theorems FUNCT_1, FUNCT_2, FUNCT_5, LATTICE3, MCART_1, ORDERS_2, RELAT_1,
RELAT_2, RELSET_1, TARSKI, WAYBEL_0, YELLOW_0, YELLOW_2, ZFMISC_1,
XBOOLE_0, BINOP_1, XTUPLE_0;
schemes FUNCT_7, RELAT_1;
begin :: Preliminaries
scheme
FraenkelA2 {A() -> non empty set, F(set, set) -> set, P[set, set], Q[set,
set] } : { F(s,t) where s is Element of A(), t is Element of A() : P[s,t] } is
Subset of A()
provided
A1: for s being Element of A(), t being Element of A() holds F(s,t) in A ()
proof
{ F(s,t) where s is Element of A(), t is Element of A() : P[s,t] } c= A ( )
proof
let q be object;
assume
q in { F(s,t) where s is Element of A(), t is Element of A() : P[s ,t] };
then ex s, t being Element of A() st q = F(s,t) & P[s,t];
hence thesis by A1;
end;
hence thesis;
end;
registration
let L be RelStr, X be empty Subset of L;
cluster downarrow X -> empty;
coherence
proof
assume downarrow X is non empty;
then consider x being object such that
A1: x in downarrow X by XBOOLE_0:def 1;
reconsider x as Element of L by A1;
ex z being Element of L st x <= z & z in X by A1,WAYBEL_0:def 15;
hence contradiction;
end;
cluster uparrow X -> empty;
coherence
proof
assume uparrow X is non empty;
then consider x being object such that
A2: x in uparrow X by XBOOLE_0:def 1;
reconsider x as Element of L by A2;
ex z being Element of L st z <= x & z in X by A2,WAYBEL_0:def 16;
hence contradiction;
end;
end;
theorem Th1:
for X, Y being set, D being Subset of [:X,Y:] holds D c= [:proj1 D, proj2 D:]
proof
let X, Y be set, D be Subset of [:X,Y:];
let q be object;
assume
A1: q in D;
then consider x, y being object such that
x in X and
y in Y and
A2: q = [x,y] by ZFMISC_1:def 2;
x in proj1 D & y in proj2 D by A1,A2,XTUPLE_0:def 12,def 13;
hence thesis by A2,ZFMISC_1:def 2;
end;
theorem
for L being with_infima transitive antisymmetric RelStr for a, b, c, d
being Element of L st a <= c & b <= d holds a "/\" b <= c "/\" d
proof
let L be with_infima transitive antisymmetric RelStr, a, b, c, d be Element
of L such that
A1: a <= c and
A2: b <= d;
A3: ex_inf_of {a,b},L by YELLOW_0:21;
then a "/\" b <= b by YELLOW_0:19;
then
A4: a "/\" b <= d by A2,ORDERS_2:3;
a "/\" b <= a by A3,YELLOW_0:19;
then
( ex x being Element of L st c >= x & d >= x & for z being Element of L
st c >= z & d >= z holds x >= z)& a "/\" b <= c by A1,LATTICE3:def 11
,ORDERS_2:3;
hence thesis by A4,LATTICE3:def 14;
end;
theorem
for L being with_suprema transitive antisymmetric RelStr for a, b, c,
d being Element of L st a <= c & b <= d holds a "\/" b <= c "\/" d
proof
let L be with_suprema transitive antisymmetric RelStr, a, b, c, d be Element
of L such that
A1: a <= c and
A2: b <= d;
A3: ex_sup_of {c,d},L by YELLOW_0:20;
then d <= c "\/" d by YELLOW_0:18;
then
A4: b <= c "\/" d by A2,ORDERS_2:3;
c <= c "\/" d by A3,YELLOW_0:18;
then
( ex x being Element of L st a <= x & b <= x & for z being Element of L
st a <= z & b <= z holds x <= z)& a <= c "\/" d by A1,LATTICE3:def 10
,ORDERS_2:3;
hence thesis by A4,LATTICE3:def 13;
end;
theorem
for L being complete reflexive antisymmetric non empty RelStr for D
being Subset of L, x being Element of L st x in D holds (sup D) "/\" x = x
proof
let L be complete reflexive antisymmetric non empty RelStr, D be Subset of
L, x be Element of L such that
A1: x in D;
D is_<=_than sup D by YELLOW_0:32;
then x <= sup D by A1;
hence thesis by YELLOW_0:25;
end;
theorem
for L being complete reflexive antisymmetric non empty RelStr for D
being Subset of L, x being Element of L st x in D holds (inf D) "\/" x = x
proof
let L be complete reflexive antisymmetric non empty RelStr, D be Subset of
L, x be Element of L such that
A1: x in D;
D is_>=_than inf D by YELLOW_0:33;
then inf D <= x by A1;
hence thesis by YELLOW_0:24;
end;
theorem
for L being RelStr, X, Y being Subset of L st X c= Y holds downarrow X
c= downarrow Y
proof
let L be RelStr, X, Y be Subset of L such that
A1: X c= Y;
let q be object;
assume
A2: q in downarrow X;
then reconsider x = q as Element of L;
ex z being Element of L st x <= z & z in X by A2,WAYBEL_0:def 15;
hence thesis by A1,WAYBEL_0:def 15;
end;
theorem
for L being RelStr, X, Y being Subset of L st X c= Y holds uparrow X
c= uparrow Y
proof
let L be RelStr, X, Y be Subset of L such that
A1: X c= Y;
let q be object;
assume
A2: q in uparrow X;
then reconsider x = q as Element of L;
ex z being Element of L st z <= x & z in X by A2,WAYBEL_0:def 16;
hence thesis by A1,WAYBEL_0:def 16;
end;
theorem
for S, T being with_infima Poset, f being Function of S, T for x, y
being Element of S holds f preserves_inf_of {x,y} iff f.(x "/\" y) = f.x "/\" f
.y
proof
let S, T be with_infima Poset, f be Function of S, T, x, y be Element of S;
A1: dom f = the carrier of S by FUNCT_2:def 1;
hereby
A2: ex_inf_of {x,y},S by YELLOW_0:21;
assume
A3: f preserves_inf_of {x,y};
thus f.(x "/\" y) = f.inf {x,y} by YELLOW_0:40
.= inf (f.:{x,y}) by A3,A2
.= inf {f.x,f.y} by A1,FUNCT_1:60
.= f.x "/\" f.y by YELLOW_0:40;
end;
assume
A4: f.(x "/\" y) = f.x "/\" f.y;
assume ex_inf_of {x,y},S;
f.:{x,y} = {f.x,f.y} by A1,FUNCT_1:60;
hence ex_inf_of f.:{x,y},T by YELLOW_0:21;
thus inf (f.:{x,y}) = inf {f.x,f.y} by A1,FUNCT_1:60
.= f.x "/\" f.y by YELLOW_0:40
.= f.inf {x,y} by A4,YELLOW_0:40;
end;
theorem
for S, T being with_suprema Poset, f being Function of S, T for x, y
being Element of S holds f preserves_sup_of {x,y} iff f.(x "\/" y) = f.x "\/" f
.y
proof
let S, T be with_suprema Poset, f be Function of S, T, x, y be Element of S;
A1: dom f = the carrier of S by FUNCT_2:def 1;
hereby
A2: ex_sup_of {x,y},S by YELLOW_0:20;
assume
A3: f preserves_sup_of {x,y};
thus f.(x "\/" y) = f.sup {x,y} by YELLOW_0:41
.= sup (f.:{x,y}) by A3,A2
.= sup {f.x,f.y} by A1,FUNCT_1:60
.= f.x "\/" f.y by YELLOW_0:41;
end;
assume
A4: f.(x "\/" y) = f.x "\/" f.y;
assume ex_sup_of {x,y},S;
f.:{x,y} = {f.x,f.y} by A1,FUNCT_1:60;
hence ex_sup_of f.:{x,y},T by YELLOW_0:20;
thus sup (f.:{x,y}) = sup {f.x,f.y} by A1,FUNCT_1:60
.= f.x "\/" f.y by YELLOW_0:41
.= f.sup {x,y} by A4,YELLOW_0:41;
end;
scheme
InfUnion { L() -> complete antisymmetric non empty RelStr, P[set] } : "/\"
({ "/\"(X,L()) where X is Subset of L(): P[X] },L()) >= "/\" (union {X where X
is Subset of L(): P[X]},L()) proof
"/\"(union {X where X is Subset of L(): P[X]},L()) is_<=_than { "/\"(X,L
()) where X is Subset of L(): P[X] }
proof
let a be Element of L();
assume a in { "/\"(X,L()) where X is Subset of L(): P[X] };
then consider q being Subset of L() such that
A1: a = "/\"(q,L()) and
A2: P[q];
A3: ex_inf_of q,L() & ex_inf_of union {X where X is Subset of L(): P[X]},L
() by YELLOW_0:17;
q in {X where X is Subset of L(): P[X]} by A2;
hence thesis by A1,A3,YELLOW_0:35,ZFMISC_1:74;
end;
hence thesis by YELLOW_0:33;
end;
scheme
InfofInfs { L() -> complete LATTICE, P[set] } : "/\" ({ "/\"(X,L()) where X
is Subset of L(): P[X] },L()) = "/\" (union {X where X is Subset of L(): P[X]},
L()) proof
union {X where X is Subset of L(): P[X]} is_>=_than "/\" ({ "/\"(X,L())
where X is Subset of L(): P[X] },L())
proof
let a be Element of L();
assume a in union {X where X is Subset of L(): P[X]};
then consider b being set such that
A1: a in b and
A2: b in {X where X is Subset of L(): P[X]} by TARSKI:def 4;
consider c being Subset of L() such that
A3: b = c and
A4: P[c] by A2;
"/\"(c,L()) in { "/\" (X,L()) where X is Subset of L(): P[X] } by A4;
then
A5: "/\"(c,L()) >= "/\" ({ "/\"(X,L()) where X is Subset of L(): P[X] } ,
L()) by YELLOW_2:22;
"/\"(c,L()) <= a by A1,A3,YELLOW_2:22;
hence thesis by A5,YELLOW_0:def 2;
end;
then
A6: "/\"(union {X where X is Subset of L(): P[X]},L()) >= "/\" ({ "/\"(X,L(
)) where X is Subset of L(): P[X] },L()) by YELLOW_0:33;
"/\" ({ "/\"(X,L()) where X is Subset of L(): P[X] },L()) >= "/\"(union
{X where X is Subset of L(): P[X]},L()) from InfUnion;
hence thesis by A6,ORDERS_2:2;
end;
scheme
SupUnion { L() -> complete antisymmetric non empty RelStr, P[set] } : "\/"
({ "\/"(X,L()) where X is Subset of L(): P[X] },L()) <= "\/" (union {X where X
is Subset of L(): P[X]},L()) proof
A1: "\/"(union {X where X is Subset of L(): P[X]},L()) is_>=_than { "\/"(X,L
()) where X is Subset of L(): P[X] }
proof
let a be Element of L();
assume a in { "\/"(X,L()) where X is Subset of L(): P[X] };
then consider q being Subset of L() such that
A2: a = "\/"(q,L()) and
A3: P[q];
A4: ex_sup_of q,L() & ex_sup_of union {X where X is Subset of L(): P[X]},L
() by YELLOW_0:17;
q in {X where X is Subset of L(): P[X]} by A3;
hence thesis by A2,A4,YELLOW_0:34,ZFMISC_1:74;
end;
ex_sup_of { "\/" (X,L()) where X is Subset of L(): P[X] },L() by YELLOW_0:17;
hence thesis by A1,YELLOW_0:def 9;
end;
scheme
SupofSups { L() -> complete LATTICE, P[set] } : "\/" ({ "\/"(X,L()) where X
is Subset of L(): P[X] },L()) = "\/" (union {X where X is Subset of L(): P[X]},
L()) proof
A1: union {X where X is Subset of L(): P[X]} is_<=_than "\/" ({ "\/"(X,L())
where X is Subset of L(): P[X] },L())
proof
let a be Element of L();
assume a in union {X where X is Subset of L(): P[X]};
then consider b being set such that
A2: a in b and
A3: b in {X where X is Subset of L(): P[X]} by TARSKI:def 4;
consider c being Subset of L() such that
A4: b = c and
A5: P[c] by A3;
"\/"(c,L()) in { "\/" (X,L()) where X is Subset of L(): P[X] } by A5;
then
A6: "\/"(c,L()) <= "\/" ({ "\/"(X,L()) where X is Subset of L(): P[X] } ,
L()) by YELLOW_2:22;
a <= "\/"(c,L()) by A2,A4,YELLOW_2:22;
hence a <= "\/" ({ "\/"(X,L()) where X is Subset of L(): P[X] },L()) by A6,
YELLOW_0:def 2;
end;
A7: "\/" ({ "\/"(X,L()) where X is Subset of L(): P[X] },L()) <= "\/"(union
{X where X is Subset of L(): P[X]},L()) from SupUnion;
ex_sup_of union {X where X is Subset of L(): P[X]},L() by YELLOW_0:17;
then
"\/"(union {X where X is Subset of L(): P[X]},L()) <= "\/" ({ "\/"(X,L(
)) where X is Subset of L(): P[X] },L()) by A1,YELLOW_0:def 9;
hence thesis by A7,ORDERS_2:2;
end;
begin :: Properties of Cartesian Products of Relational Structures
definition
let P, R be Relation;
func ["P,R"] -> Relation means
:Def1:
for x, y being object holds [x,y] in it
iff ex p,q,s,t being object
st x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R;
existence
proof
defpred P[object,object] means
ex p, s, q, t being object st $1 = [p,q] & $2 = [s,t
] & [p,s] in P & [q,t] in R;
consider Q being Relation such that
A1: for x, y being object holds [x,y] in Q iff x in [:dom P,dom R:] & y
in [:rng P,rng R:] & P[x,y] from RELAT_1:sch 1;
take Q;
let x, y be object;
hereby
assume [x,y] in Q;
then consider p, s, q, t being object such that
A2: x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R by A1;
take p, q, s, t;
thus x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R by A2;
end;
given p,q,s,t being object such that
A3: x = [p,q] and
A4: y = [s,t] and
A5: [p,s] in P & [q,t] in R;
s in rng P & t in rng R by A5,XTUPLE_0:def 13;
then
A6: y in [:rng P,rng R:] by A4,ZFMISC_1:87;
p in dom P & q in dom R by A5,XTUPLE_0:def 12;
then x in [:dom P,dom R:] by A3,ZFMISC_1:87;
hence thesis by A1,A3,A4,A5,A6;
end;
uniqueness
proof
defpred P[object,object] means
ex p,q,s,t being object st $1 = [p,q] & $2 = [s,t] &
[p,s] in P & [q,t] in R;
let A, B be Relation such that
A7: for x, y being object holds [x,y] in A iff P[x,y] and
A8: for x, y being object holds [x,y] in B iff P[x,y];
thus A = B from RELAT_1:sch 2(A7,A8);
end;
end;
theorem Th10:
for P, R being Relation, x being object holds x in ["P,R"] iff [x`1
`1,x`2`1] in P & [x`1`2,x`2`2] in R &
(ex a, b being object st x = [a,b]) &
(ex c, d being object st x`1 = [c,d]) &
ex e, f being object st x`2 = [e,f]
proof
let P, R be Relation, x be object;
hereby
assume
A1: x in ["P,R"];
then consider y, z being object such that
A2: x = [y,z] by RELAT_1:def 1;
consider p,q,s,t being object such that
A3: y = [p,q] and
A4: z = [s,t] and
A5: [p,s] in P & [q,t] in R by A1,A2,Def1;
x`1`1 = p & x`1`2 = q by A2,A3;
hence [x`1`1,x`2`1] in P & [x`1`2,x`2`2] in R by A2,A4,A5;
thus ex a, b being object st x = [a,b] by A2;
thus ex c, d being object st x`1 = [c,d] by A2,A3;
thus ex e, f being object st x`2 = [e,f] by A2,A4;
end;
assume that
A6: [x`1`1,x`2`1] in P and
A7: [x`1`2,x`2`2] in R;
given a, b being object such that
A8: x = [a,b];
given c, d being object such that
A9: x`1 = [c,d];
given e, f being object such that
A10: x`2 = [e,f];
[c,x`2`1] in P by A6,A9;
then
A11: [c,e] in P by A10;
[d,x`2`2] in R by A7,A9;
then
A12: [d,f] in R by A10;
A13: b = [e,f] by A8,A10;
a = [c,d] by A8,A9;
hence thesis by A8,A13,A11,A12,Def1;
end;
definition
let A, B, X, Y be set;
let P be Relation of A, B;
let R be Relation of X, Y;
redefine func ["P,R"] -> Relation of [:A,X:],[:B,Y:]; :: redefines [" (YELLOW_3, definition)
coherence
proof
["P,R"] c= [:[:A,X:],[:B,Y:]:]
proof
let q be object;
assume
A1: q in ["P,R"];
then consider a, b being object such that
A2: q = [a,b] by Th10;
[q`1`2,q`2`2] in R by A1,Th10;
then consider s, t being object such that
A3: [q`1`2,q`2`2] = [s,t] and
A4: s in X and
A5: t in Y by RELSET_1:2;
consider a2, b2 being object such that
A6: q`2 = [a2,b2] by A1,Th10;
[q`1`1,q`2`1] in P by A1,Th10;
then consider x, y being object such that
A7: [q`1`1,q`2`1] = [x,y] and
A8: x in A and
A9: y in B by RELSET_1:2;
consider a1, b1 being object such that
A10: q`1 = [a1,b1] by A1,Th10;
A11: b = [a2,b2] by A2,A6;
then
A12: b`2 = t by A3,A6,XTUPLE_0:1;
A13: a = [a1,b1] by A2,A10;
then
A14: a`2 = s by A3,A10,XTUPLE_0:1;
b`1 = y by A7,A6,A11,XTUPLE_0:1;
then
A15: b in [:B,Y:] by A9,A5,A11,A12,ZFMISC_1:def 2;
a`1 = x by A7,A10,A13,XTUPLE_0:1;
then a in [:A,X:] by A8,A4,A13,A14,ZFMISC_1:def 2;
hence thesis by A2,A15,ZFMISC_1:def 2;
end;
hence thesis;
end;
end;
definition
let X, Y be RelStr;
func [:X,Y:] -> strict RelStr means
:Def2:
the carrier of it = [:the carrier
of X, the carrier of Y:] & the InternalRel of it = ["the InternalRel of X, the
InternalRel of Y"];
existence
proof
take RelStr (#[:the carrier of X, the carrier of Y:], ["the InternalRel of
X, the InternalRel of Y"]#);
thus thesis;
end;
uniqueness;
end;
definition
let L1, L2 be RelStr, D be Subset of [:L1,L2:];
redefine func proj1 D -> Subset of L1; :: redefines proj1 (XTUPLE_0, definition)
coherence
proof
proj1 D c= the carrier of L1
proof
let x be object;
assume x in proj1 D;
then
A1: ex y being object st [x,y] in D by XTUPLE_0:def 12;
the carrier of [:L1,L2:] = [:the carrier of L1, the carrier of L2:]
by Def2;
hence thesis by A1,ZFMISC_1:87;
end;
hence thesis;
end;
redefine func proj2 D -> Subset of L2; :: redefines proj2 (XTUPLE_0, definition)
coherence
proof
proj2 D c= the carrier of L2
proof
let y be object;
assume y in proj2 D;
then
A2: ex x being object st [x,y] in D by XTUPLE_0:def 13;
the carrier of [:L1,L2:] = [:the carrier of L1, the carrier of L2:]
by Def2;
hence thesis by A2,ZFMISC_1:87;
end;
hence thesis;
end;
end;
definition
let S1, S2 be RelStr, D1 be Subset of S1, D2 be Subset of S2;
redefine func [:D1,D2:] -> Subset of [:S1,S2:]; :: redefines [: (ZFMISC_1, definition)
coherence
proof
[:D1,D2:] c= [:the carrier of S1,the carrier of S2:];
hence thesis by Def2;
end;
end;
definition
let S1, S2 be non empty RelStr, x be Element of S1, y be Element of S2;
redefine func [x,y] -> Element of [:S1,S2:]; :: redefines [ (TARSKI, definition)
coherence
proof
reconsider y1 = y as Element of S2;
reconsider x1 = x as Element of S1;
[x1,y1] is Element of [:S1,S2:] by Def2;
hence thesis;
end;
end;
definition
let L1, L2 be non empty RelStr, x be Element of [:L1,L2:];
redefine func x`1 -> Element of L1; :: redefines `1 (XTUPLE_0, definition)
coherence
proof
the carrier of [:L1,L2:] = [:the carrier of L1,the carrier of L2:] by Def2;
hence thesis by MCART_1:10;
end;
redefine func x`2 -> Element of L2; :: redefines `2 (XTUPLE_0, definition)
coherence
proof
the carrier of [:L1,L2:] = [:the carrier of L1,the carrier of L2:] by Def2;
hence thesis by MCART_1:10;
end;
end;
theorem Th11:
for S1, S2 being non empty RelStr for a, c being Element of S1,
b, d being Element of S2 holds a <= c & b <= d iff [a,b] <= [c,d]
proof
let S1, S2 be non empty RelStr, a, c be Element of S1, b, d be Element of S2;
set I1 = the InternalRel of S1, I2 = the InternalRel of S2, x = [[a,b],[c,d]
];
A1: x`1`1 = a & x`2`1 = c;
A2: x`1`2 = b & x`2`2 = d;
thus a <= c & b <= d implies [a,b] <= [c,d]
proof
assume a <= c & b <= d;
then [x`1`1,x`2`1] in I1 & [x`1`2,x`2`2] in I2;
then x in ["I1,I2"] by Th10;
hence [[a,b],[c,d]] in the InternalRel of [:S1,S2:] by Def2;
end;
assume [a,b] <= [c,d];
then x in the InternalRel of [:S1,S2:];
then x in ["I1,I2"] by Def2;
hence [a,c] in the InternalRel of S1 & [b,d] in the InternalRel of S2 by A1
,A2,Th10;
end;
theorem Th12:
for S1, S2 being non empty RelStr, x, y being Element of [:S1,S2
:] holds x <= y iff x`1 <= y`1 & x`2 <= y`2
proof
let S1, S2 be non empty RelStr, x, y be Element of [:S1,S2:];
A1: the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2
;
then
ex c, d being object st c in the carrier of S1 & d in the carrier of S2 & y
= [c,d] by ZFMISC_1:def 2;
then
A2: y = [y`1,y`2];
ex a, b being object st a in the carrier of S1 & b in the carrier of S2 & x
= [a,b] by A1,ZFMISC_1:def 2;
then x = [x`1,x`2];
hence thesis by A2,Th11;
end;
theorem
for A, B being RelStr, C being non empty RelStr for f, g being
Function of [:A,B:],C st for x being Element of A, y being Element of B holds f
.(x,y) = g.(x,y) holds f = g
proof
let A, B be RelStr, C be non empty RelStr, f, g be Function of [:A,B:],C;
assume
for x being Element of A, y being Element of B holds f.(x,y) = g.(x, y);
then
A1: for x, y being set st x in the carrier of A & y in the carrier of B
holds f.(x,y) = g.(x,y);
the carrier of [:A,B:] = [:the carrier of A,the carrier of B:] by Def2;
hence thesis by A1,BINOP_1:1;
end;
registration
let X, Y be non empty RelStr;
cluster [:X,Y:] -> non empty;
coherence
proof
set y = the Element of Y;
set x = the Element of X;
[x,y] in [:the carrier of X,the carrier of Y:] by ZFMISC_1:87;
hence thesis by Def2;
end;
end;
registration
let X, Y be reflexive RelStr;
cluster [:X,Y:] -> reflexive;
coherence
proof
let x be object;
assume x in the carrier of [:X,Y:];
then x in [:the carrier of X,the carrier of Y:] by Def2;
then consider x1, x2 being object such that
A1: x1 in the carrier of X and
A2: x2 in the carrier of Y and
A3: x = [x1,x2] by ZFMISC_1:def 2;
the InternalRel of X is_reflexive_in the carrier of X by ORDERS_2:def 2;
then
A4: [x1,x1] in the InternalRel of X by A1;
the InternalRel of Y is_reflexive_in the carrier of Y by ORDERS_2:def 2;
then
A5: [x2,x2] in the InternalRel of Y by A2;
set a = [[x1,x2],[x1,x2]];
A6: a`1 = [x1,x2] & a`2 = [x1,x2];
a`1`1 = x1 & a`1`2 = x2;
then [x,x] in ["the InternalRel of X,the InternalRel of Y"] by A3,A4,A5,A6
,Th10;
hence thesis by Def2;
end;
end;
registration
let X, Y be antisymmetric RelStr;
cluster [:X,Y:] -> antisymmetric;
coherence
proof
let x, y be object such that
A1: x in the carrier of [:X,Y:] and
A2: y in the carrier of [:X,Y:] and
A3: [x,y] in the InternalRel of [:X,Y:] and
A4: [y,x] in the InternalRel of [:X,Y:];
x in [:the carrier of X,the carrier of Y:] by A1,Def2;
then consider x1, x2 being object such that
A5: x1 in the carrier of X and
A6: x2 in the carrier of Y and
A7: x = [x1,x2] by ZFMISC_1:def 2;
y in [:the carrier of X,the carrier of Y:] by A2,Def2;
then consider y1, y2 being object such that
A8: y1 in the carrier of X and
A9: y2 in the carrier of Y and
A10: y = [y1,y2] by ZFMISC_1:def 2;
A11: [y,x] in ["the InternalRel of X,the InternalRel of Y"] by A4,Def2;
then [[y,x]`1`1,[y,x]`2`1] in the InternalRel of X by Th10;
then [y`1,[y,x]`2`1] in the InternalRel of X;
then [y`1,x`1] in the InternalRel of X;
then [y1,[x1,x2]`1] in the InternalRel of X by A7,A10;
then
A12: [y1,x1] in the InternalRel of X;
[[y,x]`1`2,[y,x]`2`2] in the InternalRel of Y by A11,Th10;
then [y`2,[y,x]`2`2] in the InternalRel of Y;
then [y`2,x`2] in the InternalRel of Y;
then [y2,[x1,x2]`2] in the InternalRel of Y by A7,A10;
then
A13: [y2,x2] in the InternalRel of Y;
A14: [x,y] in ["the InternalRel of X,the InternalRel of Y"] by A3,Def2;
then [[x,y]`1`2,[x,y]`2`2] in the InternalRel of Y by Th10;
then [x`2,[x,y]`2`2] in the InternalRel of Y;
then [x`2,y`2] in the InternalRel of Y;
then [x2,[y1,y2]`2] in the InternalRel of Y by A7,A10;
then
A15: [x2,y2] in the InternalRel of Y;
[[x,y]`1`1,[x,y]`2`1] in the InternalRel of X by A14,Th10;
then [x`1,[x,y]`2`1] in the InternalRel of X;
then [x`1,y`1] in the InternalRel of X;
then [x1,[y1,y2]`1] in the InternalRel of X by A7,A10;
then [x1,y1] in the InternalRel of X;
then the InternalRel of Y is_antisymmetric_in the carrier of Y & x1 = y1
by A5,A8,A12,ORDERS_2:def 4,RELAT_2:def 4;
hence thesis by A6,A7,A9,A10,A15,A13;
end;
end;
registration
let X, Y be transitive RelStr;
cluster [:X,Y:] -> transitive;
coherence
proof
set P = the InternalRel of X, R = the InternalRel of Y;
let x, y, z be object such that
A1: x in the carrier of [:X,Y:] and
A2: y in the carrier of [:X,Y:] and
A3: z in the carrier of [:X,Y:] and
A4: [x,y] in the InternalRel of [:X,Y:] and
A5: [y,z] in the InternalRel of [:X,Y:];
y in [:the carrier of X,the carrier of Y:] by A2,Def2;
then consider y1, y2 being object such that
A6: y1 in the carrier of X and
A7: y2 in the carrier of Y and
A8: y = [y1,y2] by ZFMISC_1:def 2;
z in [:the carrier of X,the carrier of Y:] by A3,Def2;
then consider z1, z2 being object such that
A9: z1 in the carrier of X and
A10: z2 in the carrier of Y and
A11: z = [z1,z2] by ZFMISC_1:def 2;
A12: [y,z] in ["P,R"] by A5,Def2;
then [[y,z]`1`1,[y,z]`2`1] in P by Th10;
then [y`1,[y,z]`2`1] in P;
then [y`1,z`1] in P;
then [y1,z`1] in P by A8;
then
A13: [y1,z1] in P by A11;
x in [:the carrier of X,the carrier of Y:] by A1,Def2;
then consider x1, x2 being object such that
A14: x1 in the carrier of X and
A15: x2 in the carrier of Y and
A16: x = [x1,x2] by ZFMISC_1:def 2;
A17: [x,y] in ["P,R"] by A4,Def2;
then [[x,y]`1`1,[x,y]`2`1] in P by Th10;
then [x`1,[x,y]`2`1] in P;
then [x`1,y`1] in P;
then [x1,y`1] in P by A16;
then P is_transitive_in the carrier of X & [x1,y1] in P by A8,ORDERS_2:def
3;
then [x1,z1] in P by A14,A6,A9,A13;
then [x1,z`1] in P by A11;
then
A18: [x`1,z`1] in P by A16;
[[y,z]`1`2,[y,z]`2`2] in R by A12,Th10;
then [y`2,[y,z]`2`2] in R;
then [y`2,z`2] in R;
then [y2,z`2] in R by A8;
then
A19: [y2,z2] in R by A11;
[[x,y]`1`2,[x,y]`2`2] in R by A17,Th10;
then [x`2,[x,y]`2`2] in R;
then [x`2,y`2] in R;
then [x2,y`2] in R by A16;
then R is_transitive_in the carrier of Y & [x2,y2] in R by A8,ORDERS_2:def
3;
then [x2,z2] in R by A15,A7,A10,A19;
then [x2,z`2] in R by A11;
then
A20: [x`2,z`2] in R by A16;
[x,z]`1 = x & [x,z]`2 = z;
then [x,z] in ["P,R"] by A16,A11,A18,A20,Th10;
hence thesis by Def2;
end;
end;
registration
let X, Y be with_suprema RelStr;
cluster [:X,Y:] -> with_suprema;
coherence
proof
set IT = [:X,Y:];
let x, y be Element of IT;
consider zx being Element of X such that
A1: x`1 <= zx & y`1 <= zx and
A2: for z9 being Element of X st x`1 <= z9 & y`1 <= z9 holds zx <= z9
by LATTICE3:def 10;
consider zy being Element of Y such that
A3: x`2 <= zy & y`2 <= zy and
A4: for z9 being Element of Y st x`2 <= z9 & y`2 <= z9 holds zy <= z9
by LATTICE3:def 10;
A5: the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
then
A6: (ex a, b being object st a in the carrier of X & b in the carrier of Y &
x = [ a,b] )&
ex c, d being object st c in the carrier of X & d in the carrier of
Y & y = [c,d] by ZFMISC_1:def 2;
take z = [zx,zy];
[x`1,x`2] <= [zx,zy] & [y`1,y`2] <= [zx,zy] by A1,A3,Th11;
hence x <= z & y <= z by A6;
let z9 be Element of IT;
A7: ex a, b being object st a in the carrier of X & b in the carrier of Y & z9
= [a,b] by A5,ZFMISC_1:def 2;
assume
A8: x <= z9 & y <= z9;
then x`2 <= z9`2 & y`2 <= z9`2 by Th12;
then
A9: zy <= z9`2 by A4;
x`1 <= z9`1 & y`1 <= z9`1 by A8,Th12;
then zx <= z9`1 by A2;
then [zx,zy] <= [z9`1,z9`2] by A9,Th11;
hence thesis by A7;
end;
end;
registration
let X, Y be with_infima RelStr;
cluster [:X,Y:] -> with_infima;
coherence
proof
set IT = [:X,Y:];
let x, y be Element of IT;
consider zx being Element of X such that
A1: x`1 >= zx & y`1 >= zx and
A2: for z9 being Element of X st x`1 >= z9 & y`1 >= z9 holds zx >= z9
by LATTICE3:def 11;
consider zy being Element of Y such that
A3: x`2 >= zy & y`2 >= zy and
A4: for z9 being Element of Y st x`2 >= z9 & y`2 >= z9 holds zy >= z9
by LATTICE3:def 11;
A5: the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
then
A6: (ex a, b being object st a in the carrier of X & b in the carrier of Y &
x = [ a,b] )&
ex c, d being object st c in the carrier of X & d in the carrier of
Y & y = [c,d] by ZFMISC_1:def 2;
take z = [zx,zy];
[x`1,x`2] >= [zx,zy] & [y`1,y`2] >= [zx,zy] by A1,A3,Th11;
hence x >= z & y >= z by A6;
let z9 be Element of IT;
A7: ex a, b being object st a in the carrier of X & b in the carrier of Y & z9
= [a,b] by A5,ZFMISC_1:def 2;
assume
A8: x >= z9 & y >= z9;
then x`2 >= z9`2 & y`2 >= z9`2 by Th12;
then
A9: zy >= z9`2 by A4;
x`1 >= z9`1 & y`1 >= z9`1 by A8,Th12;
then zx >= z9`1 by A2;
then [zx,zy] >= [z9`1,z9`2] by A9,Th11;
hence thesis by A7;
end;
end;
theorem
for X, Y being RelStr st [:X,Y:] is non empty holds X is non empty & Y
is non empty
proof
let X, Y be RelStr;
assume [:X,Y:] is non empty;
then
A1: ex x being object st x in the carrier of [:X,Y:] by XBOOLE_0:def 1;
the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
hence thesis by A1,MCART_1:10;
end;
theorem
for X, Y being non empty RelStr st [:X,Y:] is reflexive holds X is
reflexive & Y is reflexive
proof
let X, Y be non empty RelStr such that
A1: [:X,Y:] is reflexive;
for x being Element of X holds x <= x
proof
set y = the Element of Y;
let x be Element of X;
[x,y] <= [x,y] by A1,YELLOW_0:def 1;
hence thesis by Th11;
end;
hence X is reflexive by YELLOW_0:def 1;
for y being Element of Y holds y <= y
proof
set x = the Element of X;
let y be Element of Y;
[x,y] <= [x,y] by A1,YELLOW_0:def 1;
hence thesis by Th11;
end;
hence thesis by YELLOW_0:def 1;
end;
theorem
for X, Y being non empty reflexive RelStr st [:X,Y:] is antisymmetric
holds X is antisymmetric & Y is antisymmetric
proof
let X, Y be non empty reflexive RelStr such that
A1: [:X,Y:] is antisymmetric;
for x,y being Element of X st x <= y & y <= x holds x = y
proof
set z = the Element of Y;
A2: z <= z;
let x, y be Element of X;
assume x <= y & y <= x;
then [x,z] <= [y,z] & [y,z] <= [x,z] by A2,Th11;
then [x,z] = [y,z] by A1,YELLOW_0:def 3;
hence thesis by XTUPLE_0:1;
end;
hence X is antisymmetric by YELLOW_0:def 3;
for x,y being Element of Y st x <= y & y <= x holds x = y
proof
set z = the Element of X;
A3: z <= z;
let x, y be Element of Y;
assume x <= y & y <= x;
then [z,x] <= [z,y] & [z,y] <= [z,x] by A3,Th11;
then [z,x] = [z,y] by A1,YELLOW_0:def 3;
hence thesis by XTUPLE_0:1;
end;
hence thesis by YELLOW_0:def 3;
end;
theorem
for X, Y being non empty reflexive RelStr st [:X,Y:] is transitive
holds X is transitive & Y is transitive
proof
let X, Y be non empty reflexive RelStr such that
A1: [:X,Y:] is transitive;
for x,y,z being Element of X st x <= y & y <= z holds x <= z
proof
set a = the Element of Y;
A2: a <= a;
let x, y, z be Element of X;
assume x <= y & y <= z;
then [x,a] <= [y,a] & [y,a] <= [z,a] by A2,Th11;
then [x,a] <= [z,a] by A1,YELLOW_0:def 2;
hence thesis by Th11;
end;
hence X is transitive by YELLOW_0:def 2;
for x,y,z being Element of Y st x <= y & y <= z holds x <= z
proof
set a = the Element of X;
A3: a <= a;
let x, y, z be Element of Y;
assume x <= y & y <= z;
then [a,x] <= [a,y] & [a,y] <= [a,z] by A3,Th11;
then [a,x] <= [a,z] by A1,YELLOW_0:def 2;
hence thesis by Th11;
end;
hence thesis by YELLOW_0:def 2;
end;
theorem
for X, Y being non empty reflexive RelStr st [:X,Y:] is with_suprema
holds X is with_suprema & Y is with_suprema
proof
let X, Y be non empty reflexive RelStr such that
A1: [:X,Y:] is with_suprema;
A2: the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
thus X is with_suprema
proof
let x, y be Element of X;
set a = the Element of Y;
A3: a <= a;
consider z being Element of [:X,Y:] such that
A4: [x,a] <= z & [y,a] <= z and
A5: for z9 being Element of [:X,Y:] st [x,a] <= z9 & [y,a] <= z9 holds
z <= z9 by A1;
take z`1;
A6: z = [z`1,z`2] by A2,MCART_1:21;
hence x <= z`1 & y <= z`1 by A4,Th11;
let z9 be Element of X;
assume x <= z9 & y <= z9;
then [x,a] <= [z9,a] & [y,a] <= [z9,a] by A3,Th11;
then z <= [z9,a] by A5;
hence z`1 <= z9 by A6,Th11;
end;
set a = the Element of X;
A7: a <= a;
let x, y be Element of Y;
consider z being Element of [:X,Y:] such that
A8: [a,x] <= z & [a,y] <= z and
A9: for z9 being Element of [:X,Y:] st [a,x] <= z9 & [a,y] <= z9 holds
z <= z9 by A1;
take z`2;
A10: z = [z`1,z`2] by A2,MCART_1:21;
hence x <= z`2 & y <= z`2 by A8,Th11;
let z9 be Element of Y;
assume x <= z9 & y <= z9;
then [a,x] <= [a,z9] & [a,y] <= [a,z9] by A7,Th11;
then z <= [a,z9] by A9;
hence z`2 <= z9 by A10,Th11;
end;
theorem
for X, Y being non empty reflexive RelStr st [:X,Y:] is with_infima
holds X is with_infima & Y is with_infima
proof
let X, Y be non empty reflexive RelStr such that
A1: [:X,Y:] is with_infima;
A2: the carrier of [:X,Y:] = [:the carrier of X, the carrier of Y:] by Def2;
thus X is with_infima
proof
let x, y be Element of X;
set a = the Element of Y;
A3: a <= a;
consider z being Element of [:X,Y:] such that
A4: [x,a] >= z & [y,a] >= z and
A5: for z9 being Element of [:X,Y:] st [x,a] >= z9 & [y,a] >= z9 holds
z >= z9 by A1;
take z`1;
A6: z = [z`1,z`2] by A2,MCART_1:21;
hence x >= z`1 & y >= z`1 by A4,Th11;
let z9 be Element of X;
assume x >= z9 & y >= z9;
then [x,a] >= [z9,a] & [y,a] >= [z9,a] by A3,Th11;
then z >= [z9,a] by A5;
hence thesis by A6,Th11;
end;
set a = the Element of X;
A7: a <= a;
let x, y be Element of Y;
consider z being Element of [:X,Y:] such that
A8: [a,x] >= z & [a,y] >= z and
A9: for z9 being Element of [:X,Y:] st [a,x] >= z9 & [a,y] >= z9 holds
z >= z9 by A1;
take z`2;
A10: z = [z`1,z`2] by A2,MCART_1:21;
hence x >= z`2 & y >= z`2 by A8,Th11;
let z9 be Element of Y;
assume x >= z9 & y >= z9;
then [a,x] >= [a,z9] & [a,y] >= [a,z9] by A7,Th11;
then z >= [a,z9] by A9;
hence thesis by A10,Th11;
end;
registration
let S1, S2 be RelStr;
let D1 be directed Subset of S1, D2 be directed Subset of S2;
cluster [:D1,D2:] -> directed for Subset of [:S1,S2:];
coherence
proof
set X = [:D1,D2:];
X is directed
proof
let x, y be Element of [:S1,S2:];
assume that
A1: x in X and
A2: y in X;
consider x1, x2 being object such that
A3: x1 in D1 and
A4: x2 in D2 and
A5: x = [x1,x2] by A1,ZFMISC_1:def 2;
reconsider S29 = S2 as non empty RelStr by A4;
reconsider S19 = S1 as non empty RelStr by A3;
consider y1, y2 being object such that
A6: y1 in D1 and
A7: y2 in D2 and
A8: y = [y1,y2] by A2,ZFMISC_1:def 2;
reconsider x2, y2 as Element of S2 by A4,A7;
consider xy2 being Element of S2 such that
A9: xy2 in D2 and
A10: x2 <= xy2 & y2 <= xy2 by A4,A7,WAYBEL_0:def 1;
reconsider x1, y1 as Element of S1 by A3,A6;
consider xy1 being Element of S1 such that
A11: xy1 in D1 and
A12: x1 <= xy1 & y1 <= xy1 by A3,A6,WAYBEL_0:def 1;
reconsider xy29 = xy2 as Element of S29;
reconsider xy19 = xy1 as Element of S19;
[xy19,xy29] is Element of [:S19,S29:];
then reconsider z = [xy1,xy2] as Element of [:S1,S2:];
take z;
thus z in X by A11,A9,ZFMISC_1:87;
S1 is non empty & S2 is non empty by A3,A4;
hence thesis by A5,A8,A12,A10,Th11;
end;
hence thesis;
end;
end;
theorem
for S1, S2 being non empty RelStr for D1 being non empty Subset of S1,
D2 being non empty Subset of S2 st [:D1,D2:] is directed holds D1 is directed &
D2 is directed
proof
let S1, S2 be non empty RelStr, D1 be non empty Subset of S1, D2 be non
empty Subset of S2 such that
A1: [:D1,D2:] is directed;
thus D1 is directed
proof
set q1 = the Element of D2;
let x, y be Element of S1;
assume x in D1 & y in D1;
then [x,q1] in [:D1,D2:] & [y,q1] in [:D1,D2:] by ZFMISC_1:87;
then consider z being Element of [:S1,S2:] such that
A2: z in [:D1,D2:] and
A3: [x,q1] <= z & [y,q1] <= z by A1;
reconsider z2 = z`2 as Element of D2 by A2,MCART_1:10;
reconsider zz = z`1 as Element of D1 by A2,MCART_1:10;
take zz;
thus zz in D1;
ex x,y being object st x in D1 & y in D2 & z = [x,y] by A2,ZFMISC_1:def 2;
then [x,q1] <= [zz,z2] & [y,q1] <= [zz,z2] by A3;
hence thesis by Th11;
end;
set q1 = the Element of D1;
let x, y be Element of S2;
assume x in D2 & y in D2;
then [q1,x] in [:D1,D2:] & [q1,y] in [:D1,D2:] by ZFMISC_1:87;
then consider z being Element of [:S1,S2:] such that
A4: z in [:D1,D2:] and
A5: [q1,x] <= z & [q1,y] <= z by A1;
reconsider z2 = z`1 as Element of D1 by A4,MCART_1:10;
reconsider zz = z`2 as Element of D2 by A4,MCART_1:10;
take zz;
thus zz in D2;
ex x,y being object st x in D1 & y in D2 & z = [x,y] by A4,ZFMISC_1:def 2;
then [q1,x] <= [z2,zz] & [q1,y] <= [z2,zz] by A5;
hence thesis by Th11;
end;
theorem Th21:
for S1, S2 being non empty RelStr for D being non empty Subset
of [:S1,S2:] holds proj1 D is non empty & proj2 D is non empty
proof
let S1, S2 be non empty RelStr, D be non empty Subset of [:S1,S2:];
reconsider D1 = D as non empty Subset of [:the carrier of S1,the carrier of
S2:] by Def2;
proj1 D1 is non empty;
hence thesis;
end;
theorem
for S1, S2 being non empty reflexive RelStr for D being non empty
directed Subset of [:S1,S2:] holds proj1 D is directed & proj2 D is directed
proof
let S1, S2 be non empty reflexive RelStr, D be non empty directed Subset of
[:S1,S2:];
set D1 = proj1 D, D2 = proj2 D;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then
A1: D c= [:proj1 D, proj2 D:] by Th1;
thus D1 is directed
proof
let x, y be Element of S1;
assume that
A2: x in D1 and
A3: y in D1;
consider q2 being object such that
A4: [y,q2] in D by A3,XTUPLE_0:def 12;
reconsider D29 = D2 as non empty Subset of S2 by A2,FUNCT_5:16;
reconsider D19 = D1 as non empty Subset of S1 by A2;
consider q1 being object such that
A5: [x,q1] in D by A2,XTUPLE_0:def 12;
reconsider q2 as Element of D29 by A4,XTUPLE_0:def 13;
reconsider q1 as Element of D29 by A5,XTUPLE_0:def 13;
consider z being Element of [:S1,S2:] such that
A6: z in D and
A7: [x,q1] <= z & [y,q2] <= z by A5,A4,WAYBEL_0:def 1;
reconsider z2 = z`2 as Element of D29 by A1,A6,MCART_1:10;
reconsider zz = z`1 as Element of D19 by A1,A6,MCART_1:10;
take zz;
thus zz in D1;
ex x,y being object st x in D19 & y in D29 & z = [x,y]
by A1,A6,ZFMISC_1:def 2;
then z = [zz,z2];
hence x <= zz & y <= zz by A7,Th11;
end;
let x, y be Element of S2;
assume that
A8: x in D2 and
A9: y in D2;
consider q2 being object such that
A10: [q2,y] in D by A9,XTUPLE_0:def 13;
reconsider D29 = D2 as non empty Subset of S2 by A8;
reconsider D19 = D1 as non empty Subset of S1 by A8,FUNCT_5:16;
consider q1 being object such that
A11: [q1,x] in D by A8,XTUPLE_0:def 13;
reconsider q2 as Element of D19 by A10,XTUPLE_0:def 12;
reconsider q1 as Element of D19 by A11,XTUPLE_0:def 12;
consider z being Element of [:S1,S2:] such that
A12: z in D and
A13: [q1,x] <= z & [q2,y] <= z by A11,A10,WAYBEL_0:def 1;
reconsider z2 = z`1 as Element of D19 by A1,A12,MCART_1:10;
reconsider zz = z`2 as Element of D29 by A1,A12,MCART_1:10;
take zz;
thus zz in D2;
ex x,y being object st x in D19 & y in D29 & z = [x,y]
by A1,A12,ZFMISC_1:def 2;
then z = [z2,zz];
hence x <= zz & y <= zz by A13,Th11;
end;
registration
let S1, S2 be RelStr;
let D1 be filtered Subset of S1, D2 be filtered Subset of S2;
cluster [:D1,D2:] -> filtered for Subset of [:S1,S2:];
coherence
proof
set X = [:D1,D2:];
X is filtered
proof
let x, y be Element of [:S1,S2:];
assume that
A1: x in X and
A2: y in X;
consider x1, x2 being object such that
A3: x1 in D1 and
A4: x2 in D2 and
A5: x = [x1,x2] by A1,ZFMISC_1:def 2;
reconsider S29 = S2 as non empty RelStr by A4;
reconsider S19 = S1 as non empty RelStr by A3;
consider y1, y2 being object such that
A6: y1 in D1 and
A7: y2 in D2 and
A8: y = [y1,y2] by A2,ZFMISC_1:def 2;
reconsider x2, y2 as Element of S2 by A4,A7;
consider xy2 being Element of S2 such that
A9: xy2 in D2 and
A10: x2 >= xy2 & y2 >= xy2 by A4,A7,WAYBEL_0:def 2;
reconsider x1, y1 as Element of S1 by A3,A6;
consider xy1 being Element of S1 such that
A11: xy1 in D1 and
A12: x1 >= xy1 & y1 >= xy1 by A3,A6,WAYBEL_0:def 2;
reconsider xy29 = xy2 as Element of S29;
reconsider xy19 = xy1 as Element of S19;
[xy19,xy29] is Element of [:S19,S29:];
then reconsider z = [xy1,xy2] as Element of [:S1,S2:];
take z;
thus z in X by A11,A9,ZFMISC_1:87;
S1 is non empty & S2 is non empty by A3,A4;
hence thesis by A5,A8,A12,A10,Th11;
end;
hence thesis;
end;
end;
theorem
for S1, S2 being non empty RelStr for D1 being non empty Subset of S1,
D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds D1 is filtered &
D2 is filtered
proof
let S1, S2 be non empty RelStr, D1 be non empty Subset of S1, D2 be non
empty Subset of S2 such that
A1: [:D1,D2:] is filtered;
thus D1 is filtered
proof
set q1 = the Element of D2;
let x, y be Element of S1;
assume x in D1 & y in D1;
then [x,q1] in [:D1,D2:] & [y,q1] in [:D1,D2:] by ZFMISC_1:87;
then consider z being Element of [:S1,S2:] such that
A2: z in [:D1,D2:] and
A3: [x,q1] >= z & [y,q1] >= z by A1;
reconsider z2 = z`2 as Element of D2 by A2,MCART_1:10;
reconsider zz = z`1 as Element of D1 by A2,MCART_1:10;
take zz;
thus zz in D1;
ex x,y being object st x in D1 & y in D2 & z = [x,y]
by A2,ZFMISC_1:def 2;
then [x,q1] >= [zz,z2] & [y,q1] >= [zz,z2] by A3;
hence thesis by Th11;
end;
set q1 = the Element of D1;
let x, y be Element of S2;
assume x in D2 & y in D2;
then [q1,x] in [:D1,D2:] & [q1,y] in [:D1,D2:] by ZFMISC_1:87;
then consider z being Element of [:S1,S2:] such that
A4: z in [:D1,D2:] and
A5: [q1,x] >= z & [q1,y] >= z by A1;
reconsider z2 = z`1 as Element of D1 by A4,MCART_1:10;
reconsider zz = z`2 as Element of D2 by A4,MCART_1:10;
take zz;
thus zz in D2;
ex x,y being object st x in D1 & y in D2 & z = [x,y] by A4,ZFMISC_1:def 2;
then [q1,x] >= [z2,zz] & [q1,y] >= [z2,zz] by A5;
hence thesis by Th11;
end;
theorem
for S1, S2 being non empty reflexive RelStr for D being non empty
filtered Subset of [:S1,S2:] holds proj1 D is filtered & proj2 D is filtered
proof
let S1, S2 be non empty reflexive RelStr, D be non empty filtered Subset of
[:S1,S2:];
set D1 = proj1 D, D2 = proj2 D;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then
A1: D c= [:proj1 D, proj2 D:] by Th1;
thus D1 is filtered
proof
let x, y be Element of S1;
assume that
A2: x in D1 and
A3: y in D1;
consider q2 being object such that
A4: [y,q2] in D by A3,XTUPLE_0:def 12;
reconsider D29 = D2 as non empty Subset of S2 by A2,FUNCT_5:16;
reconsider D19 = D1 as non empty Subset of S1 by A2;
consider q1 being object such that
A5: [x,q1] in D by A2,XTUPLE_0:def 12;
reconsider q2 as Element of D29 by A4,XTUPLE_0:def 13;
reconsider q1 as Element of D29 by A5,XTUPLE_0:def 13;
consider z being Element of [:S1,S2:] such that
A6: z in D and
A7: [x,q1] >= z & [y,q2] >= z by A5,A4,WAYBEL_0:def 2;
reconsider z2 = z`2 as Element of D29 by A1,A6,MCART_1:10;
reconsider zz = z`1 as Element of D19 by A1,A6,MCART_1:10;
take zz;
thus zz in D1;
ex x,y being object st x in D19 & y in D29 & z = [x,y]
by A1,A6,ZFMISC_1:def 2;
then z = [zz,z2];
hence thesis by A7,Th11;
end;
let x, y be Element of S2;
assume that
A8: x in D2 and
A9: y in D2;
consider q2 being object such that
A10: [q2,y] in D by A9,XTUPLE_0:def 13;
reconsider D29 = D2 as non empty Subset of S2 by A8;
reconsider D19 = D1 as non empty Subset of S1 by A8,FUNCT_5:16;
consider q1 being object such that
A11: [q1,x] in D by A8,XTUPLE_0:def 13;
reconsider q2 as Element of D19 by A10,XTUPLE_0:def 12;
reconsider q1 as Element of D19 by A11,XTUPLE_0:def 12;
consider z being Element of [:S1,S2:] such that
A12: z in D and
A13: [q1,x] >= z & [q2,y] >= z by A11,A10,WAYBEL_0:def 2;
reconsider z2 = z`1 as Element of D19 by A1,A12,MCART_1:10;
reconsider zz = z`2 as Element of D29 by A1,A12,MCART_1:10;
take zz;
thus zz in D2;
ex x,y being object st x in D19 & y in D29 & z = [x,y]
by A1,A12,ZFMISC_1:def 2;
then z = [z2,zz];
hence thesis by A13,Th11;
end;
registration
let S1, S2 be RelStr, D1 be upper Subset of S1, D2 be upper Subset of S2;
cluster [:D1,D2:] -> upper for Subset of [:S1,S2:];
coherence
proof
set X = [:D1,D2:];
X is upper
proof
let x, y be Element of [:S1,S2:];
assume that
A1: x in X and
A2: x <= y;
consider x1, x2 being object such that
A3: x1 in D1 and
A4: x2 in D2 and
A5: x = [x1,x2] by A1,ZFMISC_1:def 2;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A3,A4;
set C1 = the carrier of s1, C2 = the carrier of s2;
the carrier of [:S1,S2:] = [:C1,C2:] by Def2;
then consider y1, y2 being object such that
A6: y1 in C1 and
A7: y2 in C2 and
A8: y = [y1,y2] by ZFMISC_1:def 2;
reconsider x2, y2 as Element of s2 by A4,A7;
x2 <= y2 by A2,A3,A5,A6,A8,Th11;
then
A9: y2 in D2 by A4,WAYBEL_0:def 20;
reconsider x1, y1 as Element of s1 by A3,A6;
x1 <= y1 by A2,A4,A5,A7,A8,Th11;
then y1 in D1 by A3,WAYBEL_0:def 20;
hence thesis by A8,A9,ZFMISC_1:87;
end;
hence thesis;
end;
end;
theorem
for S1, S2 being non empty reflexive RelStr for D1 being non empty
Subset of S1, D2 being non empty Subset of S2 st [:D1,D2:] is upper holds D1 is
upper & D2 is upper
proof
let S1, S2 be non empty reflexive RelStr, D1 be non empty Subset of S1, D2
be non empty Subset of S2 such that
A1: [:D1,D2:] is upper;
thus D1 is upper
proof
set q1 = the Element of D2;
let x, y be Element of S1;
assume that
A2: x in D1 and
A3: x <= y;
A4: [x,q1] in [:D1,D2:] by A2,ZFMISC_1:87;
q1 <= q1;
then [x,q1] <= [y,q1] by A3,Th11;
then [y,q1] in [:D1,D2:] by A1,A4;
hence thesis by ZFMISC_1:87;
end;
set q1 = the Element of D1;
let x, y be Element of S2;
assume that
A5: x in D2 and
A6: x <= y;
A7: [q1,x] in [:D1,D2:] by A5,ZFMISC_1:87;
q1 <= q1;
then [q1,x] <= [q1,y] by A6,Th11;
then [q1,y] in [:D1,D2:] by A1,A7;
hence thesis by ZFMISC_1:87;
end;
theorem
for S1, S2 being non empty reflexive RelStr for D being non empty
upper Subset of [:S1,S2:] holds proj1 D is upper & proj2 D is upper
proof
let S1, S2 be non empty reflexive RelStr, D be non empty upper Subset of [:
S1,S2:];
set D1 = proj1 D, D2 = proj2 D;
reconsider d1 = D1 as non empty Subset of S1 by Th21;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then
A1: D c= [:D1,D2:] by Th1;
thus D1 is upper
proof
reconsider d2 = D2 as non empty Subset of S2 by Th21;
let x, y be Element of S1 such that
A2: x in D1 and
A3: x <= y;
consider q1 being object such that
A4: [x,q1] in D by A2,XTUPLE_0:def 12;
reconsider q1 as Element of d2 by A1,A4,ZFMISC_1:87;
q1 <= q1;
then [x,q1] <= [y,q1] by A3,Th11;
then [y,q1] in D by A4,WAYBEL_0:def 20;
hence thesis by A1,ZFMISC_1:87;
end;
let x, y be Element of S2 such that
A5: x in D2 and
A6: x <= y;
consider q1 being object such that
A7: [q1,x] in D by A5,XTUPLE_0:def 13;
reconsider q1 as Element of d1 by A1,A7,ZFMISC_1:87;
q1 <= q1;
then [q1,x] <= [q1,y] by A6,Th11;
then [q1,y] in D by A7,WAYBEL_0:def 20;
hence thesis by A1,ZFMISC_1:87;
end;
registration
let S1, S2 be RelStr, D1 be lower Subset of S1, D2 be lower Subset of S2;
cluster [:D1,D2:] -> lower for Subset of [:S1,S2:];
coherence
proof
set X = [:D1,D2:];
X is lower
proof
let x, y be Element of [:S1,S2:];
assume that
A1: x in X and
A2: x >= y;
consider x1, x2 being object such that
A3: x1 in D1 and
A4: x2 in D2 and
A5: x = [x1,x2] by A1,ZFMISC_1:def 2;
reconsider s1 = S1, s2 = S2 as non empty RelStr by A3,A4;
set C1 = the carrier of s1, C2 = the carrier of s2;
the carrier of [:S1,S2:] = [:C1,C2:] by Def2;
then consider y1, y2 being object such that
A6: y1 in C1 and
A7: y2 in C2 and
A8: y = [y1,y2] by ZFMISC_1:def 2;
reconsider x2, y2 as Element of s2 by A4,A7;
x2 >= y2 by A2,A3,A5,A6,A8,Th11;
then
A9: y2 in D2 by A4,WAYBEL_0:def 19;
reconsider x1, y1 as Element of s1 by A3,A6;
x1 >= y1 by A2,A4,A5,A7,A8,Th11;
then y1 in D1 by A3,WAYBEL_0:def 19;
hence thesis by A8,A9,ZFMISC_1:87;
end;
hence thesis;
end;
end;
theorem
for S1, S2 being non empty reflexive RelStr for D1 being non empty
Subset of S1, D2 being non empty Subset of S2 st [:D1,D2:] is lower holds D1 is
lower & D2 is lower
proof
let S1, S2 be non empty reflexive RelStr, D1 be non empty Subset of S1, D2
be non empty Subset of S2 such that
A1: [:D1,D2:] is lower;
thus D1 is lower
proof
set q1 = the Element of D2;
let x, y be Element of S1;
assume that
A2: x in D1 and
A3: x >= y;
A4: [x,q1] in [:D1,D2:] by A2,ZFMISC_1:87;
q1 <= q1;
then [x,q1] >= [y,q1] by A3,Th11;
then [y,q1] in [:D1,D2:] by A1,A4;
hence thesis by ZFMISC_1:87;
end;
set q1 = the Element of D1;
let x, y be Element of S2;
assume that
A5: x in D2 and
A6: x >= y;
A7: [q1,x] in [:D1,D2:] by A5,ZFMISC_1:87;
q1 <= q1;
then [q1,x] >= [q1,y] by A6,Th11;
then [q1,y] in [:D1,D2:] by A1,A7;
hence thesis by ZFMISC_1:87;
end;
theorem
for S1, S2 being non empty reflexive RelStr for D being non empty
lower Subset of [:S1,S2:] holds proj1 D is lower & proj2 D is lower
proof
let S1, S2 be non empty reflexive RelStr, D be non empty lower Subset of [:
S1,S2:];
set D1 = proj1 D, D2 = proj2 D;
reconsider d1 = D1 as non empty Subset of S1 by Th21;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then
A1: D c= [:D1,D2:] by Th1;
thus D1 is lower
proof
reconsider d2 = D2 as non empty Subset of S2 by Th21;
let x, y be Element of S1 such that
A2: x in D1 and
A3: x >= y;
consider q1 being object such that
A4: [x,q1] in D by A2,XTUPLE_0:def 12;
reconsider q1 as Element of d2 by A1,A4,ZFMISC_1:87;
q1 <= q1;
then [x,q1] >= [y,q1] by A3,Th11;
then [y,q1] in D by A4,WAYBEL_0:def 19;
hence thesis by A1,ZFMISC_1:87;
end;
let x, y be Element of S2 such that
A5: x in D2 and
A6: x >= y;
consider q1 being object such that
A7: [q1,x] in D by A5,XTUPLE_0:def 13;
reconsider q1 as Element of d1 by A1,A7,ZFMISC_1:87;
q1 <= q1;
then [q1,x] >= [q1,y] by A6,Th11;
then [q1,y] in D by A7,WAYBEL_0:def 19;
hence thesis by A1,ZFMISC_1:87;
end;
definition
let R be RelStr;
attr R is void means
:Def3:
the InternalRel of R is empty;
end;
registration
cluster empty -> void for RelStr;
coherence;
end;
registration
cluster non void non empty strict for Poset;
existence
proof
set R = the non empty strict Poset;
take R;
(ex x being object st x in the carrier of R )& the InternalRel of R
is_reflexive_in the carrier of R by ORDERS_2:def 2,XBOOLE_0:def 1;
hence the InternalRel of R is non empty;
thus thesis;
end;
end;
registration
cluster non void -> non empty for RelStr;
coherence;
end;
registration
cluster non empty reflexive -> non void for RelStr;
coherence
proof
let R be RelStr;
assume R is non empty reflexive;
then reconsider R1 = R as non empty reflexive RelStr;
(ex x being object st x in the carrier of R1 )& the InternalRel of R1
is_reflexive_in the carrier of R1 by ORDERS_2:def 2,XBOOLE_0:def 1;
hence the InternalRel of R is non empty;
end;
end;
registration
let R be non void RelStr;
cluster the InternalRel of R -> non empty;
coherence by Def3;
end;
theorem Th29:
for S1, S2 being non empty RelStr for D1 being non empty Subset
of S1, D2 being non empty Subset of S2 for x being Element of S1, y being
Element of S2 st [x,y] is_>=_than [:D1,D2:] holds x is_>=_than D1 & y
is_>=_than D2
proof
let S1, S2 be non empty RelStr, D1 be non empty Subset of S1, D2 be non
empty Subset of S2, x be Element of S1, y be Element of S2 such that
A1: [x,y] is_>=_than [:D1,D2:];
thus x is_>=_than D1
proof
set a = the Element of D2;
let b be Element of S1;
assume b in D1;
then [b,a] in [:D1,D2:] by ZFMISC_1:87;
then [b,a] <= [x,y] by A1;
hence thesis by Th11;
end;
set b = the Element of D1;
let a be Element of S2;
assume a in D2;
then [b,a] in [:D1,D2:] by ZFMISC_1:87;
then [b,a] <= [x,y] by A1;
hence thesis by Th11;
end;
theorem Th30:
for S1, S2 being non empty RelStr for D1 being Subset of S1, D2
being Subset of S2 for x being Element of S1, y being Element of S2 st x
is_>=_than D1 & y is_>=_than D2 holds [x,y] is_>=_than [:D1,D2:]
proof
let S1, S2 be non empty RelStr, D1 be Subset of S1, D2 be Subset of S2, x be
Element of S1, y be Element of S2 such that
A1: x is_>=_than D1 & y is_>=_than D2;
let b be Element of [:S1,S2:];
assume b in [:D1,D2:];
then consider b1, b2 being object such that
A2: b1 in D1 and
A3: b2 in D2 and
A4: b = [b1,b2] by ZFMISC_1:def 2;
reconsider b2 as Element of S2 by A3;
reconsider b1 as Element of S1 by A2;
b1 <= x & b2 <= y by A1,A2,A3;
hence thesis by A4,Th11;
end;
theorem Th31:
for S1, S2 being non empty RelStr for D being Subset of [:S1,S2
:] for x being Element of S1, y being Element of S2 holds [x,y] is_>=_than D
iff x is_>=_than proj1 D & y is_>=_than proj2 D
proof
let S1, S2 be non empty RelStr, D be Subset of [:S1,S2:], x be Element of S1
, y be Element of S2;
set D1 = proj1 D, D2 = proj2 D;
hereby
assume
A1: [x,y] is_>=_than D;
thus x is_>=_than D1
proof
let q be Element of S1;
assume q in D1;
then consider z being object such that
A2: [q,z] in D by XTUPLE_0:def 12;
reconsider d2 = D2 as non empty Subset of S2 by A2,XTUPLE_0:def 13;
reconsider z as Element of d2 by A2,XTUPLE_0:def 13;
[x,y] >= [q,z] by A1,A2;
hence thesis by Th11;
end;
thus y is_>=_than D2
proof
let q be Element of S2;
assume q in D2;
then consider z being object such that
A3: [z,q] in D by XTUPLE_0:def 13;
reconsider d1 = D1 as non empty Subset of S1 by A3,XTUPLE_0:def 12;
reconsider z as Element of d1 by A3,XTUPLE_0:def 12;
[x,y] >= [z,q] by A1,A3;
hence thesis by Th11;
end;
end;
assume x is_>=_than proj1 D & y is_>=_than proj2 D;
then
A4: [x,y] is_>=_than [:D1,D2:] by Th30;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then D c= [:D1,D2:] by Th1;
hence thesis by A4;
end;
theorem Th32:
for S1, S2 being non empty RelStr for D1 being non empty Subset
of S1, D2 being non empty Subset of S2 for x being Element of S1, y being
Element of S2 st [x,y] is_<=_than [:D1,D2:] holds x is_<=_than D1 & y
is_<=_than D2
proof
let S1, S2 be non empty RelStr, D1 be non empty Subset of S1, D2 be non
empty Subset of S2, x be Element of S1, y be Element of S2 such that
A1: [x,y] is_<=_than [:D1,D2:];
thus x is_<=_than D1
proof
set a = the Element of D2;
let b be Element of S1;
assume b in D1;
then [b,a] in [:D1,D2:] by ZFMISC_1:87;
then [b,a] >= [x,y] by A1;
hence thesis by Th11;
end;
set b = the Element of D1;
let a be Element of S2;
assume a in D2;
then [b,a] in [:D1,D2:] by ZFMISC_1:87;
then [b,a] >= [x,y] by A1;
hence thesis by Th11;
end;
theorem Th33:
for S1, S2 being non empty RelStr for D1 being Subset of S1, D2
being Subset of S2 for x being Element of S1, y being Element of S2 st x
is_<=_than D1 & y is_<=_than D2 holds [x,y] is_<=_than [:D1,D2:]
proof
let S1, S2 be non empty RelStr, D1 be Subset of S1, D2 be Subset of S2, x be
Element of S1, y be Element of S2 such that
A1: x is_<=_than D1 & y is_<=_than D2;
let b be Element of [:S1,S2:];
assume b in [:D1,D2:];
then consider b1, b2 being object such that
A2: b1 in D1 and
A3: b2 in D2 and
A4: b = [b1,b2] by ZFMISC_1:def 2;
reconsider b2 as Element of S2 by A3;
reconsider b1 as Element of S1 by A2;
b1 >= x & b2 >= y by A1,A2,A3;
hence thesis by A4,Th11;
end;
theorem Th34:
for S1, S2 being non empty RelStr for D being Subset of [:S1,S2
:] for x being Element of S1, y being Element of S2 holds [x,y] is_<=_than D
iff x is_<=_than proj1 D & y is_<=_than proj2 D
proof
let S1, S2 be non empty RelStr, D be Subset of [:S1,S2:], x be Element of S1
, y be Element of S2;
set D1 = proj1 D, D2 = proj2 D;
hereby
assume
A1: [x,y] is_<=_than D;
thus x is_<=_than D1
proof
let q be Element of S1;
assume q in D1;
then consider z being object such that
A2: [q,z] in D by XTUPLE_0:def 12;
reconsider d2 = D2 as non empty Subset of S2 by A2,XTUPLE_0:def 13;
reconsider z as Element of d2 by A2,XTUPLE_0:def 13;
[x,y] <= [q,z] by A1,A2;
hence thesis by Th11;
end;
thus y is_<=_than D2
proof
let q be Element of S2;
assume q in D2;
then consider z being object such that
A3: [z,q] in D by XTUPLE_0:def 13;
reconsider d1 = D1 as non empty Subset of S1 by A3,XTUPLE_0:def 12;
reconsider z as Element of d1 by A3,XTUPLE_0:def 12;
[x,y] <= [z,q] by A1,A3;
hence thesis by Th11;
end;
end;
assume x is_<=_than proj1 D & y is_<=_than proj2 D;
then
A4: [x,y] is_<=_than [:D1,D2:] by Th33;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then D c= [:D1,D2:] by Th1;
hence thesis by A4;
end;
theorem Th35:
for S1, S2 being antisymmetric non empty RelStr for D1 being
Subset of S1, D2 being Subset of S2 for x being Element of S1, y being Element
of S2 st ex_sup_of D1,S1 & ex_sup_of D2,S2 & for b being Element of [:S1,S2:]
st b is_>=_than [:D1,D2:] holds [x,y] <= b holds (for c being Element of S1 st
c is_>=_than D1 holds x <= c) & for d being Element of S2 st d is_>=_than D2
holds y <= d
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be Subset of S1, D2 be
Subset of S2, x be Element of S1, y be Element of S2 such that
A1: ex_sup_of D1,S1 and
A2: ex_sup_of D2,S2 and
A3: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,
y] <= b;
thus for c being Element of S1 st c is_>=_than D1 holds x <= c
proof
A4: sup D2 is_>=_than D2 by A2,YELLOW_0:30;
let b be Element of S1;
assume b is_>=_than D1;
then [x,y] <= [b,sup D2] by A3,A4,Th30;
hence thesis by Th11;
end;
A5: sup D1 is_>=_than D1 by A1,YELLOW_0:30;
let b be Element of S2;
assume b is_>=_than D2;
then [x,y] <= [sup D1,b] by A3,A5,Th30;
hence thesis by Th11;
end;
theorem Th36:
for S1, S2 being antisymmetric non empty RelStr for D1 being
Subset of S1, D2 being Subset of S2 for x being Element of S1, y being Element
of S2 st ex_inf_of D1,S1 & ex_inf_of D2,S2 & for b being Element of [:S1,S2:]
st b is_<=_than [:D1,D2:] holds [x,y] >= b holds (for c being Element of S1 st
c is_<=_than D1 holds x >= c) & for d being Element of S2 st d is_<=_than D2
holds y >= d
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be Subset of S1, D2 be
Subset of S2, x be Element of S1, y be Element of S2 such that
A1: ex_inf_of D1,S1 and
A2: ex_inf_of D2,S2 and
A3: for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [x,
y] >= b;
thus for c being Element of S1 st c is_<=_than D1 holds x >= c
proof
A4: inf D2 is_<=_than D2 by A2,YELLOW_0:31;
let b be Element of S1;
assume b is_<=_than D1;
then [x,y] >= [b,inf D2] by A3,A4,Th33;
hence thesis by Th11;
end;
A5: inf D1 is_<=_than D1 by A1,YELLOW_0:31;
let b be Element of S2;
assume b is_<=_than D2;
then [x,y] >= [inf D1,b] by A3,A5,Th33;
hence thesis by Th11;
end;
theorem
for S1, S2 being antisymmetric non empty RelStr for D1 being non empty
Subset of S1, D2 being non empty Subset of S2 for x being Element of S1, y
being Element of S2 st (for c being Element of S1 st c is_>=_than D1 holds x <=
c) & for d being Element of S2 st d is_>=_than D2 holds y <= d holds for b
being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] <= b
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be non empty Subset of S1,
D2 be non empty Subset of S2, x be Element of S1, y be Element of S2 such that
A1: for c being Element of S1 st c is_>=_than D1 holds x <= c and
A2: for d being Element of S2 st d is_>=_than D2 holds y <= d;
let b be Element of [:S1,S2:] such that
A3: b is_>=_than [:D1,D2:];
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then
ex c, d being object st c in the carrier of S1 & d in the carrier of S2 & b
= [c,d] by ZFMISC_1:def 2;
then
A4: b = [b`1,b`2];
then b`2 is_>=_than D2 by A3,Th29;
then
A5: y <= b`2 by A2;
b`1 is_>=_than D1 by A3,A4,Th29;
then x <= b`1 by A1;
hence thesis by A4,A5,Th11;
end;
theorem
for S1, S2 being antisymmetric non empty RelStr for D1 being non empty
Subset of S1, D2 being non empty Subset of S2 for x being Element of S1, y
being Element of S2 st (for c being Element of S1 st c is_>=_than D1 holds x >=
c) & for d being Element of S2 st d is_>=_than D2 holds y >= d holds for b
being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [x,y] >= b
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be non empty Subset of S1,
D2 be non empty Subset of S2, x be Element of S1, y be Element of S2 such that
A1: for c being Element of S1 st c is_>=_than D1 holds x >= c and
A2: for d being Element of S2 st d is_>=_than D2 holds y >= d;
let b be Element of [:S1,S2:] such that
A3: b is_>=_than [:D1,D2:];
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2;
then
ex c, d being object st c in the carrier of S1 & d in the carrier of S2 & b
= [c,d] by ZFMISC_1:def 2;
then
A4: b = [b`1,b`2];
then b`2 is_>=_than D2 by A3,Th29;
then
A5: y >= b`2 by A2;
b`1 is_>=_than D1 by A3,A4,Th29;
then x >= b`1 by A1;
hence thesis by A4,A5,Th11;
end;
theorem Th39:
for S1, S2 being antisymmetric non empty RelStr for D1 being non
empty Subset of S1, D2 being non empty Subset of S2 holds ex_sup_of D1,S1 &
ex_sup_of D2,S2 iff ex_sup_of [:D1,D2:],[:S1,S2:]
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be non empty Subset of S1,
D2 be non empty Subset of S2;
hereby
assume that
A1: ex_sup_of D1,S1 and
A2: ex_sup_of D2,S2;
consider a2 being Element of S2 such that
A3: D2 is_<=_than a2 and
A4: for b being Element of S2 st D2 is_<=_than b holds a2 <= b by A2,
YELLOW_0:15;
consider a1 being Element of S1 such that
A5: D1 is_<=_than a1 and
A6: for b being Element of S1 st D1 is_<=_than b holds a1 <= b by A1,
YELLOW_0:15;
ex a being Element of [:S1,S2:] st [:D1,D2:] is_<=_than a & for b
being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds a <= b
proof
take a = [a1,a2];
thus [:D1,D2:] is_<=_than a by A5,A3,Th30;
let b be Element of [:S1,S2:] such that
A7: [:D1,D2:] is_<=_than b;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2 :]
by Def2;
then
A8: b = [b`1,b`2] by MCART_1:21;
then D2 is_<=_than b`2 by A7,Th29;
then
A9: a2 <= b`2 by A4;
D1 is_<=_than b`1 by A7,A8,Th29;
then a1 <= b`1 by A6;
hence thesis by A8,A9,Th11;
end;
hence ex_sup_of [:D1,D2:],[:S1,S2:] by YELLOW_0:15;
end;
assume ex_sup_of [:D1,D2:],[:S1,S2:];
then consider x being Element of [:S1,S2:] such that
A10: [:D1,D2:] is_<=_than x and
A11: for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds x
<= b by YELLOW_0:15;
the carrier of [:S1,S2:] = [:the carrier of S1,the carrier of S2:] by Def2;
then
A12: x = [x`1,x`2] by MCART_1:21;
then
A13: D1 is_<=_than x`1 by A10,Th29;
A14: D2 is_<=_than x`2 by A10,A12,Th29;
for b being Element of S1 st D1 is_<=_than b holds x`1 <= b
proof
let b be Element of S1;
assume D1 is_<=_than b;
then x <= [b,x`2] by A11,A14,Th30;
hence thesis by A12,Th11;
end;
hence ex_sup_of D1,S1 by A13,YELLOW_0:15;
for b being Element of S2 st D2 is_<=_than b holds x`2 <= b
proof
let b be Element of S2;
assume D2 is_<=_than b;
then x <= [x`1,b] by A11,A13,Th30;
hence thesis by A12,Th11;
end;
hence thesis by A14,YELLOW_0:15;
end;
theorem Th40:
for S1, S2 being antisymmetric non empty RelStr for D1 being non
empty Subset of S1, D2 being non empty Subset of S2 holds ex_inf_of D1,S1 &
ex_inf_of D2,S2 iff ex_inf_of [:D1,D2:],[:S1,S2:]
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be non empty Subset of S1,
D2 be non empty Subset of S2;
hereby
assume that
A1: ex_inf_of D1,S1 and
A2: ex_inf_of D2,S2;
consider a2 being Element of S2 such that
A3: D2 is_>=_than a2 and
A4: for b being Element of S2 st D2 is_>=_than b holds a2 >= b by A2,
YELLOW_0:16;
consider a1 being Element of S1 such that
A5: D1 is_>=_than a1 and
A6: for b being Element of S1 st D1 is_>=_than b holds a1 >= b by A1,
YELLOW_0:16;
ex a being Element of [:S1,S2:] st [:D1,D2:] is_>=_than a & for b
being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds a >= b
proof
take a = [a1,a2];
thus [:D1,D2:] is_>=_than a by A5,A3,Th33;
let b be Element of [:S1,S2:] such that
A7: [:D1,D2:] is_>=_than b;
the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2 :]
by Def2;
then
A8: b = [b`1,b`2] by MCART_1:21;
then D2 is_>=_than b`2 by A7,Th32;
then
A9: a2 >= b`2 by A4;
D1 is_>=_than b`1 by A7,A8,Th32;
then a1 >= b`1 by A6;
hence thesis by A8,A9,Th11;
end;
hence ex_inf_of [:D1,D2:],[:S1,S2:] by YELLOW_0:16;
end;
assume ex_inf_of [:D1,D2:],[:S1,S2:];
then consider x being Element of [:S1,S2:] such that
A10: [:D1,D2:] is_>=_than x and
A11: for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds x
>= b by YELLOW_0:16;
the carrier of [:S1,S2:] = [:the carrier of S1,the carrier of S2:] by Def2;
then
A12: x = [x`1,x`2] by MCART_1:21;
then
A13: D1 is_>=_than x`1 by A10,Th32;
A14: D2 is_>=_than x`2 by A10,A12,Th32;
for b being Element of S1 st D1 is_>=_than b holds x`1 >= b
proof
let b be Element of S1;
assume D1 is_>=_than b;
then x >= [b,x`2] by A11,A14,Th33;
hence thesis by A12,Th11;
end;
hence ex_inf_of D1,S1 by A13,YELLOW_0:16;
for b being Element of S2 st D2 is_>=_than b holds x`2 >= b
proof
let b be Element of S2;
assume D2 is_>=_than b;
then x >= [x`1,b] by A11,A13,Th33;
hence thesis by A12,Th11;
end;
hence thesis by A14,YELLOW_0:16;
end;
theorem Th41:
for S1, S2 being antisymmetric non empty RelStr for D being
Subset of [:S1,S2:] holds ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 iff
ex_sup_of D,[:S1,S2:]
proof
let S1, S2 be antisymmetric non empty RelStr, D be Subset of [:S1,S2:];
A1: the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2
;
then
A2: D c= [:proj1 D,proj2 D:] by Th1;
hereby
assume that
A3: ex_sup_of proj1 D,S1 and
A4: ex_sup_of proj2 D,S2;
ex a being Element of [:S1,S2:] st D is_<=_than a & for b being
Element of [:S1,S2:] st D is_<=_than b holds a <= b
proof
consider x2 being Element of S2 such that
A5: proj2 D is_<=_than x2 and
A6: for b being Element of S2 st proj2 D is_<=_than b holds x2 <= b
by A4,YELLOW_0:15;
consider x1 being Element of S1 such that
A7: proj1 D is_<=_than x1 and
A8: for b being Element of S1 st proj1 D is_<=_than b holds x1 <= b
by A3,YELLOW_0:15;
take a = [x1,x2];
thus D is_<=_than a
proof
let q be Element of [:S1,S2:];
assume q in D;
then consider q1, q2 being object such that
A9: q1 in proj1 D and
A10: q2 in proj2 D and
A11: q = [q1,q2] by A2,ZFMISC_1:def 2;
reconsider q2 as Element of S2 by A10;
reconsider q1 as Element of S1 by A9;
q1 <= x1 & q2 <= x2 by A7,A5,A9,A10;
hence thesis by A11,Th11;
end;
let b be Element of [:S1,S2:] such that
A12: D is_<=_than b;
A13: b = [b`1,b`2] by A1,MCART_1:21;
then proj2 D is_<=_than b`2 by A12,Th31;
then
A14: x2 <= b`2 by A6;
proj1 D is_<=_than b`1 by A12,A13,Th31;
then x1 <= b`1 by A8;
hence thesis by A13,A14,Th11;
end;
hence ex_sup_of D,[:S1,S2:] by YELLOW_0:15;
end;
assume ex_sup_of D,[:S1,S2:];
then consider x being Element of [:S1,S2:] such that
A15: D is_<=_than x and
A16: for b being Element of [:S1,S2:] st D is_<=_than b holds x <= b by
YELLOW_0:15;
A17: x = [x`1,x`2] by A1,MCART_1:21;
then
A18: proj1 D is_<=_than x`1 by A15,Th31;
A19: proj2 D is_<=_than x`2 by A15,A17,Th31;
for b being Element of S1 st proj1 D is_<=_than b holds x`1 <= b
proof
let b be Element of S1;
assume proj1 D is_<=_than b;
then D is_<=_than [b,x`2] by A19,Th31;
then x <= [b,x`2] by A16;
hence thesis by A17,Th11;
end;
hence ex_sup_of proj1 D,S1 by A18,YELLOW_0:15;
for b being Element of S2 st proj2 D is_<=_than b holds x`2 <= b
proof
let b be Element of S2;
assume proj2 D is_<=_than b;
then D is_<=_than [x`1,b] by A18,Th31;
then x <= [x`1,b] by A16;
hence thesis by A17,Th11;
end;
hence thesis by A19,YELLOW_0:15;
end;
theorem Th42:
for S1, S2 being antisymmetric non empty RelStr for D being
Subset of [:S1,S2:] holds ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 iff
ex_inf_of D,[:S1,S2:]
proof
let S1, S2 be antisymmetric non empty RelStr, D be Subset of [:S1,S2:];
A1: the carrier of [:S1,S2:] = [:the carrier of S1, the carrier of S2:] by Def2
;
then
A2: D c= [:proj1 D,proj2 D:] by Th1;
hereby
assume that
A3: ex_inf_of proj1 D,S1 and
A4: ex_inf_of proj2 D,S2;
ex a being Element of [:S1,S2:] st D is_>=_than a & for b being
Element of [:S1,S2:] st D is_>=_than b holds a >= b
proof
consider x2 being Element of S2 such that
A5: proj2 D is_>=_than x2 and
A6: for b being Element of S2 st proj2 D is_>=_than b holds x2 >= b
by A4,YELLOW_0:16;
consider x1 being Element of S1 such that
A7: proj1 D is_>=_than x1 and
A8: for b being Element of S1 st proj1 D is_>=_than b holds x1 >= b
by A3,YELLOW_0:16;
take a = [x1,x2];
thus D is_>=_than a
proof
let q be Element of [:S1,S2:];
assume q in D;
then consider q1, q2 being object such that
A9: q1 in proj1 D and
A10: q2 in proj2 D and
A11: q = [q1,q2] by A2,ZFMISC_1:def 2;
reconsider q2 as Element of S2 by A10;
reconsider q1 as Element of S1 by A9;
q1 >= x1 & q2 >= x2 by A7,A5,A9,A10;
hence thesis by A11,Th11;
end;
let b be Element of [:S1,S2:] such that
A12: D is_>=_than b;
A13: b = [b`1,b`2] by A1,MCART_1:21;
then proj2 D is_>=_than b`2 by A12,Th34;
then
A14: x2 >= b`2 by A6;
proj1 D is_>=_than b`1 by A12,A13,Th34;
then x1 >= b`1 by A8;
hence thesis by A13,A14,Th11;
end;
hence ex_inf_of D,[:S1,S2:] by YELLOW_0:16;
end;
assume ex_inf_of D,[:S1,S2:];
then consider x being Element of [:S1,S2:] such that
A15: D is_>=_than x and
A16: for b being Element of [:S1,S2:] st D is_>=_than b holds x >= b by
YELLOW_0:16;
A17: x = [x`1,x`2] by A1,MCART_1:21;
then
A18: proj1 D is_>=_than x`1 by A15,Th34;
A19: proj2 D is_>=_than x`2 by A15,A17,Th34;
for b being Element of S1 st proj1 D is_>=_than b holds x`1 >= b
proof
let b be Element of S1;
assume proj1 D is_>=_than b;
then D is_>=_than [b,x`2] by A19,Th34;
then x >= [b,x`2] by A16;
hence thesis by A17,Th11;
end;
hence ex_inf_of proj1 D,S1 by A18,YELLOW_0:16;
for b being Element of S2 st proj2 D is_>=_than b holds x`2 >= b
proof
let b be Element of S2;
assume proj2 D is_>=_than b;
then D is_>=_than [x`1,b] by A18,Th34;
then x >= [x`1,b] by A16;
hence thesis by A17,Th11;
end;
hence thesis by A19,YELLOW_0:16;
end;
theorem Th43:
for S1, S2 being antisymmetric non empty RelStr for D1 being non
empty Subset of S1, D2 being non empty Subset of S2 st ex_sup_of D1,S1 &
ex_sup_of D2,S2 holds sup [:D1,D2:] = [sup D1,sup D2]
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be non empty Subset of S1,
D2 be non empty Subset of S2 such that
A1: ex_sup_of D1,S1 & ex_sup_of D2,S2;
set s = sup [:D1,D2:];
s is Element of [:the carrier of S1,the carrier of S2:] by Def2;
then consider s1, s2 being object such that
A2: s1 in the carrier of S1 and
A3: s2 in the carrier of S2 and
A4: s = [s1,s2] by ZFMISC_1:def 2;
reconsider s2 as Element of S2 by A3;
reconsider s1 as Element of S1 by A2;
A5: ex_sup_of [:D1,D2:],[:S1,S2:] by A1,Th39;
then
A6: [s1,s2] is_>=_than [:D1,D2:] by A4,YELLOW_0:30;
then
A7: s1 is_>=_than D1 by Th29;
A8: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds [s1,s2]
<= b by A4,A5,YELLOW_0:30;
then for b being Element of S1 st b is_>=_than D1 holds s1 <= b by A1,Th35;
then
A9: s1 = sup D1 by A7,YELLOW_0:30;
A10: s2 is_>=_than D2 by A6,Th29;
for b being Element of S2 st b is_>=_than D2 holds s2 <= b by A1,A8,Th35;
hence thesis by A4,A9,A10,YELLOW_0:30;
end;
theorem Th44:
for S1, S2 being antisymmetric non empty RelStr for D1 being non
empty Subset of S1, D2 being non empty Subset of S2 st ex_inf_of D1,S1 &
ex_inf_of D2,S2 holds inf [:D1,D2:] = [inf D1,inf D2]
proof
let S1, S2 be antisymmetric non empty RelStr, D1 be non empty Subset of S1,
D2 be non empty Subset of S2 such that
A1: ex_inf_of D1,S1 & ex_inf_of D2,S2;
set s = inf [:D1,D2:];
s is Element of [:the carrier of S1,the carrier of S2:] by Def2;
then consider s1, s2 being object such that
A2: s1 in the carrier of S1 and
A3: s2 in the carrier of S2 and
A4: s = [s1,s2] by ZFMISC_1:def 2;
reconsider s2 as Element of S2 by A3;
reconsider s1 as Element of S1 by A2;
A5: ex_inf_of [:D1,D2:],[:S1,S2:] by A1,Th40;
then
A6: [s1,s2] is_<=_than [:D1,D2:] by A4,YELLOW_0:31;
then
A7: s1 is_<=_than D1 by Th32;
A8: for b being Element of [:S1,S2:] st b is_<=_than [:D1,D2:] holds [s1,s2]
>= b by A4,A5,YELLOW_0:31;
then for b being Element of S1 st b is_<=_than D1 holds s1 >= b by A1,Th36;
then
A9: s1 = inf D1 by A7,YELLOW_0:31;
A10: s2 is_<=_than D2 by A6,Th32;
for b being Element of S2 st b is_<=_than D2 holds s2 >= b by A1,A8,Th36;
hence thesis by A4,A9,A10,YELLOW_0:31;
end;
registration
let X, Y be complete antisymmetric non empty RelStr;
cluster [:X,Y:] -> complete;
coherence
proof
set IT = [:X,Y:];
for D being Subset of IT holds ex_sup_of D, IT
proof
let D be Subset of IT;
ex_sup_of proj1 D,X & ex_sup_of proj2 D,Y by YELLOW_0:17;
hence thesis by Th41;
end;
hence thesis by YELLOW_0:53;
end;
end;
theorem
for X, Y being non empty lower-bounded antisymmetric RelStr st [:X,Y:]
is complete holds X is complete & Y is complete
proof
let X, Y be non empty lower-bounded antisymmetric RelStr such that
A1: [:X,Y:] is complete;
for A being Subset of X holds ex_sup_of A,X
proof
let A be Subset of X;
per cases;
suppose
A2: A is non empty;
set B = the non empty Subset of Y;
ex_sup_of [:A,B:],[:X,Y:] by A1,YELLOW_0:17;
hence thesis by A2,Th39;
end;
suppose
A is empty;
hence thesis by YELLOW_0:42;
end;
end;
hence X is complete by YELLOW_0:53;
for B being Subset of Y holds ex_sup_of B,Y
proof
let B be Subset of Y;
per cases;
suppose
A3: B is non empty;
set A = the non empty Subset of X;
ex_sup_of [:A,B:],[:X,Y:] by A1,YELLOW_0:17;
hence thesis by A3,Th39;
end;
suppose
B is empty;
hence thesis by YELLOW_0:42;
end;
end;
hence thesis by YELLOW_0:53;
end;
theorem
for L1,L2 being antisymmetric non empty RelStr for D being non empty
Subset of [:L1,L2:] st [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] holds sup
D = [sup proj1 D,sup proj2 D]
proof
let L1,L2 be antisymmetric non empty RelStr, D be non empty Subset of [:L1,
L2:];
reconsider C1 = the carrier of L1, C2 = the carrier of L2 as non empty set;
the carrier of [:L1,L2:] = [:C1,C2:] by Def2;
then consider d1, d2 being object such that
A1: d1 in C1 and
A2: d2 in C2 and
A3: sup D = [d1,d2] by ZFMISC_1:def 2;
reconsider d1 as Element of L1 by A1;
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
proj1 D9 is non empty;
then reconsider D1=proj1 D as non empty Subset of L1;
proj2 D9 is non empty;
then reconsider D2=proj2 D as non empty Subset of L2;
A4: D9 c= [:D1,D2:] by Th1;
reconsider d2 as Element of L2 by A2;
assume [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:];
then
A5: ex_sup_of D,[:L1,L2:] by YELLOW_0:17;
then
A6: ex_sup_of D2,L2 by Th41;
A7: ex_sup_of D1,L1 by A5,Th41;
then ex_sup_of [:D1,D2:],[:L1,L2:] by A6,Th39;
then sup D <= sup [:D1,D2:] by A5,A4,YELLOW_0:34;
then
A8: sup D <= [sup proj1 D,sup proj2 D] by A7,A6,Th43;
D2 is_<=_than d2
proof
let b be Element of L2;
assume b in D2;
then consider x being object such that
A9: [x,b] in D by XTUPLE_0:def 13;
reconsider x as Element of D1 by A9,XTUPLE_0:def 12;
reconsider x as Element of L1;
D is_<=_than [d1,d2] by A5,A3,YELLOW_0:def 9;
then [x,b] <= [d1,d2] by A9;
hence thesis by Th11;
end;
then
A10: sup D2 <= d2 by A6,YELLOW_0:def 9;
D1 is_<=_than d1
proof
let b be Element of L1;
assume b in D1;
then consider x being object such that
A11: [b,x] in D by XTUPLE_0:def 12;
reconsider x as Element of D2 by A11,XTUPLE_0:def 13;
reconsider x as Element of L2;
D is_<=_than [d1,d2] by A5,A3,YELLOW_0:def 9;
then [b,x] <= [d1,d2] by A11;
hence thesis by Th11;
end;
then sup D1 <= d1 by A7,YELLOW_0:def 9;
then [sup D1,sup D2] <= sup D by A3,A10,Th11;
hence thesis by A8,ORDERS_2:2;
end;
theorem
for L1,L2 being antisymmetric non empty RelStr for D being non empty
Subset of [:L1,L2:] st [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] holds inf
D = [inf proj1 D,inf proj2 D]
proof
let L1,L2 be antisymmetric non empty RelStr, D be non empty Subset of [:L1,
L2:];
reconsider C1 = the carrier of L1, C2 = the carrier of L2 as non empty set;
the carrier of [:L1,L2:] = [:C1,C2:] by Def2;
then consider d1, d2 being object such that
A1: d1 in C1 and
A2: d2 in C2 and
A3: inf D = [d1,d2] by ZFMISC_1:def 2;
reconsider d1 as Element of L1 by A1;
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
proj1 D9 is non empty;
then reconsider D1 = proj1 D as non empty Subset of L1;
proj2 D9 is non empty;
then reconsider D2 = proj2 D as non empty Subset of L2;
A4: D9 c= [:D1,D2:] by Th1;
reconsider d2 as Element of L2 by A2;
assume [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:];
then
A5: ex_inf_of D,[:L1,L2:] by YELLOW_0:17;
then
A6: ex_inf_of D2,L2 by Th42;
A7: ex_inf_of D1,L1 by A5,Th42;
then ex_inf_of [:D1,D2:],[:L1,L2:] by A6,Th40;
then inf D >= inf [:D1,D2:] by A5,A4,YELLOW_0:35;
then
A8: inf D >= [inf proj1 D,inf proj2 D] by A7,A6,Th44;
D2 is_>=_than d2
proof
let b be Element of L2;
assume b in D2;
then consider x being object such that
A9: [x,b] in D by XTUPLE_0:def 13;
reconsider x as Element of D1 by A9,XTUPLE_0:def 12;
reconsider x as Element of L1;
D is_>=_than [d1,d2] by A5,A3,YELLOW_0:def 10;
then [x,b] >= [d1,d2] by A9;
hence thesis by Th11;
end;
then
A10: inf D2 >= d2 by A6,YELLOW_0:def 10;
D1 is_>=_than d1
proof
let b be Element of L1;
assume b in D1;
then consider x being object such that
A11: [b,x] in D by XTUPLE_0:def 12;
reconsider x as Element of D2 by A11,XTUPLE_0:def 13;
reconsider x as Element of L2;
D is_>=_than [d1,d2] by A5,A3,YELLOW_0:def 10;
then [b,x] >= [d1,d2] by A11;
hence thesis by Th11;
end;
then inf D1 >= d1 by A7,YELLOW_0:def 10;
then [inf D1,inf D2] >= inf D by A3,A10,Th11;
hence thesis by A8,ORDERS_2:2;
end;
theorem
for S1,S2 being non empty reflexive RelStr for D being non empty
directed Subset of [:S1,S2:] holds [:proj1 D,proj2 D:] c= downarrow D
proof
let S1,S2 be non empty reflexive RelStr, D be non empty directed Subset of
[:S1,S2:];
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set;
let q be object;
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
set D1 = proj1 D, D2 = proj2 D;
A1: downarrow D = {x where x is Element of [:S1,S2:] : ex y being Element of
[:S1,S2:] st x <= y & y in D} by WAYBEL_0:14;
A2: D9 c= [:D1,D2:] by Th1;
proj2 D9 is non empty;
then reconsider D2 as non empty Subset of S2;
proj1 D9 is non empty;
then reconsider D1 as non empty Subset of S1;
assume q in [:proj1 D,proj2 D:];
then consider d, e being object such that
A3: d in D1 and
A4: e in D2 and
A5: q = [d,e] by ZFMISC_1:def 2;
consider y being object such that
A6: [d,y] in D by A3,XTUPLE_0:def 12;
consider x being object such that
A7: [x,e] in D by A4,XTUPLE_0:def 13;
reconsider y, e as Element of D2 by A6,A7,XTUPLE_0:def 13;
reconsider x, d as Element of D1 by A6,A7,XTUPLE_0:def 12;
consider z being Element of [:S1,S2:] such that
A8: z in D and
A9: [d,y] <= z & [x,e] <= z by A6,A7,WAYBEL_0:def 1;
consider z1, z2 being object such that
A10: z1 in D1 and
A11: z2 in D2 and
A12: z = [z1,z2] by A2,A8,ZFMISC_1:def 2;
reconsider z2 as Element of D2 by A11;
reconsider z1 as Element of D1 by A10;
d <= z1 & e <= z2 by A9,A10,A11,A12,Th11;
then [d,e] <= [z1,z2] by Th11;
hence thesis by A5,A1,A8,A12;
end;
theorem
for S1,S2 being non empty reflexive RelStr for D being non empty
filtered Subset of [:S1,S2:] holds [:proj1 D,proj2 D:] c= uparrow D
proof
let S1,S2 be non empty reflexive RelStr, D be non empty filtered Subset of
[:S1,S2:];
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set;
let q be object;
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
set D1 = proj1 D, D2 = proj2 D;
A1: uparrow D = {x where x is Element of [:S1,S2:] : ex y being Element of
[:S1,S2:] st x >= y & y in D} by WAYBEL_0:15;
A2: D9 c= [:D1,D2:] by Th1;
proj2 D9 is non empty;
then reconsider D2 as non empty Subset of S2;
proj1 D9 is non empty;
then reconsider D1 as non empty Subset of S1;
assume q in [:proj1 D,proj2 D:];
then consider d, e being object such that
A3: d in D1 and
A4: e in D2 and
A5: q = [d,e] by ZFMISC_1:def 2;
consider y being object such that
A6: [d,y] in D by A3,XTUPLE_0:def 12;
consider x being object such that
A7: [x,e] in D by A4,XTUPLE_0:def 13;
reconsider y, e as Element of D2 by A6,A7,XTUPLE_0:def 13;
reconsider x, d as Element of D1 by A6,A7,XTUPLE_0:def 12;
consider z being Element of [:S1,S2:] such that
A8: z in D and
A9: [d,y] >= z & [x,e] >= z by A6,A7,WAYBEL_0:def 2;
consider z1, z2 being object such that
A10: z1 in D1 and
A11: z2 in D2 and
A12: z = [z1,z2] by A2,A8,ZFMISC_1:def 2;
reconsider z2 as Element of D2 by A11;
reconsider z1 as Element of D1 by A10;
d >= z1 & e >= z2 by A9,A10,A11,A12,Th11;
then [d,e] >= [z1,z2] by Th11;
hence thesis by A5,A1,A8,A12;
end;
scheme
Kappa2DS { X,Y,Z() -> non empty RelStr, F(set,set) -> set }: ex f being
Function of [:X(),Y():], Z() st for x being Element of X(), y being Element of
Y() holds f.(x,y)=F(x,y)
provided
A1: for x being Element of X(), y being Element of Y() holds F(x,y) is
Element of Z()
proof
A2: for x being Element of X(), y being Element of Y() holds F(x,y) in the
carrier of Z()
proof
let x be Element of X(), y be Element of Y();
reconsider x1 = x as Element of X();
reconsider y1 = y as Element of Y();
F(x1,y1) is Element of Z() by A1;
hence thesis;
end;
consider f being Function of [:the carrier of X(),the carrier of Y():], the
carrier of Z() such that
A3: for x being Element of X(), y being Element of Y() holds f.(x,y)=F(x
,y) from FUNCT_7:sch 1(A2);
the carrier of [:X(),Y():] = [:the carrier of X(), the carrier of Y() :]
by Def2;
then reconsider f as Function of [:X(),Y():], Z();
take f;
thus thesis by A3;
end;