let I be set ; :: thesis: for X, Y being ManySortedSet of I holds
( X = bool Y iff for A being ManySortedSet of I holds
( A in X iff A c= Y ) )
let X, Y be ManySortedSet of I; :: thesis: ( X = bool Y iff for A being ManySortedSet of I holds
( A in X iff A c= Y ) )
thus ( X = bool Y implies for A being ManySortedSet of I holds
( A in X iff A c= Y ) ) :: thesis: ( ( for A being ManySortedSet of I holds
( A in X iff A c= Y ) ) implies X = bool Y )
proof
assume A1: X = bool Y ; :: thesis: for A being ManySortedSet of I holds
( A in X iff A c= Y )
let A be ManySortedSet of I; :: thesis: ( A in X iff A c= Y )
thus ( A in X implies A c= Y ) :: thesis: ( A c= Y implies A in X )
proof
assume A2: A in X ; :: thesis: A c= Y
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or A . i c= Y . i )
assume A3: i in I ; :: thesis: A . i c= Y . i
then A4: A . i in X . i by A2, PBOOLE:def 4;
X . i = bool (Y . i) by A1, A3, Def1;
hence A . i c= Y . i by A4; :: thesis: verum
end;
assume A5: A c= Y ; :: thesis: A in X
let i be set ; :: according to PBOOLE:def 4 :: thesis: ( not i in I or A . i in X . i )
assume A6: i in I ; :: thesis: A . i in X . i
then A7: A . i c= Y . i by A5, PBOOLE:def 5;
X . i = bool (Y . i) by A1, A6, Def1;
hence A . i in X . i by A7; :: thesis: verum
end;
assume A8: for A being ManySortedSet of I holds
( A in X iff A c= Y ) ; :: thesis: X = bool Y
now
let i be set ; :: thesis: ( i in I implies X . i = (bool Y) . i )
assume A9: i in I ; :: thesis: X . i = (bool Y) . i
[[0]] I c= Y by PBOOLE:49;
then A10: [[0]] I in X by A8;
for A9 being set holds
( A9 in X . i iff A9 c= Y . i )
proof
let A9 be set ; :: thesis: ( A9 in X . i iff A9 c= Y . i )
A11: dom (i .--> A9) = {i} by FUNCOP_1:19;
dom (([[0]] I) +* (i .--> A9)) = I by A9, Lm1;
then reconsider K = ([[0]] I) +* (i .--> A9) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
i in {i} by TARSKI:def 1;
then A12: K . i = (i .--> A9) . i by A11, FUNCT_4:14
.= A9 by FUNCOP_1:87 ;
thus ( A9 in X . i implies A9 c= Y . i ) :: thesis: ( A9 c= Y . i implies A9 in X . i )
proof
assume A13: A9 in X . i ; :: thesis: A9 c= Y . i
K in X
proof
let j be set ; :: according to PBOOLE:def 4 :: thesis: ( not j in I or K . j in X . j )
assume A14: j in I ; :: thesis: K . j in X . j
now
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: K . j in X . j
hence K . j in X . j by A12, A13; :: thesis: verum
end;
end;
end;
hence K . j in X . j ; :: thesis: verum
end;
then K c= Y by A8;
hence A9 c= Y . i by A9, A12, PBOOLE:def 5; :: thesis: verum
end;
assume A15: A9 c= Y . i ; :: thesis: A9 in X . i
K c= Y
proof
let j be set ; :: according to PBOOLE:def 5 :: thesis: ( not j in I or K . j c= Y . j )
assume A16: j in I ; :: thesis: K . j c= Y . j
now
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: K . j c= Y . j
hence K . j c= Y . j by A12, A15; :: thesis: verum
end;
end;
end;
hence K . j c= Y . j ; :: thesis: verum
end;
then K in X by A8;
hence A9 in X . i by A9, A12, PBOOLE:def 4; :: thesis: verum
end;
then X . i = bool (Y . i) by ZFMISC_1:def 1;
hence X . i = (bool Y) . i by A9, Def1; :: thesis: verum
end;
hence X = bool Y by PBOOLE:3; :: thesis: verum