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