yellow_3.miz
begin
scheme ::
YELLOW_3:sch1
FraenkelA2 { A() -> non
empty
set , F(
set,
set) ->
set , P[
set,
set], Q[
set,
set] } :
{ F(s,t) where s be
Element of A(), t be
Element of A() : P[s, t] } is
Subset of A()
provided
A1: for s be
Element of A(), t be
Element of A() holds F(s,t)
in A();
{ F(s,t) where s be
Element of A(), t be
Element of A() : P[s, t] }
c= A()
proof
let q be
object;
assume q
in { F(s,t) where s be
Element of A(), t be
Element of A() : P[s, t] };
then ex s,t be
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 be
object such that
A1: x
in (
downarrow X) by
XBOOLE_0:def 1;
reconsider x as
Element of L by
A1;
ex z be
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 be
object such that
A2: x
in (
uparrow X) by
XBOOLE_0:def 1;
reconsider x as
Element of L by
A2;
ex z be
Element of L st z
<= x & z
in X by
A2,
WAYBEL_0:def 16;
hence contradiction;
end;
end
theorem ::
YELLOW_3:1
Th1: for X,Y be
set, D be
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 be
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,
XTUPLE_0:def 13;
hence thesis by
A2,
ZFMISC_1:def 2;
end;
theorem ::
YELLOW_3:2
for L be
with_infima
transitive
antisymmetric
RelStr holds for a,b,c,d be
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 be
Element of L st c
>= x & d
>= x & for z be
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 ::
YELLOW_3:3
for L be
with_suprema
transitive
antisymmetric
RelStr holds for a,b,c,d be
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 be
Element of L st a
<= x & b
<= x & for z be
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 ::
YELLOW_3:4
for L be
complete
reflexive
antisymmetric non
empty
RelStr holds for D be
Subset of L, x be
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 ::
YELLOW_3:5
for L be
complete
reflexive
antisymmetric non
empty
RelStr holds for D be
Subset of L, x be
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 ::
YELLOW_3:6
for L be
RelStr, X,Y be
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 be
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 ::
YELLOW_3:7
for L be
RelStr, X,Y be
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 be
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 ::
YELLOW_3:8
for S,T be
with_infima
Poset, f be
Function of S, T holds for x,y be
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 ::
YELLOW_3:9
for S,T be
with_suprema
Poset, f be
Function of S, T holds for x,y be
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 ::
YELLOW_3:sch2
InfUnion { L() ->
complete
antisymmetric non
empty
RelStr , P[
set] } :
(
"/\" ({ (
"/\" (X,L())) where X be
Subset of L() : P[X] },L()))
>= (
"/\" ((
union { X where X be
Subset of L() : P[X] }),L()));
(
"/\" ((
union { X where X be
Subset of L() : P[X] }),L()))
is_<=_than { (
"/\" (X,L())) where X be
Subset of L() : P[X] }
proof
let a be
Element of L();
assume a
in { (
"/\" (X,L())) where X be
Subset of L() : P[X] };
then
consider q be
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 be
Subset of L() : P[X] }),L()) by
YELLOW_0: 17;
q
in { X where X be
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 ::
YELLOW_3:sch3
InfofInfs { L() ->
complete
LATTICE , P[
set] } :
(
"/\" ({ (
"/\" (X,L())) where X be
Subset of L() : P[X] },L()))
= (
"/\" ((
union { X where X be
Subset of L() : P[X] }),L()));
(
union { X where X be
Subset of L() : P[X] })
is_>=_than (
"/\" ({ (
"/\" (X,L())) where X be
Subset of L() : P[X] },L()))
proof
let a be
Element of L();
assume a
in (
union { X where X be
Subset of L() : P[X] });
then
consider b be
set such that
A1: a
in b and
A2: b
in { X where X be
Subset of L() : P[X] } by
TARSKI:def 4;
consider c be
Subset of L() such that
A3: b
= c and
A4: P[c] by
A2;
(
"/\" (c,L()))
in { (
"/\" (X,L())) where X be
Subset of L() : P[X] } by
A4;
then
A5: (
"/\" (c,L()))
>= (
"/\" ({ (
"/\" (X,L())) where X be
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 be
Subset of L() : P[X] }),L()))
>= (
"/\" ({ (
"/\" (X,L())) where X be
Subset of L() : P[X] },L())) by
YELLOW_0: 33;
(
"/\" ({ (
"/\" (X,L())) where X be
Subset of L() : P[X] },L()))
>= (
"/\" ((
union { X where X be
Subset of L() : P[X] }),L())) from
InfUnion;
hence thesis by
A6,
ORDERS_2: 2;
end;
scheme ::
YELLOW_3:sch4
SupUnion { L() ->
complete
antisymmetric non
empty
RelStr , P[
set] } :
(
"\/" ({ (
"\/" (X,L())) where X be
Subset of L() : P[X] },L()))
<= (
"\/" ((
union { X where X be
Subset of L() : P[X] }),L()));
A1: (
"\/" ((
union { X where X be
Subset of L() : P[X] }),L()))
is_>=_than { (
"\/" (X,L())) where X be
Subset of L() : P[X] }
proof
let a be
Element of L();
assume a
in { (
"\/" (X,L())) where X be
Subset of L() : P[X] };
then
consider q be
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 be
Subset of L() : P[X] }),L()) by
YELLOW_0: 17;
q
in { X where X be
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 be
Subset of L() : P[X] },L()) by
YELLOW_0: 17;
hence thesis by
A1,
YELLOW_0:def 9;
end;
scheme ::
YELLOW_3:sch5
SupofSups { L() ->
complete
LATTICE , P[
set] } :
(
"\/" ({ (
"\/" (X,L())) where X be
Subset of L() : P[X] },L()))
= (
"\/" ((
union { X where X be
Subset of L() : P[X] }),L()));
A1: (
union { X where X be
Subset of L() : P[X] })
is_<=_than (
"\/" ({ (
"\/" (X,L())) where X be
Subset of L() : P[X] },L()))
proof
let a be
Element of L();
assume a
in (
union { X where X be
Subset of L() : P[X] });
then
consider b be
set such that
A2: a
in b and
A3: b
in { X where X be
Subset of L() : P[X] } by
TARSKI:def 4;
consider c be
Subset of L() such that
A4: b
= c and
A5: P[c] by
A3;
(
"\/" (c,L()))
in { (
"\/" (X,L())) where X be
Subset of L() : P[X] } by
A5;
then
A6: (
"\/" (c,L()))
<= (
"\/" ({ (
"\/" (X,L())) where X be
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 be
Subset of L() : P[X] },L())) by
A6,
YELLOW_0:def 2;
end;
A7: (
"\/" ({ (
"\/" (X,L())) where X be
Subset of L() : P[X] },L()))
<= (
"\/" ((
union { X where X be
Subset of L() : P[X] }),L())) from
SupUnion;
ex_sup_of ((
union { X where X be
Subset of L() : P[X] }),L()) by
YELLOW_0: 17;
then (
"\/" ((
union { X where X be
Subset of L() : P[X] }),L()))
<= (
"\/" ({ (
"\/" (X,L())) where X be
Subset of L() : P[X] },L())) by
A1,
YELLOW_0:def 9;
hence thesis by
A7,
ORDERS_2: 2;
end;
begin
definition
let P,R be
Relation;
::
YELLOW_3:def1
func
["P,R"] ->
Relation means
:
Def1: for x,y be
object holds
[x, y]
in it iff ex p,q,s,t be
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 be
object st $1
=
[p, q] & $2
=
[s, t] &
[p, s]
in P &
[q, t]
in R;
consider Q be
Relation such that
A1: for x,y be
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 be
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 be
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 be
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 be
object holds
[x, y]
in A iff
P[x, y] and
A8: for x,y be
object holds
[x, y]
in B iff
P[x, y];
thus A
= B from
RELAT_1:sch 2(
A7,
A8);
end;
end
theorem ::
YELLOW_3:10
Th10: for P,R be
Relation, x be
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 be
object st x
=
[a, b]) & (ex c,d be
object st (x
`1 )
=
[c, d]) & ex e,f be
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 be
object such that
A2: x
=
[y, z] by
RELAT_1:def 1;
consider p,q,s,t be
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 be
object st x
=
[a, b] by
A2;
thus ex c,d be
object st (x
`1 )
=
[c, d] by
A2,
A3;
thus ex e,f be
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 be
object such that
A8: x
=
[a, b];
given c,d be
object such that
A9: (x
`1 )
=
[c, d];
given e,f be
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;
:: original:
["
redefine
func
["P,R"] ->
Relation of
[:A, X:],
[:B, Y:] ;
coherence
proof
["P, R"]
c=
[:
[:A, X:],
[:B, Y:]:]
proof
let q be
object;
assume
A1: q
in
["P, R"];
then
consider a,b be
object such that
A2: q
=
[a, b] by
Th10;
[((q
`1 )
`2 ), ((q
`2 )
`2 )]
in R by
A1,
Th10;
then
consider s,t be
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 be
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 be
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 be
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;
::
YELLOW_3:def2
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:];
:: original:
proj1
redefine
func
proj1 D ->
Subset of L1 ;
coherence
proof
(
proj1 D)
c= the
carrier of L1
proof
let x be
object;
assume x
in (
proj1 D);
then
A1: ex y be
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;
:: original:
proj2
redefine
func
proj2 D ->
Subset of L2 ;
coherence
proof
(
proj2 D)
c= the
carrier of L2
proof
let y be
object;
assume y
in (
proj2 D);
then
A2: ex x be
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;
:: original:
[:
redefine
func
[:D1,D2:] ->
Subset of
[:S1, S2:] ;
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;
:: original:
[
redefine
func
[x,y] ->
Element of
[:S1, S2:] ;
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:];
:: original:
`1
redefine
func x
`1 ->
Element of L1 ;
coherence
proof
the
carrier of
[:L1, L2:]
=
[:the
carrier of L1, the
carrier of L2:] by
Def2;
hence thesis by
MCART_1: 10;
end;
:: original:
`2
redefine
func x
`2 ->
Element of L2 ;
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 ::
YELLOW_3:11
Th11: for S1,S2 be non
empty
RelStr holds for a,c be
Element of S1, b,d be
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 ::
YELLOW_3:12
Th12: for S1,S2 be non
empty
RelStr, x,y be
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 be
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 be
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 ::
YELLOW_3:13
for A,B be
RelStr, C be non
empty
RelStr holds for f,g be
Function of
[:A, B:], C st for x be
Element of A, y be
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 be
Element of A, y be
Element of B holds (f
. (x,y))
= (g
. (x,y));
then
A1: for x,y be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
Element of X such that
A1: (x
`1 )
<= zx & (y
`1 )
<= zx and
A2: for z9 be
Element of X st (x
`1 )
<= z9 & (y
`1 )
<= z9 holds zx
<= z9 by
LATTICE3:def 10;
consider zy be
Element of Y such that
A3: (x
`2 )
<= zy & (y
`2 )
<= zy and
A4: for z9 be
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 be
object st a
in the
carrier of X & b
in the
carrier of Y & x
=
[a, b]) & ex c,d be
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 be
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 be
Element of X such that
A1: (x
`1 )
>= zx & (y
`1 )
>= zx and
A2: for z9 be
Element of X st (x
`1 )
>= z9 & (y
`1 )
>= z9 holds zx
>= z9 by
LATTICE3:def 11;
consider zy be
Element of Y such that
A3: (x
`2 )
>= zy & (y
`2 )
>= zy and
A4: for z9 be
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 be
object st a
in the
carrier of X & b
in the
carrier of Y & x
=
[a, b]) & ex c,d be
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 be
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 ::
YELLOW_3:14
for X,Y be
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 be
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 ::
YELLOW_3:15
for X,Y be 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 be
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 be
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 ::
YELLOW_3:16
for X,Y be 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 be
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 be
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 ::
YELLOW_3:17
for X,Y be 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 be
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 be
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 ::
YELLOW_3:18
for X,Y be 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 be
Element of
[:X, Y:] such that
A4:
[x, a]
<= z &
[y, a]
<= z and
A5: for z9 be
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 be
Element of
[:X, Y:] such that
A8:
[a, x]
<= z &
[a, y]
<= z and
A9: for z9 be
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 ::
YELLOW_3:19
for X,Y be 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 be
Element of
[:X, Y:] such that
A4:
[x, a]
>= z &
[y, a]
>= z and
A5: for z9 be
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 be
Element of
[:X, Y:] such that
A8:
[a, x]
>= z &
[a, y]
>= z and
A9: for z9 be
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;
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 be
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 be
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 be
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 be
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 ::
YELLOW_3:20
for S1,S2 be non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 be
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 be
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 be
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 be
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 ::
YELLOW_3:21
Th21: for S1,S2 be non
empty
RelStr holds for D be 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 ::
YELLOW_3:22
for S1,S2 be non
empty
reflexive
RelStr holds for D be 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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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;
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 be
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 be
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 be
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 be
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 ::
YELLOW_3:23
for S1,S2 be non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 be
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 be
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 be
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 be
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 ::
YELLOW_3:24
for S1,S2 be non
empty
reflexive
RelStr holds for D be 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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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;
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 be
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 be
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 ::
YELLOW_3:25
for S1,S2 be non
empty
reflexive
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 ::
YELLOW_3:26
for S1,S2 be non
empty
reflexive
RelStr holds for D be 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 be
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 be
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;
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 be
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 be
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 ::
YELLOW_3:27
for S1,S2 be non
empty
reflexive
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 ::
YELLOW_3:28
for S1,S2 be non
empty
reflexive
RelStr holds for D be 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 be
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 be
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;
::
YELLOW_3:def3
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 be
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 be
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 ::
YELLOW_3:29
Th29: for S1,S2 be non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be non
empty
Subset of S2 holds for x be
Element of S1, y be
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 ::
YELLOW_3:30
Th30: for S1,S2 be non
empty
RelStr holds for D1 be
Subset of S1, D2 be
Subset of S2 holds for x be
Element of S1, y be
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 be
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 ::
YELLOW_3:31
Th31: for S1,S2 be non
empty
RelStr holds for D be
Subset of
[:S1, S2:] holds for x be
Element of S1, y be
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 be
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 be
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 ::
YELLOW_3:32
Th32: for S1,S2 be non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be non
empty
Subset of S2 holds for x be
Element of S1, y be
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 ::
YELLOW_3:33
Th33: for S1,S2 be non
empty
RelStr holds for D1 be
Subset of S1, D2 be
Subset of S2 holds for x be
Element of S1, y be
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 be
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 ::
YELLOW_3:34
Th34: for S1,S2 be non
empty
RelStr holds for D be
Subset of
[:S1, S2:] holds for x be
Element of S1, y be
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 be
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 be
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 ::
YELLOW_3:35
Th35: for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be
Subset of S1, D2 be
Subset of S2 holds for x be
Element of S1, y be
Element of S2 st
ex_sup_of (D1,S1) &
ex_sup_of (D2,S2) & for b be
Element of
[:S1, S2:] st b
is_>=_than
[:D1, D2:] holds
[x, y]
<= b holds (for c be
Element of S1 st c
is_>=_than D1 holds x
<= c) & for d be
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 be
Element of
[:S1, S2:] st b
is_>=_than
[:D1, D2:] holds
[x, y]
<= b;
thus for c be
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 ::
YELLOW_3:36
Th36: for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be
Subset of S1, D2 be
Subset of S2 holds for x be
Element of S1, y be
Element of S2 st
ex_inf_of (D1,S1) &
ex_inf_of (D2,S2) & for b be
Element of
[:S1, S2:] st b
is_<=_than
[:D1, D2:] holds
[x, y]
>= b holds (for c be
Element of S1 st c
is_<=_than D1 holds x
>= c) & for d be
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 be
Element of
[:S1, S2:] st b
is_<=_than
[:D1, D2:] holds
[x, y]
>= b;
thus for c be
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 ::
YELLOW_3:37
for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be non
empty
Subset of S2 holds for x be
Element of S1, y be
Element of S2 st (for c be
Element of S1 st c
is_>=_than D1 holds x
<= c) & for d be
Element of S2 st d
is_>=_than D2 holds y
<= d holds for b be
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 be
Element of S1 st c
is_>=_than D1 holds x
<= c and
A2: for d be
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 be
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 ::
YELLOW_3:38
for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be non
empty
Subset of S2 holds for x be
Element of S1, y be
Element of S2 st (for c be
Element of S1 st c
is_>=_than D1 holds x
>= c) & for d be
Element of S2 st d
is_>=_than D2 holds y
>= d holds for b be
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 be
Element of S1 st c
is_>=_than D1 holds x
>= c and
A2: for d be
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 be
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 ::
YELLOW_3:39
Th39: for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 be
Element of S2 such that
A3: D2
is_<=_than a2 and
A4: for b be
Element of S2 st D2
is_<=_than b holds a2
<= b by
A2,
YELLOW_0: 15;
consider a1 be
Element of S1 such that
A5: D1
is_<=_than a1 and
A6: for b be
Element of S1 st D1
is_<=_than b holds a1
<= b by
A1,
YELLOW_0: 15;
ex a be
Element of
[:S1, S2:] st
[:D1, D2:]
is_<=_than a & for b be
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 be
Element of
[:S1, S2:] such that
A10:
[:D1, D2:]
is_<=_than x and
A11: for b be
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 be
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 be
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 ::
YELLOW_3:40
Th40: for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 be
Element of S2 such that
A3: D2
is_>=_than a2 and
A4: for b be
Element of S2 st D2
is_>=_than b holds a2
>= b by
A2,
YELLOW_0: 16;
consider a1 be
Element of S1 such that
A5: D1
is_>=_than a1 and
A6: for b be
Element of S1 st D1
is_>=_than b holds a1
>= b by
A1,
YELLOW_0: 16;
ex a be
Element of
[:S1, S2:] st
[:D1, D2:]
is_>=_than a & for b be
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 be
Element of
[:S1, S2:] such that
A10:
[:D1, D2:]
is_>=_than x and
A11: for b be
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 be
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 be
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 ::
YELLOW_3:41
Th41: for S1,S2 be
antisymmetric non
empty
RelStr holds for D be
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 be
Element of
[:S1, S2:] st D
is_<=_than a & for b be
Element of
[:S1, S2:] st D
is_<=_than b holds a
<= b
proof
consider x2 be
Element of S2 such that
A5: (
proj2 D)
is_<=_than x2 and
A6: for b be
Element of S2 st (
proj2 D)
is_<=_than b holds x2
<= b by
A4,
YELLOW_0: 15;
consider x1 be
Element of S1 such that
A7: (
proj1 D)
is_<=_than x1 and
A8: for b be
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 be
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 be
Element of
[:S1, S2:] such that
A15: D
is_<=_than x and
A16: for b be
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 be
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 be
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 ::
YELLOW_3:42
Th42: for S1,S2 be
antisymmetric non
empty
RelStr holds for D be
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 be
Element of
[:S1, S2:] st D
is_>=_than a & for b be
Element of
[:S1, S2:] st D
is_>=_than b holds a
>= b
proof
consider x2 be
Element of S2 such that
A5: (
proj2 D)
is_>=_than x2 and
A6: for b be
Element of S2 st (
proj2 D)
is_>=_than b holds x2
>= b by
A4,
YELLOW_0: 16;
consider x1 be
Element of S1 such that
A7: (
proj1 D)
is_>=_than x1 and
A8: for b be
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 be
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 be
Element of
[:S1, S2:] such that
A15: D
is_>=_than x and
A16: for b be
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 be
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 be
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 ::
YELLOW_3:43
Th43: for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 be
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 be
Element of
[:S1, S2:] st b
is_>=_than
[:D1, D2:] holds
[s1, s2]
<= b by
A4,
A5,
YELLOW_0: 30;
then for b be
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 be
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 ::
YELLOW_3:44
Th44: for S1,S2 be
antisymmetric non
empty
RelStr holds for D1 be non
empty
Subset of S1, D2 be 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 be
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 be
Element of
[:S1, S2:] st b
is_<=_than
[:D1, D2:] holds
[s1, s2]
>= b by
A4,
A5,
YELLOW_0: 31;
then for b be
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 be
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 be
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 ::
YELLOW_3:45
for X,Y be 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 be
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 be
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 ::
YELLOW_3:46
for L1,L2 be
antisymmetric non
empty
RelStr holds for D be 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 be
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 be
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 be
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 ::
YELLOW_3:47
for L1,L2 be
antisymmetric non
empty
RelStr holds for D be 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 be
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 be
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 be
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 ::
YELLOW_3:48
for S1,S2 be non
empty
reflexive
RelStr holds for D be 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 be
Element of
[:S1, S2:] : ex y be
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 be
object such that
A3: d
in D1 and
A4: e
in D2 and
A5: q
=
[d, e] by
ZFMISC_1:def 2;
consider y be
object such that
A6:
[d, y]
in D by
A3,
XTUPLE_0:def 12;
consider x be
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 be
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 be
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 ::
YELLOW_3:49
for S1,S2 be non
empty
reflexive
RelStr holds for D be 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 be
Element of
[:S1, S2:] : ex y be
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 be
object such that
A3: d
in D1 and
A4: e
in D2 and
A5: q
=
[d, e] by
ZFMISC_1:def 2;
consider y be
object such that
A6:
[d, y]
in D by
A3,
XTUPLE_0:def 12;
consider x be
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 be
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 be
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 ::
YELLOW_3:sch6
Kappa2DS { X,Y,Z() -> non
empty
RelStr , F(
set,
set) ->
set } :
ex f be
Function of
[:X(), Y():], Z() st for x be
Element of X(), y be
Element of Y() holds (f
. (x,y))
= F(x,y)
provided
A1: for x be
Element of X(), y be
Element of Y() holds F(x,y) is
Element of Z();
A2: for x be
Element of X(), y be
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 be
Function of
[:the
carrier of X(), the
carrier of Y():], the
carrier of Z() such that
A3: for x be
Element of X(), y be
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;