let L be lower-bounded continuous sup-Semilattice; :: thesis: for B being with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving

let B be with_bottom CLbasis of L; :: thesis: idsMap (subrelstr B) is sups-preserving

set f = idsMap (subrelstr B);

A1: subrelstr B is join-inheriting by Def2;

A2: Bottom L in B by Def8;

then A3: Bottom L in the carrier of (subrelstr B) by YELLOW_0:def 15;

let B be with_bottom CLbasis of L; :: thesis: idsMap (subrelstr B) is sups-preserving

set f = idsMap (subrelstr B);

A1: subrelstr B is join-inheriting by Def2;

A2: Bottom L in B by Def8;

then A3: Bottom L in the carrier of (subrelstr B) by YELLOW_0:def 15;

now :: thesis: for X being Subset of (InclPoset (Ids (subrelstr B))) holds idsMap (subrelstr B) preserves_sup_of X

hence
idsMap (subrelstr B) is sups-preserving
by WAYBEL_0:def 33; :: thesis: verumlet X be Subset of (InclPoset (Ids (subrelstr B))); :: thesis: idsMap (subrelstr B) preserves_sup_of X

reconsider supX = sup X as Ideal of (subrelstr B) by YELLOW_2:41;

reconsider unionX = union X as Subset of L by WAYBEL13:3;

reconsider dfuX = downarrow (finsups (union X)) as Subset of L by WAYBEL13:3;

reconsider fuX = finsups (union X) as Subset of L by WAYBEL13:3;

A4: ex J being Subset of L st

( supX = J & (idsMap (subrelstr B)) . supX = downarrow J ) by Def11;

end;reconsider supX = sup X as Ideal of (subrelstr B) by YELLOW_2:41;

reconsider unionX = union X as Subset of L by WAYBEL13:3;

reconsider dfuX = downarrow (finsups (union X)) as Subset of L by WAYBEL13:3;

reconsider fuX = finsups (union X) as Subset of L by WAYBEL13:3;

A4: ex J being Subset of L st

( supX = J & (idsMap (subrelstr B)) . supX = downarrow J ) by Def11;

now :: thesis: ( ex_sup_of X, InclPoset (Ids (subrelstr B)) implies ( ex_sup_of (idsMap (subrelstr B)) .: X, InclPoset (Ids L) & sup ((idsMap (subrelstr B)) .: X) = (idsMap (subrelstr B)) . (sup X) ) )

hence
idsMap (subrelstr B) preserves_sup_of X
by WAYBEL_0:def 31; :: thesis: verumassume
ex_sup_of X, InclPoset (Ids (subrelstr B))
; :: thesis: ( ex_sup_of (idsMap (subrelstr B)) .: X, InclPoset (Ids L) & sup ((idsMap (subrelstr B)) .: X) = (idsMap (subrelstr B)) . (sup X) )

thus ex_sup_of (idsMap (subrelstr B)) .: X, InclPoset (Ids L) by YELLOW_0:17; :: thesis: sup ((idsMap (subrelstr B)) .: X) = (idsMap (subrelstr B)) . (sup X)

A5: downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) c= downarrow dfuX

then A41: finsups unionX c= finsups (union ((idsMap (subrelstr B)) .: X)) by Th2;

finsups (union X) c= finsups unionX by A3, A1, Th5;

then finsups (union X) c= finsups (union ((idsMap (subrelstr B)) .: X)) by A41;

then A42: downarrow fuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by YELLOW_3:6;

downarrow (finsups (union X)) c= downarrow fuX by Th11;

then dfuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by A42;

then downarrow dfuX c= downarrow (downarrow (finsups (union ((idsMap (subrelstr B)) .: X)))) by YELLOW_3:6;

then A43: downarrow dfuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by Th7;

thus sup ((idsMap (subrelstr B)) .: X) = downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by Th6

.= downarrow dfuX by A5, A43

.= (idsMap (subrelstr B)) . (sup X) by A4, Th6 ; :: thesis: verum

end;thus ex_sup_of (idsMap (subrelstr B)) .: X, InclPoset (Ids L) by YELLOW_0:17; :: thesis: sup ((idsMap (subrelstr B)) .: X) = (idsMap (subrelstr B)) . (sup X)

A5: downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) c= downarrow dfuX

proof

defpred S_{1}[ object , object ] means ex I being Element of (InclPoset (Ids (subrelstr B))) ex z1, z2 being Element of L st

( z1 = $1 & z2 = $2 & I in X & $2 in I & z1 <= z2 );

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) or x in downarrow dfuX )

assume A6: x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) ; :: thesis: x in downarrow dfuX

then reconsider x1 = x as Element of L ;

consider y1 being Element of L such that

A7: y1 >= x1 and

A8: y1 in finsups (union ((idsMap (subrelstr B)) .: X)) by A6, WAYBEL_0:def 15;

