let A, N be non empty finite set ; for f being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b ) & ( for p, p9 being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds
( ( a <_ p . i,b implies a <_ p9 . i,b ) & ( a <_ p9 . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p9 . i,a ) & ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 holds
ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b
let f be Function of (Funcs (N,(LinPreorders A))),(LinPreorders A); ( ( for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b ) & ( for p, p9 being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds
( ( a <_ p . i,b implies a <_ p9 . i,b ) & ( a <_ p9 . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p9 . i,a ) & ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds
( a <_ f . p,b iff a <_ f . p9,b ) ) & card A >= 3 implies ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b )
assume that
A1:
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds a <_ p . i,b ) holds
a <_ f . p,b
and
A2:
for p, p9 being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds
( ( a <_ p . i,b implies a <_ p9 . i,b ) & ( a <_ p9 . i,b implies a <_ p . i,b ) & ( b <_ p . i,a implies b <_ p9 . i,a ) & ( b <_ p9 . i,a implies b <_ p . i,a ) ) ) holds
( a <_ f . p,b iff a <_ f . p9,b )
and
A3:
card A >= 3
; ex n being Element of N st
for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b
defpred S1[ Element of LinPreorders A, Element of A] means ( for a being Element of A st a <> $2 holds
$2 <_ $1,a or for a being Element of A st a <> $2 holds
a <_ $1,$2 );
A4:
for p being Element of Funcs (N,(LinPreorders A))
for b being Element of A st ( for i being Element of N holds S1[p . i,b] ) holds
S1[f . p,b]
proof
assume
ex
p being
Element of
Funcs (
N,
(LinPreorders A)) ex
b being
Element of
A st
( ( for
i being
Element of
N holds
S1[
p . i,
b] ) & not
S1[
f . p,
b] )
;
contradiction
then consider p being
Element of
Funcs (
N,
(LinPreorders A)),
b being
Element of
A such that A5:
ex
a being
Element of
A st
(
a <> b &
a <=_ f . p,
b )
and A6:
ex
c being
Element of
A st
(
c <> b &
b <=_ f . p,
c )
and A7:
for
i being
Element of
N holds
S1[
p . i,
b]
;
consider a9 being
Element of
A such that A8:
(
a9 <> b &
a9 <=_ f . p,
b )
by A5;
consider c9 being
Element of
A such that A9:
(
b <> c9 &
b <=_ f . p,
c9 )
by A6;
ex
a,
c being
Element of
A st
(
a <> b &
b <> c &
a <> c &
a <=_ f . p,
b &
b <=_ f . p,
c )
then consider a,
c being
Element of
A such that A15:
(
a <> b &
b <> c )
and A16:
a <> c
and A17:
(
a <=_ f . p,
b &
b <=_ f . p,
c )
;
defpred S2[
Element of
N,
Element of
LinPreorders A]
means ( (
a <_ p . $1,
b implies
a <_ $2,
b ) & (
a <_ $2,
b implies
a <_ p . $1,
b ) & (
b <_ p . $1,
a implies
b <_ $2,
a ) & (
b <_ $2,
a implies
b <_ p . $1,
a ) & (
b <_ p . $1,
c implies
b <_ $2,
c ) & (
b <_ $2,
c implies
b <_ p . $1,
c ) & (
c <_ p . $1,
b implies
c <_ $2,
b ) & (
c <_ $2,
b implies
c <_ p . $1,
b ) &
c <_ $2,
a );
A18:
for
i being
Element of
N ex
o being
Element of
LinPreorders A st
S2[
i,
o]
proof
let i be
Element of
N;
ex o being Element of LinPreorders A st S2[i,o]
per cases
( for c being Element of A st c <> b holds
b <_ p . i,c or for a being Element of A st a <> b holds
a <_ p . i,b )
by A7;
suppose
for
c being
Element of
A st
c <> b holds
b <_ p . i,
c
;
ex o being Element of LinPreorders A st S2[i,o]then A19:
(
b <_ p . i,
a &
b <_ p . i,
c )
by A15;
consider o being
Element of
LinPreorders A such that A20:
(
b <_ o,
c &
c <_ o,
a )
by A15, A16, Th7;
take
o
;
S2[i,o]thus
S2[
i,
o]
by A19, A20, Th4, Th5;
verum end; suppose
for
a being
Element of
A st
a <> b holds
a <_ p . i,
b
;
ex o being Element of LinPreorders A st S2[i,o]then A21:
(
a <_ p . i,
b &
c <_ p . i,
b )
by A15;
consider o being
Element of
LinPreorders A such that A22:
(
c <_ o,
a &
a <_ o,
b )
by A15, A16, Th7;
take
o
;
S2[i,o]thus
S2[
i,
o]
by A21, A22, Th4, Th5;
verum end; end;
end;
consider p9 being
Function of
N,
(LinPreorders A) such that A23:
for
i being
Element of
N holds
S2[
i,
p9 . i]
from FUNCT_2:sch 3(A18);
reconsider p9 =
p9 as
Element of
Funcs (
N,
(LinPreorders A))
by FUNCT_2:8;
(
a <=_ f . p9,
b &
b <=_ f . p9,
c )
by A2, A17, A23;
then
a <=_ f . p9,
c
by Th5;
hence
contradiction
by A1, A23;
verum
end;
A24:
for b being Element of A ex nb being Element of N ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
proof
consider t being
FinSequence such that A25:
rng t = N
and A26:
t is
one-to-one
by FINSEQ_4:58;
reconsider t =
t as
FinSequence of
N by A25, FINSEQ_1:def 4;
let b be
Element of
A;
ex nb being Element of N ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
consider oI being
Element of
LinPreorders A such that A27:
for
a being
Element of
A st
a <> b holds
b <_ oI,
a
by Th8;
consider oII being
Element of
LinPreorders A such that A28:
for
a being
Element of
A st
a <> b holds
a <_ oII,
b
by Th9;
A29:
for
k0 being
Nat ex
p being
Element of
Funcs (
N,
(LinPreorders A)) st
( ( for
k being
Nat st
k in dom t &
k < k0 holds
p . (t . k) = oII ) & ( for
k being
Nat st
k in dom t &
k >= k0 holds
p . (t . k) = oI ) )
proof
let k0 be
Nat;
ex p being Element of Funcs (N,(LinPreorders A)) st
( ( for k being Nat st k in dom t & k < k0 holds
p . (t . k) = oII ) & ( for k being Nat st k in dom t & k >= k0 holds
p . (t . k) = oI ) )
defpred S2[
Element of
N,
Element of
LinPreorders A]
means ex
k being
Nat st
(
k in dom t & $1
= t . k & (
k < k0 implies $2
= oII ) & (
k >= k0 implies $2
= oI ) );
A30:
for
i being
Element of
N ex
o being
Element of
LinPreorders A st
S2[
i,
o]
consider p being
Function of
N,
(LinPreorders A) such that A35:
for
i being
Element of
N holds
S2[
i,
p . i]
from FUNCT_2:sch 3(A30);
reconsider p =
p as
Element of
Funcs (
N,
(LinPreorders A))
by FUNCT_2:8;
take
p
;
( ( for k being Nat st k in dom t & k < k0 holds
p . (t . k) = oII ) & ( for k being Nat st k in dom t & k >= k0 holds
p . (t . k) = oI ) )
thus
for
k being
Nat st
k in dom t &
k < k0 holds
p . (t . k) = oII
for k being Nat st k in dom t & k >= k0 holds
p . (t . k) = oI
let k be
Nat;
( k in dom t & k >= k0 implies p . (t . k) = oI )
assume that A38:
k in dom t
and A39:
k >= k0
;
p . (t . k) = oI
reconsider i =
t . k as
Element of
N by A38, PARTFUN1:4;
S2[
i,
p . i]
by A35;
hence
p . (t . k) = oI
by A26, A38, A39, FUNCT_1:def 4;
verum
end;
defpred S2[
Nat]
means for
p being
Element of
Funcs (
N,
(LinPreorders A)) st ( for
k being
Nat st
k in dom t &
k < $1 holds
p . (t . k) = oII ) & ( for
k being
Nat st
k in dom t &
k >= $1 holds
p . (t . k) = oI ) holds
for
a being
Element of
A st
a <> b holds
a <_ f . p,
b;
reconsider kII9 =
(len t) + 1 as
Element of
NAT by ORDINAL1:def 12;
A40:
S2[
kII9]
then A45:
ex
kII9 being
Nat st
S2[
kII9]
;
consider kII being
Nat such that A46:
(
S2[
kII] & ( for
k0 being
Nat st
S2[
k0] holds
k0 >= kII ) )
from NAT_1:sch 5(A45);
consider pII being
Element of
Funcs (
N,
(LinPreorders A))
such that A47:
for
k being
Nat st
k in dom t &
k < kII holds
pII . (t . k) = oII
and A48:
for
k being
Nat st
k in dom t &
k >= kII holds
pII . (t . k) = oI
by A29;
A49:
kII > 1
proof
assume A50:
kII <= 1
;
contradiction
consider a being
Element of
A such that A51:
a <> b
by A3, Th1, XXREAL_0:2;
A52:
for
i being
Element of
N holds
b <_ pII . i,
a
A55:
a <_ f . pII,
b
by A46, A47, A48, A51;
b <_ f . pII,
a
by A1, A52;
hence
contradiction
by A55, Th4;
verum
end;
then reconsider kI =
kII - 1 as
Nat by NAT_1:20;
reconsider kI =
kI as
Element of
NAT by ORDINAL1:def 12;
A56:
kII = kI + 1
;
kI > 1
- 1
by A49, XREAL_1:9;
then A57:
kI >= 0 + 1
by INT_1:7;
kII <= kII9
by A40, A46;
then
kI <= kII9 - 1
by XREAL_1:9;
then A58:
kI in dom t
by A57, FINSEQ_3:25;
then reconsider nb =
t . kI as
Element of
N by PARTFUN1:4;
A59:
kI + 0 < kII
by A56, XREAL_1:8;
then consider pI being
Element of
Funcs (
N,
(LinPreorders A))
such that A60:
for
k being
Nat st
k in dom t &
k < kI holds
pI . (t . k) = oII
and A61:
for
k being
Nat st
k in dom t &
k >= kI holds
pI . (t . k) = oI
and A62:
ex
a being
Element of
A st
(
a <> b & not
a <_ f . pI,
b )
by A46;
take
nb
;
ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
take
pI
;
ex pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
take
pII
;
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
thus
for
i being
Element of
N st
i <> nb holds
pI . i = pII . i
( ( for i being Element of N holds S1[pI . i,b] ) & ( for i being Element of N holds S1[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
thus A66:
for
i being
Element of
N holds
S1[
pI . i,
b]
( ( for i being Element of N holds S1[pII . i,b] ) & ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
thus
for
i being
Element of
N holds
S1[
pII . i,
b]
( ( for a being Element of A st a <> b holds
b <_ pI . nb,a ) & ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
pI . nb = oI
by A58, A61;
hence
for
a being
Element of
A st
a <> b holds
b <_ pI . nb,
a
by A27;
( ( for a being Element of A st a <> b holds
a <_ pII . nb,b ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
pII . nb = oII
by A47, A58, A59;
hence
for
a being
Element of
A st
a <> b holds
a <_ pII . nb,
b
by A28;
( ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) )
thus
for
a being
Element of
A st
a <> b holds
b <_ f . pI,
a
by A4, A62, A66;
for a being Element of A st a <> b holds
a <_ f . pII,b
thus
for
a being
Element of
A st
a <> b holds
a <_ f . pII,
b
by A46, A47, A48;
verum
end;
A67:
for b being Element of A ex nb being Element of N ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) & ( for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c ) )
proof
let b be
Element of
A;
ex nb being Element of N ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) & ( for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c ) )
consider nb being
Element of
N,
pI,
pII being
Element of
Funcs (
N,
(LinPreorders A))
such that A68:
for
i being
Element of
N st
i <> nb holds
pI . i = pII . i
and A69:
for
i being
Element of
N holds
S1[
pI . i,
b]
and A70:
for
i being
Element of
N holds
S1[
pII . i,
b]
and A71:
for
a being
Element of
A st
a <> b holds
b <_ pI . nb,
a
and A72:
for
a being
Element of
A st
a <> b holds
a <_ pII . nb,
b
and A73:
( ( for
a being
Element of
A st
a <> b holds
b <_ f . pI,
a ) & ( for
a being
Element of
A st
a <> b holds
a <_ f . pII,
b ) )
by A24;
take
nb
;
ex pI, pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) & ( for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c ) )
take
pI
;
ex pII being Element of Funcs (N,(LinPreorders A)) st
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) & ( for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c ) )
take
pII
;
( ( for i being Element of N st i <> nb holds
pI . i = pII . i ) & ( for i being Element of N holds S1[pI . i,b] ) & ( for a being Element of A st a <> b holds
b <_ f . pI,a ) & ( for a being Element of A st a <> b holds
a <_ f . pII,b ) & ( for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c ) )
thus
( ( for
i being
Element of
N st
i <> nb holds
pI . i = pII . i ) & ( for
i being
Element of
N holds
S1[
pI . i,
b] ) & ( for
a being
Element of
A st
a <> b holds
b <_ f . pI,
a ) & ( for
a being
Element of
A st
a <> b holds
a <_ f . pII,
b ) )
by A68, A69, A73;
for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,c
let p be
Element of
Funcs (
N,
(LinPreorders A));
for a, c being Element of A st a <> b & c <> b & a <_ p . nb,c holds
a <_ f . p,clet a,
c be
Element of
A;
( a <> b & c <> b & a <_ p . nb,c implies a <_ f . p,c )
assume that A74:
a <> b
and A75:
c <> b
and A76:
a <_ p . nb,
c
;
a <_ f . p,c
A77:
a <> c
by A76, Th3;
defpred S2[
Element of
N,
Element of
LinPreorders A]
means ( (
a <_ p . $1,
c implies
a <_ $2,
c ) & (
a <_ $2,
c implies
a <_ p . $1,
c ) & (
c <_ p . $1,
a implies
c <_ $2,
a ) & (
c <_ $2,
a implies
c <_ p . $1,
a ) & ( $1
= nb implies (
a <_ $2,
b &
b <_ $2,
c ) ) & ( $1
<> nb implies ( ( ( for
d being
Element of
A st
d <> b holds
b <_ pII . $1,
d ) implies (
b <_ $2,
a &
b <_ $2,
c ) ) & ( ( for
d being
Element of
A st
d <> b holds
d <_ pII . $1,
b ) implies (
a <_ $2,
b &
c <_ $2,
b ) ) ) ) );
A78:
for
i being
Element of
N ex
o being
Element of
LinPreorders A st
S2[
i,
o]
proof
let i be
Element of
N;
ex o being Element of LinPreorders A st S2[i,o]
per cases
( i = nb or i <> nb )
;
suppose A79:
i = nb
;
ex o being Element of LinPreorders A st S2[i,o]consider o being
Element of
LinPreorders A such that A80:
(
a <_ o,
b &
b <_ o,
c )
by A74, A75, A77, Th7;
take
o
;
S2[i,o]thus
S2[
i,
o]
by A76, A79, A80, Th4, Th5;
verum end; suppose A81:
i <> nb
;
ex o being Element of LinPreorders A st S2[i,o]per cases
( for d being Element of A st d <> b holds
b <_ pII . i,d or for d being Element of A st d <> b holds
d <_ pII . i,b )
by A70;
suppose
for
d being
Element of
A st
d <> b holds
b <_ pII . i,
d
;
ex o being Element of LinPreorders A st S2[i,o]then
b <_ pII . i,
a
by A74;
then A82:
not
a <_ pII . i,
b
by Th4;
consider o being
Element of
LinPreorders A such that A83:
(
b <_ o,
a &
b <_ o,
c & (
a <_ o,
c implies
a <_ p . i,
c ) & (
a <_ p . i,
c implies
a <_ o,
c ) & (
c <_ o,
a implies
c <_ p . i,
a ) & (
c <_ p . i,
a implies
c <_ o,
a ) )
by A74, A75, Th10;
take
o
;
S2[i,o]thus
S2[
i,
o]
by A74, A81, A82, A83;
verum end; suppose
for
d being
Element of
A st
d <> b holds
d <_ pII . i,
b
;
ex o being Element of LinPreorders A st S2[i,o]then
a <_ pII . i,
b
by A74;
then A84:
not
b <_ pII . i,
a
by Th4;
consider o being
Element of
LinPreorders A such that A85:
(
a <_ o,
b &
c <_ o,
b & (
a <_ o,
c implies
a <_ p . i,
c ) & (
a <_ p . i,
c implies
a <_ o,
c ) & (
c <_ o,
a implies
c <_ p . i,
a ) & (
c <_ p . i,
a implies
c <_ o,
a ) )
by A74, A75, Th11;
take
o
;
S2[i,o]thus
S2[
i,
o]
by A74, A81, A84, A85;
verum end; end; end; end;
end;
consider pIII being
Function of
N,
(LinPreorders A) such that A86:
for
i being
Element of
N holds
S2[
i,
pIII . i]
from FUNCT_2:sch 3(A78);
reconsider pIII =
pIII as
Element of
Funcs (
N,
(LinPreorders A))
by FUNCT_2:8;
for
i being
Element of
N holds
( (
a <_ pII . i,
b implies
a <_ pIII . i,
b ) & (
a <_ pIII . i,
b implies
a <_ pII . i,
b ) & (
b <_ pII . i,
a implies
b <_ pIII . i,
a ) & (
b <_ pIII . i,
a implies
b <_ pII . i,
a ) )
proof
let i be
Element of
N;
( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) )
per cases
( i = nb or i <> nb )
;
suppose
i = nb
;
( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) )then
(
a <_ pII . i,
b &
a <_ pIII . i,
b )
by A72, A74, A86;
hence
( (
a <_ pII . i,
b implies
a <_ pIII . i,
b ) & (
a <_ pIII . i,
b implies
a <_ pII . i,
b ) & (
b <_ pII . i,
a implies
b <_ pIII . i,
a ) & (
b <_ pIII . i,
a implies
b <_ pII . i,
a ) )
by Th4;
verum end; suppose A87:
i <> nb
;
( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) )per cases
( for d being Element of A st d <> b holds
b <_ pII . i,d or for d being Element of A st d <> b holds
d <_ pII . i,b )
by A70;
suppose
for
d being
Element of
A st
d <> b holds
b <_ pII . i,
d
;
( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) )then
(
b <_ pII . i,
a &
b <_ pIII . i,
a )
by A74, A86, A87;
hence
( (
a <_ pII . i,
b implies
a <_ pIII . i,
b ) & (
a <_ pIII . i,
b implies
a <_ pII . i,
b ) & (
b <_ pII . i,
a implies
b <_ pIII . i,
a ) & (
b <_ pIII . i,
a implies
b <_ pII . i,
a ) )
by Th4;
verum end; suppose
for
d being
Element of
A st
d <> b holds
d <_ pII . i,
b
;
( ( a <_ pII . i,b implies a <_ pIII . i,b ) & ( a <_ pIII . i,b implies a <_ pII . i,b ) & ( b <_ pII . i,a implies b <_ pIII . i,a ) & ( b <_ pIII . i,a implies b <_ pII . i,a ) )then
(
a <_ pII . i,
b &
a <_ pIII . i,
b )
by A74, A86, A87;
hence
( (
a <_ pII . i,
b implies
a <_ pIII . i,
b ) & (
a <_ pIII . i,
b implies
a <_ pII . i,
b ) & (
b <_ pII . i,
a implies
b <_ pIII . i,
a ) & (
b <_ pIII . i,
a implies
b <_ pII . i,
a ) )
by Th4;
verum end; end; end; end;
end;
then A88:
(
a <_ f . pII,
b iff
a <_ f . pIII,
b )
by A2;
for
i being
Element of
N holds
( (
b <_ pI . i,
c implies
b <_ pIII . i,
c ) & (
b <_ pIII . i,
c implies
b <_ pI . i,
c ) & (
c <_ pI . i,
b implies
c <_ pIII . i,
b ) & (
c <_ pIII . i,
b implies
c <_ pI . i,
b ) )
proof
let i be
Element of
N;
( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) )
per cases
( i = nb or i <> nb )
;
suppose
i = nb
;
( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) )then
(
b <_ pI . i,
c &
b <_ pIII . i,
c )
by A71, A75, A86;
hence
( (
b <_ pI . i,
c implies
b <_ pIII . i,
c ) & (
b <_ pIII . i,
c implies
b <_ pI . i,
c ) & (
c <_ pI . i,
b implies
c <_ pIII . i,
b ) & (
c <_ pIII . i,
b implies
c <_ pI . i,
b ) )
by Th4;
verum end; suppose A89:
i <> nb
;
( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) )per cases
( for d being Element of A st d <> b holds
b <_ pII . i,d or for d being Element of A st d <> b holds
d <_ pII . i,b )
by A70;
suppose A90:
for
d being
Element of
A st
d <> b holds
b <_ pII . i,
d
;
( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) )then
b <_ pII . i,
c
by A75;
then A91:
b <_ pI . i,
c
by A68, A89;
b <_ pIII . i,
c
by A86, A89, A90;
hence
( (
b <_ pI . i,
c implies
b <_ pIII . i,
c ) & (
b <_ pIII . i,
c implies
b <_ pI . i,
c ) & (
c <_ pI . i,
b implies
c <_ pIII . i,
b ) & (
c <_ pIII . i,
b implies
c <_ pI . i,
b ) )
by A91, Th4;
verum end; suppose A92:
for
d being
Element of
A st
d <> b holds
d <_ pII . i,
b
;
( ( b <_ pI . i,c implies b <_ pIII . i,c ) & ( b <_ pIII . i,c implies b <_ pI . i,c ) & ( c <_ pI . i,b implies c <_ pIII . i,b ) & ( c <_ pIII . i,b implies c <_ pI . i,b ) )then
c <_ pII . i,
b
by A75;
then A93:
c <_ pI . i,
b
by A68, A89;
c <_ pIII . i,
b
by A86, A89, A92;
hence
( (
b <_ pI . i,
c implies
b <_ pIII . i,
c ) & (
b <_ pIII . i,
c implies
b <_ pI . i,
c ) & (
c <_ pI . i,
b implies
c <_ pIII . i,
b ) & (
c <_ pIII . i,
b implies
c <_ pI . i,
b ) )
by A93, Th4;
verum end; end; end; end;
end;
then
(
b <_ f . pI,
c iff
b <_ f . pIII,
c )
by A2;
then
a <_ f . pIII,
c
by A73, A74, A88, Th5;
hence
a <_ f . p,
c
by A2, A86;
verum
end;
set b = the Element of A;
consider nb being Element of N, pI, pII being Element of Funcs (N,(LinPreorders A)) such that
A94:
for i being Element of N st i <> nb holds
pI . i = pII . i
and
A95:
for i being Element of N holds S1[pI . i, the Element of A]
and
A96:
( ( for a being Element of A st a <> the Element of A holds
the Element of A <_ f . pI,a ) & ( for a being Element of A st a <> the Element of A holds
a <_ f . pII, the Element of A ) )
and
A97:
for p being Element of Funcs (N,(LinPreorders A))
for a, c being Element of A st a <> the Element of A & c <> the Element of A & a <_ p . nb,c holds
a <_ f . p,c
by A67;
take
nb
; for p being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ p . nb,b holds
a <_ f . p,b
let p be Element of Funcs (N,(LinPreorders A)); for a, b being Element of A st a <_ p . nb,b holds
a <_ f . p,b
let a, a9 be Element of A; ( a <_ p . nb,a9 implies a <_ f . p,a9 )
assume A98:
a <_ p . nb,a9
; a <_ f . p,a9
then A99:
a <> a9
by Th4;
per cases
( ( a <> the Element of A & a9 <> the Element of A ) or a = the Element of A or a9 = the Element of A )
;
suppose A100:
(
a = the
Element of
A or
a9 = the
Element of
A )
;
a <_ f . p,a9consider c being
Element of
A such that A101:
(
c <> a &
c <> a9 )
by A3, Th2;
consider nc being
Element of
N,
pI9,
pII9 being
Element of
Funcs (
N,
(LinPreorders A))
such that
for
i being
Element of
N st
i <> nc holds
pI9 . i = pII9 . i
and
for
i being
Element of
N holds
S1[
pI9 . i,
c]
and
for
a being
Element of
A st
a <> c holds
c <_ f . pI9,
a
and
for
a being
Element of
A st
a <> c holds
a <_ f . pII9,
c
and A102:
for
p being
Element of
Funcs (
N,
(LinPreorders A))
for
a,
a9 being
Element of
A st
a <> c &
a9 <> c &
a <_ p . nc,
a9 holds
a <_ f . p,
a9
by A67;
nc = nb
proof
per cases
( a = the Element of A or a9 = the Element of A )
by A100;
suppose A103:
a = the
Element of
A
;
nc = nbassume A104:
nc <> nb
;
contradiction
( the
Element of
A <_ pI . nc,
a9 or
a9 <_ pI . nc, the
Element of
A )
by A95, A99, A103;
then
( ( the
Element of
A <_ pII . nc,
a9 &
a9 <_ f . pII, the
Element of
A ) or (
a9 <_ pI . nc, the
Element of
A & the
Element of
A <_ f . pI,
a9 ) )
by A94, A96, A99, A103, A104;
then
( ( the
Element of
A <_ pII . nc,
a9 &
a9 <=_ f . pII, the
Element of
A ) or (
a9 <_ pI . nc, the
Element of
A & the
Element of
A <=_ f . pI,
a9 ) )
by Th4;
hence
contradiction
by A101, A102, A103;
verum end; suppose A105:
a9 = the
Element of
A
;
nc = nbassume A106:
nc <> nb
;
contradiction
( the
Element of
A <_ pI . nc,
a or
a <_ pI . nc, the
Element of
A )
by A95, A99, A105;
then
( ( the
Element of
A <_ pII . nc,
a &
a <_ f . pII, the
Element of
A ) or (
a <_ pI . nc, the
Element of
A & the
Element of
A <_ f . pI,
a ) )
by A94, A96, A99, A105, A106;
then
( ( the
Element of
A <_ pII . nc,
a &
a <=_ f . pII, the
Element of
A ) or (
a <_ pI . nc, the
Element of
A & the
Element of
A <=_ f . pI,
a ) )
by Th4;
hence
contradiction
by A101, A102, A105;
verum end; end;
end; hence
a <_ f . p,
a9
by A98, A101, A102;
verum end; end;