:: YELLOW_3 semantic presentation
begin
scheme :: YELLOW_3:sch 1
FraenkelA2{ F1() -> non empty set , F2( set , set ) -> set , P1[ set , set ], P2[ set , set ] } :
{ F2(s,t) where s, t is Element of F1() : P1[s,t] } is Subset of F1()
provided
A1: for s, t being Element of F1() holds F2(s,t) in F1()
proof
{ F2(s,t) where s, t is Element of F1() : P1[s,t] } c= F1()
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { F2(s,t) where s, t is Element of F1() : P1[s,t] } or q in F1() )
assume q in { F2(s,t) where s, t is Element of F1() : P1[s,t] } ; ::_thesis: q in F1()
then ex s, t being Element of F1() st
( q = F2(s,t) & P1[s,t] ) ;
hence q in F1() by A1; ::_thesis: verum
end;
hence { F2(s,t) where s, t is Element of F1() : P1[s,t] } is Subset of F1() ; ::_thesis: verum
end;
registration
let L be RelStr ;
let X be empty Subset of L;
cluster downarrow X -> empty ;
coherence
downarrow X is empty
proof
assume not downarrow X is empty ; ::_thesis: contradiction
then consider x being set such that
A1: x in downarrow X by XBOOLE_0:def_1;
reconsider x = 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 ; ::_thesis: verum
end;
cluster uparrow X -> empty ;
coherence
uparrow X is empty
proof
assume not uparrow X is empty ; ::_thesis: contradiction
then consider x being set such that
A2: x in uparrow X by XBOOLE_0:def_1;
reconsider x = 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 ; ::_thesis: verum
end;
end;
theorem Th1: :: YELLOW_3:1
for X, Y being set
for D being Subset of [:X,Y:] holds D c= [:(proj1 D),(proj2 D):]
proof
let X, Y be set ; ::_thesis: for D being Subset of [:X,Y:] holds D c= [:(proj1 D),(proj2 D):]
let D be Subset of [:X,Y:]; ::_thesis: D c= [:(proj1 D),(proj2 D):]
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in D or q in [:(proj1 D),(proj2 D):] )
assume A1: q in D ; ::_thesis: q in [:(proj1 D),(proj2 D):]
then consider x, y being set 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 q in [:(proj1 D),(proj2 D):] by A2, ZFMISC_1:def_2; ::_thesis: verum
end;
Lm1: for x, a1, a2, b1, b2 being set st x = [[a1,a2],[b1,b2]] holds
( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 )
proof
let x, a1, a2, b1, b2 be set ; ::_thesis: ( x = [[a1,a2],[b1,b2]] implies ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) )
assume x = [[a1,a2],[b1,b2]] ; ::_thesis: ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 )
then ( x `1 = [a1,a2] & x `2 = [b1,b2] ) by MCART_1:7;
hence ( (x `1) `1 = a1 & (x `1) `2 = a2 & (x `2) `1 = b1 & (x `2) `2 = b2 ) by MCART_1:7; ::_thesis: verum
end;
theorem :: YELLOW_3:2
for L being transitive antisymmetric with_infima RelStr
for a, b, c, d being Element of L st a <= c & b <= d holds
a "/\" b <= c "/\" d
proof
let L be transitive antisymmetric with_infima RelStr ; ::_thesis: for a, b, c, d being Element of L st a <= c & b <= d holds
a "/\" b <= c "/\" d
let a, b, c, d be Element of L; ::_thesis: ( a <= c & b <= d implies a "/\" b <= c "/\" d )
assume that
A1: a <= c and
A2: b <= d ; ::_thesis: a "/\" b <= c "/\" 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 a "/\" b <= c "/\" d by A4, LATTICE3:def_14; ::_thesis: verum
end;
theorem :: YELLOW_3:3
for L being transitive antisymmetric with_suprema RelStr
for a, b, c, d being Element of L st a <= c & b <= d holds
a "\/" b <= c "\/" d
proof
let L be transitive antisymmetric with_suprema RelStr ; ::_thesis: for a, b, c, d being Element of L st a <= c & b <= d holds
a "\/" b <= c "\/" d
let a, b, c, d be Element of L; ::_thesis: ( a <= c & b <= d implies a "\/" b <= c "\/" d )
assume that
A1: a <= c and
A2: b <= d ; ::_thesis: a "\/" b <= c "\/" 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 a "\/" b <= c "\/" d by A4, LATTICE3:def_13; ::_thesis: verum
end;
theorem :: YELLOW_3:4
for L being non empty reflexive antisymmetric complete RelStr
for D being Subset of L
for x being Element of L st x in D holds
(sup D) "/\" x = x
proof
let L be non empty reflexive antisymmetric complete RelStr ; ::_thesis: for D being Subset of L
for x being Element of L st x in D holds
(sup D) "/\" x = x
let D be Subset of L; ::_thesis: for x being Element of L st x in D holds
(sup D) "/\" x = x
let x be Element of L; ::_thesis: ( x in D implies (sup D) "/\" x = x )
assume A1: x in D ; ::_thesis: (sup D) "/\" x = x
D is_<=_than sup D by YELLOW_0:32;
then x <= sup D by A1, LATTICE3:def_9;
hence (sup D) "/\" x = x by YELLOW_0:25; ::_thesis: verum
end;
theorem :: YELLOW_3:5
for L being non empty reflexive antisymmetric complete RelStr
for D being Subset of L
for x being Element of L st x in D holds
(inf D) "\/" x = x
proof
let L be non empty reflexive antisymmetric complete RelStr ; ::_thesis: for D being Subset of L
for x being Element of L st x in D holds
(inf D) "\/" x = x
let D be Subset of L; ::_thesis: for x being Element of L st x in D holds
(inf D) "\/" x = x
let x be Element of L; ::_thesis: ( x in D implies (inf D) "\/" x = x )
assume A1: x in D ; ::_thesis: (inf D) "\/" x = x
D is_>=_than inf D by YELLOW_0:33;
then inf D <= x by A1, LATTICE3:def_8;
hence (inf D) "\/" x = x by YELLOW_0:24; ::_thesis: verum
end;
theorem :: YELLOW_3:6
for L being RelStr
for X, Y being Subset of L st X c= Y holds
downarrow X c= downarrow Y
proof
let L be RelStr ; ::_thesis: for X, Y being Subset of L st X c= Y holds
downarrow X c= downarrow Y
let X, Y be Subset of L; ::_thesis: ( X c= Y implies downarrow X c= downarrow Y )
assume A1: X c= Y ; ::_thesis: downarrow X c= downarrow Y
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in downarrow X or q in downarrow Y )
assume A2: q in downarrow X ; ::_thesis: q in downarrow Y
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 q in downarrow Y by A1, WAYBEL_0:def_15; ::_thesis: verum
end;
theorem :: YELLOW_3:7
for L being RelStr
for X, Y being Subset of L st X c= Y holds
uparrow X c= uparrow Y
proof
let L be RelStr ; ::_thesis: for X, Y being Subset of L st X c= Y holds
uparrow X c= uparrow Y
let X, Y be Subset of L; ::_thesis: ( X c= Y implies uparrow X c= uparrow Y )
assume A1: X c= Y ; ::_thesis: uparrow X c= uparrow Y
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in uparrow X or q in uparrow Y )
assume A2: q in uparrow X ; ::_thesis: q in uparrow Y
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 q in uparrow Y by A1, WAYBEL_0:def_16; ::_thesis: verum
end;
theorem :: YELLOW_3:8
for S, T being with_infima Poset
for 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; ::_thesis: for 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) )
let f be Function of S,T; ::_thesis: for x, y being Element of S holds
( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )
let x, y be Element of S; ::_thesis: ( f preserves_inf_of {x,y} iff f . (x "/\" y) = (f . x) "/\" (f . y) )
A1: dom f = the carrier of S by FUNCT_2:def_1;
hereby ::_thesis: ( f . (x "/\" y) = (f . x) "/\" (f . y) implies f preserves_inf_of {x,y} )
A2: ex_inf_of {x,y},S by YELLOW_0:21;
assume A3: f preserves_inf_of {x,y} ; ::_thesis: f . (x "/\" y) = (f . x) "/\" (f . y)
thus f . (x "/\" y) = f . (inf {x,y}) by YELLOW_0:40
.= inf (f .: {x,y}) by A3, A2, WAYBEL_0:def_30
.= inf {(f . x),(f . y)} by A1, FUNCT_1:60
.= (f . x) "/\" (f . y) by YELLOW_0:40 ; ::_thesis: verum
end;
assume A4: f . (x "/\" y) = (f . x) "/\" (f . y) ; ::_thesis: f preserves_inf_of {x,y}
assume ex_inf_of {x,y},S ; :: according to WAYBEL_0:def_30 ::_thesis: ( ex_inf_of f .: {x,y},T & "/\" ((f .: {x,y}),T) = f . ("/\" ({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; ::_thesis: "/\" ((f .: {x,y}),T) = f . ("/\" ({x,y},S))
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 ; ::_thesis: verum
end;
theorem :: YELLOW_3:9
for S, T being with_suprema Poset
for 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; ::_thesis: for 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) )
let f be Function of S,T; ::_thesis: for x, y being Element of S holds
( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )
let x, y be Element of S; ::_thesis: ( f preserves_sup_of {x,y} iff f . (x "\/" y) = (f . x) "\/" (f . y) )
A1: dom f = the carrier of S by FUNCT_2:def_1;
hereby ::_thesis: ( f . (x "\/" y) = (f . x) "\/" (f . y) implies f preserves_sup_of {x,y} )
A2: ex_sup_of {x,y},S by YELLOW_0:20;
assume A3: f preserves_sup_of {x,y} ; ::_thesis: f . (x "\/" y) = (f . x) "\/" (f . y)
thus f . (x "\/" y) = f . (sup {x,y}) by YELLOW_0:41
.= sup (f .: {x,y}) by A3, A2, WAYBEL_0:def_31
.= sup {(f . x),(f . y)} by A1, FUNCT_1:60
.= (f . x) "\/" (f . y) by YELLOW_0:41 ; ::_thesis: verum
end;
assume A4: f . (x "\/" y) = (f . x) "\/" (f . y) ; ::_thesis: f preserves_sup_of {x,y}
assume ex_sup_of {x,y},S ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of f .: {x,y},T & "\/" ((f .: {x,y}),T) = f . ("\/" ({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; ::_thesis: "\/" ((f .: {x,y}),T) = f . ("\/" ({x,y},S))
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 ; ::_thesis: verum
end;
scheme :: YELLOW_3:sch 2
InfUnion{ F1() -> non empty antisymmetric complete RelStr , P1[ set ] } :
"/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1())
proof
"/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) is_<=_than { ("/\" (X,F1())) where X is Subset of F1() : P1[X] }
proof
let a be Element of F1(); :: according to LATTICE3:def_8 ::_thesis: ( not a in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } or "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a )
assume a in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ; ::_thesis: "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a
then consider q being Subset of F1() such that
A1: a = "/\" (q,F1()) and
A2: P1[q] ;
A3: ( ex_inf_of q,F1() & ex_inf_of union { X where X is Subset of F1() : P1[X] } ,F1() ) by YELLOW_0:17;
q in { X where X is Subset of F1() : P1[X] } by A2;
hence "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= a by A1, A3, YELLOW_0:35, ZFMISC_1:74; ::_thesis: verum
end;
hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by YELLOW_0:33; ::_thesis: verum
end;
scheme :: YELLOW_3:sch 3
InfofInfs{ F1() -> complete LATTICE, P1[ set ] } :
"/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1())
proof
union { X where X is Subset of F1() : P1[X] } is_>=_than "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1())
proof
let a be Element of F1(); :: according to LATTICE3:def_8 ::_thesis: ( not a in union { X where X is Subset of F1() : P1[X] } or "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a )
assume a in union { X where X is Subset of F1() : P1[X] } ; ::_thesis: "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a
then consider b being set such that
A1: a in b and
A2: b in { X where X is Subset of F1() : P1[X] } by TARSKI:def_4;
consider c being Subset of F1() such that
A3: b = c and
A4: P1[c] by A2;
"/\" (c,F1()) in { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } by A4;
then A5: "/\" (c,F1()) >= "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_2:22;
"/\" (c,F1()) <= a by A1, A3, YELLOW_2:22;
hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= a by A5, YELLOW_0:def_2; ::_thesis: verum
end;
then A6: "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) >= "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_0:33;
"/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) >= "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) from YELLOW_3:sch_2();
hence "/\" ( { ("/\" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "/\" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A6, ORDERS_2:2; ::_thesis: verum
end;
scheme :: YELLOW_3:sch 4
SupUnion{ F1() -> non empty antisymmetric complete RelStr , P1[ set ] } :
"\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1())
proof
A1: "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) is_>=_than { ("\/" (X,F1())) where X is Subset of F1() : P1[X] }
proof
let a be Element of F1(); :: according to LATTICE3:def_9 ::_thesis: ( not a in { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } or a <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) )
assume a in { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ; ::_thesis: a <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1())
then consider q being Subset of F1() such that
A2: a = "\/" (q,F1()) and
A3: P1[q] ;
A4: ( ex_sup_of q,F1() & ex_sup_of union { X where X is Subset of F1() : P1[X] } ,F1() ) by YELLOW_0:17;
q in { X where X is Subset of F1() : P1[X] } by A3;
hence a <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A2, A4, YELLOW_0:34, ZFMISC_1:74; ::_thesis: verum
end;
ex_sup_of { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1() by YELLOW_0:17;
hence "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A1, YELLOW_0:def_9; ::_thesis: verum
end;
scheme :: YELLOW_3:sch 5
SupofSups{ F1() -> complete LATTICE, P1[ set ] } :
"\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1())
proof
A1: union { X where X is Subset of F1() : P1[X] } is_<=_than "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1())
proof
let a be Element of F1(); :: according to LATTICE3:def_9 ::_thesis: ( not a in union { X where X is Subset of F1() : P1[X] } or a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) )
assume a in union { X where X is Subset of F1() : P1[X] } ; ::_thesis: a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1())
then consider b being set such that
A2: a in b and
A3: b in { X where X is Subset of F1() : P1[X] } by TARSKI:def_4;
consider c being Subset of F1() such that
A4: b = c and
A5: P1[c] by A3;
"\/" (c,F1()) in { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } by A5;
then A6: "\/" (c,F1()) <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by YELLOW_2:22;
a <= "\/" (c,F1()) by A2, A4, YELLOW_2:22;
hence a <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by A6, YELLOW_0:def_2; ::_thesis: verum
end;
A7: "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) <= "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) from YELLOW_3:sch_4();
ex_sup_of union { X where X is Subset of F1() : P1[X] } ,F1() by YELLOW_0:17;
then "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) <= "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) by A1, YELLOW_0:def_9;
hence "\/" ( { ("\/" (X,F1())) where X is Subset of F1() : P1[X] } ,F1()) = "\/" ((union { X where X is Subset of F1() : P1[X] } ),F1()) by A7, ORDERS_2:2; ::_thesis: verum
end;
begin
definition
let P, R be Relation;
func["P,R"] -> Relation means :Def1: :: YELLOW_3:def 1
for x, y being set holds
( [x,y] in it iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
proof
defpred S1[ set , set ] means ex p, s, q, t being set 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 set holds
( [x,y] in Q iff ( x in [:(dom P),(dom R):] & y in [:(rng P),(rng R):] & S1[x,y] ) ) from RELAT_1:sch_1();
take Q ; ::_thesis: for x, y being set holds
( [x,y] in Q iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
let x, y be set ; ::_thesis: ( [x,y] in Q iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) )
hereby ::_thesis: ( ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) implies [x,y] in Q )
assume [x,y] in Q ; ::_thesis: ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
then consider p, s, q, t being set such that
A2: ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) by A1;
take p = p; ::_thesis: ex q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take q = q; ::_thesis: ex s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take s = s; ::_thesis: ex t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
take t = t; ::_thesis: ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R )
thus ( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) by A2; ::_thesis: verum
end;
given p, q, s, t being set such that A3: x = [p,q] and
A4: y = [s,t] and
A5: ( [p,s] in P & [q,t] in R ) ; ::_thesis: [x,y] in Q
( 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 [x,y] in Q by A1, A3, A4, A5, A6; ::_thesis: verum
end;
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) holds
b1 = b2
proof
defpred S1[ set , set ] means ex p, q, s, t being set st
( $1 = [p,q] & $2 = [s,t] & [p,s] in P & [q,t] in R );
let A, B be Relation; ::_thesis: ( ( for x, y being set holds
( [x,y] in A iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) & ( for x, y being set holds
( [x,y] in B iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) ) implies A = B )
assume that
A7: for x, y being set holds
( [x,y] in A iff S1[x,y] ) and
A8: for x, y being set holds
( [x,y] in B iff S1[x,y] ) ; ::_thesis: A = B
thus A = B from RELAT_1:sch_2(A7, A8); ::_thesis: verum
end;
end;
:: deftheorem Def1 defines [" YELLOW_3:def_1_:_
for P, R, b3 being Relation holds
( b3 = ["P,R"] iff for x, y being set holds
( [x,y] in b3 iff ex p, q, s, t being set st
( x = [p,q] & y = [s,t] & [p,s] in P & [q,t] in R ) ) );
theorem Th10: :: YELLOW_3:10
for P, R being Relation
for x being set 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 set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )
proof
let P, R be Relation; ::_thesis: for x being set 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 set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )
let x be set ; ::_thesis: ( 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 set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] ) )
hereby ::_thesis: ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] implies x in ["P,R"] )
assume A1: x in ["P,R"] ; ::_thesis: ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R & ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
then consider y, z being set such that
A2: x = [y,z] by RELAT_1:def_1;
consider p, q, s, t being set 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, A4, Lm1;
hence ( [((x `1) `1),((x `2) `1)] in P & [((x `1) `2),((x `2) `2)] in R ) by A2, A3, A4, A5, Lm1; ::_thesis: ( ex a, b being set st x = [a,b] & ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
thus ex a, b being set st x = [a,b] by A2; ::_thesis: ( ex c, d being set st x `1 = [c,d] & ex e, f being set st x `2 = [e,f] )
thus ex c, d being set st x `1 = [c,d] by A2, A3, MCART_1:7; ::_thesis: ex e, f being set st x `2 = [e,f]
thus ex e, f being set st x `2 = [e,f] by A2, A4, MCART_1:7; ::_thesis: verum
end;
assume that
A6: [((x `1) `1),((x `2) `1)] in P and
A7: [((x `1) `2),((x `2) `2)] in R and
A8: ex a, b being set st x = [a,b] and
A9: ex c, d being set st x `1 = [c,d] and
A10: ex e, f being set st x `2 = [e,f] ; ::_thesis: x in ["P,R"]
consider c, d being set such that
A11: x `1 = [c,d] by A9;
consider e, f being set such that
A12: x `2 = [e,f] by A10;
[c,((x `2) `1)] in P by A6, A11, MCART_1:7;
then A13: [c,e] in P by A12, MCART_1:7;
consider a, b being set such that
A14: x = [a,b] by A8;
[d,((x `2) `2)] in R by A7, A11, MCART_1:7;
then A15: [d,f] in R by A12, MCART_1:7;
A16: b = [e,f] by A14, A12, MCART_1:7;
a = [c,d] by A14, A11, MCART_1:7;
hence x in ["P,R"] by A14, A16, A13, A15, Def1; ::_thesis: verum
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
["P,R"] is Relation of [:A,X:],[:B,Y:]
proof
["P,R"] c= [:[:A,X:],[:B,Y:]:]
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in ["P,R"] or q in [:[:A,X:],[:B,Y:]:] )
assume A1: q in ["P,R"] ; ::_thesis: q in [:[:A,X:],[:B,Y:]:]
then consider a, b being set such that
A2: q = [a,b] by Th10;
[((q `1) `2),((q `2) `2)] in R by A1, Th10;
then consider s, t being set 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 set 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 set 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 set such that
A10: q `1 = [a1,b1] by A1, Th10;
A11: b = [a2,b2] by A2, A6, MCART_1:7;
then A12: b `2 = t by A3, A6, XTUPLE_0:1;
A13: a = [a1,b1] by A2, A10, MCART_1:7;
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, MCART_1:11;
a `1 = x by A7, A10, A13, XTUPLE_0:1;
then a in [:A,X:] by A8, A4, A13, A14, MCART_1:11;
hence q in [:[:A,X:],[:B,Y:]:] by A2, A15, ZFMISC_1:def_2; ::_thesis: verum
end;
hence ["P,R"] is Relation of [:A,X:],[:B,Y:] ; ::_thesis: verum
end;
end;
definition
let X, Y be RelStr ;
func[:X,Y:] -> strict RelStr means :Def2: :: YELLOW_3:def 2
( 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
ex b1 being strict RelStr st
( the carrier of b1 = [: the carrier of X, the carrier of Y:] & the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] )
proof
take RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) ; ::_thesis: ( the carrier of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [: the carrier of X, the carrier of Y:] & the InternalRel of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [" the InternalRel of X, the InternalRel of Y"] )
thus ( the carrier of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [: the carrier of X, the carrier of Y:] & the InternalRel of RelStr(# [: the carrier of X, the carrier of Y:],[" the InternalRel of X, the InternalRel of Y"] #) = [" the InternalRel of X, the InternalRel of Y"] ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict RelStr st the carrier of b1 = [: the carrier of X, the carrier of Y:] & the InternalRel of b1 = [" the InternalRel of X, the InternalRel of Y"] & the carrier of b2 = [: the carrier of X, the carrier of Y:] & the InternalRel of b2 = [" the InternalRel of X, the InternalRel of Y"] holds
b1 = b2 ;
end;
:: deftheorem Def2 defines [: YELLOW_3:def_2_:_
for X, Y being RelStr
for b3 being strict RelStr holds
( b3 = [:X,Y:] iff ( the carrier of b3 = [: the carrier of X, the carrier of Y:] & the InternalRel of b3 = [" the InternalRel of X, the InternalRel of Y"] ) );
definition
let L1, L2 be RelStr ;
let D be Subset of [:L1,L2:];
:: original: proj1
redefine func proj1 D -> Subset of L1;
coherence
proj1 D is Subset of L1
proof
proj1 D c= the carrier of L1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 D or x in the carrier of L1 )
assume x in proj1 D ; ::_thesis: x in the carrier of L1
then A1: ex y being set 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 x in the carrier of L1 by A1, ZFMISC_1:87; ::_thesis: verum
end;
hence proj1 D is Subset of L1 ; ::_thesis: verum
end;
:: original: proj2
redefine func proj2 D -> Subset of L2;
coherence
proj2 D is Subset of L2
proof
proj2 D c= the carrier of L2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 D or y in the carrier of L2 )
assume y in proj2 D ; ::_thesis: y in the carrier of L2
then A2: ex x being set 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 y in the carrier of L2 by A2, ZFMISC_1:87; ::_thesis: verum
end;
hence proj2 D is Subset of L2 ; ::_thesis: verum
end;
end;
definition
let S1, S2 be RelStr ;
let D1 be Subset of S1;
let D2 be Subset of S2;
:: original: [:
redefine func[:D1,D2:] -> Subset of [:S1,S2:];
coherence
[:D1,D2:] is Subset of [:S1,S2:]
proof
[:D1,D2:] c= [: the carrier of S1, the carrier of S2:] ;
hence [:D1,D2:] is Subset of [:S1,S2:] by Def2; ::_thesis: verum
end;
end;
definition
let S1, S2 be non empty RelStr ;
let x be Element of S1;
let y be Element of S2;
:: original: [
redefine func[x,y] -> Element of [:S1,S2:];
coherence
[x,y] is Element of [:S1,S2:]
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 [x,y] is Element of [:S1,S2:] ; ::_thesis: verum
end;
end;
definition
let L1, L2 be non empty RelStr ;
let x be Element of [:L1,L2:];
:: original: `1
redefine funcx `1 -> Element of L1;
coherence
x `1 is Element of L1
proof
the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2;
hence x `1 is Element of L1 by MCART_1:10; ::_thesis: verum
end;
:: original: `2
redefine funcx `2 -> Element of L2;
coherence
x `2 is Element of L2
proof
the carrier of [:L1,L2:] = [: the carrier of L1, the carrier of L2:] by Def2;
hence x `2 is Element of L2 by MCART_1:10; ::_thesis: verum
end;
end;
theorem Th11: :: YELLOW_3:11
for S1, S2 being non empty RelStr
for a, c being Element of S1
for b, d being Element of S2 holds
( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
proof
let S1, S2 be non empty RelStr ; ::_thesis: for a, c being Element of S1
for b, d being Element of S2 holds
( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
let a, c be Element of S1; ::_thesis: for b, d being Element of S2 holds
( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
let b, d be Element of S2; ::_thesis: ( ( a <= c & b <= d ) iff [a,b] <= [c,d] )
set I1 = the InternalRel of S1;
set I2 = the InternalRel of S2;
set x = [[a,b],[c,d]];
A1: ( ([[a,b],[c,d]] `1) `1 = a & ([[a,b],[c,d]] `2) `1 = c ) ;
A2: ( ([[a,b],[c,d]] `1) `2 = b & ([[a,b],[c,d]] `2) `2 = d ) ;
thus ( a <= c & b <= d implies [a,b] <= [c,d] ) ::_thesis: ( [a,b] <= [c,d] implies ( a <= c & b <= d ) )
proof
assume ( a <= c & b <= d ) ; ::_thesis: [a,b] <= [c,d]
then ( [(([[a,b],[c,d]] `1) `1),(([[a,b],[c,d]] `2) `1)] in the InternalRel of S1 & [(([[a,b],[c,d]] `1) `2),(([[a,b],[c,d]] `2) `2)] in the InternalRel of S2 ) by ORDERS_2:def_5;
then [[a,b],[c,d]] in [" the InternalRel of S1, the InternalRel of S2"] by Th10;
hence [[a,b],[c,d]] in the InternalRel of [:S1,S2:] by Def2; :: according to ORDERS_2:def_5 ::_thesis: verum
end;
assume [a,b] <= [c,d] ; ::_thesis: ( a <= c & b <= d )
then [[a,b],[c,d]] in the InternalRel of [:S1,S2:] by ORDERS_2:def_5;
then [[a,b],[c,d]] in [" the InternalRel of S1, the InternalRel of S2"] by Def2;
hence ( [a,c] in the InternalRel of S1 & [b,d] in the InternalRel of S2 ) by A1, A2, Th10; :: according to ORDERS_2:def_5 ::_thesis: verum
end;
theorem Th12: :: YELLOW_3:12
for S1, S2 being non empty RelStr
for 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 ; ::_thesis: for x, y being Element of [:S1,S2:] holds
( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) )
let x, y be Element of [:S1,S2:]; ::_thesis: ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) )
A1: the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then ex c, d being set 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)] by MCART_1:8;
ex a, b being set 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)] by MCART_1:8;
hence ( x <= y iff ( x `1 <= y `1 & x `2 <= y `2 ) ) by A2, Th11; ::_thesis: verum
end;
theorem :: YELLOW_3:13
for A, B being RelStr
for C being non empty RelStr
for f, g being Function of [:A,B:],C st ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) holds
f = g
proof
let A, B be RelStr ; ::_thesis: for C being non empty RelStr
for f, g being Function of [:A,B:],C st ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) holds
f = g
let C be non empty RelStr ; ::_thesis: for f, g being Function of [:A,B:],C st ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) holds
f = g
let f, g be Function of [:A,B:],C; ::_thesis: ( ( for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ) implies f = g )
assume for x being Element of A
for y being Element of B holds f . (x,y) = g . (x,y) ; ::_thesis: f = g
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 f = g by A1, BINOP_1:1; ::_thesis: verum
end;
registration
let X, Y be non empty RelStr ;
cluster[:X,Y:] -> non empty strict ;
coherence
not [:X,Y:] is empty
proof
set y = the Element of Y;
set x = the Element of X;
[ the Element of X, the Element of Y] in [: the carrier of X, the carrier of Y:] by ZFMISC_1:87;
hence not [:X,Y:] is empty by Def2; ::_thesis: verum
end;
end;
registration
let X, Y be reflexive RelStr ;
cluster[:X,Y:] -> strict reflexive ;
coherence
[:X,Y:] is reflexive
proof
let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of [:X,Y:] or [x,x] in the InternalRel of [:X,Y:] )
assume x in the carrier of [:X,Y:] ; ::_thesis: [x,x] in the InternalRel of [:X,Y:]
then x in [: the carrier of X, the carrier of Y:] by Def2;
then consider x1, x2 being set 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, RELAT_2:def_1;
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, RELAT_2:def_1;
set a = [[x1,x2],[x1,x2]];
A6: ( [[x1,x2],[x1,x2]] `1 = [x1,x2] & [[x1,x2],[x1,x2]] `2 = [x1,x2] ) ;
( ([[x1,x2],[x1,x2]] `1) `1 = x1 & ([[x1,x2],[x1,x2]] `1) `2 = x2 ) ;
then [x,x] in [" the InternalRel of X, the InternalRel of Y"] by A3, A4, A5, A6, Th10;
hence [x,x] in the InternalRel of [:X,Y:] by Def2; ::_thesis: verum
end;
end;
registration
let X, Y be antisymmetric RelStr ;
cluster[:X,Y:] -> strict antisymmetric ;
coherence
[:X,Y:] is antisymmetric
proof
let x, y be set ; :: according to RELAT_2:def_4,ORDERS_2:def_4 ::_thesis: ( not x in the carrier of [:X,Y:] or not y in the carrier of [:X,Y:] or not [x,y] in the InternalRel of [:X,Y:] or not [y,x] in the InternalRel of [:X,Y:] or x = y )
assume 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:] ; ::_thesis: x = y
x in [: the carrier of X, the carrier of Y:] by A1, Def2;
then consider x1, x2 being set 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 set 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, MCART_1:7;
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, MCART_1:7;
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, MCART_1:7;
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, MCART_1:7;
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 x = y by A6, A7, A9, A10, A15, A13, RELAT_2:def_4; ::_thesis: verum
end;
end;
registration
let X, Y be transitive RelStr ;
cluster[:X,Y:] -> strict transitive ;
coherence
[:X,Y:] is transitive
proof
set P = the InternalRel of X;
set R = the InternalRel of Y;
let x, y, z be set ; :: according to RELAT_2:def_8,ORDERS_2:def_3 ::_thesis: ( not x in the carrier of [:X,Y:] or not y in the carrier of [:X,Y:] or not z in the carrier of [:X,Y:] or not [x,y] in the InternalRel of [:X,Y:] or not [y,z] in the InternalRel of [:X,Y:] or [x,z] in the InternalRel of [:X,Y:] )
assume 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:] ; ::_thesis: [x,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 set 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 set 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 [" the InternalRel of X, the InternalRel of Y"] by A5, Def2;
then [(([y,z] `1) `1),(([y,z] `2) `1)] in the InternalRel of X by Th10;
then [(y `1),(([y,z] `2) `1)] in the InternalRel of X ;
then [(y `1),(z `1)] in the InternalRel of X ;
then [y1,(z `1)] in the InternalRel of X by A8, MCART_1:7;
then A13: [y1,z1] in the InternalRel of X by A11, MCART_1:7;
x in [: the carrier of X, the carrier of Y:] by A1, Def2;
then consider x1, x2 being set 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 [" the InternalRel of X, the InternalRel of Y"] by A4, Def2;
then [(([x,y] `1) `1),(([x,y] `2) `1)] in the InternalRel of X by 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,(y `1)] in the InternalRel of X by A16, MCART_1:7;
then ( the InternalRel of X is_transitive_in the carrier of X & [x1,y1] in the InternalRel of X ) by A8, MCART_1:7, ORDERS_2:def_3;
then [x1,z1] in the InternalRel of X by A14, A6, A9, A13, RELAT_2:def_8;
then [x1,(z `1)] in the InternalRel of X by A11, MCART_1:7;
then A18: [(x `1),(z `1)] in the InternalRel of X by A16, MCART_1:7;
[(([y,z] `1) `2),(([y,z] `2) `2)] in the InternalRel of Y by A12, Th10;
then [(y `2),(([y,z] `2) `2)] in the InternalRel of Y ;
then [(y `2),(z `2)] in the InternalRel of Y ;
then [y2,(z `2)] in the InternalRel of Y by A8, MCART_1:7;
then A19: [y2,z2] in the InternalRel of Y by A11, MCART_1:7;
[(([x,y] `1) `2),(([x,y] `2) `2)] in the InternalRel of Y by A17, 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,(y `2)] in the InternalRel of Y by A16, MCART_1:7;
then ( the InternalRel of Y is_transitive_in the carrier of Y & [x2,y2] in the InternalRel of Y ) by A8, MCART_1:7, ORDERS_2:def_3;
then [x2,z2] in the InternalRel of Y by A15, A7, A10, A19, RELAT_2:def_8;
then [x2,(z `2)] in the InternalRel of Y by A11, MCART_1:7;
then A20: [(x `2),(z `2)] in the InternalRel of Y by A16, MCART_1:7;
( [x,z] `1 = x & [x,z] `2 = z ) ;
then [x,z] in [" the InternalRel of X, the InternalRel of Y"] by A16, A11, A18, A20, Th10;
hence [x,z] in the InternalRel of [:X,Y:] by Def2; ::_thesis: verum
end;
end;
registration
let X, Y be with_suprema RelStr ;
cluster[:X,Y:] -> strict with_suprema ;
coherence
[:X,Y:] is with_suprema
proof
set IT = [:X,Y:];
let x, y be Element of [:X,Y:]; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of [:X,Y:] st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of [:X,Y:] holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
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 set st
( a in the carrier of X & b in the carrier of Y & x = [a,b] ) & ex c, d being set 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]; ::_thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of [:X,Y:] holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )
( [(x `1),(x `2)] <= [zx,zy] & [(y `1),(y `2)] <= [zx,zy] ) by A1, A3, Th11;
hence ( x <= z & y <= z ) by A6, MCART_1:8; ::_thesis: for b1 being Element of the carrier of [:X,Y:] holds
( not x <= b1 or not y <= b1 or z <= b1 )
let z9 be Element of [:X,Y:]; ::_thesis: ( not x <= z9 or not y <= z9 or z <= z9 )
A7: ex a, b being set 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 ) ; ::_thesis: z <= 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 z <= z9 by A7, MCART_1:8; ::_thesis: verum
end;
end;
registration
let X, Y be with_infima RelStr ;
cluster[:X,Y:] -> strict with_infima ;
coherence
[:X,Y:] is with_infima
proof
set IT = [:X,Y:];
let x, y be Element of [:X,Y:]; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of [:X,Y:] st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of [:X,Y:] holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
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 set st
( a in the carrier of X & b in the carrier of Y & x = [a,b] ) & ex c, d being set 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]; ::_thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of [:X,Y:] holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )
( [(x `1),(x `2)] >= [zx,zy] & [(y `1),(y `2)] >= [zx,zy] ) by A1, A3, Th11;
hence ( x >= z & y >= z ) by A6, MCART_1:8; ::_thesis: for b1 being Element of the carrier of [:X,Y:] holds
( not b1 <= x or not b1 <= y or b1 <= z )
let z9 be Element of [:X,Y:]; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= z )
A7: ex a, b being set 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 ) ; ::_thesis: z9 <= z
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 z9 <= z by A7, MCART_1:8; ::_thesis: verum
end;
end;
theorem :: YELLOW_3:14
for X, Y being RelStr st not [:X,Y:] is empty holds
( not X is empty & not Y is empty )
proof
let X, Y be RelStr ; ::_thesis: ( not [:X,Y:] is empty implies ( not X is empty & not Y is empty ) )
assume not [:X,Y:] is empty ; ::_thesis: ( not X is empty & not Y is empty )
then A1: ex x being set 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 ( not X is empty & not Y is empty ) by A1, MCART_1:10; ::_thesis: verum
end;
theorem :: YELLOW_3:15
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 ; ::_thesis: ( [:X,Y:] is reflexive implies ( X is reflexive & Y is reflexive ) )
assume A1: [:X,Y:] is reflexive ; ::_thesis: ( X is reflexive & 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; ::_thesis: x <= x
[x, the Element of Y] <= [x, the Element of Y] by A1, YELLOW_0:def_1;
hence x <= x by Th11; ::_thesis: verum
end;
hence X is reflexive by YELLOW_0:def_1; ::_thesis: Y is reflexive
for y being Element of Y holds y <= y
proof
set x = the Element of X;
let y be Element of Y; ::_thesis: y <= y
[ the Element of X,y] <= [ the Element of X,y] by A1, YELLOW_0:def_1;
hence y <= y by Th11; ::_thesis: verum
end;
hence Y is reflexive by YELLOW_0:def_1; ::_thesis: verum
end;
theorem :: YELLOW_3:16
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 ; ::_thesis: ( [:X,Y:] is antisymmetric implies ( X is antisymmetric & Y is antisymmetric ) )
assume A1: [:X,Y:] is antisymmetric ; ::_thesis: ( X is antisymmetric & 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: the Element of Y <= the Element of Y ;
let x, y be Element of X; ::_thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; ::_thesis: x = y
then ( [x, the Element of Y] <= [y, the Element of Y] & [y, the Element of Y] <= [x, the Element of Y] ) by A2, Th11;
then [x, the Element of Y] = [y, the Element of Y] by A1, YELLOW_0:def_3;
hence x = y by XTUPLE_0:1; ::_thesis: verum
end;
hence X is antisymmetric by YELLOW_0:def_3; ::_thesis: Y is antisymmetric
for x, y being Element of Y st x <= y & y <= x holds
x = y
proof
set z = the Element of X;
A3: the Element of X <= the Element of X ;
let x, y be Element of Y; ::_thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; ::_thesis: x = y
then ( [ the Element of X,x] <= [ the Element of X,y] & [ the Element of X,y] <= [ the Element of X,x] ) by A3, Th11;
then [ the Element of X,x] = [ the Element of X,y] by A1, YELLOW_0:def_3;
hence x = y by XTUPLE_0:1; ::_thesis: verum
end;
hence Y is antisymmetric by YELLOW_0:def_3; ::_thesis: verum
end;
theorem :: YELLOW_3:17
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 ; ::_thesis: ( [:X,Y:] is transitive implies ( X is transitive & Y is transitive ) )
assume A1: [:X,Y:] is transitive ; ::_thesis: ( X is transitive & 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: the Element of Y <= the Element of Y ;
let x, y, z be Element of X; ::_thesis: ( x <= y & y <= z implies x <= z )
assume ( x <= y & y <= z ) ; ::_thesis: x <= z
then ( [x, the Element of Y] <= [y, the Element of Y] & [y, the Element of Y] <= [z, the Element of Y] ) by A2, Th11;
then [x, the Element of Y] <= [z, the Element of Y] by A1, YELLOW_0:def_2;
hence x <= z by Th11; ::_thesis: verum
end;
hence X is transitive by YELLOW_0:def_2; ::_thesis: Y is transitive
for x, y, z being Element of Y st x <= y & y <= z holds
x <= z
proof
set a = the Element of X;
A3: the Element of X <= the Element of X ;
let x, y, z be Element of Y; ::_thesis: ( x <= y & y <= z implies x <= z )
assume ( x <= y & y <= z ) ; ::_thesis: x <= z
then ( [ the Element of X,x] <= [ the Element of X,y] & [ the Element of X,y] <= [ the Element of X,z] ) by A3, Th11;
then [ the Element of X,x] <= [ the Element of X,z] by A1, YELLOW_0:def_2;
hence x <= z by Th11; ::_thesis: verum
end;
hence Y is transitive by YELLOW_0:def_2; ::_thesis: verum
end;
theorem :: YELLOW_3:18
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 ; ::_thesis: ( [:X,Y:] is with_suprema implies ( X is with_suprema & Y is with_suprema ) )
assume A1: [:X,Y:] is with_suprema ; ::_thesis: ( X is with_suprema & 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 ::_thesis: Y is with_suprema
proof
let x, y be Element of X; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of X st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of X holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
set a = the Element of Y;
A3: the Element of Y <= the Element of Y ;
consider z being Element of [:X,Y:] such that
A4: ( [x, the Element of Y] <= z & [y, the Element of Y] <= z ) and
A5: for z9 being Element of [:X,Y:] st [x, the Element of Y] <= z9 & [y, the Element of Y] <= z9 holds
z <= z9 by A1, LATTICE3:def_10;
take z `1 ; ::_thesis: ( x <= z `1 & y <= z `1 & ( for b1 being Element of the carrier of X holds
( not x <= b1 or not y <= b1 or z `1 <= b1 ) ) )
A6: z = [(z `1),(z `2)] by A2, MCART_1:21;
hence ( x <= z `1 & y <= z `1 ) by A4, Th11; ::_thesis: for b1 being Element of the carrier of X holds
( not x <= b1 or not y <= b1 or z `1 <= b1 )
let z9 be Element of X; ::_thesis: ( not x <= z9 or not y <= z9 or z `1 <= z9 )
assume ( x <= z9 & y <= z9 ) ; ::_thesis: z `1 <= z9
then ( [x, the Element of Y] <= [z9, the Element of Y] & [y, the Element of Y] <= [z9, the Element of Y] ) by A3, Th11;
then z <= [z9, the Element of Y] by A5;
hence z `1 <= z9 by A6, Th11; ::_thesis: verum
end;
set a = the Element of X;
A7: the Element of X <= the Element of X ;
let x, y be Element of Y; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of Y st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of Y holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )
consider z being Element of [:X,Y:] such that
A8: ( [ the Element of X,x] <= z & [ the Element of X,y] <= z ) and
A9: for z9 being Element of [:X,Y:] st [ the Element of X,x] <= z9 & [ the Element of X,y] <= z9 holds
z <= z9 by A1, LATTICE3:def_10;
take z `2 ; ::_thesis: ( x <= z `2 & y <= z `2 & ( for b1 being Element of the carrier of Y holds
( not x <= b1 or not y <= b1 or z `2 <= b1 ) ) )
A10: z = [(z `1),(z `2)] by A2, MCART_1:21;
hence ( x <= z `2 & y <= z `2 ) by A8, Th11; ::_thesis: for b1 being Element of the carrier of Y holds
( not x <= b1 or not y <= b1 or z `2 <= b1 )
let z9 be Element of Y; ::_thesis: ( not x <= z9 or not y <= z9 or z `2 <= z9 )
assume ( x <= z9 & y <= z9 ) ; ::_thesis: z `2 <= z9
then ( [ the Element of X,x] <= [ the Element of X,z9] & [ the Element of X,y] <= [ the Element of X,z9] ) by A7, Th11;
then z <= [ the Element of X,z9] by A9;
hence z `2 <= z9 by A10, Th11; ::_thesis: verum
end;
theorem :: YELLOW_3:19
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 ; ::_thesis: ( [:X,Y:] is with_infima implies ( X is with_infima & Y is with_infima ) )
assume A1: [:X,Y:] is with_infima ; ::_thesis: ( X is with_infima & 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 ::_thesis: Y is with_infima
proof
let x, y be Element of X; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of X st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of X holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
set a = the Element of Y;
A3: the Element of Y <= the Element of Y ;
consider z being Element of [:X,Y:] such that
A4: ( [x, the Element of Y] >= z & [y, the Element of Y] >= z ) and
A5: for z9 being Element of [:X,Y:] st [x, the Element of Y] >= z9 & [y, the Element of Y] >= z9 holds
z >= z9 by A1, LATTICE3:def_11;
take z `1 ; ::_thesis: ( z `1 <= x & z `1 <= y & ( for b1 being Element of the carrier of X holds
( not b1 <= x or not b1 <= y or b1 <= z `1 ) ) )
A6: z = [(z `1),(z `2)] by A2, MCART_1:21;
hence ( x >= z `1 & y >= z `1 ) by A4, Th11; ::_thesis: for b1 being Element of the carrier of X holds
( not b1 <= x or not b1 <= y or b1 <= z `1 )
let z9 be Element of X; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= z `1 )
assume ( x >= z9 & y >= z9 ) ; ::_thesis: z9 <= z `1
then ( [x, the Element of Y] >= [z9, the Element of Y] & [y, the Element of Y] >= [z9, the Element of Y] ) by A3, Th11;
then z >= [z9, the Element of Y] by A5;
hence z9 <= z `1 by A6, Th11; ::_thesis: verum
end;
set a = the Element of X;
A7: the Element of X <= the Element of X ;
let x, y be Element of Y; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of Y st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of Y holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )
consider z being Element of [:X,Y:] such that
A8: ( [ the Element of X,x] >= z & [ the Element of X,y] >= z ) and
A9: for z9 being Element of [:X,Y:] st [ the Element of X,x] >= z9 & [ the Element of X,y] >= z9 holds
z >= z9 by A1, LATTICE3:def_11;
take z `2 ; ::_thesis: ( z `2 <= x & z `2 <= y & ( for b1 being Element of the carrier of Y holds
( not b1 <= x or not b1 <= y or b1 <= z `2 ) ) )
A10: z = [(z `1),(z `2)] by A2, MCART_1:21;
hence ( x >= z `2 & y >= z `2 ) by A8, Th11; ::_thesis: for b1 being Element of the carrier of Y holds
( not b1 <= x or not b1 <= y or b1 <= z `2 )
let z9 be Element of Y; ::_thesis: ( not z9 <= x or not z9 <= y or z9 <= z `2 )
assume ( x >= z9 & y >= z9 ) ; ::_thesis: z9 <= z `2
then ( [ the Element of X,x] >= [ the Element of X,z9] & [ the Element of X,y] >= [ the Element of X,z9] ) by A7, Th11;
then z >= [ the Element of X,z9] by A9;
hence z9 <= z `2 by A10, Th11; ::_thesis: verum
end;
definition
let S1, S2 be RelStr ;
let D1 be directed Subset of S1;
let D2 be directed Subset of S2;
:: original: [:
redefine func[:D1,D2:] -> directed Subset of [:S1,S2:];
coherence
[:D1,D2:] is directed Subset of [:S1,S2:]
proof
set X = [:D1,D2:];
[:D1,D2:] is directed
proof
let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in [:D1,D2:] or not y in [:D1,D2:] or ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & x <= b1 & y <= b1 ) )
assume that
A1: x in [:D1,D2:] and
A2: y in [:D1,D2:] ; ::_thesis: ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & x <= b1 & y <= b1 )
consider x1, x2 being set 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 set such that
A6: y1 in D1 and
A7: y2 in D2 and
A8: y = [y1,y2] by A2, ZFMISC_1:def_2;
reconsider x2 = x2, y2 = 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 = x1, y1 = 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 ; ::_thesis: ( z in [:D1,D2:] & x <= z & y <= z )
thus z in [:D1,D2:] by A11, A9, ZFMISC_1:87; ::_thesis: ( x <= z & y <= z )
( not S1 is empty & not S2 is empty ) by A3, A4;
hence ( x <= z & y <= z ) by A5, A8, A12, A10, Th11; ::_thesis: verum
end;
hence [:D1,D2:] is directed Subset of [:S1,S2:] ; ::_thesis: verum
end;
end;
theorem :: YELLOW_3:20
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for 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 ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds
( D1 is directed & D2 is directed )
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is directed holds
( D1 is directed & D2 is directed )
let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is directed implies ( D1 is directed & D2 is directed ) )
assume A1: [:D1,D2:] is directed ; ::_thesis: ( D1 is directed & D2 is directed )
thus D1 is directed ::_thesis: D2 is directed
proof
set q1 = the Element of D2;
let x, y be Element of S1; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in D1 or not y in D1 or ex b1 being Element of the carrier of S1 st
( b1 in D1 & x <= b1 & y <= b1 ) )
assume ( x in D1 & y in D1 ) ; ::_thesis: ex b1 being Element of the carrier of S1 st
( b1 in D1 & x <= b1 & y <= b1 )
then ( [x, the Element of D2] in [:D1,D2:] & [y, the Element of D2] 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, the Element of D2] <= z & [y, the Element of D2] <= z ) by A1, WAYBEL_0:def_1;
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 ; ::_thesis: ( zz in D1 & x <= zz & y <= zz )
thus zz in D1 ; ::_thesis: ( x <= zz & y <= zz )
ex x, y being set st
( x in D1 & y in D2 & z = [x,y] ) by A2, ZFMISC_1:def_2;
then ( [x, the Element of D2] <= [zz,z2] & [y, the Element of D2] <= [zz,z2] ) by A3, MCART_1:8;
hence ( x <= zz & y <= zz ) by Th11; ::_thesis: verum
end;
set q1 = the Element of D1;
let x, y be Element of S2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in D2 or not y in D2 or ex b1 being Element of the carrier of S2 st
( b1 in D2 & x <= b1 & y <= b1 ) )
assume ( x in D2 & y in D2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st
( b1 in D2 & x <= b1 & y <= b1 )
then ( [ the Element of D1,x] in [:D1,D2:] & [ the Element of D1,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: ( [ the Element of D1,x] <= z & [ the Element of D1,y] <= z ) by A1, WAYBEL_0:def_1;
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 ; ::_thesis: ( zz in D2 & x <= zz & y <= zz )
thus zz in D2 ; ::_thesis: ( x <= zz & y <= zz )
ex x, y being set st
( x in D1 & y in D2 & z = [x,y] ) by A4, ZFMISC_1:def_2;
then ( [ the Element of D1,x] <= [z2,zz] & [ the Element of D1,y] <= [z2,zz] ) by A5, MCART_1:8;
hence ( x <= zz & y <= zz ) by Th11; ::_thesis: verum
end;
theorem Th21: :: YELLOW_3:21
for S1, S2 being non empty RelStr
for D being non empty Subset of [:S1,S2:] holds
( not proj1 D is empty & not proj2 D is empty )
proof
let S1, S2 be non empty RelStr ; ::_thesis: for D being non empty Subset of [:S1,S2:] holds
( not proj1 D is empty & not proj2 D is empty )
let D be non empty Subset of [:S1,S2:]; ::_thesis: ( not proj1 D is empty & not proj2 D is empty )
reconsider D1 = D as non empty Subset of [: the carrier of S1, the carrier of S2:] by Def2;
not proj1 D1 is empty ;
hence ( not proj1 D is empty & not proj2 D is empty ) ; ::_thesis: verum
end;
theorem :: YELLOW_3:22
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 ; ::_thesis: for D being non empty directed Subset of [:S1,S2:] holds
( proj1 D is directed & proj2 D is directed )
let D be non empty directed Subset of [:S1,S2:]; ::_thesis: ( proj1 D is directed & proj2 D is directed )
set D1 = proj1 D;
set 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 proj1 D is directed ::_thesis: proj2 D is directed
proof
let x, y be Element of S1; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in proj1 D or not y in proj1 D or ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & x <= b1 & y <= b1 ) )
assume that
A2: x in proj1 D and
A3: y in proj1 D ; ::_thesis: ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & x <= b1 & y <= b1 )
consider q2 being set such that
A4: [y,q2] in D by A3, XTUPLE_0:def_12;
reconsider D29 = proj2 D as non empty Subset of S2 by A2, FUNCT_5:16;
reconsider D19 = proj1 D as non empty Subset of S1 by A2;
consider q1 being set such that
A5: [x,q1] in D by A2, XTUPLE_0:def_12;
reconsider q2 = q2 as Element of D29 by A4, XTUPLE_0:def_13;
reconsider q1 = 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 ; ::_thesis: ( zz in proj1 D & x <= zz & y <= zz )
thus zz in proj1 D ; ::_thesis: ( x <= zz & y <= zz )
ex x, y being set st
( x in D19 & y in D29 & z = [x,y] ) by A1, A6, ZFMISC_1:def_2;
then z = [zz,z2] by MCART_1:8;
hence ( x <= zz & y <= zz ) by A7, Th11; ::_thesis: verum
end;
let x, y be Element of S2; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in proj2 D or not y in proj2 D or ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & x <= b1 & y <= b1 ) )
assume that
A8: x in proj2 D and
A9: y in proj2 D ; ::_thesis: ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & x <= b1 & y <= b1 )
consider q2 being set such that
A10: [q2,y] in D by A9, XTUPLE_0:def_13;
reconsider D29 = proj2 D as non empty Subset of S2 by A8;
reconsider D19 = proj1 D as non empty Subset of S1 by A8, FUNCT_5:16;
consider q1 being set such that
A11: [q1,x] in D by A8, XTUPLE_0:def_13;
reconsider q2 = q2 as Element of D19 by A10, XTUPLE_0:def_12;
reconsider q1 = 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 ; ::_thesis: ( zz in proj2 D & x <= zz & y <= zz )
thus zz in proj2 D ; ::_thesis: ( x <= zz & y <= zz )
ex x, y being set st
( x in D19 & y in D29 & z = [x,y] ) by A1, A12, ZFMISC_1:def_2;
then z = [z2,zz] by MCART_1:8;
hence ( x <= zz & y <= zz ) by A13, Th11; ::_thesis: verum
end;
definition
let S1, S2 be RelStr ;
let D1 be filtered Subset of S1;
let D2 be filtered Subset of S2;
:: original: [:
redefine func[:D1,D2:] -> filtered Subset of [:S1,S2:];
coherence
[:D1,D2:] is filtered Subset of [:S1,S2:]
proof
set X = [:D1,D2:];
[:D1,D2:] is filtered
proof
let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in [:D1,D2:] or not y in [:D1,D2:] or ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & b1 <= x & b1 <= y ) )
assume that
A1: x in [:D1,D2:] and
A2: y in [:D1,D2:] ; ::_thesis: ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & b1 <= x & b1 <= y )
consider x1, x2 being set 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 set such that
A6: y1 in D1 and
A7: y2 in D2 and
A8: y = [y1,y2] by A2, ZFMISC_1:def_2;
reconsider x2 = x2, y2 = 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 = x1, y1 = 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 ; ::_thesis: ( z in [:D1,D2:] & z <= x & z <= y )
thus z in [:D1,D2:] by A11, A9, ZFMISC_1:87; ::_thesis: ( z <= x & z <= y )
( not S1 is empty & not S2 is empty ) by A3, A4;
hence ( z <= x & z <= y ) by A5, A8, A12, A10, Th11; ::_thesis: verum
end;
hence [:D1,D2:] is filtered Subset of [:S1,S2:] ; ::_thesis: verum
end;
end;
theorem :: YELLOW_3:23
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for 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 ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds
( D1 is filtered & D2 is filtered )
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is filtered holds
( D1 is filtered & D2 is filtered )
let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is filtered implies ( D1 is filtered & D2 is filtered ) )
assume A1: [:D1,D2:] is filtered ; ::_thesis: ( D1 is filtered & D2 is filtered )
thus D1 is filtered ::_thesis: D2 is filtered
proof
set q1 = the Element of D2;
let x, y be Element of S1; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in D1 or not y in D1 or ex b1 being Element of the carrier of S1 st
( b1 in D1 & b1 <= x & b1 <= y ) )
assume ( x in D1 & y in D1 ) ; ::_thesis: ex b1 being Element of the carrier of S1 st
( b1 in D1 & b1 <= x & b1 <= y )
then ( [x, the Element of D2] in [:D1,D2:] & [y, the Element of D2] 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, the Element of D2] >= z & [y, the Element of D2] >= z ) by A1, WAYBEL_0:def_2;
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 ; ::_thesis: ( zz in D1 & zz <= x & zz <= y )
thus zz in D1 ; ::_thesis: ( zz <= x & zz <= y )
ex x, y being set st
( x in D1 & y in D2 & z = [x,y] ) by A2, ZFMISC_1:def_2;
then ( [x, the Element of D2] >= [zz,z2] & [y, the Element of D2] >= [zz,z2] ) by A3, MCART_1:8;
hence ( zz <= x & zz <= y ) by Th11; ::_thesis: verum
end;
set q1 = the Element of D1;
let x, y be Element of S2; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in D2 or not y in D2 or ex b1 being Element of the carrier of S2 st
( b1 in D2 & b1 <= x & b1 <= y ) )
assume ( x in D2 & y in D2 ) ; ::_thesis: ex b1 being Element of the carrier of S2 st
( b1 in D2 & b1 <= x & b1 <= y )
then ( [ the Element of D1,x] in [:D1,D2:] & [ the Element of D1,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: ( [ the Element of D1,x] >= z & [ the Element of D1,y] >= z ) by A1, WAYBEL_0:def_2;
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 ; ::_thesis: ( zz in D2 & zz <= x & zz <= y )
thus zz in D2 ; ::_thesis: ( zz <= x & zz <= y )
ex x, y being set st
( x in D1 & y in D2 & z = [x,y] ) by A4, ZFMISC_1:def_2;
then ( [ the Element of D1,x] >= [z2,zz] & [ the Element of D1,y] >= [z2,zz] ) by A5, MCART_1:8;
hence ( zz <= x & zz <= y ) by Th11; ::_thesis: verum
end;
theorem :: YELLOW_3:24
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 ; ::_thesis: for D being non empty filtered Subset of [:S1,S2:] holds
( proj1 D is filtered & proj2 D is filtered )
let D be non empty filtered Subset of [:S1,S2:]; ::_thesis: ( proj1 D is filtered & proj2 D is filtered )
set D1 = proj1 D;
set 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 proj1 D is filtered ::_thesis: proj2 D is filtered
proof
let x, y be Element of S1; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in proj1 D or not y in proj1 D or ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & b1 <= x & b1 <= y ) )
assume that
A2: x in proj1 D and
A3: y in proj1 D ; ::_thesis: ex b1 being Element of the carrier of S1 st
( b1 in proj1 D & b1 <= x & b1 <= y )
consider q2 being set such that
A4: [y,q2] in D by A3, XTUPLE_0:def_12;
reconsider D29 = proj2 D as non empty Subset of S2 by A2, FUNCT_5:16;
reconsider D19 = proj1 D as non empty Subset of S1 by A2;
consider q1 being set such that
A5: [x,q1] in D by A2, XTUPLE_0:def_12;
reconsider q2 = q2 as Element of D29 by A4, XTUPLE_0:def_13;
reconsider q1 = 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 ; ::_thesis: ( zz in proj1 D & zz <= x & zz <= y )
thus zz in proj1 D ; ::_thesis: ( zz <= x & zz <= y )
ex x, y being set st
( x in D19 & y in D29 & z = [x,y] ) by A1, A6, ZFMISC_1:def_2;
then z = [zz,z2] by MCART_1:8;
hence ( zz <= x & zz <= y ) by A7, Th11; ::_thesis: verum
end;
let x, y be Element of S2; :: according to WAYBEL_0:def_2 ::_thesis: ( not x in proj2 D or not y in proj2 D or ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & b1 <= x & b1 <= y ) )
assume that
A8: x in proj2 D and
A9: y in proj2 D ; ::_thesis: ex b1 being Element of the carrier of S2 st
( b1 in proj2 D & b1 <= x & b1 <= y )
consider q2 being set such that
A10: [q2,y] in D by A9, XTUPLE_0:def_13;
reconsider D29 = proj2 D as non empty Subset of S2 by A8;
reconsider D19 = proj1 D as non empty Subset of S1 by A8, FUNCT_5:16;
consider q1 being set such that
A11: [q1,x] in D by A8, XTUPLE_0:def_13;
reconsider q2 = q2 as Element of D19 by A10, XTUPLE_0:def_12;
reconsider q1 = 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 ; ::_thesis: ( zz in proj2 D & zz <= x & zz <= y )
thus zz in proj2 D ; ::_thesis: ( zz <= x & zz <= y )
ex x, y being set st
( x in D19 & y in D29 & z = [x,y] ) by A1, A12, ZFMISC_1:def_2;
then z = [z2,zz] by MCART_1:8;
hence ( zz <= x & zz <= y ) by A13, Th11; ::_thesis: verum
end;
definition
let S1, S2 be RelStr ;
let D1 be upper Subset of S1;
let D2 be upper Subset of S2;
:: original: [:
redefine func[:D1,D2:] -> upper Subset of [:S1,S2:];
coherence
[:D1,D2:] is upper Subset of [:S1,S2:]
proof
set X = [:D1,D2:];
[:D1,D2:] is upper
proof
let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in [:D1,D2:] or not x <= y or y in [:D1,D2:] )
assume that
A1: x in [:D1,D2:] and
A2: x <= y ; ::_thesis: y in [:D1,D2:]
consider x1, x2 being set 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;
set C2 = the carrier of s2;
the carrier of [:S1,S2:] = [: the carrier of s1, the carrier of s2:] by Def2;
then consider y1, y2 being set such that
A6: y1 in the carrier of s1 and
A7: y2 in the carrier of s2 and
A8: y = [y1,y2] by ZFMISC_1:def_2;
reconsider x2 = x2, y2 = 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 = x1, y1 = 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 y in [:D1,D2:] by A8, A9, ZFMISC_1:87; ::_thesis: verum
end;
hence [:D1,D2:] is upper Subset of [:S1,S2:] ; ::_thesis: verum
end;
end;
theorem :: YELLOW_3:25
for S1, S2 being non empty reflexive RelStr
for D1 being non empty Subset of S1
for 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 ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds
( D1 is upper & D2 is upper )
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is upper holds
( D1 is upper & D2 is upper )
let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is upper implies ( D1 is upper & D2 is upper ) )
assume A1: [:D1,D2:] is upper ; ::_thesis: ( D1 is upper & D2 is upper )
thus D1 is upper ::_thesis: D2 is upper
proof
set q1 = the Element of D2;
let x, y be Element of S1; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in D1 or not x <= y or y in D1 )
assume that
A2: x in D1 and
A3: x <= y ; ::_thesis: y in D1
A4: [x, the Element of D2] in [:D1,D2:] by A2, ZFMISC_1:87;
the Element of D2 <= the Element of D2 ;
then [x, the Element of D2] <= [y, the Element of D2] by A3, Th11;
then [y, the Element of D2] in [:D1,D2:] by A1, A4, WAYBEL_0:def_20;
hence y in D1 by ZFMISC_1:87; ::_thesis: verum
end;
set q1 = the Element of D1;
let x, y be Element of S2; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in D2 or not x <= y or y in D2 )
assume that
A5: x in D2 and
A6: x <= y ; ::_thesis: y in D2
A7: [ the Element of D1,x] in [:D1,D2:] by A5, ZFMISC_1:87;
the Element of D1 <= the Element of D1 ;
then [ the Element of D1,x] <= [ the Element of D1,y] by A6, Th11;
then [ the Element of D1,y] in [:D1,D2:] by A1, A7, WAYBEL_0:def_20;
hence y in D2 by ZFMISC_1:87; ::_thesis: verum
end;
theorem :: YELLOW_3:26
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 ; ::_thesis: for D being non empty upper Subset of [:S1,S2:] holds
( proj1 D is upper & proj2 D is upper )
let D be non empty upper Subset of [:S1,S2:]; ::_thesis: ( proj1 D is upper & proj2 D is upper )
set D1 = proj1 D;
set D2 = proj2 D;
reconsider d1 = proj1 D 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= [:(proj1 D),(proj2 D):] by Th1;
thus proj1 D is upper ::_thesis: proj2 D is upper
proof
reconsider d2 = proj2 D as non empty Subset of S2 by Th21;
let x, y be Element of S1; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in proj1 D or not x <= y or y in proj1 D )
assume that
A2: x in proj1 D and
A3: x <= y ; ::_thesis: y in proj1 D
consider q1 being set such that
A4: [x,q1] in D by A2, XTUPLE_0:def_12;
reconsider q1 = 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 y in proj1 D by A1, ZFMISC_1:87; ::_thesis: verum
end;
let x, y be Element of S2; :: according to WAYBEL_0:def_20 ::_thesis: ( not x in proj2 D or not x <= y or y in proj2 D )
assume that
A5: x in proj2 D and
A6: x <= y ; ::_thesis: y in proj2 D
consider q1 being set such that
A7: [q1,x] in D by A5, XTUPLE_0:def_13;
reconsider q1 = 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 y in proj2 D by A1, ZFMISC_1:87; ::_thesis: verum
end;
definition
let S1, S2 be RelStr ;
let D1 be lower Subset of S1;
let D2 be lower Subset of S2;
:: original: [:
redefine func[:D1,D2:] -> lower Subset of [:S1,S2:];
coherence
[:D1,D2:] is lower Subset of [:S1,S2:]
proof
set X = [:D1,D2:];
[:D1,D2:] is lower
proof
let x, y be Element of [:S1,S2:]; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in [:D1,D2:] or not y <= x or y in [:D1,D2:] )
assume that
A1: x in [:D1,D2:] and
A2: x >= y ; ::_thesis: y in [:D1,D2:]
consider x1, x2 being set 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;
set C2 = the carrier of s2;
the carrier of [:S1,S2:] = [: the carrier of s1, the carrier of s2:] by Def2;
then consider y1, y2 being set such that
A6: y1 in the carrier of s1 and
A7: y2 in the carrier of s2 and
A8: y = [y1,y2] by ZFMISC_1:def_2;
reconsider x2 = x2, y2 = 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 = x1, y1 = 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 y in [:D1,D2:] by A8, A9, ZFMISC_1:87; ::_thesis: verum
end;
hence [:D1,D2:] is lower Subset of [:S1,S2:] ; ::_thesis: verum
end;
end;
theorem :: YELLOW_3:27
for S1, S2 being non empty reflexive RelStr
for D1 being non empty Subset of S1
for 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 ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower & D2 is lower )
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2 st [:D1,D2:] is lower holds
( D1 is lower & D2 is lower )
let D2 be non empty Subset of S2; ::_thesis: ( [:D1,D2:] is lower implies ( D1 is lower & D2 is lower ) )
assume A1: [:D1,D2:] is lower ; ::_thesis: ( D1 is lower & D2 is lower )
thus D1 is lower ::_thesis: D2 is lower
proof
set q1 = the Element of D2;
let x, y be Element of S1; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in D1 or not y <= x or y in D1 )
assume that
A2: x in D1 and
A3: x >= y ; ::_thesis: y in D1
A4: [x, the Element of D2] in [:D1,D2:] by A2, ZFMISC_1:87;
the Element of D2 <= the Element of D2 ;
then [x, the Element of D2] >= [y, the Element of D2] by A3, Th11;
then [y, the Element of D2] in [:D1,D2:] by A1, A4, WAYBEL_0:def_19;
hence y in D1 by ZFMISC_1:87; ::_thesis: verum
end;
set q1 = the Element of D1;
let x, y be Element of S2; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in D2 or not y <= x or y in D2 )
assume that
A5: x in D2 and
A6: x >= y ; ::_thesis: y in D2
A7: [ the Element of D1,x] in [:D1,D2:] by A5, ZFMISC_1:87;
the Element of D1 <= the Element of D1 ;
then [ the Element of D1,x] >= [ the Element of D1,y] by A6, Th11;
then [ the Element of D1,y] in [:D1,D2:] by A1, A7, WAYBEL_0:def_19;
hence y in D2 by ZFMISC_1:87; ::_thesis: verum
end;
theorem :: YELLOW_3:28
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 ; ::_thesis: for D being non empty lower Subset of [:S1,S2:] holds
( proj1 D is lower & proj2 D is lower )
let D be non empty lower Subset of [:S1,S2:]; ::_thesis: ( proj1 D is lower & proj2 D is lower )
set D1 = proj1 D;
set D2 = proj2 D;
reconsider d1 = proj1 D 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= [:(proj1 D),(proj2 D):] by Th1;
thus proj1 D is lower ::_thesis: proj2 D is lower
proof
reconsider d2 = proj2 D as non empty Subset of S2 by Th21;
let x, y be Element of S1; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in proj1 D or not y <= x or y in proj1 D )
assume that
A2: x in proj1 D and
A3: x >= y ; ::_thesis: y in proj1 D
consider q1 being set such that
A4: [x,q1] in D by A2, XTUPLE_0:def_12;
reconsider q1 = 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 y in proj1 D by A1, ZFMISC_1:87; ::_thesis: verum
end;
let x, y be Element of S2; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in proj2 D or not y <= x or y in proj2 D )
assume that
A5: x in proj2 D and
A6: x >= y ; ::_thesis: y in proj2 D
consider q1 being set such that
A7: [q1,x] in D by A5, XTUPLE_0:def_13;
reconsider q1 = 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 y in proj2 D by A1, ZFMISC_1:87; ::_thesis: verum
end;
definition
let R be RelStr ;
attrR is void means :Def3: :: YELLOW_3:def 3
the InternalRel of R is empty ;
end;
:: deftheorem Def3 defines void YELLOW_3:def_3_:_
for R being RelStr holds
( R is void iff the InternalRel of R is empty );
registration
cluster empty -> void for RelStr ;
coherence
for b1 being RelStr st b1 is empty holds
b1 is void
proof
let R be RelStr ; ::_thesis: ( R is empty implies R is void )
assume R is empty ; ::_thesis: R is void
then reconsider R1 = R as empty RelStr ;
the InternalRel of R1 is empty ;
hence the InternalRel of R is empty ; :: according to YELLOW_3:def_3 ::_thesis: verum
end;
end;
registration
cluster non empty strict V55() reflexive transitive antisymmetric non void for RelStr ;
existence
ex b1 being Poset st
( not b1 is void & not b1 is empty & b1 is strict )
proof
set R = the non empty strict Poset;
take the non empty strict Poset ; ::_thesis: ( not the non empty strict Poset is void & not the non empty strict Poset is empty & the non empty strict Poset is strict )
( ex x being set st x in the carrier of the non empty strict Poset & the InternalRel of the non empty strict Poset is_reflexive_in the carrier of the non empty strict Poset ) by ORDERS_2:def_2, XBOOLE_0:def_1;
hence not the InternalRel of the non empty strict Poset is empty by RELAT_2:def_1; :: according to YELLOW_3:def_3 ::_thesis: ( not the non empty strict Poset is empty & the non empty strict Poset is strict )
thus ( not the non empty strict Poset is empty & the non empty strict Poset is strict ) ; ::_thesis: verum
end;
end;
registration
cluster non void -> non empty for RelStr ;
coherence
for b1 being RelStr st not b1 is void holds
not b1 is empty ;
end;
registration
cluster non empty reflexive -> non void for RelStr ;
coherence
for b1 being RelStr st not b1 is empty & b1 is reflexive holds
not b1 is void
proof
let R be RelStr ; ::_thesis: ( not R is empty & R is reflexive implies not R is void )
assume ( not R is empty & R is reflexive ) ; ::_thesis: not R is void
then reconsider R1 = R as non empty reflexive RelStr ;
( ex x being set 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 not the InternalRel of R is empty by RELAT_2:def_1; :: according to YELLOW_3:def_3 ::_thesis: verum
end;
end;
registration
let R be non void RelStr ;
cluster the InternalRel of R -> non empty ;
coherence
not the InternalRel of R is empty by Def3;
end;
theorem Th29: :: YELLOW_3:29
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for 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 ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds
( x is_>=_than D1 & y is_>=_than D2 )
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds
( x is_>=_than D1 & y is_>=_than D2 )
let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1
for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds
( x is_>=_than D1 & y is_>=_than D2 )
let x be Element of S1; ::_thesis: for y being Element of S2 st [x,y] is_>=_than [:D1,D2:] holds
( x is_>=_than D1 & y is_>=_than D2 )
let y be Element of S2; ::_thesis: ( [x,y] is_>=_than [:D1,D2:] implies ( x is_>=_than D1 & y is_>=_than D2 ) )
assume A1: [x,y] is_>=_than [:D1,D2:] ; ::_thesis: ( x is_>=_than D1 & y is_>=_than D2 )
thus x is_>=_than D1 ::_thesis: y is_>=_than D2
proof
set a = the Element of D2;
let b be Element of S1; :: according to LATTICE3:def_9 ::_thesis: ( not b in D1 or b <= x )
assume b in D1 ; ::_thesis: b <= x
then [b, the Element of D2] in [:D1,D2:] by ZFMISC_1:87;
then [b, the Element of D2] <= [x,y] by A1, LATTICE3:def_9;
hence b <= x by Th11; ::_thesis: verum
end;
set b = the Element of D1;
let a be Element of S2; :: according to LATTICE3:def_9 ::_thesis: ( not a in D2 or a <= y )
assume a in D2 ; ::_thesis: a <= y
then [ the Element of D1,a] in [:D1,D2:] by ZFMISC_1:87;
then [ the Element of D1,a] <= [x,y] by A1, LATTICE3:def_9;
hence a <= y by Th11; ::_thesis: verum
end;
theorem Th30: :: YELLOW_3:30
for S1, S2 being non empty RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for 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 ; ::_thesis: for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds
[x,y] is_>=_than [:D1,D2:]
let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds
[x,y] is_>=_than [:D1,D2:]
let D2 be Subset of S2; ::_thesis: for x being Element of S1
for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds
[x,y] is_>=_than [:D1,D2:]
let x be Element of S1; ::_thesis: for y being Element of S2 st x is_>=_than D1 & y is_>=_than D2 holds
[x,y] is_>=_than [:D1,D2:]
let y be Element of S2; ::_thesis: ( x is_>=_than D1 & y is_>=_than D2 implies [x,y] is_>=_than [:D1,D2:] )
assume A1: ( x is_>=_than D1 & y is_>=_than D2 ) ; ::_thesis: [x,y] is_>=_than [:D1,D2:]
let b be Element of [:S1,S2:]; :: according to LATTICE3:def_9 ::_thesis: ( not b in [:D1,D2:] or b <= [x,y] )
assume b in [:D1,D2:] ; ::_thesis: b <= [x,y]
then consider b1, b2 being set such that
A2: b1 in D1 and
A3: b2 in D2 and
A4: b = [b1,b2] by ZFMISC_1:def_2;
reconsider b2 = b2 as Element of S2 by A3;
reconsider b1 = b1 as Element of S1 by A2;
( b1 <= x & b2 <= y ) by A1, A2, A3, LATTICE3:def_9;
hence b <= [x,y] by A4, Th11; ::_thesis: verum
end;
theorem Th31: :: YELLOW_3:31
for S1, S2 being non empty RelStr
for D being Subset of [:S1,S2:]
for x being Element of S1
for 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 ; ::_thesis: for D being Subset of [:S1,S2:]
for x being Element of S1
for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
let D be Subset of [:S1,S2:]; ::_thesis: for x being Element of S1
for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
let x be Element of S1; ::_thesis: for y being Element of S2 holds
( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
let y be Element of S2; ::_thesis: ( [x,y] is_>=_than D iff ( x is_>=_than proj1 D & y is_>=_than proj2 D ) )
set D1 = proj1 D;
set D2 = proj2 D;
hereby ::_thesis: ( x is_>=_than proj1 D & y is_>=_than proj2 D implies [x,y] is_>=_than D )
assume A1: [x,y] is_>=_than D ; ::_thesis: ( x is_>=_than proj1 D & y is_>=_than proj2 D )
thus x is_>=_than proj1 D ::_thesis: y is_>=_than proj2 D
proof
let q be Element of S1; :: according to LATTICE3:def_9 ::_thesis: ( not q in proj1 D or q <= x )
assume q in proj1 D ; ::_thesis: q <= x
then consider z being set such that
A2: [q,z] in D by XTUPLE_0:def_12;
reconsider d2 = proj2 D as non empty Subset of S2 by A2, XTUPLE_0:def_13;
reconsider z = z as Element of d2 by A2, XTUPLE_0:def_13;
[x,y] >= [q,z] by A1, A2, LATTICE3:def_9;
hence q <= x by Th11; ::_thesis: verum
end;
thus y is_>=_than proj2 D ::_thesis: verum
proof
let q be Element of S2; :: according to LATTICE3:def_9 ::_thesis: ( not q in proj2 D or q <= y )
assume q in proj2 D ; ::_thesis: q <= y
then consider z being set such that
A3: [z,q] in D by XTUPLE_0:def_13;
reconsider d1 = proj1 D as non empty Subset of S1 by A3, XTUPLE_0:def_12;
reconsider z = z as Element of d1 by A3, XTUPLE_0:def_12;
[x,y] >= [z,q] by A1, A3, LATTICE3:def_9;
hence q <= y by Th11; ::_thesis: verum
end;
end;
assume ( x is_>=_than proj1 D & y is_>=_than proj2 D ) ; ::_thesis: [x,y] is_>=_than D
then A4: [x,y] is_>=_than [:(proj1 D),(proj2 D):] by Th30;
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then D c= [:(proj1 D),(proj2 D):] by Th1;
hence [x,y] is_>=_than D by A4, YELLOW_0:9; ::_thesis: verum
end;
theorem Th32: :: YELLOW_3:32
for S1, S2 being non empty RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for 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 ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds
( x is_<=_than D1 & y is_<=_than D2 )
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2
for x being Element of S1
for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds
( x is_<=_than D1 & y is_<=_than D2 )
let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1
for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds
( x is_<=_than D1 & y is_<=_than D2 )
let x be Element of S1; ::_thesis: for y being Element of S2 st [x,y] is_<=_than [:D1,D2:] holds
( x is_<=_than D1 & y is_<=_than D2 )
let y be Element of S2; ::_thesis: ( [x,y] is_<=_than [:D1,D2:] implies ( x is_<=_than D1 & y is_<=_than D2 ) )
assume A1: [x,y] is_<=_than [:D1,D2:] ; ::_thesis: ( x is_<=_than D1 & y is_<=_than D2 )
thus x is_<=_than D1 ::_thesis: y is_<=_than D2
proof
set a = the Element of D2;
let b be Element of S1; :: according to LATTICE3:def_8 ::_thesis: ( not b in D1 or x <= b )
assume b in D1 ; ::_thesis: x <= b
then [b, the Element of D2] in [:D1,D2:] by ZFMISC_1:87;
then [b, the Element of D2] >= [x,y] by A1, LATTICE3:def_8;
hence x <= b by Th11; ::_thesis: verum
end;
set b = the Element of D1;
let a be Element of S2; :: according to LATTICE3:def_8 ::_thesis: ( not a in D2 or y <= a )
assume a in D2 ; ::_thesis: y <= a
then [ the Element of D1,a] in [:D1,D2:] by ZFMISC_1:87;
then [ the Element of D1,a] >= [x,y] by A1, LATTICE3:def_8;
hence y <= a by Th11; ::_thesis: verum
end;
theorem Th33: :: YELLOW_3:33
for S1, S2 being non empty RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for 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 ; ::_thesis: for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2
for x being Element of S1
for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let D2 be Subset of S2; ::_thesis: for x being Element of S1
for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let x be Element of S1; ::_thesis: for y being Element of S2 st x is_<=_than D1 & y is_<=_than D2 holds
[x,y] is_<=_than [:D1,D2:]
let y be Element of S2; ::_thesis: ( x is_<=_than D1 & y is_<=_than D2 implies [x,y] is_<=_than [:D1,D2:] )
assume A1: ( x is_<=_than D1 & y is_<=_than D2 ) ; ::_thesis: [x,y] is_<=_than [:D1,D2:]
let b be Element of [:S1,S2:]; :: according to LATTICE3:def_8 ::_thesis: ( not b in [:D1,D2:] or [x,y] <= b )
assume b in [:D1,D2:] ; ::_thesis: [x,y] <= b
then consider b1, b2 being set such that
A2: b1 in D1 and
A3: b2 in D2 and
A4: b = [b1,b2] by ZFMISC_1:def_2;
reconsider b2 = b2 as Element of S2 by A3;
reconsider b1 = b1 as Element of S1 by A2;
( b1 >= x & b2 >= y ) by A1, A2, A3, LATTICE3:def_8;
hence [x,y] <= b by A4, Th11; ::_thesis: verum
end;
theorem Th34: :: YELLOW_3:34
for S1, S2 being non empty RelStr
for D being Subset of [:S1,S2:]
for x being Element of S1
for 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 ; ::_thesis: for D being Subset of [:S1,S2:]
for x being Element of S1
for y being Element of S2 holds
( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
let D be Subset of [:S1,S2:]; ::_thesis: for x being Element of S1
for y being Element of S2 holds
( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
let x be Element of S1; ::_thesis: for y being Element of S2 holds
( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
let y be Element of S2; ::_thesis: ( [x,y] is_<=_than D iff ( x is_<=_than proj1 D & y is_<=_than proj2 D ) )
set D1 = proj1 D;
set D2 = proj2 D;
hereby ::_thesis: ( x is_<=_than proj1 D & y is_<=_than proj2 D implies [x,y] is_<=_than D )
assume A1: [x,y] is_<=_than D ; ::_thesis: ( x is_<=_than proj1 D & y is_<=_than proj2 D )
thus x is_<=_than proj1 D ::_thesis: y is_<=_than proj2 D
proof
let q be Element of S1; :: according to LATTICE3:def_8 ::_thesis: ( not q in proj1 D or x <= q )
assume q in proj1 D ; ::_thesis: x <= q
then consider z being set such that
A2: [q,z] in D by XTUPLE_0:def_12;
reconsider d2 = proj2 D as non empty Subset of S2 by A2, XTUPLE_0:def_13;
reconsider z = z as Element of d2 by A2, XTUPLE_0:def_13;
[x,y] <= [q,z] by A1, A2, LATTICE3:def_8;
hence x <= q by Th11; ::_thesis: verum
end;
thus y is_<=_than proj2 D ::_thesis: verum
proof
let q be Element of S2; :: according to LATTICE3:def_8 ::_thesis: ( not q in proj2 D or y <= q )
assume q in proj2 D ; ::_thesis: y <= q
then consider z being set such that
A3: [z,q] in D by XTUPLE_0:def_13;
reconsider d1 = proj1 D as non empty Subset of S1 by A3, XTUPLE_0:def_12;
reconsider z = z as Element of d1 by A3, XTUPLE_0:def_12;
[x,y] <= [z,q] by A1, A3, LATTICE3:def_8;
hence y <= q by Th11; ::_thesis: verum
end;
end;
assume ( x is_<=_than proj1 D & y is_<=_than proj2 D ) ; ::_thesis: [x,y] is_<=_than D
then A4: [x,y] is_<=_than [:(proj1 D),(proj2 D):] by Th33;
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then D c= [:(proj1 D),(proj2 D):] by Th1;
hence [x,y] is_<=_than D by A4, YELLOW_0:9; ::_thesis: verum
end;
theorem Th35: :: YELLOW_3:35
for S1, S2 being non empty antisymmetric RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for 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 ) )
let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2
for x being Element of S1
for 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 ) )
let D2 be Subset of S2; ::_thesis: for x being Element of S1
for 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 ) )
let x be Element of S1; ::_thesis: for 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 ) )
let y be Element of S2; ::_thesis: ( 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 ) implies ( ( 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 ) ) )
assume 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 ; ::_thesis: ( ( 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 ) )
thus for c being Element of S1 st c is_>=_than D1 holds
x <= c ::_thesis: for d being Element of S2 st d is_>=_than D2 holds
y <= d
proof
A4: sup D2 is_>=_than D2 by A2, YELLOW_0:30;
let b be Element of S1; ::_thesis: ( b is_>=_than D1 implies x <= b )
assume b is_>=_than D1 ; ::_thesis: x <= b
then [x,y] <= [b,(sup D2)] by A3, A4, Th30;
hence x <= b by Th11; ::_thesis: verum
end;
A5: sup D1 is_>=_than D1 by A1, YELLOW_0:30;
let b be Element of S2; ::_thesis: ( b is_>=_than D2 implies y <= b )
assume b is_>=_than D2 ; ::_thesis: y <= b
then [x,y] <= [(sup D1),b] by A3, A5, Th30;
hence y <= b by Th11; ::_thesis: verum
end;
theorem Th36: :: YELLOW_3:36
for S1, S2 being non empty antisymmetric RelStr
for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being Subset of S1
for D2 being Subset of S2
for x being Element of S1
for 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 ) )
let D1 be Subset of S1; ::_thesis: for D2 being Subset of S2
for x being Element of S1
for 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 ) )
let D2 be Subset of S2; ::_thesis: for x being Element of S1
for 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 ) )
let x be Element of S1; ::_thesis: for 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 ) )
let y be Element of S2; ::_thesis: ( 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 ) implies ( ( 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 ) ) )
assume 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 ; ::_thesis: ( ( 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 ) )
thus for c being Element of S1 st c is_<=_than D1 holds
x >= c ::_thesis: for d being Element of S2 st d is_<=_than D2 holds
y >= d
proof
A4: inf D2 is_<=_than D2 by A2, YELLOW_0:31;
let b be Element of S1; ::_thesis: ( b is_<=_than D1 implies x >= b )
assume b is_<=_than D1 ; ::_thesis: x >= b
then [x,y] >= [b,(inf D2)] by A3, A4, Th33;
hence x >= b by Th11; ::_thesis: verum
end;
A5: inf D1 is_<=_than D1 by A1, YELLOW_0:31;
let b be Element of S2; ::_thesis: ( b is_<=_than D2 implies y >= b )
assume b is_<=_than D2 ; ::_thesis: y >= b
then [x,y] >= [(inf D1),b] by A3, A5, Th33;
hence y >= b by Th11; ::_thesis: verum
end;
theorem :: YELLOW_3:37
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for 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
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2
for x being Element of S1
for 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
let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1
for 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
let x be Element of S1; ::_thesis: for 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
let y be Element of S2; ::_thesis: ( ( 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 ) implies for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b )
assume 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 ; ::_thesis: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] <= b
let b be Element of [:S1,S2:]; ::_thesis: ( b is_>=_than [:D1,D2:] implies [x,y] <= b )
assume A3: b is_>=_than [:D1,D2:] ; ::_thesis: [x,y] <= b
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then ex c, d being set 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)] by MCART_1:8;
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 [x,y] <= b by A4, A5, Th11; ::_thesis: verum
end;
theorem :: YELLOW_3:38
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1
for D2 being non empty Subset of S2
for x being Element of S1
for 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
let D1 be non empty Subset of S1; ::_thesis: for D2 being non empty Subset of S2
for x being Element of S1
for 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
let D2 be non empty Subset of S2; ::_thesis: for x being Element of S1
for 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
let x be Element of S1; ::_thesis: for 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
let y be Element of S2; ::_thesis: ( ( 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 ) implies for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b )
assume 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 ; ::_thesis: for b being Element of [:S1,S2:] st b is_>=_than [:D1,D2:] holds
[x,y] >= b
let b be Element of [:S1,S2:]; ::_thesis: ( b is_>=_than [:D1,D2:] implies [x,y] >= b )
assume A3: b is_>=_than [:D1,D2:] ; ::_thesis: [x,y] >= b
the carrier of [:S1,S2:] = [: the carrier of S1, the carrier of S2:] by Def2;
then ex c, d being set 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)] by MCART_1:8;
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 [x,y] >= b by A4, A5, Th11; ::_thesis: verum
end;
theorem Th39: :: YELLOW_3:39
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1
for 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:] )
let D1 be non empty Subset of S1; ::_thesis: for 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:] )
let D2 be non empty Subset of S2; ::_thesis: ( ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) iff ex_sup_of [:D1,D2:],[:S1,S2:] )
hereby ::_thesis: ( ex_sup_of [:D1,D2:],[:S1,S2:] implies ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) )
assume that
A1: ex_sup_of D1,S1 and
A2: ex_sup_of D2,S2 ; ::_thesis: ex_sup_of [:D1,D2:],[:S1,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]; ::_thesis: ( [:D1,D2:] is_<=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds
a <= b ) )
thus [:D1,D2:] is_<=_than a by A5, A3, Th30; ::_thesis: for b being Element of [:S1,S2:] st [:D1,D2:] is_<=_than b holds
a <= b
let b be Element of [:S1,S2:]; ::_thesis: ( [:D1,D2:] is_<=_than b implies a <= b )
assume A7: [:D1,D2:] is_<=_than b ; ::_thesis: a <= 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 a <= b by A8, A9, Th11; ::_thesis: verum
end;
hence ex_sup_of [:D1,D2:],[:S1,S2:] by YELLOW_0:15; ::_thesis: verum
end;
assume ex_sup_of [:D1,D2:],[:S1,S2:] ; ::_thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,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; ::_thesis: ( D1 is_<=_than b implies x `1 <= b )
assume D1 is_<=_than b ; ::_thesis: x `1 <= b
then x <= [b,(x `2)] by A11, A14, Th30;
hence x `1 <= b by A12, Th11; ::_thesis: verum
end;
hence ex_sup_of D1,S1 by A13, YELLOW_0:15; ::_thesis: ex_sup_of D2,S2
for b being Element of S2 st D2 is_<=_than b holds
x `2 <= b
proof
let b be Element of S2; ::_thesis: ( D2 is_<=_than b implies x `2 <= b )
assume D2 is_<=_than b ; ::_thesis: x `2 <= b
then x <= [(x `1),b] by A11, A13, Th30;
hence x `2 <= b by A12, Th11; ::_thesis: verum
end;
hence ex_sup_of D2,S2 by A14, YELLOW_0:15; ::_thesis: verum
end;
theorem Th40: :: YELLOW_3:40
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1
for 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:] )
let D1 be non empty Subset of S1; ::_thesis: for 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:] )
let D2 be non empty Subset of S2; ::_thesis: ( ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) iff ex_inf_of [:D1,D2:],[:S1,S2:] )
hereby ::_thesis: ( ex_inf_of [:D1,D2:],[:S1,S2:] implies ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) )
assume that
A1: ex_inf_of D1,S1 and
A2: ex_inf_of D2,S2 ; ::_thesis: ex_inf_of [:D1,D2:],[:S1,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]; ::_thesis: ( [:D1,D2:] is_>=_than a & ( for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds
a >= b ) )
thus [:D1,D2:] is_>=_than a by A5, A3, Th33; ::_thesis: for b being Element of [:S1,S2:] st [:D1,D2:] is_>=_than b holds
a >= b
let b be Element of [:S1,S2:]; ::_thesis: ( [:D1,D2:] is_>=_than b implies a >= b )
assume A7: [:D1,D2:] is_>=_than b ; ::_thesis: a >= 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 a >= b by A8, A9, Th11; ::_thesis: verum
end;
hence ex_inf_of [:D1,D2:],[:S1,S2:] by YELLOW_0:16; ::_thesis: verum
end;
assume ex_inf_of [:D1,D2:],[:S1,S2:] ; ::_thesis: ( ex_inf_of D1,S1 & ex_inf_of D2,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; ::_thesis: ( D1 is_>=_than b implies x `1 >= b )
assume D1 is_>=_than b ; ::_thesis: x `1 >= b
then x >= [b,(x `2)] by A11, A14, Th33;
hence x `1 >= b by A12, Th11; ::_thesis: verum
end;
hence ex_inf_of D1,S1 by A13, YELLOW_0:16; ::_thesis: ex_inf_of D2,S2
for b being Element of S2 st D2 is_>=_than b holds
x `2 >= b
proof
let b be Element of S2; ::_thesis: ( D2 is_>=_than b implies x `2 >= b )
assume D2 is_>=_than b ; ::_thesis: x `2 >= b
then x >= [(x `1),b] by A11, A13, Th33;
hence x `2 >= b by A12, Th11; ::_thesis: verum
end;
hence ex_inf_of D2,S2 by A14, YELLOW_0:16; ::_thesis: verum
end;
theorem Th41: :: YELLOW_3:41
for S1, S2 being non empty antisymmetric 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 non empty antisymmetric RelStr ; ::_thesis: 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:] )
let D be Subset of [:S1,S2:]; ::_thesis: ( ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) iff ex_sup_of D,[: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 ::_thesis: ( ex_sup_of D,[:S1,S2:] implies ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,S2 ) )
assume that
A3: ex_sup_of proj1 D,S1 and
A4: ex_sup_of proj2 D,S2 ; ::_thesis: ex_sup_of D,[:S1,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]; ::_thesis: ( D is_<=_than a & ( for b being Element of [:S1,S2:] st D is_<=_than b holds
a <= b ) )
thus D is_<=_than a ::_thesis: for b being Element of [:S1,S2:] st D is_<=_than b holds
a <= b
proof
let q be Element of [:S1,S2:]; :: according to LATTICE3:def_9 ::_thesis: ( not q in D or q <= a )
assume q in D ; ::_thesis: q <= a
then consider q1, q2 being set 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 = q2 as Element of S2 by A10;
reconsider q1 = q1 as Element of S1 by A9;
( q1 <= x1 & q2 <= x2 ) by A7, A5, A9, A10, LATTICE3:def_9;
hence q <= a by A11, Th11; ::_thesis: verum
end;
let b be Element of [:S1,S2:]; ::_thesis: ( D is_<=_than b implies a <= b )
assume A12: D is_<=_than b ; ::_thesis: a <= 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 a <= b by A13, A14, Th11; ::_thesis: verum
end;
hence ex_sup_of D,[:S1,S2:] by YELLOW_0:15; ::_thesis: verum
end;
assume ex_sup_of D,[:S1,S2:] ; ::_thesis: ( ex_sup_of proj1 D,S1 & ex_sup_of proj2 D,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; ::_thesis: ( proj1 D is_<=_than b implies x `1 <= b )
assume proj1 D is_<=_than b ; ::_thesis: x `1 <= b
then D is_<=_than [b,(x `2)] by A19, Th31;
then x <= [b,(x `2)] by A16;
hence x `1 <= b by A17, Th11; ::_thesis: verum
end;
hence ex_sup_of proj1 D,S1 by A18, YELLOW_0:15; ::_thesis: ex_sup_of proj2 D,S2
for b being Element of S2 st proj2 D is_<=_than b holds
x `2 <= b
proof
let b be Element of S2; ::_thesis: ( proj2 D is_<=_than b implies x `2 <= b )
assume proj2 D is_<=_than b ; ::_thesis: x `2 <= b
then D is_<=_than [(x `1),b] by A18, Th31;
then x <= [(x `1),b] by A16;
hence x `2 <= b by A17, Th11; ::_thesis: verum
end;
hence ex_sup_of proj2 D,S2 by A19, YELLOW_0:15; ::_thesis: verum
end;
theorem Th42: :: YELLOW_3:42
for S1, S2 being non empty antisymmetric 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 non empty antisymmetric RelStr ; ::_thesis: 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:] )
let D be Subset of [:S1,S2:]; ::_thesis: ( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[: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 ::_thesis: ( ex_inf_of D,[:S1,S2:] implies ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) )
assume that
A3: ex_inf_of proj1 D,S1 and
A4: ex_inf_of proj2 D,S2 ; ::_thesis: ex_inf_of D,[:S1,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]; ::_thesis: ( D is_>=_than a & ( for b being Element of [:S1,S2:] st D is_>=_than b holds
a >= b ) )
thus D is_>=_than a ::_thesis: for b being Element of [:S1,S2:] st D is_>=_than b holds
a >= b
proof
let q be Element of [:S1,S2:]; :: according to LATTICE3:def_8 ::_thesis: ( not q in D or a <= q )
assume q in D ; ::_thesis: a <= q
then consider q1, q2 being set 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 = q2 as Element of S2 by A10;
reconsider q1 = q1 as Element of S1 by A9;
( q1 >= x1 & q2 >= x2 ) by A7, A5, A9, A10, LATTICE3:def_8;
hence a <= q by A11, Th11; ::_thesis: verum
end;
let b be Element of [:S1,S2:]; ::_thesis: ( D is_>=_than b implies a >= b )
assume A12: D is_>=_than b ; ::_thesis: a >= 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 a >= b by A13, A14, Th11; ::_thesis: verum
end;
hence ex_inf_of D,[:S1,S2:] by YELLOW_0:16; ::_thesis: verum
end;
assume ex_inf_of D,[:S1,S2:] ; ::_thesis: ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,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; ::_thesis: ( proj1 D is_>=_than b implies x `1 >= b )
assume proj1 D is_>=_than b ; ::_thesis: x `1 >= b
then D is_>=_than [b,(x `2)] by A19, Th34;
then x >= [b,(x `2)] by A16;
hence x `1 >= b by A17, Th11; ::_thesis: verum
end;
hence ex_inf_of proj1 D,S1 by A18, YELLOW_0:16; ::_thesis: ex_inf_of proj2 D,S2
for b being Element of S2 st proj2 D is_>=_than b holds
x `2 >= b
proof
let b be Element of S2; ::_thesis: ( proj2 D is_>=_than b implies x `2 >= b )
assume proj2 D is_>=_than b ; ::_thesis: x `2 >= b
then D is_>=_than [(x `1),b] by A18, Th34;
then x >= [(x `1),b] by A16;
hence x `2 >= b by A17, Th11; ::_thesis: verum
end;
hence ex_inf_of proj2 D,S2 by A19, YELLOW_0:16; ::_thesis: verum
end;
theorem Th43: :: YELLOW_3:43
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1
for 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)]
let D1 be non empty Subset of S1; ::_thesis: for 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)]
let D2 be non empty Subset of S2; ::_thesis: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 implies sup [:D1,D2:] = [(sup D1),(sup D2)] )
assume A1: ( ex_sup_of D1,S1 & ex_sup_of D2,S2 ) ; ::_thesis: sup [:D1,D2:] = [(sup D1),(sup D2)]
set s = sup [:D1,D2:];
sup [:D1,D2:] is Element of [: the carrier of S1, the carrier of S2:] by Def2;
then consider s1, s2 being set such that
A2: s1 in the carrier of S1 and
A3: s2 in the carrier of S2 and
A4: sup [:D1,D2:] = [s1,s2] by ZFMISC_1:def_2;
reconsider s2 = s2 as Element of S2 by A3;
reconsider s1 = 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 sup [:D1,D2:] = [(sup D1),(sup D2)] by A4, A9, A10, YELLOW_0:30; ::_thesis: verum
end;
theorem Th44: :: YELLOW_3:44
for S1, S2 being non empty antisymmetric RelStr
for D1 being non empty Subset of S1
for 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 non empty antisymmetric RelStr ; ::_thesis: for D1 being non empty Subset of S1
for 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)]
let D1 be non empty Subset of S1; ::_thesis: for 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)]
let D2 be non empty Subset of S2; ::_thesis: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 implies inf [:D1,D2:] = [(inf D1),(inf D2)] )
assume A1: ( ex_inf_of D1,S1 & ex_inf_of D2,S2 ) ; ::_thesis: inf [:D1,D2:] = [(inf D1),(inf D2)]
set s = inf [:D1,D2:];
inf [:D1,D2:] is Element of [: the carrier of S1, the carrier of S2:] by Def2;
then consider s1, s2 being set such that
A2: s1 in the carrier of S1 and
A3: s2 in the carrier of S2 and
A4: inf [:D1,D2:] = [s1,s2] by ZFMISC_1:def_2;
reconsider s2 = s2 as Element of S2 by A3;
reconsider s1 = 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 inf [:D1,D2:] = [(inf D1),(inf D2)] by A4, A9, A10, YELLOW_0:31; ::_thesis: verum
end;
registration
let X, Y be non empty antisymmetric complete RelStr ;
cluster[:X,Y:] -> strict complete ;
coherence
[:X,Y:] is complete
proof
set IT = [:X,Y:];
for D being Subset of [:X,Y:] holds ex_sup_of D,[:X,Y:]
proof
let D be Subset of [:X,Y:]; ::_thesis: ex_sup_of D,[:X,Y:]
( ex_sup_of proj1 D,X & ex_sup_of proj2 D,Y ) by YELLOW_0:17;
hence ex_sup_of D,[:X,Y:] by Th41; ::_thesis: verum
end;
hence [:X,Y:] is complete by YELLOW_0:53; ::_thesis: verum
end;
end;
theorem :: YELLOW_3:45
for X, Y being non empty antisymmetric lower-bounded RelStr st [:X,Y:] is complete holds
( X is complete & Y is complete )
proof
let X, Y be non empty antisymmetric lower-bounded RelStr ; ::_thesis: ( [:X,Y:] is complete implies ( X is complete & Y is complete ) )
assume A1: [:X,Y:] is complete ; ::_thesis: ( X is complete & Y is complete )
for A being Subset of X holds ex_sup_of A,X
proof
let A be Subset of X; ::_thesis: ex_sup_of A,X
percases ( not A is empty or A is empty ) ;
supposeA2: not A is empty ; ::_thesis: ex_sup_of A,X
set B = the non empty Subset of Y;
ex_sup_of [:A, the non empty Subset of Y:],[:X,Y:] by A1, YELLOW_0:17;
hence ex_sup_of A,X by A2, Th39; ::_thesis: verum
end;
suppose A is empty ; ::_thesis: ex_sup_of A,X
hence ex_sup_of A,X by YELLOW_0:42; ::_thesis: verum
end;
end;
end;
hence X is complete by YELLOW_0:53; ::_thesis: Y is complete
for B being Subset of Y holds ex_sup_of B,Y
proof
let B be Subset of Y; ::_thesis: ex_sup_of B,Y
percases ( not B is empty or B is empty ) ;
supposeA3: not B is empty ; ::_thesis: ex_sup_of B,Y
set A = the non empty Subset of X;
ex_sup_of [: the non empty Subset of X,B:],[:X,Y:] by A1, YELLOW_0:17;
hence ex_sup_of B,Y by A3, Th39; ::_thesis: verum
end;
suppose B is empty ; ::_thesis: ex_sup_of B,Y
hence ex_sup_of B,Y by YELLOW_0:42; ::_thesis: verum
end;
end;
end;
hence Y is complete by YELLOW_0:53; ::_thesis: verum
end;
theorem :: YELLOW_3:46
for L1, L2 being non empty antisymmetric 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 non empty antisymmetric RelStr ; ::_thesis: 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))]
let D be non empty Subset of [:L1,L2:]; ::_thesis: ( ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) implies sup D = [(sup (proj1 D)),(sup (proj2 D))] )
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 set such that
A1: d1 in C1 and
A2: d2 in C2 and
A3: sup D = [d1,d2] by ZFMISC_1:def_2;
reconsider d1 = d1 as Element of L1 by A1;
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
not proj1 D9 is empty ;
then reconsider D1 = proj1 D as non empty Subset of L1 ;
not proj2 D9 is empty ;
then reconsider D2 = proj2 D as non empty Subset of L2 ;
A4: D9 c= [:D1,D2:] by Th1;
reconsider d2 = d2 as Element of L2 by A2;
assume ( [:L1,L2:] is complete or ex_sup_of D,[:L1,L2:] ) ; ::_thesis: sup D = [(sup (proj1 D)),(sup (proj2 D))]
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; :: according to LATTICE3:def_9 ::_thesis: ( not b in D2 or b <= d2 )
assume b in D2 ; ::_thesis: b <= d2
then consider x being set such that
A9: [x,b] in D by XTUPLE_0:def_13;
reconsider x = x as Element of D1 by A9, XTUPLE_0:def_12;
reconsider x = x as Element of L1 ;
D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9;
then [x,b] <= [d1,d2] by A9, LATTICE3:def_9;
hence b <= d2 by Th11; ::_thesis: verum
end;
then A10: sup D2 <= d2 by A6, YELLOW_0:def_9;
D1 is_<=_than d1
proof
let b be Element of L1; :: according to LATTICE3:def_9 ::_thesis: ( not b in D1 or b <= d1 )
assume b in D1 ; ::_thesis: b <= d1
then consider x being set such that
A11: [b,x] in D by XTUPLE_0:def_12;
reconsider x = x as Element of D2 by A11, XTUPLE_0:def_13;
reconsider x = x as Element of L2 ;
D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def_9;
then [b,x] <= [d1,d2] by A11, LATTICE3:def_9;
hence b <= d1 by Th11; ::_thesis: verum
end;
then sup D1 <= d1 by A7, YELLOW_0:def_9;
then [(sup D1),(sup D2)] <= sup D by A3, A10, Th11;
hence sup D = [(sup (proj1 D)),(sup (proj2 D))] by A8, ORDERS_2:2; ::_thesis: verum
end;
theorem :: YELLOW_3:47
for L1, L2 being non empty antisymmetric 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 non empty antisymmetric RelStr ; ::_thesis: 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))]
let D be non empty Subset of [:L1,L2:]; ::_thesis: ( ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) implies inf D = [(inf (proj1 D)),(inf (proj2 D))] )
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 set such that
A1: d1 in C1 and
A2: d2 in C2 and
A3: inf D = [d1,d2] by ZFMISC_1:def_2;
reconsider d1 = d1 as Element of L1 by A1;
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
not proj1 D9 is empty ;
then reconsider D1 = proj1 D as non empty Subset of L1 ;
not proj2 D9 is empty ;
then reconsider D2 = proj2 D as non empty Subset of L2 ;
A4: D9 c= [:D1,D2:] by Th1;
reconsider d2 = d2 as Element of L2 by A2;
assume ( [:L1,L2:] is complete or ex_inf_of D,[:L1,L2:] ) ; ::_thesis: inf D = [(inf (proj1 D)),(inf (proj2 D))]
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; :: according to LATTICE3:def_8 ::_thesis: ( not b in D2 or d2 <= b )
assume b in D2 ; ::_thesis: d2 <= b
then consider x being set such that
A9: [x,b] in D by XTUPLE_0:def_13;
reconsider x = x as Element of D1 by A9, XTUPLE_0:def_12;
reconsider x = x as Element of L1 ;
D is_>=_than [d1,d2] by A5, A3, YELLOW_0:def_10;
then [x,b] >= [d1,d2] by A9, LATTICE3:def_8;
hence d2 <= b by Th11; ::_thesis: verum
end;
then A10: inf D2 >= d2 by A6, YELLOW_0:def_10;
D1 is_>=_than d1
proof
let b be Element of L1; :: according to LATTICE3:def_8 ::_thesis: ( not b in D1 or d1 <= b )
assume b in D1 ; ::_thesis: d1 <= b
then consider x being set such that
A11: [b,x] in D by XTUPLE_0:def_12;
reconsider x = x as Element of D2 by A11, XTUPLE_0:def_13;
reconsider x = x as Element of L2 ;
D is_>=_than [d1,d2] by A5, A3, YELLOW_0:def_10;
then [b,x] >= [d1,d2] by A11, LATTICE3:def_8;
hence d1 <= b by Th11; ::_thesis: verum
end;
then inf D1 >= d1 by A7, YELLOW_0:def_10;
then [(inf D1),(inf D2)] >= inf D by A3, A10, Th11;
hence inf D = [(inf (proj1 D)),(inf (proj2 D))] by A8, ORDERS_2:2; ::_thesis: verum
end;
theorem :: YELLOW_3:48
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 ; ::_thesis: for D being non empty directed Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= downarrow D
let D be non empty directed Subset of [:S1,S2:]; ::_thesis: [:(proj1 D),(proj2 D):] c= downarrow D
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set ;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [:(proj1 D),(proj2 D):] or q in downarrow D )
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
set D1 = proj1 D;
set 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= [:(proj1 D),(proj2 D):] by Th1;
not proj2 D9 is empty ;
then reconsider D2 = proj2 D as non empty Subset of S2 ;
not proj1 D9 is empty ;
then reconsider D1 = proj1 D as non empty Subset of S1 ;
assume q in [:(proj1 D),(proj2 D):] ; ::_thesis: q in downarrow D
then consider d, e being set such that
A3: d in D1 and
A4: e in D2 and
A5: q = [d,e] by ZFMISC_1:def_2;
consider y being set such that
A6: [d,y] in D by A3, XTUPLE_0:def_12;
consider x being set such that
A7: [x,e] in D by A4, XTUPLE_0:def_13;
reconsider y = y, e = e as Element of D2 by A6, A7, XTUPLE_0:def_13;
reconsider x = x, d = 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 set 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 = z2 as Element of D2 by A11;
reconsider z1 = 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 q in downarrow D by A5, A1, A8, A12; ::_thesis: verum
end;
theorem :: YELLOW_3:49
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 ; ::_thesis: for D being non empty filtered Subset of [:S1,S2:] holds [:(proj1 D),(proj2 D):] c= uparrow D
let D be non empty filtered Subset of [:S1,S2:]; ::_thesis: [:(proj1 D),(proj2 D):] c= uparrow D
reconsider C1 = the carrier of S1, C2 = the carrier of S2 as non empty set ;
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in [:(proj1 D),(proj2 D):] or q in uparrow D )
reconsider D9 = D as non empty Subset of [:C1,C2:] by Def2;
set D1 = proj1 D;
set 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= [:(proj1 D),(proj2 D):] by Th1;
not proj2 D9 is empty ;
then reconsider D2 = proj2 D as non empty Subset of S2 ;
not proj1 D9 is empty ;
then reconsider D1 = proj1 D as non empty Subset of S1 ;
assume q in [:(proj1 D),(proj2 D):] ; ::_thesis: q in uparrow D
then consider d, e being set such that
A3: d in D1 and
A4: e in D2 and
A5: q = [d,e] by ZFMISC_1:def_2;
consider y being set such that
A6: [d,y] in D by A3, XTUPLE_0:def_12;
consider x being set such that
A7: [x,e] in D by A4, XTUPLE_0:def_13;
reconsider y = y, e = e as Element of D2 by A6, A7, XTUPLE_0:def_13;
reconsider x = x, d = 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 set 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 = z2 as Element of D2 by A11;
reconsider z1 = 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 q in uparrow D by A5, A1, A8, A12; ::_thesis: verum
end;
scheme :: YELLOW_3:sch 6
Kappa2DS{ F1() -> non empty RelStr , F2() -> non empty RelStr , F3() -> non empty RelStr , F4( set , set ) -> set } :
ex f being Function of [:F1(),F2():],F3() st
for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y)
provided
A1: for x being Element of F1()
for y being Element of F2() holds F4(x,y) is Element of F3()
proof
A2: for x being Element of F1()
for y being Element of F2() holds F4(x,y) in the carrier of F3()
proof
let x be Element of F1(); ::_thesis: for y being Element of F2() holds F4(x,y) in the carrier of F3()
let y be Element of F2(); ::_thesis: F4(x,y) in the carrier of F3()
reconsider x1 = x as Element of F1() ;
reconsider y1 = y as Element of F2() ;
F4(x1,y1) is Element of F3() by A1;
hence F4(x,y) in the carrier of F3() ; ::_thesis: verum
end;
consider f being Function of [: the carrier of F1(), the carrier of F2():], the carrier of F3() such that
A3: for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y) from FUNCT_7:sch_1(A2);
the carrier of [:F1(),F2():] = [: the carrier of F1(), the carrier of F2():] by Def2;
then reconsider f = f as Function of [:F1(),F2():],F3() ;
take f ; ::_thesis: for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y)
thus for x being Element of F1()
for y being Element of F2() holds f . (x,y) = F4(x,y) by A3; ::_thesis: verum
end;