y1 in { ("\/" (V,L)) where V is finite Subset of (union ((idsMap (subrelstr B)) .: X)) : ex_sup_of V,L } by A8, WAYBEL_0:def 27;

then consider Y being finite Subset of (union ((idsMap (subrelstr B)) .: X)) such that

A9: y1 = "\/" (Y,L) and

ex_sup_of Y,L ;

A10: for z being object st z in Y holds

ex v being Element of B st S_{1}[z,v]

A19: for z being object st z in Y holds

S_{1}[z,g . z]
from MONOID_1:sch 1(A10);

reconsider Z = rng g as finite Subset of (subrelstr B) by YELLOW_0:def 15;

A20: dom g = Y by FUNCT_2:def 1;

A21: "\/" ((rng g),L) is_>=_than Y

then A30: "\/" ((rng g),(subrelstr B)) in finsups (union X) by WAYBEL_0:def 27;

"\/" (Z,L) in the carrier of (subrelstr B)

reconsider srg = "\/" ((rng g),(subrelstr B)) as Element of L by YELLOW_0:58;

A31: ex_sup_of Z,L by YELLOW_0:17;

xl is_>=_than Z

then "\/" (Y,L) <= srg by A21, YELLOW_0:32;

then A35: x1 <= srg by A7, A9, YELLOW_0:def 2;

finsups (union X) c= downarrow (finsups (union X)) by WAYBEL_0:16;

hence x in downarrow dfuX by A35, A30, WAYBEL_0:def 15; :: thesis: verum

end;( z1 = $1 & z2 = $2 & I in X & $2 in I & z1 <= z2 );

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) or x in downarrow dfuX )

assume A6: x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) ; :: thesis: x in downarrow dfuX

then reconsider x1 = x as Element of L ;

consider y1 being Element of L such that

A7: y1 >= x1 and

A8: y1 in finsups (union ((idsMap (subrelstr B)) .: X)) by A6, WAYBEL_0:def 15;

y1 in { ("\/" (V,L)) where V is finite Subset of (union ((idsMap (subrelstr B)) .: X)) : ex_sup_of V,L } by A8, WAYBEL_0:def 27;

then consider Y being finite Subset of (union ((idsMap (subrelstr B)) .: X)) such that

A9: y1 = "\/" (Y,L) and

ex_sup_of Y,L ;

A10: for z being object st z in Y holds

ex v being Element of B st S

proof

consider g being Function of Y,B such that
let z be object ; :: thesis: ( z in Y implies ex v being Element of B st S_{1}[z,v] )

assume z in Y ; :: thesis: ex v being Element of B st S_{1}[z,v]

then consider J being set such that

A11: z in J and

A12: J in (idsMap (subrelstr B)) .: X by TARSKI:def 4;

consider I being object such that

I in dom (idsMap (subrelstr B)) and

A13: I in X and

A14: J = (idsMap (subrelstr B)) . I by A12, FUNCT_1:def 6;

reconsider I = I as Element of (InclPoset (Ids (subrelstr B))) by A13;

(idsMap (subrelstr B)) . I is Element of (InclPoset (Ids L)) ;

then reconsider J = J as Element of (InclPoset (Ids L)) by A14;

J is Ideal of L by YELLOW_2:41;

then reconsider z1 = z as Element of L by A11;

reconsider I1 = I as Ideal of (subrelstr B) by YELLOW_2:41;

consider I2 being Subset of L such that

A15: I1 = I2 and

A16: (idsMap (subrelstr B)) . I1 = downarrow I2 by Def11;

consider z2 being Element of L such that

A17: z2 >= z1 and

A18: z2 in I2 by A11, A14, A16, WAYBEL_0:def 15;

reconsider v = z2 as Element of B by A15, A18, YELLOW_0:def 15;

take v ; :: thesis: S_{1}[z,v]

take I ; :: thesis: ex z1, z2 being Element of L st

( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )

take z1 ; :: thesis: ex z2 being Element of L st

( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )

take z2 ; :: thesis: ( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )

thus ( z1 = z & z2 = v & I in X & v in I & z1 <= z2 ) by A13, A15, A17, A18; :: thesis: verum

end;assume z in Y ; :: thesis: ex v being Element of B st S

then consider J being set such that

A11: z in J and

A12: J in (idsMap (subrelstr B)) .: X by TARSKI:def 4;

consider I being object such that

I in dom (idsMap (subrelstr B)) and

A13: I in X and

A14: J = (idsMap (subrelstr B)) . I by A12, FUNCT_1:def 6;

reconsider I = I as Element of (InclPoset (Ids (subrelstr B))) by A13;

(idsMap (subrelstr B)) . I is Element of (InclPoset (Ids L)) ;

then reconsider J = J as Element of (InclPoset (Ids L)) by A14;

J is Ideal of L by YELLOW_2:41;

