let L be lower-bounded sup-Semilattice; :: thesis: (Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
set LS = (Map2Rel L) * (Rel2Map L);
set R = id (dom (Rel2Map L));
dom ((Map2Rel L) * (Rel2Map L)) = the carrier of (InclPoset (Aux L))
by FUNCT_2:def 1;
then A1:
dom ((Map2Rel L) * (Rel2Map L)) = Aux L
by YELLOW_1:1;
dom (id (dom (Rel2Map L))) = dom (Rel2Map L)
by FUNCT_1:34;
then
dom (id (dom (Rel2Map L))) = the carrier of (InclPoset (Aux L))
by FUNCT_2:def 1;
then A2:
dom (id (dom (Rel2Map L))) = Aux L
by YELLOW_1:1;
for a being set st a in Aux L holds
((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
proof
let a be
set ;
:: thesis: ( a in Aux L implies ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a )
assume A3:
a in Aux L
;
:: thesis: ((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
then reconsider AR =
a as
auxiliary Relation of
L by Def9;
A4:
a in the
carrier of
(InclPoset (Aux L))
by A3, YELLOW_1:1;
then A5:
a in dom (Rel2Map L)
by FUNCT_2:def 1;
then
((Map2Rel L) * (Rel2Map L)) . a = (Map2Rel L) . ((Rel2Map L) . AR)
by FUNCT_1:23;
then A6:
((Map2Rel L) * (Rel2Map L)) . a = (Map2Rel L) . (AR -below )
by Def15;
((Map2Rel L) * (Rel2Map L)) . a in the
carrier of
(InclPoset (Aux L))
by A4, FUNCT_2:7;
then
((Map2Rel L) * (Rel2Map L)) . a in Aux L
by YELLOW_1:1;
then reconsider La =
((Map2Rel L) * (Rel2Map L)) . a as
auxiliary Relation of
L by Def9;
A7:
AR -below in the
carrier of
(MonSet L)
by Th18;
La = AR
proof
for
c,
b being
set holds
(
[c,b] in La iff
[c,b] in AR )
proof
let c,
b be
set ;
:: thesis: ( [c,b] in La iff [c,b] in AR )
hereby :: thesis: ( [c,b] in AR implies [c,b] in La )
assume A8:
[c,b] in La
;
:: thesis: [c,b] in ARconsider AR' being
auxiliary Relation of
L such that A9:
(
AR' = (Map2Rel L) . (AR -below ) & ( for
c,
b being
set holds
(
[c,b] in AR' iff ex
c',
b' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
c' = c &
b' = b &
s' = AR -below &
c' in s' . b' ) ) ) )
by A7, Def16;
consider c',
b' being
Element of
L,
s' being
Function of
L,
(InclPoset (Ids L)) such that A10:
(
c' = c &
b' = b &
s' = AR -below &
c' in s' . b' )
by A6, A8, A9;
c' in AR -below b'
by A10, Def13;
hence
[c,b] in AR
by A10, Th13;
:: thesis: verum
end;
assume A11:
[c,b] in AR
;
:: thesis: [c,b] in La
then reconsider c' =
c,
b' =
b as
Element of
L by ZFMISC_1:106;
c' in AR -below b'
by A11;
then A12:
c' in (AR -below ) . b'
by Def13;
consider AR' being
auxiliary Relation of
L such that A13:
(
AR' = (Map2Rel L) . (AR -below ) & ( for
c,
b being
set holds
(
[c,b] in AR' iff ex
c',
b' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
c' = c &
b' = b &
s' = AR -below &
c' in s' . b' ) ) ) )
by A7, Def16;
thus
[c,b] in La
by A6, A12, A13;
:: thesis: verum
end;
hence
La = AR
by RELAT_1:def 2;
:: thesis: verum
end;
hence
((Map2Rel L) * (Rel2Map L)) . a = (id (dom (Rel2Map L))) . a
by A5, FUNCT_1:35;
:: thesis: verum
end;
hence
(Map2Rel L) * (Rel2Map L) = id (dom (Rel2Map L))
by A1, A2, FUNCT_1:9; :: thesis: verum