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, 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 iff a <_ p' . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p',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, 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 iff a <_ p' . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p',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, 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 iff a <_ p' . i,b ) ) holds
( a <_ f . p,b iff a <_ f . p',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 )
consider o being 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 <=_ o,$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 o' being Element of LinPreorders A ex o1 being Element of LinOrders A st S2[o',o1]
proof
let o' be Element of LinPreorders A; :: thesis: ex o1 being Element of LinOrders A st S2[o',o1]
defpred S3[ Element of A, Element of A] means S1[o',$1,$2];
consider o1 being Relation of 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
let a, b be Element of A; :: thesis: ( [a,b] in o1 or [b,a] in o1 )
A7: ( S3[a,b] or S3[b,a] ) by Th4;
thus ( [a,b] in o1 or [b,a] in o1 ) by A5, A7; :: thesis: verum
end;
A8: now
let a, b, c be Element of A; :: thesis: ( [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 )
A9: ( S3[a,b] & S3[b,c] implies S3[a,c] ) by Th5;
thus ( [a,b] in o1 & [b,c] in o1 implies [a,c] in o1 ) by A5, A9; :: thesis: verum
end;
reconsider o1 = o1 as Element of LinPreorders A by A6, A8, Def1;
A10: now
let a, b be Element of A; :: thesis: ( [a,b] in o1 & [b,a] in o1 implies a = b )
A11: ( S3[a,b] & S3[b,a] implies a = b ) by Th6;
thus ( [a,b] in o1 & [b,a] in o1 implies a = b ) by A5, A11; :: thesis: verum
end;
reconsider o1 = o1 as Element of LinOrders A by A10, Def2;
take o1 ; :: thesis: S2[o',o1]
let a, b be Element of A; :: thesis: ( S1[o',a,b] iff a <=_ o1,b )
A12: ( [a,b] in o1 iff S3[a,b] ) by A5;
thus ( S1[o',a,b] iff a <=_ o1,b ) by A12, Def4; :: 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];
A13: for q being Element of Funcs N,(LinPreorders A)
for p, p' being Element of Funcs N,(LinOrders A) st S3[q,p] & S3[q,p'] holds
p = p'
proof
let q be Element of Funcs N,(LinPreorders A); :: thesis: for p, p' being Element of Funcs N,(LinOrders A) st S3[q,p] & S3[q,p'] holds
p = p'
let p, p' be Element of Funcs N,(LinOrders A); :: thesis: ( S3[q,p] & S3[q,p'] implies p = p' )
assume that
A14: S3[q,p] and
A15: S3[q,p'] ; :: thesis: p = p'
let i be Element of N; :: according to FUNCT_2:def 9 :: thesis: p . i = p' . i
reconsider pi = p . i as Relation of by Def1;
reconsider pi' = p' . i as Relation of by Def1;
A16: now
let a, b be Element of A; :: thesis: ( [a,b] in p . i iff [a,b] in p' . i )
A17: ( S1[q . i,a,b] iff a <=_ p . i,b ) by A14;
A18: ( S1[q . i,a,b] iff a <=_ p' . i,b ) by A15;
thus ( [a,b] in p . i iff [a,b] in p' . i ) by A17, A18, Def4; :: thesis: verum
end;
A19: pi = pi' by A16, RELSET_1:def 3;
thus p . i = p' . i by A19; :: thesis: verum
end;
A20: 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];
A21: 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
A22: for i being Element of N holds S4[i,p . i] from FUNCT_2:sch 3(A21);
 reconsider p = p as Element of Funcs N,(LinOrders A) by FUNCT_2:11;
take p ; :: thesis: S3[q,p]
thus S3[q,p] by A22; :: 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 );
A23: for q being Element of Funcs N,(LinPreorders A) ex o' being Element of LinPreorders A st S4[q,o']
proof
let q be Element of Funcs N,(LinPreorders A); :: thesis: ex o' being Element of LinPreorders A st S4[q,o']
consider p being Element of Funcs N,(LinOrders A) such that
A24: S3[q,p] by A20;
take f . p ; :: thesis: S4[q,f . p]
thus S4[q,f . p] by A24; :: thesis: verum
end;
consider f' being Function of Funcs N,(LinPreorders A), LinPreorders A such that
A25: for q being Element of Funcs N,(LinPreorders A) holds S4[q,f' . q] from FUNCT_2:sch 3(A23);
 A26: 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 <_ f' . 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 <_ f' . q,b
let a, b be Element of A; :: thesis: ( ( for i being Element of N holds a <_ q . i,b ) implies a <_ f' . q,b )
assume A27: for i being Element of N holds a <_ q . i,b ; :: thesis: a <_ f' . q,b
consider p being Element of Funcs N,(LinOrders A) such that
A28: S3[q,p] and
A29: f . p = f' . q by A25;
A30: now
let i be Element of N; :: thesis: a <_ p . i,b
A31: not S1[q . i,b,a] by A27;
thus a <_ p . i,b by A28, A31; :: thesis: verum
end;
thus a <_ f' . q,b by A1, A29, A30; :: thesis: verum
end;
A32: now
let q, 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 implies a <_ q' . i,b ) & ( a <_ q' . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q' . i,a ) & ( b <_ q' . i,a implies b <_ q . i,a ) ) ) holds
( a <_ f' . q,b iff a <_ f' . q',b )
let a, b be Element of A; :: thesis: ( ( for i being Element of N holds
( ( a <_ q . i,b implies a <_ q' . i,b ) & ( a <_ q' . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q' . i,a ) & ( b <_ q' . i,a implies b <_ q . i,a ) ) ) implies ( a <_ f' . q,b iff a <_ f' . q',b ) )
assume A33: for i being Element of N holds
( ( a <_ q . i,b implies a <_ q' . i,b ) & ( a <_ q' . i,b implies a <_ q . i,b ) & ( b <_ q . i,a implies b <_ q' . i,a ) & ( b <_ q' . i,a implies b <_ q . i,a ) ) ; :: thesis: ( a <_ f' . q,b iff a <_ f' . q',b )
consider p being Element of Funcs N,(LinOrders A) such that
A34: S3[q,p] and
A35: f . p = f' . q by A25;
consider p' being Element of Funcs N,(LinOrders A) such that
A36: S3[q',p'] and
A37: f . p' = f' . q' by A25;
A38: for i being Element of N holds
( a <_ p . i,b iff a <_ p' . i,b )
proof
let i be Element of N; :: thesis: ( a <_ p . i,b iff a <_ p' . i,b )
A39: ( S1[q . i,b,a] iff S1[q' . i,b,a] ) by A33;
thus ( a <_ p . i,b iff a <_ p' . i,b ) by A34, A36, A39; :: thesis: verum
end;
thus ( a <_ f' . q,b iff a <_ f' . q',b ) by A2, A35, A37, A38; :: thesis: verum
end;
consider n being Element of N such that
A40: for q being Element of Funcs N,(LinPreorders A)
for a, b being Element of A st a <_ q . n,b holds
a <_ f' . q,b by A3, A26, A32, 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 )
A41: now
A42: rng p c= LinOrders A by RELAT_1:def 19;
A43: ( dom p = N & rng p c= LinPreorders A ) by A42, FUNCT_2:def 1, XBOOLE_1:1;
reconsider q = p as Element of Funcs N,(LinPreorders A) by A43, FUNCT_2:def 2;
A44: 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 )
A45: ( a <_ p . i,b or a = b or a >_ p . i,b ) by Th6;
thus ( S1[q . i,a,b] iff a <=_ p . i,b ) by A45, Th4; :: thesis: verum
end;
A46: ex p' being Element of Funcs N,(LinOrders A) st
( S3[q,p'] & f . p' = f' . q ) by A25;
let a, b be Element of A; :: thesis: ( a <_ p . n,b implies a <_ f . p,b )
assume A47: a <_ p . n,b ; :: thesis: a <_ f . p,b
A48: a <_ f' . q,b by A40, A47;
thus a <_ f . p,b by A13, A44, A46, A48; :: thesis: verum
end;
thus for a, b being Element of A holds
( a <_ p . n,b iff a <_ f . p,b ) by A41, Th13; :: thesis: verum