let L be lower-bounded sup-Semilattice; (Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)
set LS = (Rel2Map L) * (Map2Rel L);
set R = id the carrier of (MonSet L);
A1:
dom ((Rel2Map L) * (Map2Rel L)) = the carrier of (MonSet L)
by FUNCT_2:def 1;
A2:
dom (id the carrier of (MonSet L)) = the carrier of (MonSet L)
;
for a being object st a in the carrier of (MonSet L) holds
((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
proof
let a be
object ;
( a in the carrier of (MonSet L) implies ((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a )
assume A3:
a in the
carrier of
(MonSet L)
;
((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
then consider s being
Function of
L,
(InclPoset (Ids L)) such that A4:
a = s
and
s is
monotone
and
for
x being
Element of
L holds
s . x c= downarrow x
by Def13;
((Rel2Map L) * (Map2Rel L)) . s in the
carrier of
(MonSet L)
by A3, A4, FUNCT_2:5;
then consider Ls being
Function of
L,
(InclPoset (Ids L)) such that A5:
((Rel2Map L) * (Map2Rel L)) . s = Ls
and
Ls is
monotone
and
for
x being
Element of
L holds
Ls . x c= downarrow x
by Def13;
set AR =
(Map2Rel L) . s;
(Map2Rel L) . s in the
carrier of
(InclPoset (Aux L))
by A3, A4, FUNCT_2:5;
then
(Map2Rel L) . s in Aux L
by YELLOW_1:1;
then reconsider AR =
(Map2Rel L) . s as
auxiliary Relation of
L by Def8;
dom (Map2Rel L) = the
carrier of
(MonSet L)
by FUNCT_2:def 1;
then
Ls = (Rel2Map L) . AR
by A3, A4, A5, FUNCT_1:13;
then A6:
Ls = AR -below
by Def14;
A7:
dom Ls = the
carrier of
L
by FUNCT_2:def 1;
A8:
dom s = the
carrier of
L
by FUNCT_2:def 1;
now for b being object st b in the carrier of L holds
Ls . b = s . blet b be
object ;
( b in the carrier of L implies Ls . b = s . b )assume A9:
b in the
carrier of
L
;
Ls . b = s . bthen reconsider b9 =
b as
Element of
L ;
A10:
Ls . b c= s . b
proof
let d be
object ;
TARSKI:def 3 ( not d in Ls . b or d in s . b )
assume
d in Ls . b
;
d in s . b
then
d in AR -below b9
by A6, Def12;
then A11:
[d,b9] in AR
by Th13;
ex
AR9 being
auxiliary Relation of
L st
(
AR9 = (Map2Rel L) . s & ( for
d,
b9 being
object holds
(
[d,b9] in AR9 iff ex
d9,
b99 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
d9 = d &
b99 = b9 &
s9 = s &
d9 in s9 . b99 ) ) ) )
by A3, A4, Def15;
then
ex
d9,
b99 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
d9 = d &
b99 = b9 &
s9 = s &
d9 in s9 . b99 )
by A11;
hence
d in s . b
;
verum
end;
s . b c= Ls . b
hence
Ls . b = s . b
by A10;
verum end;
then
Ls = s
by A7, A8, FUNCT_1:2;
hence
((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
by A3, A4, A5, FUNCT_1:18;
verum
end;
hence
(Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)
by A1, A2, FUNCT_1:2; verum