then reconsider z1 = z as Element of L by A11;

reconsider I1 = I as Ideal of (subrelstr B) by YELLOW_2:41;

consider I2 being Subset of L such that

A15: I1 = I2 and

A16: (idsMap (subrelstr B)) . I1 = downarrow I2 by Def11;

consider z2 being Element of L such that

A17: z2 >= z1 and

A18: z2 in I2 by A11, A14, A16, WAYBEL_0:def 15;

reconsider v = z2 as Element of B by A15, A18, YELLOW_0:def 15;

take v ; :: thesis: S

take I ; :: thesis: ex z1, z2 being Element of L st

( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )

take z1 ; :: thesis: ex z2 being Element of L st

( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )

take z2 ; :: thesis: ( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )

thus ( z1 = z & z2 = v & I in X & v in I & z1 <= z2 ) by A13, A15, A17, A18; :: thesis: verum

A19: for z being object st z in Y holds

S

reconsider Z = rng g as finite Subset of (subrelstr B) by YELLOW_0:def 15;

A20: dom g = Y by FUNCT_2:def 1;

A21: "\/" ((rng g),L) is_>=_than Y

proof

A27:
ex_sup_of Z, subrelstr B
let a be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not a in Y or a <= "\/" ((rng g),L) )

A22: "\/" ((rng g),L) is_>=_than rng g by YELLOW_0:32;

assume A23: a in Y ; :: thesis: a <= "\/" ((rng g),L)

then consider I being Element of (InclPoset (Ids (subrelstr B))), a1, a2 being Element of L such that

A24: a1 = a and

A25: a2 = g . a and

I in X and

g . a in I and

A26: a1 <= a2 by A19;

g . a in rng g by A20, A23, FUNCT_1:def 3;

then a2 <= "\/" ((rng g),L) by A25, A22;

hence a <= "\/" ((rng g),L) by A24, A26, YELLOW_0:def 2; :: thesis: verum

end;A22: "\/" ((rng g),L) is_>=_than rng g by YELLOW_0:32;

assume A23: a in Y ; :: thesis: a <= "\/" ((rng g),L)

then consider I being Element of (InclPoset (Ids (subrelstr B))), a1, a2 being Element of L such that

A24: a1 = a and

A25: a2 = g . a and

I in X and

g . a in I and

A26: a1 <= a2 by A19;

g . a in rng g by A20, A23, FUNCT_1:def 3;

then a2 <= "\/" ((rng g),L) by A25, A22;

hence a <= "\/" ((rng g),L) by A24, A26, YELLOW_0:def 2; :: thesis: verum

proof
end;

rng g c= union X
proof

then
"\/" (Z,(subrelstr B)) in { ("\/" (V,(subrelstr B))) where V is finite Subset of (union X) : ex_sup_of V, subrelstr B }
by A27;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng g or a in union X )

assume a in rng g ; :: thesis: a in union X

then consider b being object such that

A28: b in dom g and

A29: a = g . b by FUNCT_1:def 3;

ex I being Element of (InclPoset (Ids (subrelstr B))) ex b1, b2 being Element of L st

( b1 = b & b2 = g . b & I in X & g . b in I & b1 <= b2 ) by A19, A28;

hence a in union X by A29, TARSKI:def 4; :: thesis: verum

end;assume a in rng g ; :: thesis: a in union X

then consider b being object such that

A28: b in dom g and

A29: a = g . b by FUNCT_1:def 3;

ex I being Element of (InclPoset (Ids (subrelstr B))) ex b1, b2 being Element of L st

( b1 = b & b2 = g . b & I in X & g . b in I & b1 <= b2 ) by A19, A28;

hence a in union X by A29, TARSKI:def 4; :: thesis: verum

then A30: "\/" ((rng g),(subrelstr B)) in finsups (union X) by WAYBEL_0:def 27;

"\/" (Z,L) in the carrier of (subrelstr B)

proof
end;

then reconsider xl = "\/" (Z,L) as Element of (subrelstr B) ;reconsider srg = "\/" ((rng g),(subrelstr B)) as Element of L by YELLOW_0:58;

A31: ex_sup_of Z,L by YELLOW_0:17;

A32: now :: thesis: for b being Element of (subrelstr B) st b is_>=_than Z holds

xl <= b

A34:
"\/" (Z,L) is_>=_than Z
by A31, YELLOW_0:30;xl <= b

let b be Element of (subrelstr B); :: thesis: ( b is_>=_than Z implies xl <= b )

reconsider b1 = b as Element of L by YELLOW_0:58;

assume A33: b is_>=_than Z ; :: thesis: xl <= b

b1 is_>=_than Z by A33, YELLOW_0:59;

then "\/" (Z,L) <= b1 by A31, YELLOW_0:30;

hence xl <= b by YELLOW_0:60; :: thesis: verum

