let L be lower-bounded sup-Semilattice; :: thesis: Map2Rel L is monotone
set f = Map2Rel L;
A1:
InclPoset (Aux L) = RelStr(# (Aux L),(RelIncl (Aux L)) #)
by YELLOW_1:def 1;
let x, y be Element of (MonSet L); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 ) )
assume
x <= y
; :: thesis: for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 )
then
[x,y] in the InternalRel of (MonSet L)
by ORDERS_2:def 9;
then consider s, t being Function of L,(InclPoset (Ids L)) such that
A2:
x = s
and
A3:
y = t
and
x in the carrier of (MonSet L)
and
y in the carrier of (MonSet L)
and
A4:
s <= t
by Def14;
A5:
(Map2Rel L) . s in the carrier of (InclPoset (Aux L))
by A2, FUNCT_2:7;
A6:
(Map2Rel L) . t in the carrier of (InclPoset (Aux L))
by A3, FUNCT_2:7;
A7:
(Map2Rel L) . s in Aux L
by A5, YELLOW_1:1;
A8:
(Map2Rel L) . t in Aux L
by A6, YELLOW_1:1;
then reconsider AS = (Map2Rel L) . s, AT = (Map2Rel L) . t as auxiliary Relation of L by A7, Def9;
reconsider AS' = AS, AT' = AT as Element of (InclPoset (Aux L)) by A2, A3, FUNCT_2:7;
for a, b being set st [a,b] in AS holds
[a,b] in AT
proof
let a,
b be
set ;
:: thesis: ( [a,b] in AS implies [a,b] in AT )
assume A9:
[a,b] in AS
;
:: thesis: [a,b] in AT
then A10:
b in the
carrier of
L
by ZFMISC_1:106;
reconsider a' =
a,
b' =
b as
Element of
L by A9, ZFMISC_1:106;
reconsider sb =
s . b',
tb =
t . b' as
Element of
(InclPoset (Ids L)) ;
ex
a1,
b1 being
Element of
(InclPoset (Ids L)) st
(
a1 = s . b &
b1 = t . b &
a1 <= b1 )
by A4, A10, YELLOW_2:def 1;
then A11:
sb c= tb
by YELLOW_1:3;
ex
AR being
auxiliary Relation of
L st
(
AR = (Map2Rel L) . x & ( for
a',
b' being
set holds
(
[a',b'] in AR iff ex
x',
y' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = a' &
y' = b' &
s' = x &
x' in s' . y' ) ) ) )
by Def16;
then A12:
ex
x',
y' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = a' &
y' = b' &
s' = s &
x' in s' . y' )
by A2, A9;
ex
AR1 being
auxiliary Relation of
L st
(
AR1 = (Map2Rel L) . y & ( for
a',
b' being
set holds
(
[a',b'] in AR1 iff ex
x',
y' being
Element of
L ex
s' being
Function of
L,
(InclPoset (Ids L)) st
(
x' = a' &
y' = b' &
s' = y &
x' in s' . y' ) ) ) )
by Def16;
hence
[a,b] in AT
by A3, A11, A12;
:: thesis: verum
end;
then
AS' c= AT'
by RELAT_1:def 3;
then
[AS',AT'] in RelIncl (Aux L)
by A7, A8, WELLORD2:def 1;
hence
for b1, b2 being Element of the carrier of (InclPoset (Aux L)) holds
( not b1 = (Map2Rel L) . x or not b2 = (Map2Rel L) . y or b1 <= b2 )
by A1, A2, A3, ORDERS_2:def 9; :: thesis: verum