let A, N be non empty finite set ; :: thesis: for f being Function of (Funcs (N,(LinOrders A))),(LinPreorders A) st ( for p being Element of Funcs (N,(LinOrders 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,(LinOrders A))
for a, b being Element of A st ( for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b ) ) 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,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
let f be Function of (Funcs (N,(LinOrders A))),(LinPreorders A); :: thesis: ( ( for p being Element of Funcs (N,(LinOrders 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,(LinOrders A))
for a, b being Element of A st ( for i being Element of N 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 being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b ) )
assume that
A1: for p being Element of Funcs (N,(LinOrders 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,(LinOrders A))
for a, b being Element of A st ( for i being Element of N 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 ; :: thesis: ex n being Element of N st
for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
set o = the Element of LinOrders A;
defpred S1[ Element of LinPreorders A, Element of A, Element of A] means ( $2 <=_ $1,$3 & ( $2 <_ $1,$3 or $2 <=_ the Element of LinOrders A,$3 ) );
defpred S2[ Element of LinPreorders A, Element of LinOrders A] means for a, b being Element of A holds
( S1[$1,a,b] iff a <=_ $2,b );
A4: for o9 being Element of LinPreorders A ex o1 being Element of LinOrders A st S2[o9,o1]
proof
let o9 be Element of LinPreorders A; :: thesis: ex o1 being Element of LinOrders A st S2[o9,o1]
defpred S3[ Element of A, Element of A] means S1[o9,$1,$2];
consider o1 being Relation of A such that
A5: for a, b being Element of A holds
( [a,b] in o1 iff S3[a,b] ) from RELSET_1:sch 2();
A6: now :: thesis: for a, b being Element of A holds
( [a,b] in o1 or [b,a] in o1 )
let a, b be Element of A; :: thesis: ( [a,b] in o1 or [b,a] in o1 )
( S3[a,b] or S3[b,a] ) by Th4;
hence ( [a,b] in o1 or [b,a] in o1 ) by A5; :: thesis: verum
end;
now :: thesis: for a, b, c being Element of A st [a,b] in o1 & [b,c] in o1 holds
[a,c] in o1
let a, b, c be Element of A; :: thesis: ( [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 )
( S3[a,b] & S3[b,c] implies S3[a,c] ) by Th5;
hence ( [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 ) by A5; :: thesis: verum
end;
then reconsider o1 = o1 as Element of LinPreorders A by A6, Def1;
now :: thesis: for a, b being Element of A st [a,b] in o1 & [b,a] in o1 holds
a = b
let a, b be Element of A; :: thesis: ( [a,b] in o1 & [b,a] in o1 implies a = b )
( S3[a,b] & S3[b,a] implies a = b ) by Th6;
hence ( [a,b] in o1 & [b,a] in o1 implies a = b ) by A5; :: thesis: verum
end;
then reconsider o1 = o1 as Element of LinOrders A by Def2;
take o1 ; :: thesis: S2[o9,o1]
let a, b be Element of A; :: thesis: ( S1[o9,a,b] iff a <=_ o1,b )
( [a,b] in o1 iff S3[a,b] ) by A5;
hence ( S1[o9,a,b] iff a <=_ o1,b ) ; :: thesis: verum
end;
defpred S3[ Element of Funcs (N,(LinPreorders A)), Element of Funcs (N,(LinOrders A))] means for i being Element of N holds S2[$1 . i,$2 . i];
A7: for q being Element of Funcs (N,(LinPreorders A))
for p, p9 being Element of Funcs (N,(LinOrders A)) st S3[q,p] & S3[q,p9] holds
p = p9
proof
let q be Element of Funcs (N,(LinPreorders A)); :: thesis: for p, p9 being Element of Funcs (N,(LinOrders A)) st S3[q,p] & S3[q,p9] holds
p = p9
let p, p9 be Element of Funcs (N,(LinOrders A)); :: thesis: ( S3[q,p] & S3[q,p9] implies p = p9 )
assume that
A8: S3[q,p] and
A9: S3[q,p9] ; :: thesis: p = p9
let i be Element of N; :: according to FUNCT_2:def 8 :: thesis: p . i = p9 . i
reconsider pi = p . i as Relation of A by Def1;
reconsider pi9 = p9 . i as Relation of A by Def1;
now :: thesis: for a, b being Element of A holds
( [a,b] in p . i iff [a,b] in p9 . i )
let a, b be Element of A; :: thesis: ( [a,b] in p . i iff [a,b] in p9 . i )
A10: ( S1[q . i,a,b] iff a <=_ p . i,b ) by A8;
( S1[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; :: thesis: verum
end;
then pi = pi9 by RELSET_1:def 2;
hence p . i = p9 . i ; :: thesis: verum
end;
A11: for q being Element of Funcs (N,(LinPreorders A)) ex p being Element of Funcs (N,(LinOrders A)) st S3[q,p]
proof
let q be Element of Funcs (N,(LinPreorders A)); :: thesis: ex p being Element of Funcs (N,(LinOrders A)) st S3[q,p]
defpred S4[ Element of N, Element of LinOrders A] means S2[q . $1,$2];
A12: for i being Element of N ex o1 being Element of LinOrders A st S4[i,o1] by A4;
consider p being Function of N,(LinOrders A) such that
A13: for i being Element of N holds S4[i,p . i] from FUNCT_2:sch 3(A12);
 reconsider p = p as Element of Funcs (N,(LinOrders A)) by FUNCT_2:8;
take p ; :: thesis: S3[q,p]
thus S3[q,p] by A13; :: thesis: verum
end;
defpred S4[ Element of Funcs (N,(LinPreorders A)), Element of LinPreorders A] means ex p being Element of Funcs (N,(LinOrders A)) st
( S3[$1,p] & f . p = $2 );
A14: for q being Element of Funcs (N,(LinPreorders A)) ex o9 being Element of LinPreorders A st S4[q,o9]
proof
let q be Element of Funcs (N,(LinPreorders A)); :: thesis: ex o9 being Element of LinPreorders A st S4[q,o9]
consider p being Element of Funcs (N,(LinOrders A)) such that
A15: S3[q,p] by A11;
take f . p ; :: thesis: S4[q,f . p]
thus S4[q,f . p] by A15; :: thesis: verum
end;
consider f9 being Function of (Funcs (N,(LinPreorders A))),(LinPreorders A) such that
A16: for q being Element of Funcs (N,(LinPreorders A)) holds S4[q,f9 . q] from FUNCT_2:sch 3(A14);
 A17: for q being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds a <_ q . i,b ) holds
a <_ f9 . q,b
proof
let q be Element of Funcs (N,(LinPreorders A)); :: thesis: for a, b being Element of A st ( for i being Element of N holds a <_ q . i,b ) holds
a <_ f9 . q,b
let a, b be Element of A; :: thesis: ( ( for i being Element of N holds a <_ q . i,b ) implies a <_ f9 . q,b )
assume A18: for i being Element of N holds a <_ q . i,b ; :: thesis: a <_ f9 . q,b
consider p being Element of Funcs (N,(LinOrders A)) such that
A19: S3[q,p] and
A20: f . p = f9 . q by A16;
now :: thesis: for i being Element of N holds a <_ p . i,b
let i be Element of N; :: thesis: a <_ p . i,b
not S1[q . i,b,a] by A18;
hence a <_ p . i,b by A19; :: thesis: verum
end;
hence a <_ f9 . q,b by A1, A20; :: thesis: verum
end;
now :: thesis: for q, q9 being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st ( for i being Element of N holds
( ( a <_ q . i,b implies a <_ q9 . i,b ) & ( a <_ q9 . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q9 . i,a ) & ( b <_ q9 . i,a implies b <_ q . i,a ) ) ) holds
( a <_ f9 . q,b iff a <_ f9 . q9,b )
let q, q9 be Element of Funcs (N,(LinPreorders A)); :: thesis: for a, b being Element of A st ( for i being Element of N holds
( ( a <_ q . i,b implies a <_ q9 . i,b ) & ( a <_ q9 . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q9 . i,a ) & ( b <_ q9 . i,a implies b <_ q . i,a ) ) ) holds
( a <_ f9 . q,b iff a <_ f9 . q9,b )
let a, b be Element of A; :: thesis: ( ( for i being Element of N holds
( ( a <_ q . i,b implies a <_ q9 . i,b ) & ( a <_ q9 . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q9 . i,a ) & ( b <_ q9 . i,a implies b <_ q . i,a ) ) ) implies ( a <_ f9 . q,b iff a <_ f9 . q9,b ) )
assume A21: for i being Element of N holds
( ( a <_ q . i,b implies a <_ q9 . i,b ) & ( a <_ q9 . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q9 . i,a ) & ( b <_ q9 . i,a implies b <_ q . i,a ) ) ; :: thesis: ( a <_ f9 . q,b iff a <_ f9 . q9,b )
consider p being Element of Funcs (N,(LinOrders A)) such that
A22: S3[q,p] and
A23: f . p = f9 . q by A16;
consider p9 being Element of Funcs (N,(LinOrders A)) such that
A24: S3[q9,p9] and
A25: f . p9 = f9 . q9 by A16;
for i being Element of N holds
( a <_ p . i,b iff a <_ p9 . i,b )
proof
let i be Element of N; :: thesis: ( a <_ p . i,b iff a <_ p9 . i,b )
( S1[q . i,b,a] iff S1[q9 . i,b,a] ) by A21;
hence ( a <_ p . i,b iff a <_ p9 . i,b ) by A22, A24; :: thesis: verum
end;
hence ( a <_ f9 . q,b iff a <_ f9 . q9,b ) by A2, A23, A25; :: thesis: verum
end;
then consider n being Element of N such that
A26: for q being Element of Funcs (N,(LinPreorders A))
for a, b being Element of A st a <_ q . n,b holds
a <_ f9 . q,b by A3, A17, Th14;
take n ; :: thesis: for p being Element of Funcs (N,(LinOrders A))
for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
let p be Element of Funcs (N,(LinOrders A)); :: thesis: for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b )
now :: thesis: for a, b being Element of A st a <_ p . n,b holds
a <_ f . p,b
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: S3[q,p]
proof
let i be Element of N; :: thesis: S2[q . i,p . i]
let a, b be Element of A; :: thesis: ( S1[q . i,a,b] iff a <=_ p . i,b )
( a <_ p . i,b or a = b or a >_ p . i,b ) by Th6;
hence ( S1[q . i,a,b] iff a <=_ p . i,b ) by Th4; :: thesis: verum
end;
A28: ex p9 being Element of Funcs (N,(LinOrders A)) st
( S3[q,p9] & f . p9 = f9 . q ) by A16;
let a, b be Element of A; :: thesis: ( a <_ p . n,b implies a <_ f . p,b )
assume a <_ p . n,b ; :: thesis: a <_ f . p,b
then a <_ f9 . q,b by A26;
hence a <_ f . p,b by A7, A27, A28; :: thesis: verum
end;
hence for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b ) by Th13; :: thesis: verum