end;reconsider b1 = b as Element of L by YELLOW_0:58;

assume A33: b is_>=_than Z ; :: thesis: xl <= b

b1 is_>=_than Z by A33, YELLOW_0:59;

then "\/" (Z,L) <= b1 by A31, YELLOW_0:30;

hence xl <= b by YELLOW_0:60; :: thesis: verum

xl is_>=_than Z

proof

then
"\/" (Z,(subrelstr B)) = "\/" (Z,L)
by A32, YELLOW_0:30;
let b be Element of (subrelstr B); :: according to LATTICE3:def 9 :: thesis: ( not b in Z or b <= xl )

reconsider b1 = b as Element of L by YELLOW_0:58;

assume b in Z ; :: thesis: b <= xl

then b1 <= "\/" (Z,L) by A34;

hence b <= xl by YELLOW_0:60; :: thesis: verum

end;reconsider b1 = b as Element of L by YELLOW_0:58;

assume b in Z ; :: thesis: b <= xl

then b1 <= "\/" (Z,L) by A34;

hence b <= xl by YELLOW_0:60; :: thesis: verum

then "\/" (Y,L) <= srg by A21, YELLOW_0:32;

then A35: x1 <= srg by A7, A9, YELLOW_0:def 2;

finsups (union X) c= downarrow (finsups (union X)) by WAYBEL_0:16;

hence x in downarrow dfuX by A35, A30, WAYBEL_0:def 15; :: thesis: verum

now :: thesis: for x being set st x in X holds

x c= union ((idsMap (subrelstr B)) .: X)

then
union X c= union ((idsMap (subrelstr B)) .: X)
by ZFMISC_1:76;x c= union ((idsMap (subrelstr B)) .: X)

let x be set ; :: thesis: ( x in X implies x c= union ((idsMap (subrelstr B)) .: X) )

assume A36: x in X ; :: thesis: x c= union ((idsMap (subrelstr B)) .: X)

then reconsider x1 = x as Ideal of (subrelstr B) by YELLOW_2:41;

consider x2 being Subset of L such that

A37: x1 = x2 and

A38: (idsMap (subrelstr B)) . x1 = downarrow x2 by Def11;

x in the carrier of (InclPoset (Ids (subrelstr B))) by A36;

then x1 in dom (idsMap (subrelstr B)) by FUNCT_2:def 1;

then A39: (idsMap (subrelstr B)) . x1 in (idsMap (subrelstr B)) .: X by A36, FUNCT_1:def 6;

thus x c= union ((idsMap (subrelstr B)) .: X) :: thesis: verum

end;assume A36: x in X ; :: thesis: x c= union ((idsMap (subrelstr B)) .: X)

then reconsider x1 = x as Ideal of (subrelstr B) by YELLOW_2:41;

consider x2 being Subset of L such that

A37: x1 = x2 and

A38: (idsMap (subrelstr B)) . x1 = downarrow x2 by Def11;

x in the carrier of (InclPoset (Ids (subrelstr B))) by A36;

then x1 in dom (idsMap (subrelstr B)) by FUNCT_2:def 1;

then A39: (idsMap (subrelstr B)) . x1 in (idsMap (subrelstr B)) .: X by A36, FUNCT_1:def 6;

thus x c= union ((idsMap (subrelstr B)) .: X) :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in x or y in union ((idsMap (subrelstr B)) .: X) )

assume A40: y in x ; :: thesis: y in union ((idsMap (subrelstr B)) .: X)

x c= downarrow x2 by A37, WAYBEL_0:16;

hence y in union ((idsMap (subrelstr B)) .: X) by A38, A39, A40, TARSKI:def 4; :: thesis: verum

end;assume A40: y in x ; :: thesis: y in union ((idsMap (subrelstr B)) .: X)

x c= downarrow x2 by A37, WAYBEL_0:16;

hence y in union ((idsMap (subrelstr B)) .: X) by A38, A39, A40, TARSKI:def 4; :: thesis: verum

then A41: finsups unionX c= finsups (union ((idsMap (subrelstr B)) .: X)) by Th2;

finsups (union X) c= finsups unionX by A3, A1, Th5;

then finsups (union X) c= finsups (union ((idsMap (subrelstr B)) .: X)) by A41;

then A42: downarrow fuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by YELLOW_3:6;

downarrow (finsups (union X)) c= downarrow fuX by Th11;

then dfuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by A42;

then downarrow dfuX c= downarrow (downarrow (finsups (union ((idsMap (subrelstr B)) .: X)))) by YELLOW_3:6;

then A43: downarrow dfuX c= downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by Th7;

thus sup ((idsMap (subrelstr B)) .: X) = downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) by Th6

.= downarrow dfuX by A5, A43

.= (idsMap (subrelstr B)) . (sup X) by A4, Th6 ; :: thesis: verum