let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is symmetric
let L be lower-bounded LATTICE; :: thesis: for d being BiFunction of A,L st d is symmetric holds
for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is symmetric
let d be BiFunction of A,L; :: thesis: ( d is symmetric implies for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is symmetric )
assume A1:
d is symmetric
; :: thesis: for q being QuadrSeq of d
for O being Ordinal holds ConsecutiveDelta2 q,O is symmetric
let q be QuadrSeq of d; :: thesis: for O being Ordinal holds ConsecutiveDelta2 q,O is symmetric
let O be Ordinal; :: thesis: ConsecutiveDelta2 q,O is symmetric
defpred S1[ Ordinal] means ConsecutiveDelta2 q,$1 is symmetric ;
A2:
S1[ {} ]
proof
let x,
y be
Element of
ConsecutiveSet2 A,
{} ;
:: according to LATTICE5:def 6 :: thesis: (ConsecutiveDelta2 q,{} ) . x,y = (ConsecutiveDelta2 q,{} ) . y,x
reconsider x' =
x,
y' =
y as
Element of
A by Th15;
thus (ConsecutiveDelta2 q,{} ) . x,
y =
d . x',
y'
by Th19
.=
d . y',
x'
by A1, LATTICE5:def 6
.=
(ConsecutiveDelta2 q,{} ) . y,
x
by Th19
;
:: thesis: verum
end;
A3:
for O1 being Ordinal st S1[O1] holds
S1[ succ O1]
proof
let O1 be
Ordinal;
:: thesis: ( S1[O1] implies S1[ succ O1] )
assume
ConsecutiveDelta2 q,
O1 is
symmetric
;
:: thesis: S1[ succ O1]
then A4:
new_bi_fun2 (ConsecutiveDelta2 q,O1),
(Quadr2 q,O1) is
symmetric
by Th11;
let x,
y be
Element of
ConsecutiveSet2 A,
(succ O1);
:: according to LATTICE5:def 6 :: thesis: (ConsecutiveDelta2 q,(succ O1)) . x,y = (ConsecutiveDelta2 q,(succ O1)) . y,x
reconsider x' =
x,
y' =
y as
Element of
new_set2 (ConsecutiveSet2 A,O1) by Th16;
A5:
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,
y =
(new_bi_fun2 (ConsecutiveDelta2 q,O1),(Quadr2 q,O1)) . y',
x'
by A4, LATTICE5:def 6
.=
(ConsecutiveDelta2 q,(succ O1)) . y,
x
by A5
;
:: thesis: verum
end;
A6:
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
let O2 be
Ordinal;
:: thesis: ( O2 <> {} & O2 is limit_ordinal & ( for O2 being Ordinal st O2 in O2 holds
S1[O2] ) implies S1[O2] )
assume A7:
(
O2 <> {} &
O2 is
limit_ordinal & ( for
O1 being
Ordinal st
O1 in O2 holds
ConsecutiveDelta2 q,
O1 is
symmetric ) )
;
:: thesis: S1[O2]
deffunc H1(
Ordinal)
-> BiFunction of
(ConsecutiveSet2 A,$1),
L =
ConsecutiveDelta2 q,$1;
consider Ls being
T-Sequence such that A8:
(
dom Ls = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ls . O1 = H1(
O1) ) )
from ORDINAL2:sch 2();
A9:
ConsecutiveDelta2 q,
O2 = union (rng Ls)
by A7, A8, Th21;
deffunc H2(
Ordinal)
-> set =
ConsecutiveSet2 A,$1;
consider Ts being
T-Sequence such that A10:
(
dom Ts = O2 & ( for
O1 being
Ordinal st
O1 in O2 holds
Ts . O1 = H2(
O1) ) )
from ORDINAL2:sch 2();
A11:
ConsecutiveSet2 A,
O2 = union (rng Ts)
by A7, A10, Th17;
set CS =
ConsecutiveSet2 A,
O2;
reconsider f =
union (rng Ls) as
BiFunction of
(ConsecutiveSet2 A,O2),
L by A9;
f is
symmetric
proof
let x,
y be
Element of
ConsecutiveSet2 A,
O2;
:: according to LATTICE5:def 6 :: thesis: f . x,y = f . y,x
consider x1 being
set such that A12:
(
x in x1 &
x1 in rng Ts )
by A11, TARSKI:def 4;
consider o1 being
set such that A13:
(
o1 in dom Ts &
x1 = Ts . o1 )
by A12, FUNCT_1:def 5;
consider y1 being
set such that A14:
(
y in y1 &
y1 in rng Ts )
by A11, TARSKI:def 4;
consider o2 being
set such that A15:
(
o2 in dom Ts &
y1 = Ts . o2 )
by A14, FUNCT_1:def 5;
reconsider o1 =
o1,
o2 =
o2 as
Ordinal by A13, A15;
A16:
x in ConsecutiveSet2 A,
o1
by A10, A12, A13;
A17:
y in ConsecutiveSet2 A,
o2
by A10, A14, A15;
A18:
Ls . o1 = ConsecutiveDelta2 q,
o1
by A8, A10, A13;
then reconsider h1 =
Ls . o1 as
BiFunction of
(ConsecutiveSet2 A,o1),
L ;
A19:
h1 is
symmetric
proof
let x,
y be
Element of
ConsecutiveSet2 A,
o1;
:: according to LATTICE5:def 6 :: thesis: h1 . x,y = h1 . y,x
A20:
ConsecutiveDelta2 q,
o1 is
symmetric
by A7, A10, A13;
thus h1 . x,
y =
(ConsecutiveDelta2 q,o1) . x,
y
by A8, A10, A13
.=
(ConsecutiveDelta2 q,o1) . y,
x
by A20, LATTICE5:def 6
.=
h1 . y,
x
by A8, A10, A13
;
:: thesis: verum
end;
A21:
dom h1 = [:(ConsecutiveSet2 A,o1),(ConsecutiveSet2 A,o1):]
by FUNCT_2:def 1;
A22:
Ls . o2 = ConsecutiveDelta2 q,
o2
by A8, A10, A15;
then reconsider h2 =
Ls . o2 as
BiFunction of
(ConsecutiveSet2 A,o2),
L ;
A23:
h2 is
symmetric
proof
let x,
y be
Element of
ConsecutiveSet2 A,
o2;
:: according to LATTICE5:def 6 :: thesis: h2 . x,y = h2 . y,x
A24:
ConsecutiveDelta2 q,
o2 is
symmetric
by A7, A10, A15;
thus h2 . x,
y =
(ConsecutiveDelta2 q,o2) . x,
y
by A8, A10, A15
.=
(ConsecutiveDelta2 q,o2) . y,
x
by A24, LATTICE5:def 6
.=
h2 . y,
x
by A8, A10, A15
;
:: thesis: verum
end;
A25:
dom h2 = [:(ConsecutiveSet2 A,o2),(ConsecutiveSet2 A,o2):]
by FUNCT_2:def 1;
per cases
( o1 c= o2 or o2 c= o1 )
;
suppose
o1 c= o2
;
:: thesis: f . x,y = f . y,xthen A26:
ConsecutiveSet2 A,
o1 c= ConsecutiveSet2 A,
o2
by Th22;
then reconsider x' =
x,
y' =
y as
Element of
ConsecutiveSet2 A,
o2 by A10, A14, A15, A16;
ConsecutiveDelta2 q,
o2 in rng Ls
by A8, A10, A15, A22, FUNCT_1:def 5;
then A27:
h2 c= f
by A22, ZFMISC_1:92;
A28:
(
[x,y] in dom h2 &
[y,x] in dom h2 )
by A16, A17, A25, A26, ZFMISC_1:106;
hence f . x,
y =
h2 . x',
y'
by A27, GRFUNC_1:8
.=
h2 . y',
x'
by A23, LATTICE5:def 6
.=
f . y,
x
by A27, A28, GRFUNC_1:8
;
:: thesis: verum end; suppose
o2 c= o1
;
:: thesis: f . x,y = f . y,xthen A29:
ConsecutiveSet2 A,
o2 c= ConsecutiveSet2 A,
o1
by Th22;
then reconsider x' =
x,
y' =
y as
Element of
ConsecutiveSet2 A,
o1 by A10, A12, A13, A17;
ConsecutiveDelta2 q,
o1 in rng Ls
by A8, A10, A13, A18, FUNCT_1:def 5;
then A30:
h1 c= f
by A18, ZFMISC_1:92;
A31:
(
[x,y] in dom h1 &
[y,x] in dom h1 )
by A16, A17, A21, A29, ZFMISC_1:106;
hence f . x,
y =
h1 . x',
y'
by A30, GRFUNC_1:8
.=
h1 . y',
x'
by A19, LATTICE5:def 6
.=
f . y,
x
by A30, A31, GRFUNC_1:8
;
:: thesis: verum end;
end;
hence
S1[
O2]
by A7, A8, Th21;
:: thesis: verum
end;
for O being Ordinal holds S1[O]
from ORDINAL2:sch 1(A2, A3, A6);
hence
ConsecutiveDelta2 q,O is symmetric
; :: thesis: verum