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
A1:
Bottom L in B
by Def8;
then A2:
Bottom L in the carrier of (subrelstr B)
by YELLOW_0:def 15;
A3:
subrelstr B is join-inheriting
by Def2;
set f = idsMap (subrelstr B);
now let X be
Subset of
(InclPoset (Ids (subrelstr B)));
:: thesis: idsMap (subrelstr B) preserves_sup_of Xreconsider supX =
sup X as
Ideal of
(subrelstr B) by YELLOW_2:43;
reconsider unionX =
union X as
Subset of
L by WAYBEL13:3;
consider J being
Subset of
L such that A4:
supX = J
and A5:
(idsMap (subrelstr B)) . supX = downarrow J
by Def11;
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;
now assume
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)A6:
downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) c= downarrow dfuX
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in downarrow (finsups (union ((idsMap (subrelstr B)) .: X))) or x in downarrow dfuX )
assume A7:
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 A8:
y1 >= x1
and A9:
y1 in finsups (union ((idsMap (subrelstr B)) .: X))
by A7, 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 A9, WAYBEL_0:def 27;
then consider Y being
finite Subset of
(union ((idsMap (subrelstr B)) .: X)) such that A10:
y1 = "\/" Y,
L
and
ex_sup_of Y,
L
;
defpred S1[
set ,
set ]
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 );
A11:
for
z being
set st
z in Y holds
ex
v being
Element of
B st
S1[
z,
v]
proof
let z be
set ;
:: thesis: ( z in Y implies ex v being Element of B st S1[z,v] )
assume
z in Y
;
:: thesis: ex v being Element of B st S1[z,v]
then consider J being
set such that A12:
z in J
and A13:
J in (idsMap (subrelstr B)) .: X
by TARSKI:def 4;
consider I being
set such that
I in dom (idsMap (subrelstr B))
and A14:
I in X
and A15:
J = (idsMap (subrelstr B)) . I
by A13, FUNCT_1:def 12;
reconsider I =
I as
Element of
(InclPoset (Ids (subrelstr B))) by A14;
reconsider I1 =
I as
Ideal of
(subrelstr B) by YELLOW_2:43;
(idsMap (subrelstr B)) . I is
Element of
(InclPoset (Ids L))
;
then reconsider J =
J as
Element of
(InclPoset (Ids L)) by A15;
J is
Ideal of
L
by YELLOW_2:43;
then reconsider z1 =
z as
Element of
L by A12;
consider I2 being
Subset of
L such that A16:
I1 = I2
and A17:
(idsMap (subrelstr B)) . I1 = downarrow I2
by Def11;
consider z2 being
Element of
L such that A18:
z2 >= z1
and A19:
z2 in I2
by A12, A15, A17, WAYBEL_0:def 15;
reconsider v =
z2 as
Element of
B by A16, A19, YELLOW_0:def 15;
take
v
;
:: thesis: S1[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 A14, A16, A18, A19;
:: thesis: verum
end;
consider g being
Function of
Y,
B such that A20:
for
z being
set st
z in Y holds
S1[
z,
g . z]
from MONOID_1:sch 1(A11);
reconsider srg =
"\/" (rng g),
(subrelstr B) as
Element of
L by YELLOW_0:59;
A21:
dom g = Y
by FUNCT_2:def 1;
reconsider Z =
rng g as
finite Subset of
(subrelstr B) by YELLOW_0:def 15;
A22:
ex_sup_of Z,
subrelstr B
A23:
ex_sup_of Z,
L
by YELLOW_0:17;
"\/" Z,
L in the
carrier of
(subrelstr B)
then reconsider xl =
"\/" Z,
L as
Element of
(subrelstr B) ;
A24:
(
"\/" Z,
L is_>=_than Z & ( for
b being
Element of
L st
b is_>=_than Z holds
"\/" Z,
L <= b ) )
by A23, YELLOW_0:30;
A25:
xl is_>=_than Z
then A28:
"\/" Z,
(subrelstr B) = "\/" Z,
L
by A25, YELLOW_0:30;
"\/" (rng g),
L is_>=_than Y
proof
let a be
Element of
L;
:: according to LATTICE3:def 9 :: thesis: ( not a in Y or a <= "\/" (rng g),L )
assume A29:
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 A30:
a1 = a
and A31:
a2 = g . a
and
I in X
and
g . a in I
and A32:
a1 <= a2
by A20;
A33:
g . a in rng g
by A21, A29, FUNCT_1:def 5;
"\/" (rng g),
L is_>=_than rng g
by YELLOW_0:32;
then
a2 <= "\/" (rng g),
L
by A31, A33, LATTICE3:def 9;
hence
a <= "\/" (rng g),
L
by A30, A32, YELLOW_0:def 2;
:: thesis: verum
end;
then
"\/" Y,
L <= srg
by A28, YELLOW_0:32;
then A34:
x1 <= srg
by A8, A10, YELLOW_0:def 2;
A35:
finsups (union X) c= downarrow (finsups (union X))
by WAYBEL_0:16;
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 A22;
then
"\/" (rng g),
(subrelstr B) in finsups (union X)
by WAYBEL_0:def 27;
hence
x in downarrow dfuX
by A34, A35, WAYBEL_0:def 15;
:: thesis: verum
end; then
union X c= union ((idsMap (subrelstr B)) .: X)
by ZFMISC_1:94;
then A46:
finsups unionX c= finsups (union ((idsMap (subrelstr B)) .: X))
by Th2;
finsups (union X) c= finsups unionX
by A2, A3, Th5;
then
finsups (union X) c= finsups (union ((idsMap (subrelstr B)) .: X))
by A46, XBOOLE_1:1;
then A47:
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 A47, XBOOLE_1:1;
then
downarrow dfuX c= downarrow (downarrow (finsups (union ((idsMap (subrelstr B)) .: X))))
by YELLOW_3:6;
then A48:
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 A6, A48, XBOOLE_0:def 10
.=
(idsMap (subrelstr B)) . (sup X)
by A4, A5, Th6
;
:: thesis: verum end; hence
idsMap (subrelstr B) preserves_sup_of X
by WAYBEL_0:def 31;
:: thesis: verum end;
hence
idsMap (subrelstr B) is sups-preserving
by WAYBEL_0:def 33; :: thesis: verum