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