let I be set ; :: thesis: for M being V8() V39() ManySortedSet of I st ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ) holds
ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
K c= m ) )
let M be V8() V39() ManySortedSet of I; :: thesis: ( ( for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ) implies ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
K c= m ) ) )
assume A1: for A, B being ManySortedSet of I st A in M & B in M & not A c= B holds
B c= A ; :: thesis: ex m being ManySortedSet of I st
( m in M & ( for K being ManySortedSet of I st K in M holds
K c= m ) )
defpred S1[ object , object ] means ex X being set st
( X = $2 & $2 in M . $1 & ( for D9 being set st D9 in M . $1 holds
D9 c= X ) );
A2: for i being object st i in I holds
ex j being object st S1[i,j]
proof
let i be object ; :: thesis: ( i in I implies ex j being object st S1[i,j] )
assume A3: i in I ; :: thesis: ex j being object st S1[i,j]
M . i is c=-linear
proof
consider c9 being ManySortedSet of I such that
A4: c9 in M by PBOOLE:134;
consider b9 being ManySortedSet of I such that
A5: b9 in M by PBOOLE:134;
let B9, C9 be set ; :: according to ORDINAL1:def 8 :: thesis: ( not B9 in M . i or not C9 in M . i or B9,C9 are_c=-comparable )
assume that
A6: B9 in M . i and
A7: C9 in M . i ; :: thesis: B9,C9 are_c=-comparable
A8: dom (i .--> B9) = {i} ;
set qc = c9 +* (i .--> C9);
dom (c9 +* (i .--> C9)) = I by A3, PZFMISC1:1;
then reconsider qc = c9 +* (i .--> C9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A9: dom (i .--> C9) = {i} ;
i in {i} by TARSKI:def 1;
then A10: qc . i = (i .--> C9) . i by A9, FUNCT_4:13
.= C9 by FUNCOP_1:72 ;
A11: qc in M
proof
let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or qc . j in M . j )
assume A12: j in I ; :: thesis: qc . j in M . j
now :: thesis: ( ( j = i & qc . j in M . j ) or ( j <> i & qc . j in M . j ) )
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: qc . j in M . j
hence qc . j in M . j by A7, A10; :: thesis: verum
end;
case j <> i ; :: thesis: qc . j in M . j
then not j in dom (i .--> C9) by TARSKI:def 1;
then qc . j = c9 . j by FUNCT_4:11;
hence qc . j in M . j by A4, A12; :: thesis: verum
end;
end;
end;
hence qc . j in M . j ; :: thesis: verum
end;
set qb = b9 +* (i .--> B9);
dom (b9 +* (i .--> B9)) = I by A3, PZFMISC1:1;
then reconsider qb = b9 +* (i .--> B9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
assume A13: not B9 c= C9 ; :: according to XBOOLE_0:def 9 :: thesis: C9 c= B9
i in {i} by TARSKI:def 1;
then A14: qb . i = (i .--> B9) . i by A8, FUNCT_4:13
.= B9 by FUNCOP_1:72 ;
qb in M
proof
let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or qb . j in M . j )
assume A15: j in I ; :: thesis: qb . j in M . j
now :: thesis: ( ( j = i & qb . j in M . j ) or ( j <> i & qb . j in M . j ) )
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: qb . j in M . j
hence qb . j in M . j by A6, A14; :: thesis: verum
end;
case j <> i ; :: thesis: qb . j in M . j
then not j in dom (i .--> B9) by TARSKI:def 1;
then qb . j = b9 . j by FUNCT_4:11;
hence qb . j in M . j by A5, A15; :: thesis: verum
end;
end;
end;
hence qb . j in M . j ; :: thesis: verum
end;
then ( qb c= qc or qc c= qb ) by A1, A11;
hence C9 c= B9 by A3, A13, A14, A10; :: thesis: verum
end;
then consider m9 being set such that
A16: ( m9 in M . i & ( for D9 being set st D9 in M . i holds
D9 c= m9 ) ) by A3, FINSET_1:12;
take m9 ; :: thesis: S1[i,m9]
thus S1[i,m9] by A16; :: thesis: verum
end;
consider m being ManySortedSet of I such that
A17: for i being object st i in I holds
S1[i,m . i] from PBOOLE:sch 3(A2);
 take m ; :: thesis: ( m in M & ( for K being ManySortedSet of I st K in M holds
K c= m ) )
thus m in M :: thesis: for K being ManySortedSet of I st K in M holds
K c= m
proof
let i be object ; :: according to PBOOLE:def 1 :: thesis: ( not i in I or m . i in M . i )
assume i in I ; :: thesis: m . i in M . i
then S1[i,m . i] by A17;
hence m . i in M . i ; :: thesis: verum
end;
thus for K being ManySortedSet of I st K in M holds
K c= m :: thesis: verum
proof
let K be ManySortedSet of I; :: thesis: ( K in M implies K c= m )
assume A18: K in M ; :: thesis: K c= m
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or K . i c= m . i )
assume A19: i in I ; :: thesis: K . i c= m . i
then A20: K . i in M . i by A18;
S1[i,m . i] by A17, A19;
hence K . i c= m . i by A20; :: thesis: verum
end;