let A be non empty set ; for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
let L be lower-bounded LATTICE; for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
let O be Ordinal; for d being BiFunction of A,L
for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
let d be BiFunction of A,L; for q being QuadrSeq of d holds ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
let q be QuadrSeq of d; ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
defpred S1[ Ordinal] means ConsecutiveDelta (q,$1) is BiFunction of (ConsecutiveSet (A,$1)),L;
A1:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
( S1[O1] implies S1[ succ O1] )
assume
ConsecutiveDelta (
q,
O1) is
BiFunction of
(ConsecutiveSet (A,O1)),
L
;
S1[ succ O1]
then reconsider CD =
ConsecutiveDelta (
q,
O1) as
BiFunction of
(ConsecutiveSet (A,O1)),
L ;
A2:
ConsecutiveSet (
A,
(succ O1))
= new_set (ConsecutiveSet (A,O1))
by Th22;
ConsecutiveDelta (
q,
(succ O1)) =
new_bi_fun (
(BiFun ((ConsecutiveDelta (q,O1)),(ConsecutiveSet (A,O1)),L)),
(Quadr (q,O1)))
by Th27
.=
new_bi_fun (
CD,
(Quadr (q,O1)))
by Def15
;
hence
S1[
succ O1]
by A2;
verum
end;
A3:
for O1 being Ordinal st O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) holds
S1[O1]
proof
deffunc H1(
Ordinal)
-> set =
ConsecutiveDelta (
q,$1);
let O1 be
Ordinal;
( O1 <> 0 & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S1[O2] ) implies S1[O1] )
assume that A4:
O1 <> 0
and A5:
O1 is
limit_ordinal
and A6:
for
O2 being
Ordinal st
O2 in O1 holds
ConsecutiveDelta (
q,
O2) is
BiFunction of
(ConsecutiveSet (A,O2)),
L
;
S1[O1]
consider Ls being
Sequence such that A7:
(
dom Ls = O1 & ( for
O2 being
Ordinal st
O2 in O1 holds
Ls . O2 = H1(
O2) ) )
from ORDINAL2:sch 2();
A8:
for
O,
O2 being
Ordinal st
O c= O2 &
O2 in dom Ls holds
Ls . O c= Ls . O2
proof
let O be
Ordinal;
for O2 being Ordinal st O c= O2 & O2 in dom Ls holds
Ls . O c= Ls . O2
defpred S2[
Ordinal]
means (
O c= $1 & $1
in dom Ls implies
Ls . O c= Ls . $1 );
A9:
for
O2 being
Ordinal st
O2 <> 0 &
O2 is
limit_ordinal & ( for
O3 being
Ordinal st
O3 in O2 holds
S2[
O3] ) holds
S2[
O2]
A17:
for
O2 being
Ordinal st
S2[
O2] holds
S2[
succ O2]
proof
let O2 be
Ordinal;
( S2[O2] implies S2[ succ O2] )
assume A18:
(
O c= O2 &
O2 in dom Ls implies
Ls . O c= Ls . O2 )
;
S2[ succ O2]
assume that A19:
O c= succ O2
and A20:
succ O2 in dom Ls
;
Ls . O c= Ls . (succ O2)
per cases
( O = succ O2 or O <> succ O2 )
;
suppose
O <> succ O2
;
Ls . O c= Ls . (succ O2)then
O c< succ O2
by A19;
then A21:
O in succ O2
by ORDINAL1:11;
A22:
O2 in succ O2
by ORDINAL1:6;
then
O2 in dom Ls
by A20, ORDINAL1:10;
then reconsider cd2 =
ConsecutiveDelta (
q,
O2) as
BiFunction of
(ConsecutiveSet (A,O2)),
L by A6, A7;
Ls . (succ O2) =
ConsecutiveDelta (
q,
(succ O2))
by A7, A20
.=
new_bi_fun (
(BiFun ((ConsecutiveDelta (q,O2)),(ConsecutiveSet (A,O2)),L)),
(Quadr (q,O2)))
by Th27
.=
new_bi_fun (
cd2,
(Quadr (q,O2)))
by Def15
;
then
ConsecutiveDelta (
q,
O2)
c= Ls . (succ O2)
by Th19;
then
Ls . O2 c= Ls . (succ O2)
by A7, A20, A22, ORDINAL1:10;
hence
Ls . O c= Ls . (succ O2)
by A18, A20, A21, A22, ORDINAL1:10, ORDINAL1:22;
verum end; end;
end;
A23:
S2[
0 ]
;
thus
for
O2 being
Ordinal holds
S2[
O2]
from ORDINAL2:sch 1(A23, A17, A9); verum
end;
for
x,
y being
set st
x in rng Ls &
y in rng Ls holds
x,
y are_c=-comparable
proof
let x,
y be
set ;
( x in rng Ls & y in rng Ls implies x,y are_c=-comparable )
assume that A24:
x in rng Ls
and A25:
y in rng Ls
;
x,y are_c=-comparable
consider o1 being
object such that A26:
o1 in dom Ls
and A27:
Ls . o1 = x
by A24, FUNCT_1:def 3;
consider o2 being
object such that A28:
o2 in dom Ls
and A29:
Ls . o2 = y
by A25, FUNCT_1:def 3;
reconsider o19 =
o1,
o29 =
o2 as
Ordinal by A26, A28;
(
o19 c= o29 or
o29 c= o19 )
;
then
(
x c= y or
y c= x )
by A8, A26, A27, A28, A29;
hence
x,
y are_c=-comparable
;
verum
end;
then A30:
rng Ls is
c=-linear
;
set Y = the
carrier of
L;
set X =
[:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):];
set f =
union (rng Ls);
rng Ls c= PFuncs (
[:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the
carrier of
L)
proof
let z be
object ;
TARSKI:def 3 ( not z in rng Ls or z in PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L) )
assume
z in rng Ls
;
z in PFuncs ([:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the carrier of L)
then consider o being
object such that A31:
o in dom Ls
and A32:
z = Ls . o
by FUNCT_1:def 3;
reconsider o =
o as
Ordinal by A31;
Ls . o = ConsecutiveDelta (
q,
o)
by A7, A31;
then reconsider h =
Ls . o as
BiFunction of
(ConsecutiveSet (A,o)),
L by A6, A7, A31;
o c= O1
by A7, A31, ORDINAL1:def 2;
then
(
dom h = [:(ConsecutiveSet (A,o)),(ConsecutiveSet (A,o)):] &
ConsecutiveSet (
A,
o)
c= ConsecutiveSet (
A,
O1) )
by Th29, FUNCT_2:def 1;
then
(
rng h c= the
carrier of
L &
dom h c= [:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):] )
by ZFMISC_1:96;
hence
z in PFuncs (
[:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the
carrier of
L)
by A32, PARTFUN1:def 3;
verum
end;
then
union (rng Ls) in PFuncs (
[:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):], the
carrier of
L)
by A30, TREES_2:40;
then A33:
ex
g being
Function st
(
union (rng Ls) = g &
dom g c= [:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):] &
rng g c= the
carrier of
L )
by PARTFUN1:def 3;
reconsider o1 =
O1 as non
empty Ordinal by A4;
set YY =
{ [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } ;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet (
A,$1);
consider Ts being
Sequence such that A34:
(
dom Ts = O1 & ( for
O2 being
Ordinal st
O2 in O1 holds
Ts . O2 = H2(
O2) ) )
from ORDINAL2:sch 2();
Ls is
Function-yielding
then reconsider LsF =
Ls as
Function-yielding Function ;
A36:
rng (doms LsF) = { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
proof
thus
rng (doms LsF) c= { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
XBOOLE_0:def 10 { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } c= rng (doms LsF)proof
let Z be
object ;
TARSKI:def 3 ( not Z in rng (doms LsF) or Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } )
assume
Z in rng (doms LsF)
;
Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
then consider o being
object such that A37:
o in dom (doms LsF)
and A38:
Z = (doms LsF) . o
by FUNCT_1:def 3;
A39:
o in dom LsF
by A37, FUNCT_6:59;
then reconsider o9 =
o as
Element of
o1 by A7;
Ls . o9 = ConsecutiveDelta (
q,
o9)
by A7;
then reconsider ls =
Ls . o9 as
BiFunction of
(ConsecutiveSet (A,o9)),
L by A6;
Z =
dom ls
by A38, A39, FUNCT_6:22
.=
[:(ConsecutiveSet (A,o9)),(ConsecutiveSet (A,o9)):]
by FUNCT_2:def 1
;
hence
Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
;
verum
end;
let Z be
object ;
TARSKI:def 3 ( not Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } or Z in rng (doms LsF) )
assume
Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
;
Z in rng (doms LsF)
then consider o being
Element of
o1 such that A40:
Z = [:(ConsecutiveSet (A,o)),(ConsecutiveSet (A,o)):]
;
Ls . o = ConsecutiveDelta (
q,
o)
by A7;
then reconsider ls =
Ls . o as
BiFunction of
(ConsecutiveSet (A,o)),
L by A6;
o in dom LsF
by A7;
then A41:
o in dom (doms LsF)
by FUNCT_6:59;
Z =
dom ls
by A40, FUNCT_2:def 1
.=
(doms LsF) . o
by A7, FUNCT_6:22
;
hence
Z in rng (doms LsF)
by A41, FUNCT_1:def 3;
verum
end;
{} in O1
by A4, ORDINAL3:8;
then reconsider RTs =
rng Ts as non
empty set by A34, FUNCT_1:3;
reconsider f =
union (rng Ls) as
Function by A33;
A42:
dom f = union (rng (doms LsF))
by Th1;
A43:
{ [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } = { [:a,a:] where a is Element of RTs : a in RTs }
proof
set XX =
{ [:a,a:] where a is Element of RTs : a in RTs } ;
thus
{ [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } c= { [:a,a:] where a is Element of RTs : a in RTs }
XBOOLE_0:def 10 { [:a,a:] where a is Element of RTs : a in RTs } c= { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } proof
let Z be
object ;
TARSKI:def 3 ( not Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } or Z in { [:a,a:] where a is Element of RTs : a in RTs } )
assume
Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
;
Z in { [:a,a:] where a is Element of RTs : a in RTs }
then consider o being
Element of
o1 such that A44:
Z = [:(ConsecutiveSet (A,o)),(ConsecutiveSet (A,o)):]
;
Ts . o = ConsecutiveSet (
A,
o)
by A34;
then reconsider CoS =
ConsecutiveSet (
A,
o) as
Element of
RTs by A34, FUNCT_1:def 3;
Z = [:CoS,CoS:]
by A44;
hence
Z in { [:a,a:] where a is Element of RTs : a in RTs }
;
verum
end;
let Z be
object ;
TARSKI:def 3 ( not Z in { [:a,a:] where a is Element of RTs : a in RTs } or Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum } )
assume
Z in { [:a,a:] where a is Element of RTs : a in RTs }
;
Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
then consider a being
Element of
RTs such that A45:
Z = [:a,a:]
and
a in RTs
;
consider o being
object such that A46:
o in dom Ts
and A47:
a = Ts . o
by FUNCT_1:def 3;
reconsider o9 =
o as
Ordinal by A46;
a = ConsecutiveSet (
A,
o9)
by A34, A46, A47;
hence
Z in { [:(ConsecutiveSet (A,O2)),(ConsecutiveSet (A,O2)):] where O2 is Element of o1 : verum }
by A34, A45, A46;
verum
end;
for
x,
y being
set st
x in RTs &
y in RTs holds
x,
y are_c=-comparable
proof
let x,
y be
set ;
( x in RTs & y in RTs implies x,y are_c=-comparable )
assume that A48:
x in RTs
and A49:
y in RTs
;
x,y are_c=-comparable
consider o1 being
object such that A50:
o1 in dom Ts
and A51:
Ts . o1 = x
by A48, FUNCT_1:def 3;
consider o2 being
object such that A52:
o2 in dom Ts
and A53:
Ts . o2 = y
by A49, FUNCT_1:def 3;
reconsider o19 =
o1,
o29 =
o2 as
Ordinal by A50, A52;
A54:
Ts . o29 = ConsecutiveSet (
A,
o29)
by A34, A52;
A55:
(
o19 c= o29 or
o29 c= o19 )
;
Ts . o19 = ConsecutiveSet (
A,
o19)
by A34, A50;
then
(
x c= y or
y c= x )
by A51, A53, A54, A55, Th29;
hence
x,
y are_c=-comparable
;
verum
end;
then A56:
RTs is
c=-linear
;
A57:
ConsecutiveDelta (
q,
O1)
= union (rng Ls)
by A4, A5, A7, Th28;
[:(ConsecutiveSet (A,O1)),(ConsecutiveSet (A,O1)):] =
[:(union (rng Ts)),(ConsecutiveSet (A,O1)):]
by A4, A5, A34, Th23
.=
[:(union RTs),(union RTs):]
by A4, A5, A34, Th23
.=
dom f
by A42, A36, A56, A43, Th3
;
hence
S1[
O1]
by A57, A33, FUNCT_2:def 1, RELSET_1:4;
verum
end;
ConsecutiveSet (A,{}) = A
by Th21;
then A58:
S1[ 0 ]
by Th26;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A58, A1, A3);
hence
ConsecutiveDelta (q,O) is BiFunction of (ConsecutiveSet (A,O)),L
; verum