let L be lower-bounded continuous sup-Semilattice; for B being with_bottom CLbasis of L holds idsMap (subrelstr B) is sups-preserving
let B be with_bottom CLbasis of L; 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 for X being Subset of (InclPoset (Ids (subrelstr B))) holds idsMap (subrelstr B) preserves_sup_of Xlet X be
Subset of
(InclPoset (Ids (subrelstr B)));
idsMap (subrelstr B) preserves_sup_of Xreconsider 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 ( 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) ) )assume
ex_sup_of X,
InclPoset (Ids (subrelstr B))
;
( 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;
sup ((idsMap (subrelstr B)) .: X) = (idsMap (subrelstr B)) . (sup X)A5:
downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) c= downarrow dfuX
proof
defpred S1[
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 ;
TARSKI:def 3 ( 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)))
;
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
S1[
z,
v]
proof
let z be
object ;
( z in Y implies ex v being Element of B st S1[z,v] )
assume
z in Y
;
ex v being Element of B st S1[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
;
S1[z,v]
take
I
;
ex z1, z2 being Element of L st
( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )
take
z1
;
ex z2 being Element of L st
( z1 = z & z2 = v & I in X & v in I & z1 <= z2 )
take
z2
;
( 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;
verum
end;
consider g being
Function of
Y,
B such that A19:
for
z being
object st
z in Y holds
S1[
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
proof
let a be
Element of
L;
LATTICE3:def 9 ( 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
;
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;
verum
end;
A27:
ex_sup_of Z,
subrelstr B
rng g c= union X
then
"\/" (
Z,
(subrelstr B))
in { ("\/" (V,(subrelstr B))) where V is finite Subset of (union X) : ex_sup_of V, subrelstr B }
by A27;
then A30:
"\/" (
(rng g),
(subrelstr B))
in finsups (union X)
by WAYBEL_0:def 27;
"\/" (
Z,
L)
in the
carrier of
(subrelstr B)
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;
A34:
"\/" (
Z,
L)
is_>=_than Z
by A31, YELLOW_0:30;
xl is_>=_than Z
then
"\/" (
Z,
(subrelstr B))
= "\/" (
Z,
L)
by A32, YELLOW_0:30;
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;
verum
end; then
union X c= union ((idsMap (subrelstr B)) .: X)
by ZFMISC_1:76;
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
;
verum end; hence
idsMap (subrelstr B) preserves_sup_of X
by WAYBEL_0:def 31;
verum end;
hence
idsMap (subrelstr B) is sups-preserving
by WAYBEL_0:def 33; verum