let L be lower-bounded sup-Semilattice; :: thesis: (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)
by FUNCT_1:34;
for a being set 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
set ;
:: thesis: ( 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)
;
:: thesis: ((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 &
s is
monotone & ( for
x being
Element of
L holds
s . x c= downarrow x ) )
by Def14;
((Rel2Map L) * (Map2Rel L)) . s in the
carrier of
(MonSet L)
by A3, A4, FUNCT_2:7;
then consider Ls being
Function of
L,
(InclPoset (Ids L)) such that A5:
(
((Rel2Map L) * (Map2Rel L)) . s = Ls &
Ls is
monotone & ( for
x being
Element of
L holds
Ls . x c= downarrow x ) )
by Def14;
set AR =
(Map2Rel L) . s;
(Map2Rel L) . s in the
carrier of
(InclPoset (Aux L))
by A3, A4, FUNCT_2:7;
then
(Map2Rel L) . s in Aux L
by YELLOW_1:1;
then reconsider AR =
(Map2Rel L) . s as
auxiliary Relation of
L by Def9;
dom (Map2Rel L) = the
carrier of
(MonSet L)
by FUNCT_2:def 1;
then
Ls = (Rel2Map L) . AR
by A3, A4, A5, FUNCT_1:23;
then A6:
Ls = AR -below
by Def15;
Ls = s
proof
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 let b be
set ;
:: thesis: ( b in the carrier of L implies Ls . b = s . b )assume A9:
b in the
carrier of
L
;
:: thesis: Ls . b = s . bthen reconsider b' =
b as
Element of
L ;
thus
Ls . b = s . b
:: thesis: verumproof
thus
Ls . b c= s . b
:: according to XBOOLE_0:def 10 :: thesis: s . b c= Ls . bproof
let d be
set ;
:: according to TARSKI:def 3 :: thesis: ( not d in Ls . b or d in s . b )
assume
d in Ls . b
;
:: thesis: d in s . b
then
d in AR -below b'
by A6, Def13;
then A10:
[d,b'] in AR
by Th13;
consider AR' being
auxiliary Relation of
L such that A11:
(
AR' = (Map2Rel L) . s & ( for
d,
b' being
set holds
(
[d,b'] in AR' iff ex
d',
b'' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
d' = d &
b'' = b' &
s' = s &
d' in s' . b'' ) ) ) )
by A3, A4, Def16;
consider d',
b'' being
Element of
L,
s' being
Function of
L,
(InclPoset (Ids L)) such that A12:
(
d' = d &
b'' = b' &
s' = s &
d' in s' . b'' )
by A10, A11;
thus
d in s . b
by A12;
:: thesis: verum
end;
thus
s . b c= Ls . b
:: thesis: verumproof
let d be
set ;
:: according to TARSKI:def 3 :: thesis: ( not d in s . b or d in Ls . b )
assume A13:
d in s . b
;
:: thesis: d in Ls . b
s . b in the
carrier of
(InclPoset (Ids L))
by A9, FUNCT_2:7;
then
s . b in Ids L
by YELLOW_1:1;
then consider X being
Ideal of
L such that A14:
s . b = X
;
reconsider d' =
d as
Element of
L by A13, A14;
consider AR' being
auxiliary Relation of
L such that A15:
(
AR' = (Map2Rel L) . s & ( for
d,
b' being
set holds
(
[d,b'] in AR' iff ex
d',
b'' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
d' = d &
b'' = b' &
s' = s &
d' in s' . b'' ) ) ) )
by A3, A4, Def16;
[d',b'] in AR
by A13, A15;
then
d' in AR -below b'
;
hence
d in Ls . b
by A6, Def13;
:: thesis: verum
end;
end; end;
hence
Ls = s
by A7, A8, FUNCT_1:9;
:: thesis: verum
end;
hence
((Rel2Map L) * (Map2Rel L)) . a = (id the carrier of (MonSet L)) . a
by A3, A4, A5, FUNCT_1:35;
:: thesis: verum
end;
hence
(Rel2Map L) * (Map2Rel L) = id the carrier of (MonSet L)
by A1, A2, FUNCT_1:9; :: thesis: verum