:: Arrow's Impossibility Theorem
:: by Freek Wiedijk
::
:: Received August 13, 2007
:: Copyright (c) 2007-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, FINSET_1, CARD_1, XXREAL_0,
TARSKI, ARYTM_1, RELAT_1, ZFMISC_1, RELAT_2, ORDERS_1, WELLORD1, FUNCT_2,
NAT_1, FINSEQ_1, ARYTM_3, ARROW;
notations ORDERS_1, RELAT_1, RELAT_2, RELSET_1, XBOOLE_0, SUBSET_1, TARSKI,
FINSET_1, FUNCT_1, FUNCT_2, CARD_1, XXREAL_0, ZFMISC_1, ORDINAL1, NAT_1,
NUMBERS, FINSEQ_1, XCMPLX_0, WELLORD1;
constructors XXREAL_0, FUNCT_2, REAL_1, FINSEQ_1, INT_1, RELAT_2, PARTFUN1,
WELLORD1, RELSET_1;
registrations RELSET_1, FINSET_1, INT_1, XREAL_0, XBOOLE_0, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions FUNCT_2;
equalities RELAT_1, WELLORD1;
expansions WELLORD1;
theorems RELSET_1, ZFMISC_1, TARSKI, FUNCT_2, FINSEQ_4, FINSEQ_1, FINSEQ_3,
NAT_1, ORDINAL1, XREAL_1, FUNCT_1, XXREAL_0, PARTFUN1, INT_1, CARD_2,
CARD_1, XBOOLE_0, SUBSET_1, RELAT_2, RELAT_1, ORDERS_1, XBOOLE_1,
WELLORD2, XTUPLE_0;
schemes FUNCT_2, NAT_1, RELSET_1, XFAMILY;
begin :: Preliminaries
definition
let A,B9 be non empty set;
let B be non empty Subset of B9;
let f be Function of A,B;
let x be Element of A;
redefine func f.x -> Element of B; :: redefines . (FUNCT_1, definition)
coherence
proof
thus f.x is Element of B;
end;
end;
theorem Th1:
for A being finite set st card A >= 2 holds for a being Element of A holds
ex b being Element of A st b <> a
proof
let A9 be finite set;
assume
A1: card A9 >= 2;
then reconsider A = A9 as finite non empty set by CARD_1:27;
let a be Element of A9;
{a} c= A by ZFMISC_1:31;
then card (A \ {a}) = card A - card {a} by CARD_2:44
.= card A - 1 by CARD_1:30;
then card (A \ {a}) <> 0 by A1;
then consider b being object such that
A2: b in A \ {a} by CARD_1:27,XBOOLE_0:def 1;
reconsider b as Element of A9 by A2;
take b;
not b in {a} by A2,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
theorem Th2:
for A being finite set st card A >= 3 holds for a,b being Element of A holds
ex c being Element of A st c <> a & c <> b
proof
let A9 be finite set;
assume
A1: card A9 >= 3;
then reconsider A = A9 as finite non empty set by CARD_1:27;
let a,b be Element of A9;
{a,b} c= A by ZFMISC_1:32;
then A2: card (A \ {a,b}) = card A - card {a,b} by CARD_2:44;
card {a,b} <= 2 by CARD_2:50;
then card (A \ {a,b}) >= 3 - 2 by A1,A2,XREAL_1:13;
then card (A \ {a,b}) <> 0;
then consider c being object such that
A3: c in A \ {a,b} by CARD_1:27,XBOOLE_0:def 1;
reconsider c as Element of A9 by A3;
take c;
not c in {a,b} by A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 2;
end;
begin :: Linear preorders and linear orders
reserve A for non empty set;
reserve a,b,c,x,y,z for Element of A;
definition
let A;
defpred P[set] means $1 is Relation of A &
(for a,b holds [a,b] in $1 or [b,a] in $1) &
(for a,b,c st [a,b] in $1 & [b,c] in $1 holds [a,c] in $1);
defpred Q[set] means for R being set holds R in $1 iff P[R];
func LinPreorders A -> set means
:Def1:
for R being set holds R in it iff
R is Relation of A & (for a,b holds [a,b] in R or [b,a] in R) &
for a,b,c st [a,b] in R & [b,c] in R holds [a,c] in R;
existence
proof
consider it0 being set such that
A1: for R being set holds R in it0 iff R in bool [:A,A:] & P[R]
from XFAMILY:sch 1;
take it0;
let R be set;
thus R in it0 implies P[R] by A1;
assume
A2: P[R];
[:A,A:] in bool [:A,A:] by ZFMISC_1:def 1;
hence thesis by A1,A2;
end;
uniqueness
proof
let it1,it2 be set;
assume that
A3: Q[it1] and
A4: Q[it2];
now
let R be object;
reconsider RR=R as set by TARSKI:1;
R in it1 iff P[RR] by A3;
hence R in it1 iff R in it2 by A4;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let A;
cluster LinPreorders A -> non empty;
coherence
proof
[:A,A:] c= [:A,A:];
then reconsider R = [:A,A:] as Relation of A;
(
for a,b holds [a,b] in R or [b,a] in R)& for a,b,c st [a,b] in R & [b,c] in
R holds [a,c] in R by ZFMISC_1:87;
hence thesis by Def1;
end;
end;
definition
let A;
defpred P[set] means for a,b st [a,b] in $1 & [b,a] in $1 holds a = b;
defpred Q[set] means
for R being Element of LinPreorders A holds R in $1 iff P[R];
func LinOrders A -> Subset of LinPreorders A means
:Def2:
for R being Element of LinPreorders A holds R in it iff
for a,b st [a,b] in R & [b,a] in R holds a = b;
existence
proof
consider it0 being set such that
A1: for R being set holds R in it0 iff R in LinPreorders A & P[R]
from XFAMILY:sch 1;
for R being object st R in it0 holds R in LinPreorders A by A1;
then reconsider it0 as Subset of LinPreorders A by TARSKI:def 3;
take it0;
let R be Element of LinPreorders A;
thus R in it0 implies P[R] by A1;
assume P[R];
hence thesis by A1;
end;
uniqueness
proof
let it1,it2 be Subset of LinPreorders A;
assume that
A2: Q[it1] and
A3: Q[it2];
now
let R be Element of LinPreorders A;
R in it1 iff P[R] by A2;
hence R in it1 iff R in it2 by A3;
end;
hence thesis by SUBSET_1:3;
end;
end;
registration
let A be set;
cluster connected for Order of A;
existence
proof
consider R9 being Relation such that
A1: R9 well_orders A by WELLORD2:17;
set R = R9 |_2 A;
A2: R is well-ordering by A1,WELLORD2:16;
reconsider R as Relation of A by XBOOLE_1:17;
now
let a be object;
assume
A3: a in A;
R9 is_reflexive_in A by A1;
then A4: [a,a] in R9 by A3,RELAT_2:def 1;
[a,a] in [:A,A:] by A3,ZFMISC_1:def 2;
then [a,a] in R by A4,XBOOLE_0:def 4;
hence a in dom R by XTUPLE_0:def 12;
end;
then A c= dom R by TARSKI:def 3;
then dom R = A by XBOOLE_0:def 10;
then reconsider R as Order of A by A2,PARTFUN1:def 2;
take R;
thus thesis by A2;
end;
end;
definition
let A;
redefine func LinOrders A means :: redefines LinOrders (ARROW, definition)
:Def3:
for R being set holds R in it iff R is connected Order of A;
compatibility
proof
A1: now
let R be set;
assume
A2: R in LinOrders A;
then reconsider R9 = R as Relation of A by Def1;
now
let a be object;
assume a in A;
then [a,a] in R by A2,Def1;
hence a in dom R9 by XTUPLE_0:def 12;
end;
then A c= dom R9 by TARSKI:def 3;
then A3: dom R9 = A by XBOOLE_0:def 10;
now
let a be object;
assume a in A;
then [a,a] in R by A2,Def1;
hence a in rng R9 by XTUPLE_0:def 13;
end;
then A c= rng R9 by TARSKI:def 3;
then A4: field R9 = A \/ A by A3,XBOOLE_0:def 10;
for a,b being object st a in A & b in A & a <> b
holds [a,b] in R or [b,a] in R by A2,Def1;
then A5: R9 is_connected_in A by RELAT_2:def 6;
for a being object st a in A holds [a,a] in R by A2,Def1;
then A6: R9 is_reflexive_in A by RELAT_2:def 1;
for a,b being object st a in A & b in A & [a,b] in R & [b,a] in R
holds a = b
by A2,Def2;
then A7: R9 is_antisymmetric_in A by RELAT_2:def 4;
for a,b,c being object
st a in A & b in A & c in A & [a,b] in R & [b,c] in
R holds [a,c] in R by A2,Def1;
then R9 is_transitive_in A by RELAT_2:def 8;
hence R is connected Order of A
by A3,A4,A5,A6,A7,PARTFUN1:def 2,RELAT_2:def 9,def 12,def 14,def 16;
end;
A8: now
let R be set;
assume
A9: R is connected Order of A;
then reconsider R9 = R as connected Order of A;
A10: now
let a,b;
dom R9 = A by PARTFUN1:def 2;
then A c= dom R9 \/ rng R9 by XBOOLE_1:7;
then A11: field R9 = A by XBOOLE_0:def 10;
A12: R9
is_connected_in field R9 & R9 is_reflexive_in field R9 by RELAT_2:def 9,def 14
;
a = b or a <> b;
hence [a,b] in R or [b,a] in R by A11,A12,RELAT_2:def 1,def 6;
end;
for a,b,c st [a,b] in R & [b,c] in R holds [a,c] in R by A9,ORDERS_1:5;
then A13: R in LinPreorders A by A9,A10,Def1;
for a,b st [a,b] in R & [b,a] in R holds a = b by A9,ORDERS_1:4;
hence R in LinOrders A by A13,Def2;
end;
let it0 be Subset of LinPreorders A;
thus it0 = LinOrders A implies
for R being set holds R in it0 iff R is connected Order of A by A1,A8;
assume
A14: for R being set holds R in it0 iff R is connected Order of A;
now
let R be object;
R in it0 iff R is connected Order of A by A14;
hence R in it0 iff R in LinOrders A by A1,A8;
end;
hence thesis by TARSKI:2;
end;
end;
registration
let A;
cluster LinOrders A -> non empty;
coherence
proof
set R = the connected Order of A;
R in LinOrders A by Def3;
hence thesis;
end;
end;
registration let A;
cluster -> Relation-like for Element of LinPreorders A;
coherence by Def1;
cluster -> Relation-like for Element of LinOrders A;
coherence;
end;
reserve o,o9 for Element of LinPreorders A;
reserve o99 for Element of LinOrders A;
definition
let o be Relation, a,b be set;
pred a <=_o, b means
[a,b] in o;
end;
notation
let o be Relation, a,b be set;
synonym b >=_o, a for a <=_o, b;
antonym b <_o, a for a <=_o, b;
antonym a >_o, b for a <=_o, b;
end;
theorem Th3:
a <=_o, a
by Def1;
theorem Th4:
a <=_o, b or b <=_o, a
by Def1;
theorem Th5:
(a <=_o, b or a <_o, b) & (b <=_ o, c or b <_o, c) implies a <=_o, c
proof
assume a <=_o, b or a <_o, b;
then a <=_o, b by Th4;
then A1: [a,b] in o;
assume b <=_o, c or b <_o, c;
then b <=_o, c by Th4;
then [b,c] in o;
hence [a,c] in o by A1,Def1;
end;
theorem Th6:
a <=_o99, b & b <=_o99, a implies a = b
by Def2;
theorem Th7:
a <> b & b <> c & a <> c implies ex o st a <_o, b & b <_o, c
proof
assume that
A1: a <> b & b <> c and
A2: a <> c;
defpred P[set,set] means ($1 = a or $2 <> a) & ($1 <> c or $2 = c);
consider R being Relation of A such that
A3: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A4: now
let x,y;
P[x,y] or P[y,x] by A2;
hence [x,y] in R or [y,x] in R by A3;
end;
now
let x,y,z;
assume [x,y] in R & [y,z] in R;
then ( P[x,y])& P[y,z] by A3;
hence [x,z] in R by A3;
end;
then reconsider o = R as Element of LinPreorders A by A4,Def1;
take o;
( not [b,a] in R)& not [c,b] in R by A1,A3;
hence thesis;
end;
theorem Th8:
ex o st for a st a <> b holds b <_o, a
proof
defpred P[set,set] means $1 = b or $2 <> b;
consider R being Relation of A such that
A1: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A2: now
let x,y;
P[x,y] or P[y,x];
hence [x,y] in R or [y,x] in R by A1;
end;
now
let x,y,z;
assume that
A3: [x,y] in R and
A4: [y,z] in R;
P[y,z] by A1,A4;
hence [x,z] in R by A1,A3;
end;
then reconsider o = R as Element of LinPreorders A by A2,Def1;
take o;
let a;
assume a <> b;
then not [a,b] in R by A1;
hence thesis;
end;
theorem Th9:
ex o st for a st a <> b holds a <_o, b
proof
defpred P[set,set] means $1 <> b or $2 = b;
consider R being Relation of A such that
A1: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A2: now
let x,y;
P[x,y] or P[y,x];
hence [x,y] in R or [y,x] in R by A1;
end;
now
let x,y,z;
assume that
A3: [x,y] in R and
A4: [y,z] in R;
P[x,y] by A1,A3;
hence [x,z] in R by A1,A4;
end;
then reconsider o = R as Element of LinPreorders A by A2,Def1;
take o;
let a;
assume a <> b;
then not [b,a] in R by A1;
hence thesis;
end;
theorem Th10:
a <> b & a <> c implies ex o st a <_o, b & a <_o, c &
(b <_o, c iff b <_o9, c) & (c <_o, b iff c <_o9, b)
proof
assume
A1: a <> b & a <> c;
defpred P[Element of A,Element of A] means
$1 = a or ($1 <=_o9, $2 & $2 <> a);
consider R being Relation of A such that
A2: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A3: now
let x,y;
P[x,y] or P[y,x] by Th4;
hence [x,y] in R or [y,x] in R by A2;
end;
now
let x,y,z;
assume [x,y] in R & [y,z] in R;
then ( P[x,y])& P[y,z] by A2;
then P[x,z] by Th5;
hence [x,z] in R by A2;
end;
then reconsider o = R as Element of LinPreorders A by A3,Def1;
take o;
A4: ( not [b,a] in R)& not [c,a] in R by A1,A2;
A5: not [c,b] in R iff b <_o9, c by A1,A2;
not [b,c] in R iff c <_o9, b by A1,A2;
hence thesis by A4,A5;
end;
theorem Th11:
a <> b & a <> c implies ex o st b <_o, a & c <_o, a &
(b <_o, c iff b <_o9, c) & (c <_o, b iff c <_o9, b)
proof
assume
A1: a <> b & a <> c;
defpred P[Element of A,Element of A] means
($1 <> a & $1 <=_o9, $2) or $2 = a;
consider R being Relation of A such that
A2: for x,y holds [x,y] in R iff P[x,y] from RELSET_1:sch 2;
A3: now
let x,y;
P[x,y] or P[y,x] by Th4;
hence [x,y] in R or [y,x] in R by A2;
end;
now
let x,y,z;
assume [x,y] in R & [y,z] in R;
then ( P[x,y])& P[y,z] by A2;
then P[x,z] by Th5;
hence [x,z] in R by A2;
end;
then reconsider o = R as Element of LinPreorders A by A3,Def1;
take o;
A4: ( not [a,b] in R)& not [a,c] in R by A1,A2;
A5: not [c,b] in R iff b <_o9, c by A1,A2;
not [b,c] in R iff c <_o9, b by A1,A2;
hence thesis by A4,A5;
end;
theorem
for o,o9 being Element of LinOrders A holds
(a <_o, b iff a <_o9, b) & (b <_o, a iff b <_o9, a) iff
(a <_o, b iff a <_o9, b)
proof
let o,o9 be Element of LinOrders A;
thus (a <_o, b iff a <_o9, b) & (b <_o, a iff b <_o9, a) implies
(a <_o, b iff a <_o9, b);
assume
A1: a <_o, b iff a <_o9, b;
hence a <_o, b iff a <_o9, b;
hereby
assume
A2: b <_o, a;
then a <> b by Th4;
hence b <_o9, a by A1,A2,Th4,Th6;
end;
assume
A3: b <_o9, a;
then a <> b by Th4;
hence thesis by A1,A3,Th4,Th6;
end;
theorem Th13:
for o being Element of LinOrders A, o9 being Element of LinPreorders A holds
(for a,b st a <_o, b holds a <_o9, b) iff
for a,b holds a <_o, b iff a <_o9, b
proof
let o be Element of LinOrders A, o9 be Element of LinPreorders A;
hereby
assume
A1: for a,b st a <_o, b holds a <_o9, b;
let a,b;
per cases by Th6;
suppose
a <_o, b;
hence a <_o, b iff a <_o9, b by A1;
end;
suppose
a = b;
hence a <_o, b iff a <_o9, b by Th3;
end;
suppose
A2: b <_o, a;
then b <_o9, a by A1;
hence a <_o, b iff a <_o9, b by A2,Th4;
end;
end;
thus thesis;
end;
begin :: Arrow's theorem
:: version with weak orders, the one from the paper
reserve A,N for finite non empty set;
reserve a,b,c,d,a9,c9 for Element of A;
reserve i,n,nb,nc for Element of N;
reserve o,oI,oII for Element of LinPreorders A;
reserve p,p9,pI,pII,pI9,pII9 for Element of Funcs(N,LinPreorders A);
reserve f for Function of Funcs(N,LinPreorders A),LinPreorders A;
reserve k,k0 for Nat;
::$L https://en.wikipedia.org/wiki/Arrow's_impossibility_theorem Arrow's impossibility theorem
theorem Th14:
(for p,a,b st for i holds a <_p.i, b holds a <_f.p, b) & (for p,p9,a,b st
for i holds (a <_p.i, b iff a <_p9.i, b) & (b <_p.i, a iff b <_p9.i, a)
holds a <_f.p, b iff a <_f.p9, b) & card A >= 3 implies
ex n st for p,a,b st a <_p.n, b holds a <_f.p, b
proof
assume that
A1: for p,a,b st for i holds a <_p.i, b holds a <_f.p, b and
A2: for p,p9,a,b st
for i holds (a <_p.i, b iff a <_p9.i, b) & (b <_p.i, a iff b <_p9.i, a)
holds a <_f.p, b iff a <_f.p9, b and
A3: card A >= 3;
defpred extreme[Element of LinPreorders A,Element of A] means
(for a st a <> $2 holds $2 <_$1, a) or (for a st a <> $2 holds a <_$1, $2);
A4: for p,b st for i holds extreme[p.i,b] holds extreme[f.p,b]
proof
assume not thesis;
then consider p,b such that
A5: ex a st a <> b & a <=_f.p, b and
A6: ex c st c <> b & b <=_f.p, c and
A7: for i holds extreme[p.i,b];
consider a9 such that
A8: a9 <> b & a9 <=_f.p, b by A5;
consider c9 such that
A9: b <> c9 & b <=_f.p, c9 by A6;
ex a,c st a <> b & b <> c & a <> c & a <=_f.p, b & b <=_f.p, c
proof
per cases;
suppose
A10: a9 <> c9;
take a9,c9;
thus thesis by A8,A9,A10;
end;
suppose
A11: a9 = c9;
consider d such that
A12: d <> b & d <> a9 by A3,Th2;
per cases by Th4;
suppose
A13: d <=_f.p, b;
take d,c9;
thus thesis by A9,A11,A12,A13;
end;
suppose
A14: b <=_f.p, d;
take a9,d;
thus thesis by A8,A12,A14;
end;
end;
end;
then consider a,c such that
A15: a <> b & b <> c and
A16: a <> c and
A17: a <=_f.p, b & b <=_f.p, c;
defpred P[Element of N,Element of LinPreorders A] means
(a <_p.$1, b iff a <_$2, b) & (b <_p.$1, a iff b <_$2, a) &
(b <_p.$1, c iff b <_$2, c) & (c <_p.$1, b iff c <_$2, b) & c <_$2, a;
A18: for i holds ex o st P[i,o]
proof
let i;
per cases by A7;
suppose
for c st c <> b holds b <_p.i, c;
then A19: b <_p.i, a & b <_p.i, c by A15;
consider o such that
A20: b <_o, c & c <_o, a by A15,A16,Th7;
take o;
thus thesis by A19,A20,Th4,Th5;
end;
suppose
for a st a <> b holds a <_p.i, b;
then A21: a <_p.i, b & c <_p.i, b by A15;
consider o such that
A22: c <_o, a & a <_o, b by A15,A16,Th7;
take o;
thus thesis by A21,A22,Th4,Th5;
end;
end;
consider p9 being Function of N,LinPreorders A such that
A23: for i holds P[i,p9.i] from FUNCT_2:sch 3(A18);
reconsider 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;
end;
A24: for b holds ex nb,pI,pII st (for i st i <> nb holds pI.i = pII.i) &
(for i holds extreme[pI.i,b]) & (for i holds extreme[pII.i,b]) &
(for a st a <> b holds b <_pI.nb, a) &
(for a st a <> b holds a <_pII.nb, b) &
(for a st a <> b holds b <_f.pI, a) & for 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 as FinSequence of N by A25,FINSEQ_1:def 4;
let b;
consider oI such that
A27: for a st a <> b holds b <_oI, a by Th8;
consider oII such that
A28: for a st a <> b holds a <_oII, b by Th9;
A29: for k0 holds ex p st (for k st k in dom t & k < k0 holds p.(t.k) = oII) &
for k st k in dom t & k >= k0 holds p.(t.k) = oI
proof
let k0;
defpred P[Element of N,Element of LinPreorders A] means
ex k st k in dom t & $1 = t.k &
(k < k0 implies $2 = oII) & (k >= k0 implies $2 = oI);
A30: for i holds ex o st P[i,o]
proof
let i;
consider k being object such that
A31: k in dom t and
A32: i = t.k by A25,FUNCT_1:def 3;
reconsider k as Nat by A31;
per cases;
suppose
A33: k < k0;
take oII;
thus thesis by A31,A32,A33;
end;
suppose
A34: k >= k0;
take oI;
thus thesis by A31,A32,A34;
end;
end;
consider p being Function of N,LinPreorders A such that
A35: for i holds P[i,p.i] from FUNCT_2:sch 3(A30);
reconsider p as Element of Funcs(N,LinPreorders A) by FUNCT_2:8;
take p;
thus for k st k in dom t & k < k0 holds p.(t.k) = oII
proof
let k;
assume that
A36: k in dom t and
A37: k < k0;
reconsider i = t.k as Element of N by A36,PARTFUN1:4;
P[i,p.i] by A35;
hence thesis by A26,A36,A37,FUNCT_1:def 4;
end;
let k;
assume that
A38: k in dom t and
A39: k >= k0;
reconsider i = t.k as Element of N by A38,PARTFUN1:4;
P[i,p.i] by A35;
hence thesis by A26,A38,A39,FUNCT_1:def 4;
end;
defpred Q[Nat] means for p st
(for k st k in dom t & k < $1 holds p.(t.k) = oII) &
(for k st k in dom t & k >= $1 holds p.(t.k) = oI)
holds for a st a <> b holds a <_f.p, b;
reconsider kII9 = len t + 1 as Element of NAT by ORDINAL1:def 12;
A40: Q[kII9]
proof
let p;
assume that
A41: for k st k in dom t & k < kII9 holds p.(t.k) = oII
and for k st k in dom t & k >= kII9 holds p.(t.k) = oI;
let a;
assume
A42: a <> b;
for i holds a <_p.i, b
proof
let i;
consider k being object such that
A43: k in dom t and
A44: i = t.k by A25,FUNCT_1:def 3;
reconsider k as Nat by A43;
k <= len t by A43,FINSEQ_3:25;
then k + 0 < kII9 by XREAL_1:8;
then p.i = oII by A41,A43,A44;
hence thesis by A28,A42;
end;
hence thesis by A1;
end;
then A45: ex kII9 being Nat st Q[kII9];
consider kII being Nat such that
A46: Q[kII] & for k0 being Nat st Q[k0] holds k0 >= kII from NAT_1:sch 5(A45
);
consider pII such that
A47: for k st k in dom t & k < kII holds pII.(t.k) = oII and
A48: for k st k in dom t & k >= kII holds pII.(t.k) = oI by A29;
A49: kII > 1
proof
assume
A50: kII <= 1;
consider a such that
A51: a <> b by A3,Th1,XXREAL_0:2;
A52: for i holds b <_pII.i, a
proof
let i;
consider k being object such that
A53: k in dom t and
A54: i = t.k by A25,FUNCT_1:def 3;
reconsider k as Nat by A53;
k >= 1 by A53,FINSEQ_3:25;
then pII.i = oI by A48,A50,A53,A54,XXREAL_0:2;
hence thesis by A27,A51;
end;
A55: a <_f.pII, b by A46,A47,A48,A51;
b <_f.pII, a by A1,A52;
hence contradiction by A55,Th4;
end;
then reconsider kI = kII - 1 as Nat by NAT_1:20;
reconsider 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 such that
A60: for k st k in dom t & k < kI holds pI.(t.k) = oII and
A61: for k st k in dom t & k >= kI holds pI.(t.k) = oI and
A62: not(for a st a <> b holds a <_f.pI, b) by A46;
take nb,pI,pII;
thus for i st i <> nb holds pI.i = pII.i
proof
let i;
assume
A63: i <> nb;
consider k being object such that
A64: k in dom t and
A65: i = t.k by A25,FUNCT_1:def 3;
reconsider k as Nat by A64;
per cases by A63,A65,XXREAL_0:1;
suppose
k < kI;
then k + 0 < kII & pI.i = oII by A56,A60,A64,A65,XREAL_1:8;
hence thesis by A47,A64,A65;
end;
suppose
k > kI;
then k >= kII & pI.i = oI by A56,A61,A64,A65,INT_1:7;
hence thesis by A48,A64,A65;
end;
end;
thus
A66: for i holds extreme[pI.i,b]
proof
let i;
ex k being object st k in dom t & i = t.k by A25,FUNCT_1:def 3;
then pI.i = oII or pI.i = oI by A60,A61;
hence thesis by A27,A28;
end;
thus for i holds extreme[pII.i,b]
proof
let i;
ex k being object st k in dom t & i = t.k by A25,FUNCT_1:def 3;
then pII.i = oII or pII.i = oI by A47,A48;
hence thesis by A27,A28;
end;
pI.nb = oI by A58,A61;
hence for a st a <> b holds b <_pI.nb, a by A27;
pII.nb = oII by A47,A58,A59;
hence for a st a <> b holds a <_pII.nb, b by A28;
thus for a st a <> b holds b <_f.pI, a by A4,A62,A66;
thus thesis by A46,A47,A48;
end;
A67: for b holds ex nb,pI,pII st (for i st i <> nb holds pI.i = pII.i) &
(for i holds extreme[pI.i,b]) &
(for a st a <> b holds b <_f.pI, a) & (for a st a <> b holds a <_f.pII, b) &
for p,a,c st a <> b & c <> b & a <_p.nb, c holds a <_f.p, c
proof
let b;
consider nb,pI,pII such that
A68: for i st i <> nb holds pI.i = pII.i and
A69: for i holds extreme[pI.i,b] and
A70: for i holds extreme[pII.i,b] and
A71: for a st a <> b holds b <_pI.nb, a and
A72: for a st a <> b holds a <_pII.nb, b and
A73: (
for a st a <> b holds b <_f.pI, a)& for a st a <> b holds a <_f.pII, b
by A24;
take nb,pI,pII;
thus (for i st i <> nb holds pI.i = pII.i) &
(for i holds extreme[pI.i,b]) &
(for a st a <> b holds b <_f.pI, a) & for a st a <> b holds a <_f.pII, b
by A68,A69,A73;
let p,a,c;
assume that
A74: a <> b and
A75: c <> b and
A76: a <_p.nb, c;
A77: a <> c by A76,Th3;
defpred P[Element of N,Element of LinPreorders A] means
(a <_p.$1, c iff a <_$2, c) & (c <_p.$1, a iff c <_$2, a) &
($1 = nb implies a <_$2, b & b <_$2, c) & ($1 <> nb implies
((for d st d <> b holds b <_pII.$1, d) implies b <_$2, a & b <_$2, c) &
((for d st d <> b holds d <_pII.$1, b) implies a <_$2, b & c <_$2, b));
A78: for i holds ex o st P[i,o]
proof
let i;
per cases;
suppose
A79: i = nb;
consider o such that
A80: a <_o, b & b <_o, c by A74,A75,A77,Th7;
take o;
thus thesis by A76,A79,A80,Th4,Th5;
end;
suppose
A81: i <> nb;
per cases by A70;
suppose
for d st d <> b holds b <_pII.i, d;
then b <_pII.i, a by A74;
then A82: not a <_pII.i, b by Th4;
consider o such that
A83: b
<_o, a & b <_o, c & ( a <_o, c iff a <_p.i, c)&( c <_o, a iff c <_p.i,
a)
by A74,A75,Th10;
take o;
thus thesis by A74,A81,A82,A83;
end;
suppose
for d st d <> b holds d <_pII.i, b;
then a <_pII.i, b by A74;
then A84: not b <_pII.i, a by Th4;
consider o such that
A85: a
<_o, b & c <_o, b & ( a <_o, c iff a <_p.i, c)&( c <_o, a iff c <_p.i,
a)
by A74,A75,Th11;
take o;
thus thesis by A74,A81,A84,A85;
end;
end;
end;
consider pIII being Function of N,LinPreorders A such that
A86: for i holds P[i,pIII.i] from FUNCT_2:sch 3(A78);
reconsider pIII as Element of Funcs(N,LinPreorders A) by FUNCT_2:8;
for i holds (a <_pII.i, b iff a <_pIII.i, b) &
(b <_pII.i, a iff b <_pIII.i, a)
proof
let i;
per cases;
suppose
i = nb;
then a <_pII.i, b & a <_pIII.i, b by A72,A74,A86;
hence thesis by Th4;
end;
suppose
A87: i <> nb;
per cases by A70;
suppose
for d st d <> b holds b <_pII.i, d;
then b <_pII.i, a & b <_pIII.i, a by A74,A86,A87;
hence thesis by Th4;
end;
suppose
for d st d <> b holds d <_pII.i, b;
then a <_pII.i, b & a <_pIII.i, b by A74,A86,A87;
hence thesis by Th4;
end;
end;
end;
then A88: a <_f.pII, b iff a <_f.pIII, b by A2;
for
i holds (b <_pI.i, c iff b <_pIII.i, c) & (c <_pI.i, b iff c <_pIII.i, b )
proof
let i;
per cases;
suppose
i = nb;
then b <_pI.i, c & b <_pIII.i, c by A71,A75,A86;
hence thesis by Th4;
end;
suppose
A89: i <> nb;
per cases by A70;
suppose
A90: for d st d <> b holds b <_pII.i, d;
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 thesis by A91,Th4;
end;
suppose
A92: for d st d <> b holds d <_pII.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 thesis by A93,Th4;
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 thesis by A2,A86;
end;
set b = the Element of A;
consider nb,pI,pII such that
A94: for i st i <> nb holds pI.i = pII.i and
A95: for i holds extreme[pI.i,b] and
A96: (
for a st a <> b holds b <_f.pI, a)& for a st a <> b holds a <_f.pII, b and
A97: for p,a,c st a <> b & c <> b & a <_p.nb, c holds a <_f.p, c by A67;
take nb;
let p,a,a9;
assume
A98: a <_p.nb, a9;
then A99: a <> a9 by Th4;
per cases;
suppose
a <> b & a9 <> b;
hence thesis by A97,A98;
end;
suppose
A100: a = b or a9 = b;
consider c such that
A101: c <> a & c <> a9 by A3,Th2;
consider nc,pI9,pII9 such that
for i st i <> nc holds pI9.i = pII9.i and
for i holds extreme[pI9.i,c] and
for a st a <> c holds c <_f.pI9, a and
for a st a <> c holds a <_f.pII9, c and
A102: for p,a,a9 st a <> c & a9 <> c & a <_p.nc, a9 holds a <_f.p, a9 by A67;
nc = nb
proof
per cases by A100;
suppose
A103: a = b;
assume
A104: nc <> nb;
b <_pI.nc, a9 or a9 <_pI.nc, b by A95,A99,A103;
then b <_pII.nc, a9 & a9 <_f.pII, b or
a9 <_pI.nc, b & b <_f.pI, a9 by A94,A96,A99,A103,A104;
then b <_pII.nc, a9 & a9 <=_f.pII, b or
a9 <_pI.nc, b & b <=_f.pI, a9 by Th4;
hence contradiction by A101,A102,A103;
end;
suppose
A105: a9 = b;
assume
A106: nc <> nb;
b <_pI.nc, a or a <_pI.nc, b by A95,A99,A105;
then b <_pII.nc, a & a <_f.pII, b or
a <_pI.nc, b & b <_f.pI, a by A94,A96,A99,A105,A106;
then b <_pII.nc, a & a <=_f.pII, b or
a <_pI.nc, b & b <=_f.pI, a by Th4;
hence contradiction by A101,A102,A105;
end;
end;
hence thesis by A98,A101,A102;
end;
end;
:: and then a stronger version
reserve o,o1 for Element of LinOrders A;
reserve o9 for Element of LinPreorders A;
reserve p,p9 for Element of Funcs(N,LinOrders A);
reserve q,q9 for Element of Funcs(N,LinPreorders A);
reserve f for Function of Funcs(N,LinOrders A),LinPreorders A;
theorem
(for p,a,b st for i holds a <_p.i, b holds a <_f.p, b) & (for p,p9,a,b st
for i holds a <_p.i, b iff a <_p9.i, b holds a <_f.p, b iff a <_f.p9, b) &
card A >= 3 implies ex n st for p,a,b holds a <_p.n, b iff a <_f.p, b
proof
assume that
A1: for p,a,b st for i holds a <_p.i, b holds a <_f.p, b and
A2: for p,p9,a,b st for i holds a <_p.i, b iff a <_p9.i, b
holds a <_f.p, b iff a <_f.p9, b and
A3: card A >= 3;
set o = the Element of LinOrders A;
defpred O[Element of LinPreorders A,Element of A,Element of A] means
$2 <=_$1, $3 & ($2 <_$1, $3 or $2 <=_o, $3);
defpred P[Element of LinPreorders A,Element of LinOrders A] means
for a,b holds O[$1,a,b] iff a <=_$2, b;
A4: for o9 ex o1 st P[o9,o1]
proof
let o9;
defpred Q[Element of A,Element of A] means O[o9,$1,$2];
consider o1 being Relation of A such that
A5: for a,b holds [a,b] in o1 iff Q[a,b] from RELSET_1:sch 2;
A6: now
let a,b;
Q[a,b] or Q[b,a] by Th4;
hence [a,b] in o1 or [b,a] in o1 by A5;
end;
now
let a,b,c;
Q[a,b] & Q[b,c] implies Q[a,c] by Th5;
hence [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 by A5;
end;
then reconsider o1 as Element of LinPreorders A by A6,Def1;
now
let a,b;
Q[a,b] & Q[b,a] implies a = b by Th6;
hence [a,b] in o1 & [b,a] in o1 implies a = b by A5;
end;
then reconsider o1 as Element of LinOrders A by Def2;
take o1;
let a,b;
[a,b] in o1 iff Q[a,b] by A5;
hence thesis;
end;
defpred R[Element of Funcs(N,LinPreorders A),Element of Funcs(N,LinOrders A)]
means for i holds P[$1.i,$2.i];
A7: for q,p,p9 st R[q,p] & R[q,p9] holds p = p9
proof
let q,p,p9;
assume that
A8: R[q,p] and
A9: R[q,p9];
let i;
reconsider pi = p.i as Relation of A by Def1;
reconsider pi9 = p9.i as Relation of A by Def1;
now
let a,b;
A10: O[q.i,a,b] iff a <=_p.i, b by A8;
O[q.i,a,b] iff a <=_p9.i, b by A9;
hence [a,b] in p.i iff [a,b] in p9.i by A10;
end;
then pi = pi9 by RELSET_1:def 2;
hence p.i = p9.i;
end;
A11: for q ex p st R[q,p]
proof
let q;
defpred S[Element of N,Element of LinOrders A] means P[q.$1,$2];
A12: for i ex o1 st S[i,o1] by A4;
consider p being Function of N,LinOrders A such that
A13: for i holds S[i,p.i qua Element of LinOrders A] from FUNCT_2:sch 3(A12);
reconsider p as Element of Funcs(N,LinOrders A) by FUNCT_2:8;
take p;
thus thesis by A13;
end;
defpred T[Element of Funcs(N,LinPreorders A),Element of LinPreorders A] means
ex p st R[$1,p] & f.p = $2;
A14: for q ex o9 st T[q,o9]
proof
let q;
consider p such that
A15: R[q,p] by A11;
take f.p;
thus thesis by A15;
end;
consider f9 being Function of Funcs(N,LinPreorders A),LinPreorders A such that
A16: for q holds T[q,f9.q] from FUNCT_2:sch 3(A14);
A17: for q,a,b st for i holds a <_q.i, b holds a <_f9.q, b
proof
let q,a,b;
assume
A18: for i holds a <_q.i, b;
consider p such that
A19: R[q,p] and
A20: f.p = f9.q by A16;
now
let i;
not O[q.i,b,a] by A18;
hence a <_p.i, b by A19;
end;
hence thesis by A1,A20;
end;
now
let q,q9,a,b;
assume
A21: for i holds (a <_q.i, b iff a <_q9.i, b) & (b <_q.i, a iff b <_q9.i, a);
consider p such that
A22: R[q,p] and
A23: f.p = f9.q by A16;
consider p9 such that
A24: R[q9,p9] and
A25: f.p9 = f9.q9 by A16;
for i holds a <_p.i, b iff a <_p9.i, b
proof
let i;
O[q.i,b,a] iff O[q9.i,b,a] by A21;
hence thesis by A22,A24;
end;
hence a <_f9.q, b iff a <_f9.q9, b by A2,A23,A25;
end;
then consider n such that
A26: for q,a,b st a <_q.n, b holds a <_f9.q, b by A3,A17,Th14;
take n;
let p;
now
rng p c= LinOrders A by RELAT_1:def 19;
then dom p = N & rng p c= LinPreorders A by FUNCT_2:def 1,XBOOLE_1:1;
then
reconsider q = p as Element of Funcs(N,LinPreorders A) by FUNCT_2:def 2;
A27: R[q,p]
proof
let i;
let a,b;
a <_p.i, b or a = b or a >_p.i, b by Th6;
hence thesis by Th4;
end;
A28: ex p9 st ( R[q,p9])& f.p9 = f9.q by A16;
let a,b;
assume a <_p.n, b;
then a <_f9.q, b by A26;
hence a <_f.p, b by A7,A27,A28;
end;
hence thesis by Th13;
end;