defpred S1[ object , object ] means ex AR being auxiliary Relation of L st
( AR = $2 & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = $1 & x9 in s9 . y9 ) ) ) );
A1:
for a being object st a in the carrier of (MonSet L) holds
ex b being object st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
proof
let a be
object ;
( a in the carrier of (MonSet L) implies ex b being object st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] ) )
assume A2:
a in the
carrier of
(MonSet L)
;
ex b being object st
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
defpred S2[
object ,
object ]
means ex
x9,
y9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
x9 = $1 &
y9 = $2 &
s9 = a &
x9 in s9 . y9 );
consider R being
Relation of the
carrier of
L, the
carrier of
L such that A3:
for
x,
y being
object holds
(
[x,y] in R iff (
x in the
carrier of
L &
y in the
carrier of
L &
S2[
x,
y] ) )
from RELSET_1:sch 1();
reconsider R =
R as
Relation of
L ;
A4:
R is
auxiliary(i)
proof
let x,
y be
Element of
L;
WAYBEL_4:def 3 ( [x,y] in R implies x <= y )
assume
[x,y] in R
;
x <= y
then consider x9,
y9 being
Element of
L,
s9 being
Function of
L,
(InclPoset (Ids L)) such that A5:
x9 = x
and A6:
y9 = y
and A7:
s9 = a
and A8:
x9 in s9 . y9
by A3;
ex
s being
Function of
L,
(InclPoset (Ids L)) st
(
a = s &
s is
monotone & ( for
x being
Element of
L holds
s . x c= downarrow x ) )
by A2, Def13;
then
s9 . y c= downarrow y
by A7;
hence
x <= y
by A5, A6, A8, WAYBEL_0:17;
verum
end;
A9:
R is
auxiliary(ii)
proof
let x,
y,
z,
u be
Element of
L;
WAYBEL_4:def 4 ( u <= x & [x,y] in R & y <= z implies [u,z] in R )
assume that A10:
u <= x
and A11:
[x,y] in R
and A12:
y <= z
;
[u,z] in R
A13:
ex
x9,
y9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
x9 = x &
y9 = y &
s9 = a &
x9 in s9 . y9 )
by A3, A11;
consider s being
Function of
L,
(InclPoset (Ids L)) such that A14:
a = s
and A15:
s is
monotone
and
for
x being
Element of
L holds
s . x c= downarrow x
by A2, Def13;
reconsider sy =
s . y,
sz =
s . z as
Element of
(InclPoset (Ids L)) ;
sy <= sz
by A12, A15;
then A16:
s . y c= s . z
by YELLOW_1:3;
s . z in the
carrier of
(InclPoset (Ids L))
;
then
s . z in Ids L
by YELLOW_1:1;
then consider sz being
Ideal of
L such that A17:
s . z = sz
;
u in sz
by A10, A13, A14, A16, A17, WAYBEL_0:def 19;
hence
[u,z] in R
by A3, A14, A17;
verum
end;
A18:
R is
auxiliary(iii)
proof
let x,
y,
z be
Element of
L;
WAYBEL_4:def 5 ( [x,z] in R & [y,z] in R implies [(x "\/" y),z] in R )
assume that A19:
[x,z] in R
and A20:
[y,z] in R
;
[(x "\/" y),z] in R
consider x1,
z1 being
Element of
L,
s1 being
Function of
L,
(InclPoset (Ids L)) such that A21:
x1 = x
and A22:
z1 = z
and A23:
s1 = a
and A24:
x1 in s1 . z1
by A3, A19;
A25:
ex
y2,
z2 being
Element of
L ex
s2 being
Function of
L,
(InclPoset (Ids L)) st
(
y2 = y &
z2 = z &
s2 = a &
y2 in s2 . z2 )
by A3, A20;
s1 . z in the
carrier of
(InclPoset (Ids L))
;
then
s1 . z in Ids L
by YELLOW_1:1;
then consider sz being
Ideal of
L such that A26:
s1 . z = sz
;
consider z3 being
Element of
L such that A27:
z3 in sz
and A28:
x <= z3
and A29:
y <= z3
by A21, A22, A23, A24, A25, A26, WAYBEL_0:def 1;
ex
q being
Element of
L st
(
x <= q &
y <= q & ( for
c being
Element of
L st
x <= c &
y <= c holds
q <= c ) )
by LATTICE3:def 10;
then
x "\/" y <= z3
by A28, A29, LATTICE3:def 13;
then
x "\/" y in sz
by A27, WAYBEL_0:def 19;
hence
[(x "\/" y),z] in R
by A3, A23, A26;
verum
end;
R is
auxiliary(iv)
then reconsider R =
R as
auxiliary Relation of
L by A4, A9, A18;
A32:
for
x,
y being
object holds
(
[x,y] in R iff ex
x9,
y9 being
Element of
L ex
s9 being
Function of
L,
(InclPoset (Ids L)) st
(
x9 = x &
y9 = y &
s9 = a &
x9 in s9 . y9 ) )
by A3;
take b =
R;
( b in the carrier of (InclPoset (Aux L)) & S1[a,b] )
b in Aux L
by Def8;
hence
(
b in the
carrier of
(InclPoset (Aux L)) &
S1[
a,
b] )
by A32, YELLOW_1:1;
verum
end;
consider f being Function of the carrier of (MonSet L), the carrier of (InclPoset (Aux L)) such that
A33:
for a being object st a in the carrier of (MonSet L) holds
S1[a,f . a]
from FUNCT_2:sch 1(A1);
reconsider f9 = f as Function of (MonSet L),(InclPoset (Aux L)) ;
take
f9
; for s being object st s in the carrier of (MonSet L) holds
ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
let s be object ; ( s in the carrier of (MonSet L) implies ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) ) )
assume A34:
s in the carrier of (MonSet L)
; ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
then reconsider s9 = s as Element of (MonSet L) ;
f9 . s9 in the carrier of (InclPoset (Aux L))
;
then
f9 . s9 in Aux L
by YELLOW_1:1;
then reconsider fs = f9 . s9 as auxiliary Relation of L by Def8;
take
fs
; ( fs = f9 . s & ( for x, y being object holds
( [x,y] in fs iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
ex AR being auxiliary Relation of L st
( AR = f9 . s & ( for x, y being object holds
( [x,y] in AR iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
by A33, A34;
hence
( fs = f9 . s & ( for x, y being object holds
( [x,y] in fs iff ex x9, y9 being Element of L ex s9 being Function of L,(InclPoset (Ids L)) st
( x9 = x & y9 = y & s9 = s & x9 in s9 . y9 ) ) ) )
; verum