let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta q,O is u.t.i.
let L be lower-bounded LATTICE; :: thesis: for O being Ordinal
for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta q,O is u.t.i.
let O be Ordinal; :: thesis: for d being BiFunction of A,L st d is symmetric & d is u.t.i. holds
for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta q,O is u.t.i.
let d be BiFunction of A,L; :: thesis: ( d is symmetric & d is u.t.i. implies for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta q,O is u.t.i. )
assume that
A1:
d is symmetric
and
A2:
d is u.t.i.
; :: thesis: for q being QuadrSeq of d st O c= DistEsti d holds
ConsecutiveDelta q,O is u.t.i.
let q be QuadrSeq of d; :: thesis: ( O c= DistEsti d implies ConsecutiveDelta q,O is u.t.i. )
defpred S1[ Ordinal] means ( $1 c= DistEsti d implies ConsecutiveDelta q,$1 is u.t.i. );
A3:
S1[ {} ]
proof
assume
{} c= DistEsti d
;
:: thesis: ConsecutiveDelta q,{} is u.t.i.
let x,
y,
z be
Element of
ConsecutiveSet A,
{} ;
:: according to LATTICE5:def 8 :: thesis: ((ConsecutiveDelta q,{} ) . x,y) "\/" ((ConsecutiveDelta q,{} ) . y,z) >= (ConsecutiveDelta q,{} ) . x,z
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
A by Th24;
A4:
ConsecutiveDelta q,
{} = d
by Th29;
d . x',
z' <= (d . x',y') "\/" (d . y',z')
by A2, Def8;
hence
(ConsecutiveDelta q,{} ) . x,
z <= ((ConsecutiveDelta q,{} ) . x,y) "\/" ((ConsecutiveDelta q,{} ) . y,z)
by A4;
:: thesis: verum
end;
A5:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
:: thesis: ( S1[O1] implies S1[ succ O1] )
assume that A6:
(
O1 c= DistEsti d implies
ConsecutiveDelta q,
O1 is
u.t.i. )
and A7:
succ O1 c= DistEsti d
;
:: thesis: ConsecutiveDelta q,(succ O1) is u.t.i.
A8:
O1 in DistEsti d
by A7, ORDINAL1:33;
A9:
ConsecutiveDelta q,
O1 is
symmetric
by A1, Th37;
let x,
y,
z be
Element of
ConsecutiveSet A,
(succ O1);
:: according to LATTICE5:def 8 :: thesis: ((ConsecutiveDelta q,(succ O1)) . x,y) "\/" ((ConsecutiveDelta q,(succ O1)) . y,z) >= (ConsecutiveDelta q,(succ O1)) . x,z
set f =
new_bi_fun (ConsecutiveDelta q,O1),
(Quadr q,O1);
reconsider x' =
x,
y' =
y,
z' =
z as
Element of
new_set (ConsecutiveSet A,O1) by Th25;
A10:
O1 in dom q
by A8, Th28;
then
q . O1 in rng q
by FUNCT_1:def 5;
then
q . O1 in { [u,v,a',b'] where u, v is Element of A, a', b' is Element of L : d . u,v <= a' "\/" b' }
by Def14;
then consider u,
v being
Element of
A,
a',
b' being
Element of
L such that A11:
(
q . O1 = [u,v,a',b'] &
d . u,
v <= a' "\/" b' )
;
set X =
(Quadr q,O1) `1 ;
set Y =
(Quadr q,O1) `2 ;
reconsider a =
(Quadr q,O1) `3 ,
b =
(Quadr q,O1) `4 as
Element of
L ;
A12:
Quadr q,
O1 = [u,v,a',b']
by A10, A11, Def15;
then A13:
u = (Quadr q,O1) `1
by MCART_1:def 8;
A14:
v = (Quadr q,O1) `2
by A12, MCART_1:def 9;
A15:
a' = a
by A12, MCART_1:def 10;
A16:
b' = b
by A12, MCART_1:def 11;
A17:
dom d = [:A,A:]
by FUNCT_2:def 1;
A18:
d c= ConsecutiveDelta q,
O1
by Th34;
d . u,
v =
d . [u,v]
.=
(ConsecutiveDelta q,O1) . ((Quadr q,O1) `1 ),
((Quadr q,O1) `2 )
by A13, A14, A17, A18, GRFUNC_1:8
;
then A19:
new_bi_fun (ConsecutiveDelta q,O1),
(Quadr q,O1) is
u.t.i.
by A6, A8, A9, A11, A15, A16, Th20, ORDINAL1:def 2;
A20:
ConsecutiveDelta q,
(succ O1) =
new_bi_fun (BiFun (ConsecutiveDelta q,O1),(ConsecutiveSet A,O1),L),
(Quadr q,O1)
by Th30
.=
new_bi_fun (ConsecutiveDelta q,O1),
(Quadr q,O1)
by Def16
;
(new_bi_fun (ConsecutiveDelta q,O1),(Quadr q,O1)) . x',
z' <= ((new_bi_fun (ConsecutiveDelta q,O1),(Quadr q,O1)) . x',y') "\/" ((new_bi_fun (ConsecutiveDelta q,O1),(Quadr q,O1)) . y',z')
by A19, Def8;
hence
(ConsecutiveDelta q,(succ O1)) . x,
z <= ((ConsecutiveDelta q,(succ O1)) . x,y) "\/" ((ConsecutiveDelta q,(succ O1)) . y,z)
by A20;
:: thesis: verum
end;
A21:
for O2 being Ordinal st O2 <> {} & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) holds
S1[O2]
proof
let O2 be
Ordinal;
:: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O1 being Ordinal st O1 in O2 holds
S1[O1] ) implies S1[O2] )
assume that A22:
(
O2 <> {} &
O2 is
limit_ordinal & ( for
O1 being
Ordinal st
O1 in O2 &
O1 c= DistEsti d holds
ConsecutiveDelta q,
O1 is
u.t.i. ) )
and A23:
O2 c= DistEsti d
;
:: thesis: ConsecutiveDelta q,O2 is u.t.i.
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet A,$1),
L =
ConsecutiveDelta q,$1;
consider Ls being
T-Sequence such that A24:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
A25:
ConsecutiveDelta q,
O2 = union (rng Ls)
by A22, A24, Th31;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet A,$1;
consider Ts being
T-Sequence such that A26:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
O1) ) )
from ORDINAL2:sch 2();
A27:
ConsecutiveSet A,
O2 = union (rng Ts)
by A22, A26, Th26;
set CS =
ConsecutiveSet A,
O2;
reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet A,O2),
L by A25;
f is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet A,
O2;
:: according to LATTICE5:def 8 :: thesis: (f . x,y) "\/" (f . y,z) >= f . x,z
consider X being
set such that A28:
(
x in X &
X in rng Ts )
by A27, TARSKI:def 4;
consider o1 being
set such that A29:
(
o1 in dom Ts &
X = Ts . o1 )
by A28, FUNCT_1:def 5;
consider Y being
set such that A30:
(
y in Y &
Y in rng Ts )
by A27, TARSKI:def 4;
consider o2 being
set such that A31:
(
o2 in dom Ts &
Y = Ts . o2 )
by A30, FUNCT_1:def 5;
consider Z being
set such that A32:
(
z in Z &
Z in rng Ts )
by A27, TARSKI:def 4;
consider o3 being
set such that A33:
(
o3 in dom Ts &
Z = Ts . o3 )
by A32, FUNCT_1:def 5;
reconsider o1 =
o1,
o2 =
o2,
o3 =
o3 as
Ordinal by A29, A31, A33;
A34:
x in ConsecutiveSet A,
o1
by A26, A28, A29;
A35:
y in ConsecutiveSet A,
o2
by A26, A30, A31;
A36:
z in ConsecutiveSet A,
o3
by A26, A32, A33;
A37:
Ls . o1 = ConsecutiveDelta q,
o1
by A24, A26, A29;
then reconsider h1 =
Ls . o1 as
BiFunction of
(ConsecutiveSet A,o1),
L ;
A38:
h1 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet A,
o1;
:: according to LATTICE5:def 8 :: thesis: (h1 . x,y) "\/" (h1 . y,z) >= h1 . x,z
A39:
ConsecutiveDelta q,
o1 = h1
by A24, A26, A29;
o1 c= DistEsti d
by A23, A26, A29, ORDINAL1:def 2;
then
ConsecutiveDelta q,
o1 is
u.t.i.
by A22, A26, A29;
hence
h1 . x,
z <= (h1 . x,y) "\/" (h1 . y,z)
by A39, Def8;
:: thesis: verum
end;
A40:
dom h1 = [:(ConsecutiveSet A,o1),(ConsecutiveSet A,o1):]
by FUNCT_2:def 1;
A41:
Ls . o2 = ConsecutiveDelta q,
o2
by A24, A26, A31;
then reconsider h2 =
Ls . o2 as
BiFunction of
(ConsecutiveSet A,o2),
L ;
A42:
h2 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet A,
o2;
:: according to LATTICE5:def 8 :: thesis: (h2 . x,y) "\/" (h2 . y,z) >= h2 . x,z
A43:
ConsecutiveDelta q,
o2 = h2
by A24, A26, A31;
o2 c= DistEsti d
by A23, A26, A31, ORDINAL1:def 2;
then
ConsecutiveDelta q,
o2 is
u.t.i.
by A22, A26, A31;
hence
h2 . x,
z <= (h2 . x,y) "\/" (h2 . y,z)
by A43, Def8;
:: thesis: verum
end;
A44:
dom h2 = [:(ConsecutiveSet A,o2),(ConsecutiveSet A,o2):]
by FUNCT_2:def 1;
A45:
Ls . o3 = ConsecutiveDelta q,
o3
by A24, A26, A33;
then reconsider h3 =
Ls . o3 as
BiFunction of
(ConsecutiveSet A,o3),
L ;
A46:
h3 is
u.t.i.
proof
let x,
y,
z be
Element of
ConsecutiveSet A,
o3;
:: according to LATTICE5:def 8 :: thesis: (h3 . x,y) "\/" (h3 . y,z) >= h3 . x,z
A47:
ConsecutiveDelta q,
o3 = h3
by A24, A26, A33;
o3 c= DistEsti d
by A23, A26, A33, ORDINAL1:def 2;
then
ConsecutiveDelta q,
o3 is
u.t.i.
by A22, A26, A33;
hence
h3 . x,
z <= (h3 . x,y) "\/" (h3 . y,z)
by A47, Def8;
:: thesis: verum
end;
A48:
dom h3 = [:(ConsecutiveSet A,o3),(ConsecutiveSet A,o3):]
by FUNCT_2:def 1;
per cases
( o1 c= o3 or o3 c= o1 )
;
suppose A49:
o1 c= o3
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A50:
ConsecutiveSet A,
o1 c= ConsecutiveSet A,
o3
by Th32;
thus
(f . x,y) "\/" (f . y,z) >= f . x,
z
:: thesis: verumproof
per cases
( o2 c= o3 or o3 c= o2 )
;
suppose
o2 c= o3
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A51:
ConsecutiveSet A,
o2 c= ConsecutiveSet A,
o3
by Th32;
then reconsider y' =
y as
Element of
ConsecutiveSet A,
o3 by A35;
reconsider x' =
x as
Element of
ConsecutiveSet A,
o3 by A34, A50;
reconsider z' =
z as
Element of
ConsecutiveSet A,
o3 by A26, A32, A33;
ConsecutiveDelta q,
o3 in rng Ls
by A24, A26, A33, A45, FUNCT_1:def 5;
then A52:
h3 c= f
by A45, ZFMISC_1:92;
A53:
[x,y] in dom h3
by A34, A35, A48, A50, A51, ZFMISC_1:106;
A54:
[y,z] in dom h3
by A35, A36, A48, A51, ZFMISC_1:106;
A55:
[x,z] in dom h3
by A34, A36, A48, A50, ZFMISC_1:106;
A56:
f . x,
y = h3 . x',
y'
by A52, A53, GRFUNC_1:8;
A57:
f . y,
z = h3 . y',
z'
by A52, A54, GRFUNC_1:8;
f . x,
z = h3 . x',
z'
by A52, A55, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A46, A56, A57, Def8;
:: thesis: verum end; suppose
o3 c= o2
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A58:
ConsecutiveSet A,
o3 c= ConsecutiveSet A,
o2
by Th32;
then reconsider z' =
z as
Element of
ConsecutiveSet A,
o2 by A36;
ConsecutiveSet A,
o1 c= ConsecutiveSet A,
o3
by A49, Th32;
then A59:
ConsecutiveSet A,
o1 c= ConsecutiveSet A,
o2
by A58, XBOOLE_1:1;
then reconsider x' =
x as
Element of
ConsecutiveSet A,
o2 by A34;
reconsider y' =
y as
Element of
ConsecutiveSet A,
o2 by A26, A30, A31;
ConsecutiveDelta q,
o2 in rng Ls
by A24, A26, A31, A41, FUNCT_1:def 5;
then A60:
h2 c= f
by A41, ZFMISC_1:92;
A61:
[x,y] in dom h2
by A34, A35, A44, A59, ZFMISC_1:106;
A62:
[y,z] in dom h2
by A35, A36, A44, A58, ZFMISC_1:106;
A63:
[x,z] in dom h2
by A34, A36, A44, A58, A59, ZFMISC_1:106;
A64:
f . x,
y = h2 . x',
y'
by A60, A61, GRFUNC_1:8;
A65:
f . y,
z = h2 . y',
z'
by A60, A62, GRFUNC_1:8;
f . x,
z = h2 . x',
z'
by A60, A63, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A42, A64, A65, Def8;
:: thesis: verum end;
end; end; suppose A66:
o3 c= o1
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A67:
ConsecutiveSet A,
o3 c= ConsecutiveSet A,
o1
by Th32;
thus
(f . x,y) "\/" (f . y,z) >= f . x,
z
:: thesis: verumproof
per cases
( o1 c= o2 or o2 c= o1 )
;
suppose
o1 c= o2
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A68:
ConsecutiveSet A,
o1 c= ConsecutiveSet A,
o2
by Th32;
then reconsider x' =
x as
Element of
ConsecutiveSet A,
o2 by A34;
ConsecutiveSet A,
o3 c= ConsecutiveSet A,
o1
by A66, Th32;
then A69:
ConsecutiveSet A,
o3 c= ConsecutiveSet A,
o2
by A68, XBOOLE_1:1;
then reconsider z' =
z as
Element of
ConsecutiveSet A,
o2 by A36;
reconsider y' =
y as
Element of
ConsecutiveSet A,
o2 by A26, A30, A31;
ConsecutiveDelta q,
o2 in rng Ls
by A24, A26, A31, A41, FUNCT_1:def 5;
then A70:
h2 c= f
by A41, ZFMISC_1:92;
A71:
[x,y] in dom h2
by A34, A35, A44, A68, ZFMISC_1:106;
A72:
[y,z] in dom h2
by A35, A36, A44, A69, ZFMISC_1:106;
A73:
[x,z] in dom h2
by A34, A36, A44, A68, A69, ZFMISC_1:106;
A74:
f . x,
y = h2 . x',
y'
by A70, A71, GRFUNC_1:8;
A75:
f . y,
z = h2 . y',
z'
by A70, A72, GRFUNC_1:8;
f . x,
z = h2 . x',
z'
by A70, A73, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A42, A74, A75, Def8;
:: thesis: verum end; suppose
o2 c= o1
;
:: thesis: (f . x,y) "\/" (f . y,z) >= f . x,zthen A76:
ConsecutiveSet A,
o2 c= ConsecutiveSet A,
o1
by Th32;
then reconsider y' =
y as
Element of
ConsecutiveSet A,
o1 by A35;
reconsider z' =
z as
Element of
ConsecutiveSet A,
o1 by A36, A67;
reconsider x' =
x as
Element of
ConsecutiveSet A,
o1 by A26, A28, A29;
ConsecutiveDelta q,
o1 in rng Ls
by A24, A26, A29, A37, FUNCT_1:def 5;
then A77:
h1 c= f
by A37, ZFMISC_1:92;
A78:
[x,y] in dom h1
by A34, A35, A40, A76, ZFMISC_1:106;
A79:
[y,z] in dom h1
by A35, A36, A40, A67, A76, ZFMISC_1:106;
A80:
[x,z] in dom h1
by A34, A36, A40, A67, ZFMISC_1:106;
A81:
f . x,
y = h1 . x',
y'
by A77, A78, GRFUNC_1:8;
A82:
f . y,
z = h1 . y',
z'
by A77, A79, GRFUNC_1:8;
f . x,
z = h1 . x',
z'
by A77, A80, GRFUNC_1:8;
hence
(f . x,y) "\/" (f . y,z) >= f . x,
z
by A38, A81, A82, Def8;
:: thesis: verum end;
end; end;
end;
hence
ConsecutiveDelta q,
O2 is
u.t.i.
by A22, A24, Th31;
:: thesis: verum
end;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A3, A5, A21);
hence
( O c= DistEsti d implies ConsecutiveDelta q,O is u.t.i. )
; :: thesis: verum