:: MBOOLEAN semantic presentation
begin
definition
let I be set ;
let A be ManySortedSet of I;
func bool A -> ManySortedSet of I means :Def1: :: MBOOLEAN:def 1
for i being set st i in I holds
it . i = bool (A . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = bool (A . i)
proof
deffunc H1( set ) -> set = bool (A . $1);
thus ex X being ManySortedSet of I st
for i being set st i in I holds
X . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = bool (A . i) ) & ( for i being set st i in I holds
b2 . i = bool (A . i) ) holds
b1 = b2
proof
let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = bool (A . i) ) & ( for i being set st i in I holds
Y . i = bool (A . i) ) implies X = Y )
assume that
A1: for i being set st i in I holds
X . i = bool (A . i) and
A2: for i being set st i in I holds
Y . i = bool (A . i) ; ::_thesis: X = Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A3: i in I ; ::_thesis: X . i = Y . i
hence X . i = bool (A . i) by A1
.= Y . i by A2, A3 ;
::_thesis: verum
end;
hence X = Y by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines bool MBOOLEAN:def_1_:_
for I being set
for A, b3 being ManySortedSet of I holds
( b3 = bool A iff for i being set st i in I holds
b3 . i = bool (A . i) );
registration
let I be set ;
let A be ManySortedSet of I;
cluster bool A -> V2() ;
coherence
bool A is non-empty
proof
let i be set ; :: according to PBOOLE:def_13 ::_thesis: ( not i in I or not (bool A) . i is empty )
assume A1: i in I ; ::_thesis: not (bool A) . i is empty
not bool (A . i) is empty ;
hence not (bool A) . i is empty by A1, Def1; ::_thesis: verum
end;
end;
Lm1: for i, I, X being set
for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
proof
let i, I, X be set ; ::_thesis: for M being ManySortedSet of I st i in I holds
dom (M +* (i .--> X)) = I
let M be ManySortedSet of I; ::_thesis: ( i in I implies dom (M +* (i .--> X)) = I )
assume A1: i in I ; ::_thesis: dom (M +* (i .--> X)) = I
thus dom (M +* (i .--> X)) = (dom M) \/ (dom (i .--> X)) by FUNCT_4:def_1
.= I \/ (dom (i .--> X)) by PARTFUN1:def_2
.= I \/ {i} by FUNCOP_1:13
.= I by A1, ZFMISC_1:40 ; ::_thesis: verum
end;
Lm2: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A \/ B)) . i = bool ((A . i) \/ (B . i))
hence (bool (A \/ B)) . i = bool ((A \/ B) . i) by Def1
.= bool ((A . i) \/ (B . i)) by A1, PBOOLE:def_4 ;
::_thesis: verum
end;
Lm3: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A /\ B)) . i = bool ((A . i) /\ (B . i))
hence (bool (A /\ B)) . i = bool ((A /\ B) . i) by Def1
.= bool ((A . i) /\ (B . i)) by A1, PBOOLE:def_5 ;
::_thesis: verum
end;
Lm4: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A \ B)) . i = bool ((A . i) \ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A \ B)) . i = bool ((A . i) \ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A \ B)) . i = bool ((A . i) \ (B . i))
hence (bool (A \ B)) . i = bool ((A \ B) . i) by Def1
.= bool ((A . i) \ (B . i)) by A1, PBOOLE:def_6 ;
::_thesis: verum
end;
Lm5: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
let i be set ; ::_thesis: ( i in I implies (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) )
assume A1: i in I ; ::_thesis: (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i))
hence (bool (A \+\ B)) . i = bool ((A \+\ B) . i) by Def1
.= bool ((A . i) \+\ (B . i)) by A1, PBOOLE:4 ;
::_thesis: verum
end;
theorem Th1: :: MBOOLEAN:1
for I being set
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 ) )
proof
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_2 ::_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_1;
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_1 ::_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_2;
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__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_(bool_Y)_._i
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:43;
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:13;
dom (([[0]] I) +* (i .--> A9)) = I by A9, Lm1;
then reconsider K = ([[0]] I) +* (i .--> A9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
i in {i} by TARSKI:def_1;
then A12: K . i = (i .--> A9) . i by A11, FUNCT_4:13
.= A9 by FUNCOP_1:72 ;
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_1 ::_thesis: ( not j in I or K . j in X . j )
assume A14: j in I ; ::_thesis: K . j in X . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_X_._j_)_or_(_j_<>_i_&_K_._j_in_X_._j_)_)
percases ( 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;
case j <> i ; ::_thesis: K . j in X . j
then not j in dom (i .--> A9) by A11, TARSKI:def_1;
then K . j = ([[0]] I) . j by FUNCT_4:11;
hence K . j in X . j by A10, A14, PBOOLE:def_1; ::_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_2; ::_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_2 ::_thesis: ( not j in I or K . j c= Y . j )
assume A16: j in I ; ::_thesis: K . j c= Y . j
now__::_thesis:_(_(_j_=_i_&_K_._j_c=_Y_._j_)_or_(_j_<>_i_&_K_._j_c=_Y_._j_)_)
percases ( 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;
case j <> i ; ::_thesis: K . j c= Y . j
then not j in dom (i .--> A9) by A11, TARSKI:def_1;
then A17: K . j = ([[0]] I) . j by FUNCT_4:11;
[[0]] I c= Y by PBOOLE:43;
hence K . j c= Y . j by A16, A17, PBOOLE:def_2; ::_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_1; ::_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
end;
theorem :: MBOOLEAN:2
for I being set holds bool ([[0]] I) = I --> {{}}
proof
let I be set ; ::_thesis: bool ([[0]] I) = I --> {{}}
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_([[0]]_I))_._i_=_(I_-->_{{}})_._i
let i be set ; ::_thesis: ( i in I implies (bool ([[0]] I)) . i = (I --> {{}}) . i )
assume A1: i in I ; ::_thesis: (bool ([[0]] I)) . i = (I --> {{}}) . i
then (bool ([[0]] I)) . i = bool (([[0]] I) . i) by Def1
.= {{}} by PBOOLE:5, ZFMISC_1:1 ;
hence (bool ([[0]] I)) . i = (I --> {{}}) . i by A1, FUNCOP_1:7; ::_thesis: verum
end;
hence bool ([[0]] I) = I --> {{}} by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:3
for I, x being set holds bool (I --> x) = I --> (bool x)
proof
let I, x be set ; ::_thesis: bool (I --> x) = I --> (bool x)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_(I_-->_x))_._i_=_(I_-->_(bool_x))_._i
let i be set ; ::_thesis: ( i in I implies (bool (I --> x)) . i = (I --> (bool x)) . i )
assume A1: i in I ; ::_thesis: (bool (I --> x)) . i = (I --> (bool x)) . i
hence (bool (I --> x)) . i = bool ((I --> x) . i) by Def1
.= bool x by A1, FUNCOP_1:7
.= (I --> (bool x)) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence bool (I --> x) = I --> (bool x) by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:4
for I, x being set holds bool (I --> {x}) = I --> {{},{x}}
proof
let I, x be set ; ::_thesis: bool (I --> {x}) = I --> {{},{x}}
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_(I_-->_{x}))_._i_=_(I_-->_{{},{x}})_._i
let i be set ; ::_thesis: ( i in I implies (bool (I --> {x})) . i = (I --> {{},{x}}) . i )
assume A1: i in I ; ::_thesis: (bool (I --> {x})) . i = (I --> {{},{x}}) . i
hence (bool (I --> {x})) . i = bool ((I --> {x}) . i) by Def1
.= bool {x} by A1, FUNCOP_1:7
.= {{},{x}} by ZFMISC_1:24
.= (I --> {{},{x}}) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence bool (I --> {x}) = I --> {{},{x}} by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:5
for I being set
for A being ManySortedSet of I holds [[0]] I c= A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds [[0]] I c= A
let A be ManySortedSet of I; ::_thesis: [[0]] I c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ([[0]] I) . i c= A . i )
assume i in I ; ::_thesis: ([[0]] I) . i c= A . i
([[0]] I) . i = {} by PBOOLE:5;
hence ([[0]] I) . i c= A . i by XBOOLE_1:2; ::_thesis: verum
end;
theorem :: MBOOLEAN:6
for I being set
for A, B being ManySortedSet of I st A c= B holds
bool A c= bool B
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A c= B holds
bool A c= bool B
let A, B be ManySortedSet of I; ::_thesis: ( A c= B implies bool A c= bool B )
assume A1: A c= B ; ::_thesis: bool A c= bool B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (bool A) . i c= (bool B) . i )
assume A2: i in I ; ::_thesis: (bool A) . i c= (bool B) . i
then A3: A . i c= B . i by A1, PBOOLE:def_2;
( (bool A) . i = bool (A . i) & (bool B) . i = bool (B . i) ) by A2, Def1;
hence (bool A) . i c= (bool B) . i by A3, ZFMISC_1:67; ::_thesis: verum
end;
theorem :: MBOOLEAN:7
for I being set
for A, B being ManySortedSet of I holds (bool A) \/ (bool B) c= bool (A \/ B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (bool A) \/ (bool B) c= bool (A \/ B)
let A, B be ManySortedSet of I; ::_thesis: (bool A) \/ (bool B) c= bool (A \/ B)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i )
assume A1: i in I ; ::_thesis: ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i
then A2: (bool (A \/ B)) . i = bool ((A . i) \/ (B . i)) by Lm2;
((bool A) \/ (bool B)) . i = ((bool A) . i) \/ ((bool B) . i) by A1, PBOOLE:def_4
.= (bool (A . i)) \/ ((bool B) . i) by A1, Def1
.= (bool (A . i)) \/ (bool (B . i)) by A1, Def1 ;
hence ((bool A) \/ (bool B)) . i c= (bool (A \/ B)) . i by A2, ZFMISC_1:69; ::_thesis: verum
end;
theorem :: MBOOLEAN:8
for I being set
for A, B being ManySortedSet of I st (bool A) \/ (bool B) = bool (A \/ B) holds
for i being set st i in I holds
A . i,B . i are_c=-comparable
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st (bool A) \/ (bool B) = bool (A \/ B) holds
for i being set st i in I holds
A . i,B . i are_c=-comparable
let A, B be ManySortedSet of I; ::_thesis: ( (bool A) \/ (bool B) = bool (A \/ B) implies for i being set st i in I holds
A . i,B . i are_c=-comparable )
assume A1: (bool A) \/ (bool B) = bool (A \/ B) ; ::_thesis: for i being set st i in I holds
A . i,B . i are_c=-comparable
let i be set ; ::_thesis: ( i in I implies A . i,B . i are_c=-comparable )
assume A2: i in I ; ::_thesis: A . i,B . i are_c=-comparable
bool ((A . i) \/ (B . i)) = ((bool A) \/ (bool B)) . i by A1, A2, Lm2
.= ((bool A) . i) \/ ((bool B) . i) by A2, PBOOLE:def_4
.= ((bool A) . i) \/ (bool (B . i)) by A2, Def1
.= (bool (A . i)) \/ (bool (B . i)) by A2, Def1 ;
hence A . i,B . i are_c=-comparable by ZFMISC_1:70; ::_thesis: verum
end;
theorem :: MBOOLEAN:9
for I being set
for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds bool (A /\ B) = (bool A) /\ (bool B)
let A, B be ManySortedSet of I; ::_thesis: bool (A /\ B) = (bool A) /\ (bool B)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(bool_(A_/\_B))_._i_=_((bool_A)_/\_(bool_B))_._i
let i be set ; ::_thesis: ( i in I implies (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i )
assume A1: i in I ; ::_thesis: (bool (A /\ B)) . i = ((bool A) /\ (bool B)) . i
hence (bool (A /\ B)) . i = bool ((A . i) /\ (B . i)) by Lm3
.= (bool (A . i)) /\ (bool (B . i)) by ZFMISC_1:71
.= (bool (A . i)) /\ ((bool B) . i) by A1, Def1
.= ((bool A) . i) /\ ((bool B) . i) by A1, Def1
.= ((bool A) /\ (bool B)) . i by A1, PBOOLE:def_5 ;
::_thesis: verum
end;
hence bool (A /\ B) = (bool A) /\ (bool B) by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:10
for I being set
for A, B being ManySortedSet of I holds bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B))
let A, B be ManySortedSet of I; ::_thesis: bool (A \ B) c= (I --> {{}}) \/ ((bool A) \ (bool B))
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i )
assume A1: i in I ; ::_thesis: (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i
then A2: (bool (A \ B)) . i = bool ((A . i) \ (B . i)) by Lm4;
((I --> {{}}) \/ ((bool A) \ (bool B))) . i = ((I --> {{}}) . i) \/ (((bool A) \ (bool B)) . i) by A1, PBOOLE:def_4
.= {{}} \/ (((bool A) \ (bool B)) . i) by A1, FUNCOP_1:7
.= {{}} \/ (((bool A) . i) \ ((bool B) . i)) by A1, PBOOLE:def_6
.= {{}} \/ ((bool (A . i)) \ ((bool B) . i)) by A1, Def1
.= {{}} \/ ((bool (A . i)) \ (bool (B . i))) by A1, Def1 ;
hence (bool (A \ B)) . i c= ((I --> {{}}) \/ ((bool A) \ (bool B))) . i by A2, ZFMISC_1:72; ::_thesis: verum
end;
theorem :: MBOOLEAN:11
for I being set
for X, A, B being ManySortedSet of I holds
( X c= A \ B iff ( X c= A & X misses B ) )
proof
let I be set ; ::_thesis: for X, A, B being ManySortedSet of I holds
( X c= A \ B iff ( X c= A & X misses B ) )
let X, A, B be ManySortedSet of I; ::_thesis: ( X c= A \ B iff ( X c= A & X misses B ) )
thus ( X c= A \ B implies ( X c= A & X misses B ) ) ::_thesis: ( X c= A & X misses B implies X c= A \ B )
proof
assume X c= A \ B ; ::_thesis: ( X c= A & X misses B )
then A1: X in bool (A \ B) by Th1;
thus X c= A ::_thesis: X misses B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i )
assume A2: i in I ; ::_thesis: X . i c= A . i
then X . i in (bool (A \ B)) . i by A1, PBOOLE:def_1;
then X . i in bool ((A . i) \ (B . i)) by A2, Lm4;
hence X . i c= A . i by XBOOLE_1:106; ::_thesis: verum
end;
let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( not i in I or X . i misses B . i )
assume A3: i in I ; ::_thesis: X . i misses B . i
then X . i in (bool (A \ B)) . i by A1, PBOOLE:def_1;
then X . i in bool ((A . i) \ (B . i)) by A3, Lm4;
hence X . i misses B . i by XBOOLE_1:106; ::_thesis: verum
end;
assume A4: ( X c= A & X misses B ) ; ::_thesis: X c= A \ B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \ B) . i )
assume A5: i in I ; ::_thesis: X . i c= (A \ B) . i
then ( X . i c= A . i & X . i misses B . i ) by A4, PBOOLE:def_2, PBOOLE:def_8;
then X . i c= (A . i) \ (B . i) by XBOOLE_1:86;
hence X . i c= (A \ B) . i by A5, PBOOLE:def_6; ::_thesis: verum
end;
theorem :: MBOOLEAN:12
for I being set
for A, B being ManySortedSet of I holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
let A, B be ManySortedSet of I; ::_thesis: (bool (A \ B)) \/ (bool (B \ A)) c= bool (A \+\ B)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i )
assume A1: i in I ; ::_thesis: ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i
then A2: (bool (A \+\ B)) . i = bool ((A . i) \+\ (B . i)) by Lm5;
((bool (A \ B)) \/ (bool (B \ A))) . i = ((bool (A \ B)) . i) \/ ((bool (B \ A)) . i) by A1, PBOOLE:def_4
.= (bool ((A . i) \ (B . i))) \/ ((bool (B \ A)) . i) by A1, Lm4
.= (bool ((A . i) \ (B . i))) \/ (bool ((B . i) \ (A . i))) by A1, Lm4 ;
hence ((bool (A \ B)) \/ (bool (B \ A))) . i c= (bool (A \+\ B)) . i by A2, ZFMISC_1:73; ::_thesis: verum
end;
theorem :: MBOOLEAN:13
for I being set
for X, A, B being ManySortedSet of I holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
proof
let I be set ; ::_thesis: for X, A, B being ManySortedSet of I holds
( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
let X, A, B be ManySortedSet of I; ::_thesis: ( X c= A \+\ B iff ( X c= A \/ B & X misses A /\ B ) )
thus ( X c= A \+\ B implies ( X c= A \/ B & X misses A /\ B ) ) ::_thesis: ( X c= A \/ B & X misses A /\ B implies X c= A \+\ B )
proof
assume X c= A \+\ B ; ::_thesis: ( X c= A \/ B & X misses A /\ B )
then A1: X in bool (A \+\ B) by Th1;
thus X c= A \/ B ::_thesis: X misses A /\ B
proof
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \/ B) . i )
assume A2: i in I ; ::_thesis: X . i c= (A \/ B) . i
then X . i in (bool (A \+\ B)) . i by A1, PBOOLE:def_1;
then X . i in bool ((A . i) \+\ (B . i)) by A2, Lm5;
then X . i c= (A . i) \/ (B . i) by XBOOLE_1:107;
hence X . i c= (A \/ B) . i by A2, PBOOLE:def_4; ::_thesis: verum
end;
let i be set ; :: according to PBOOLE:def_8 ::_thesis: ( not i in I or X . i misses (A /\ B) . i )
assume A3: i in I ; ::_thesis: X . i misses (A /\ B) . i
then X . i in (bool (A \+\ B)) . i by A1, PBOOLE:def_1;
then X . i in bool ((A . i) \+\ (B . i)) by A3, Lm5;
then X . i misses (A . i) /\ (B . i) by XBOOLE_1:107;
hence X . i misses (A /\ B) . i by A3, PBOOLE:def_5; ::_thesis: verum
end;
assume that
A4: X c= A \/ B and
A5: X misses A /\ B ; ::_thesis: X c= A \+\ B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (A \+\ B) . i )
assume A6: i in I ; ::_thesis: X . i c= (A \+\ B) . i
then X . i misses (A /\ B) . i by A5, PBOOLE:def_8;
then A7: X . i misses (A . i) /\ (B . i) by A6, PBOOLE:def_5;
X . i c= (A \/ B) . i by A4, A6, PBOOLE:def_2;
then X . i c= (A . i) \/ (B . i) by A6, PBOOLE:def_4;
then X . i c= (A . i) \+\ (B . i) by A7, XBOOLE_1:107;
hence X . i c= (A \+\ B) . i by A6, PBOOLE:4; ::_thesis: verum
end;
theorem :: MBOOLEAN:14
for I being set
for X, A, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds
X /\ Y c= A
proof
let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds
X /\ Y c= A
let X, A, Y be ManySortedSet of I; ::_thesis: ( ( X c= A or Y c= A ) implies X /\ Y c= A )
assume A1: ( X c= A or Y c= A ) ; ::_thesis: X /\ Y c= A
percases ( X c= A or Y c= A ) by A1;
supposeA2: X c= A ; ::_thesis: X /\ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X /\ Y) . i c= A . i )
assume A3: i in I ; ::_thesis: (X /\ Y) . i c= A . i
then X . i c= A . i by A2, PBOOLE:def_2;
then (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108;
hence (X /\ Y) . i c= A . i by A3, PBOOLE:def_5; ::_thesis: verum
end;
supposeA4: Y c= A ; ::_thesis: X /\ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X /\ Y) . i c= A . i )
assume A5: i in I ; ::_thesis: (X /\ Y) . i c= A . i
then Y . i c= A . i by A4, PBOOLE:def_2;
then (X . i) /\ (Y . i) c= A . i by XBOOLE_1:108;
hence (X /\ Y) . i c= A . i by A5, PBOOLE:def_5; ::_thesis: verum
end;
end;
end;
theorem :: MBOOLEAN:15
for I being set
for X, A, Y being ManySortedSet of I st X c= A holds
X \ Y c= A
proof
let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st X c= A holds
X \ Y c= A
let X, A, Y be ManySortedSet of I; ::_thesis: ( X c= A implies X \ Y c= A )
assume A1: X c= A ; ::_thesis: X \ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X \ Y) . i c= A . i )
assume A2: i in I ; ::_thesis: (X \ Y) . i c= A . i
then X . i c= A . i by A1, PBOOLE:def_2;
then (X . i) \ (Y . i) c= A . i by XBOOLE_1:109;
hence (X \ Y) . i c= A . i by A2, PBOOLE:def_6; ::_thesis: verum
end;
theorem :: MBOOLEAN:16
for I being set
for X, A, Y being ManySortedSet of I st X c= A & Y c= A holds
X \+\ Y c= A
proof
let I be set ; ::_thesis: for X, A, Y being ManySortedSet of I st X c= A & Y c= A holds
X \+\ Y c= A
let X, A, Y be ManySortedSet of I; ::_thesis: ( X c= A & Y c= A implies X \+\ Y c= A )
assume A1: ( X c= A & Y c= A ) ; ::_thesis: X \+\ Y c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (X \+\ Y) . i c= A . i )
assume A2: i in I ; ::_thesis: (X \+\ Y) . i c= A . i
then ( X . i c= A . i & Y . i c= A . i ) by A1, PBOOLE:def_2;
then (X . i) \+\ (Y . i) c= A . i by XBOOLE_1:110;
then (X . i) \+\ (Y . i) in bool (A . i) ;
then (X \+\ Y) . i in bool (A . i) by A2, PBOOLE:4;
hence (X \+\ Y) . i c= A . i ; ::_thesis: verum
end;
theorem :: MBOOLEAN:17
for I being set
for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X \/ Y))
proof
let I be set ; ::_thesis: for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X \/ Y))
let X, Y be ManySortedSet of I; ::_thesis: [|X,Y|] c= bool (bool (X \/ Y))
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or [|X,Y|] . i c= (bool (bool (X \/ Y))) . i )
assume A1: i in I ; ::_thesis: [|X,Y|] . i c= (bool (bool (X \/ Y))) . i
then A2: [|X,Y|] . i = [:(X . i),(Y . i):] by PBOOLE:def_16;
(bool (bool (X \/ Y))) . i = bool ((bool (X \/ Y)) . i) by A1, Def1
.= bool (bool ((X . i) \/ (Y . i))) by A1, Lm2 ;
hence [|X,Y|] . i c= (bool (bool (X \/ Y))) . i by A2, ZFMISC_1:86; ::_thesis: verum
end;
theorem :: MBOOLEAN:18
for I being set
for X, A being ManySortedSet of I holds
( X c= A iff X in bool A )
proof
let I be set ; ::_thesis: for X, A being ManySortedSet of I holds
( X c= A iff X in bool A )
let X, A be ManySortedSet of I; ::_thesis: ( X c= A iff X in bool A )
thus ( X c= A implies X in bool A ) ::_thesis: ( X in bool A implies X c= A )
proof
assume A1: X c= A ; ::_thesis: X in bool A
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or X . i in (bool A) . i )
assume A2: i in I ; ::_thesis: X . i in (bool A) . i
then X . i c= A . i by A1, PBOOLE:def_2;
then X . i in bool (A . i) ;
hence X . i in (bool A) . i by A2, Def1; ::_thesis: verum
end;
assume A3: X in bool A ; ::_thesis: X c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i )
assume A4: i in I ; ::_thesis: X . i c= A . i
then X . i in (bool A) . i by A3, PBOOLE:def_1;
then X . i in bool (A . i) by A4, Def1;
hence X . i c= A . i ; ::_thesis: verum
end;
theorem :: MBOOLEAN:19
for I being set
for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|]
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|]
let A, B be ManySortedSet of I; ::_thesis: (Funcs) (A,B) c= bool [|A,B|]
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i )
assume A1: i in I ; ::_thesis: ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i
then A2: ((Funcs) (A,B)) . i = Funcs ((A . i),(B . i)) by PBOOLE:def_17;
(bool [|A,B|]) . i = bool ([|A,B|] . i) by A1, Def1
.= bool [:(A . i),(B . i):] by A1, PBOOLE:def_16 ;
hence ((Funcs) (A,B)) . i c= (bool [|A,B|]) . i by A2, FRAENKEL:2; ::_thesis: verum
end;
begin
definition
let I be set ;
let A be ManySortedSet of I;
func union A -> ManySortedSet of I means :Def2: :: MBOOLEAN:def 2
for i being set st i in I holds
it . i = union (A . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = union (A . i)
proof
deffunc H1( set ) -> set = union (A . $1);
thus ex X being ManySortedSet of I st
for i being set st i in I holds
X . i = H1(i) from PBOOLE:sch_4(); ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = union (A . i) ) & ( for i being set st i in I holds
b2 . i = union (A . i) ) holds
b1 = b2
proof
let X, Y be ManySortedSet of I; ::_thesis: ( ( for i being set st i in I holds
X . i = union (A . i) ) & ( for i being set st i in I holds
Y . i = union (A . i) ) implies X = Y )
assume that
A1: for i being set st i in I holds
X . i = union (A . i) and
A2: for i being set st i in I holds
Y . i = union (A . i) ; ::_thesis: X = Y
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
X_._i_=_Y_._i
let i be set ; ::_thesis: ( i in I implies X . i = Y . i )
assume A3: i in I ; ::_thesis: X . i = Y . i
hence X . i = union (A . i) by A1
.= Y . i by A2, A3 ;
::_thesis: verum
end;
hence X = Y by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines union MBOOLEAN:def_2_:_
for I being set
for A, b3 being ManySortedSet of I holds
( b3 = union A iff for i being set st i in I holds
b3 . i = union (A . i) );
registration
let I be set ;
cluster union ([[0]] I) -> V3() ;
coherence
union ([[0]] I) is empty-yielding
proof
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( not i in I or (union ([[0]] I)) . i is empty )
A1: union (([[0]] I) . i) is empty by PBOOLE:5, ZFMISC_1:2;
assume i in I ; ::_thesis: (union ([[0]] I)) . i is empty
hence (union ([[0]] I)) . i is empty by A1, Def2; ::_thesis: verum
end;
end;
Lm6: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(union (A \/ B)) . i = union ((A . i) \/ (B . i))
let i be set ; ::_thesis: ( i in I implies (union (A \/ B)) . i = union ((A . i) \/ (B . i)) )
assume A1: i in I ; ::_thesis: (union (A \/ B)) . i = union ((A . i) \/ (B . i))
hence (union (A \/ B)) . i = union ((A \/ B) . i) by Def2
.= union ((A . i) \/ (B . i)) by A1, PBOOLE:def_4 ;
::_thesis: verum
end;
Lm7: for I being set
for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I
for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
let A, B be ManySortedSet of I; ::_thesis: for i being set st i in I holds
(union (A /\ B)) . i = union ((A . i) /\ (B . i))
let i be set ; ::_thesis: ( i in I implies (union (A /\ B)) . i = union ((A . i) /\ (B . i)) )
assume A1: i in I ; ::_thesis: (union (A /\ B)) . i = union ((A . i) /\ (B . i))
hence (union (A /\ B)) . i = union ((A /\ B) . i) by Def2
.= union ((A . i) /\ (B . i)) by A1, PBOOLE:def_5 ;
::_thesis: verum
end;
theorem :: MBOOLEAN:20
for I being set
for A, X being ManySortedSet of I holds
( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
proof
let I be set ; ::_thesis: for A, X being ManySortedSet of I holds
( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
let A, X be ManySortedSet of I; ::_thesis: ( A in union X iff ex Y being ManySortedSet of I st
( A in Y & Y in X ) )
thus ( A in union X implies ex Y being ManySortedSet of I st
( A in Y & Y in X ) ) ::_thesis: ( ex Y being ManySortedSet of I st
( A in Y & Y in X ) implies A in union X )
proof
defpred S1[ set , set ] means ( A . $1 in $2 & $2 in X . $1 );
assume A1: A in union X ; ::_thesis: ex Y being ManySortedSet of I st
( A in Y & Y in X )
A2: for i being set st i in I holds
ex Y being set st S1[i,Y]
proof
let i be set ; ::_thesis: ( i in I implies ex Y being set st S1[i,Y] )
assume A3: i in I ; ::_thesis: ex Y being set st S1[i,Y]
then A . i in (union X) . i by A1, PBOOLE:def_1;
then A . i in union (X . i) by A3, Def2;
hence ex Y being set st S1[i,Y] by TARSKI:def_4; ::_thesis: verum
end;
consider K being ManySortedSet of I such that
A4: for i being set st i in I holds
S1[i,K . i] from PBOOLE:sch_3(A2);
take K ; ::_thesis: ( A in K & K in X )
thus A in K ::_thesis: K in X
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in K . i )
assume i in I ; ::_thesis: A . i in K . i
hence A . i in K . i by A4; ::_thesis: verum
end;
thus K in X ::_thesis: verum
proof
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or K . i in X . i )
assume i in I ; ::_thesis: K . i in X . i
hence K . i in X . i by A4; ::_thesis: verum
end;
end;
given Y being ManySortedSet of I such that A5: ( A in Y & Y in X ) ; ::_thesis: A in union X
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or A . i in (union X) . i )
assume A6: i in I ; ::_thesis: A . i in (union X) . i
then ( A . i in Y . i & Y . i in X . i ) by A5, PBOOLE:def_1;
then A . i in union (X . i) by TARSKI:def_4;
hence A . i in (union X) . i by A6, Def2; ::_thesis: verum
end;
theorem :: MBOOLEAN:21
for I being set holds union ([[0]] I) = [[0]] I
proof
let I be set ; ::_thesis: union ([[0]] I) = [[0]] I
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_([[0]]_I))_._i_=_([[0]]_I)_._i
let i be set ; ::_thesis: ( i in I implies (union ([[0]] I)) . i = ([[0]] I) . i )
assume i in I ; ::_thesis: (union ([[0]] I)) . i = ([[0]] I) . i
hence (union ([[0]] I)) . i = union (([[0]] I) . i) by Def2
.= {} by PBOOLE:5, ZFMISC_1:2
.= ([[0]] I) . i by PBOOLE:5 ;
::_thesis: verum
end;
hence union ([[0]] I) = [[0]] I by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:22
for I, x being set holds union (I --> x) = I --> (union x)
proof
let I, x be set ; ::_thesis: union (I --> x) = I --> (union x)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(I_-->_x))_._i_=_(I_-->_(union_x))_._i
let i be set ; ::_thesis: ( i in I implies (union (I --> x)) . i = (I --> (union x)) . i )
assume A1: i in I ; ::_thesis: (union (I --> x)) . i = (I --> (union x)) . i
hence (union (I --> x)) . i = union ((I --> x) . i) by Def2
.= union x by A1, FUNCOP_1:7
.= (I --> (union x)) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence union (I --> x) = I --> (union x) by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:23
for I, x being set holds union (I --> {x}) = I --> x
proof
let I, x be set ; ::_thesis: union (I --> {x}) = I --> x
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(I_-->_{x}))_._i_=_(I_-->_x)_._i
let i be set ; ::_thesis: ( i in I implies (union (I --> {x})) . i = (I --> x) . i )
assume A1: i in I ; ::_thesis: (union (I --> {x})) . i = (I --> x) . i
hence (union (I --> {x})) . i = union ((I --> {x}) . i) by Def2
.= union {x} by A1, FUNCOP_1:7
.= x by ZFMISC_1:25
.= (I --> x) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence union (I --> {x}) = I --> x by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:24
for I, x, y being set holds union (I --> {{x},{y}}) = I --> {x,y}
proof
let I, x, y be set ; ::_thesis: union (I --> {{x},{y}}) = I --> {x,y}
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(I_-->_{{x},{y}}))_._i_=_(I_-->_{x,y})_._i
let i be set ; ::_thesis: ( i in I implies (union (I --> {{x},{y}})) . i = (I --> {x,y}) . i )
assume A1: i in I ; ::_thesis: (union (I --> {{x},{y}})) . i = (I --> {x,y}) . i
hence (union (I --> {{x},{y}})) . i = union ((I --> {{x},{y}}) . i) by Def2
.= union {{x},{y}} by A1, FUNCOP_1:7
.= {x,y} by ZFMISC_1:26
.= (I --> {x,y}) . i by A1, FUNCOP_1:7 ;
::_thesis: verum
end;
hence union (I --> {{x},{y}}) = I --> {x,y} by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:25
for I being set
for X, A being ManySortedSet of I st X in A holds
X c= union A
proof
let I be set ; ::_thesis: for X, A being ManySortedSet of I st X in A holds
X c= union A
let X, A be ManySortedSet of I; ::_thesis: ( X in A implies X c= union A )
assume A1: X in A ; ::_thesis: X c= union A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (union A) . i )
assume A2: i in I ; ::_thesis: X . i c= (union A) . i
then X . i in A . i by A1, PBOOLE:def_1;
then X . i c= union (A . i) by ZFMISC_1:74;
hence X . i c= (union A) . i by A2, Def2; ::_thesis: verum
end;
theorem :: MBOOLEAN:26
for I being set
for A, B being ManySortedSet of I st A c= B holds
union A c= union B
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A c= B holds
union A c= union B
let A, B be ManySortedSet of I; ::_thesis: ( A c= B implies union A c= union B )
assume A1: A c= B ; ::_thesis: union A c= union B
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union A) . i c= (union B) . i )
assume A2: i in I ; ::_thesis: (union A) . i c= (union B) . i
then A . i c= B . i by A1, PBOOLE:def_2;
then union (A . i) c= union (B . i) by ZFMISC_1:77;
then (union A) . i c= union (B . i) by A2, Def2;
hence (union A) . i c= (union B) . i by A2, Def2; ::_thesis: verum
end;
theorem :: MBOOLEAN:27
for I being set
for A, B being ManySortedSet of I holds union (A \/ B) = (union A) \/ (union B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds union (A \/ B) = (union A) \/ (union B)
let A, B be ManySortedSet of I; ::_thesis: union (A \/ B) = (union A) \/ (union B)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(A_\/_B))_._i_=_((union_A)_\/_(union_B))_._i
let i be set ; ::_thesis: ( i in I implies (union (A \/ B)) . i = ((union A) \/ (union B)) . i )
assume A1: i in I ; ::_thesis: (union (A \/ B)) . i = ((union A) \/ (union B)) . i
hence (union (A \/ B)) . i = union ((A . i) \/ (B . i)) by Lm6
.= (union (A . i)) \/ (union (B . i)) by ZFMISC_1:78
.= ((union A) . i) \/ (union (B . i)) by A1, Def2
.= ((union A) . i) \/ ((union B) . i) by A1, Def2
.= ((union A) \/ (union B)) . i by A1, PBOOLE:def_4 ;
::_thesis: verum
end;
hence union (A \/ B) = (union A) \/ (union B) by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:28
for I being set
for A, B being ManySortedSet of I holds union (A /\ B) c= (union A) /\ (union B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I holds union (A /\ B) c= (union A) /\ (union B)
let A, B be ManySortedSet of I; ::_thesis: union (A /\ B) c= (union A) /\ (union B)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union (A /\ B)) . i c= ((union A) /\ (union B)) . i )
assume A1: i in I ; ::_thesis: (union (A /\ B)) . i c= ((union A) /\ (union B)) . i
then A2: (union (A /\ B)) . i = union ((A . i) /\ (B . i)) by Lm7;
((union A) /\ (union B)) . i = ((union A) . i) /\ ((union B) . i) by A1, PBOOLE:def_5
.= (union (A . i)) /\ ((union B) . i) by A1, Def2
.= (union (A . i)) /\ (union (B . i)) by A1, Def2 ;
hence (union (A /\ B)) . i c= ((union A) /\ (union B)) . i by A2, ZFMISC_1:79; ::_thesis: verum
end;
theorem :: MBOOLEAN:29
for I being set
for A being ManySortedSet of I holds union (bool A) = A
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds union (bool A) = A
let A be ManySortedSet of I; ::_thesis: union (bool A) = A
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(bool_A))_._i_=_A_._i
let i be set ; ::_thesis: ( i in I implies (union (bool A)) . i = A . i )
assume A1: i in I ; ::_thesis: (union (bool A)) . i = A . i
hence (union (bool A)) . i = union ((bool A) . i) by Def2
.= union (bool (A . i)) by A1, Def1
.= A . i by ZFMISC_1:81 ;
::_thesis: verum
end;
hence union (bool A) = A by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:30
for I being set
for A being ManySortedSet of I holds A c= bool (union A)
proof
let I be set ; ::_thesis: for A being ManySortedSet of I holds A c= bool (union A)
let A be ManySortedSet of I; ::_thesis: A c= bool (union A)
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or A . i c= (bool (union A)) . i )
assume A1: i in I ; ::_thesis: A . i c= (bool (union A)) . i
then (bool (union A)) . i = bool ((union A) . i) by Def1
.= bool (union (A . i)) by A1, Def2 ;
hence A . i c= (bool (union A)) . i by ZFMISC_1:82; ::_thesis: verum
end;
theorem :: MBOOLEAN:31
for I being set
for Y, A, X being ManySortedSet of I st union Y c= A & X in Y holds
X c= A
proof
let I be set ; ::_thesis: for Y, A, X being ManySortedSet of I st union Y c= A & X in Y holds
X c= A
let Y, A, X be ManySortedSet of I; ::_thesis: ( union Y c= A & X in Y implies X c= A )
assume that
A1: union Y c= A and
A2: X in Y ; ::_thesis: X c= A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= A . i )
assume A3: i in I ; ::_thesis: X . i c= A . i
then (union Y) . i c= A . i by A1, PBOOLE:def_2;
then A4: union (Y . i) c= A . i by A3, Def2;
X . i in Y . i by A2, A3, PBOOLE:def_1;
hence X . i c= A . i by A4, SETFAM_1:41; ::_thesis: verum
end;
theorem :: MBOOLEAN:32
for I being set
for Z being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X c= Z ) holds
union A c= Z
proof
let I be set ; ::_thesis: for Z being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X c= Z ) holds
union A c= Z
let Z be ManySortedSet of I; ::_thesis: for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X c= Z ) holds
union A c= Z
let A be V2() ManySortedSet of I; ::_thesis: ( ( for X being ManySortedSet of I st X in A holds
X c= Z ) implies union A c= Z )
assume A1: for X being ManySortedSet of I st X in A holds
X c= Z ; ::_thesis: union A c= Z
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or (union A) . i c= Z . i )
assume A2: i in I ; ::_thesis: (union A) . i c= Z . i
for X9 being set st X9 in A . i holds
X9 c= Z . i
proof
consider M being ManySortedSet of I such that
A3: M in A by PBOOLE:134;
let X9 be set ; ::_thesis: ( X9 in A . i implies X9 c= Z . i )
assume A4: X9 in A . i ; ::_thesis: X9 c= Z . i
dom (M +* (i .--> X9)) = I by A2, Lm1;
then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> X9) = {i} by FUNCOP_1:13;
i in {i} by TARSKI:def_1;
then A6: K . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
K in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in A . j )
assume A7: j in I ; ::_thesis: K . j in A . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_A_._j_)_or_(_j_<>_i_&_K_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j in A . j
hence K . j in A . j by A4, A6; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j in A . j
then not j in dom (i .--> X9) by A5, TARSKI:def_1;
then K . j = M . j by FUNCT_4:11;
hence K . j in A . j by A3, A7, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence K . j in A . j ; ::_thesis: verum
end;
then K c= Z by A1;
hence X9 c= Z . i by A2, A6, PBOOLE:def_2; ::_thesis: verum
end;
then union (A . i) c= Z . i by ZFMISC_1:76;
hence (union A) . i c= Z . i by A2, Def2; ::_thesis: verum
end;
theorem :: MBOOLEAN:33
for I being set
for B being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) holds
(union A) /\ B = [[0]] I
proof
let I be set ; ::_thesis: for B being ManySortedSet of I
for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) holds
(union A) /\ B = [[0]] I
let B be ManySortedSet of I; ::_thesis: for A being V2() ManySortedSet of I st ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) holds
(union A) /\ B = [[0]] I
let A be V2() ManySortedSet of I; ::_thesis: ( ( for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ) implies (union A) /\ B = [[0]] I )
assume A1: for X being ManySortedSet of I st X in A holds
X /\ B = [[0]] I ; ::_thesis: (union A) /\ B = [[0]] I
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
((union_A)_/\_B)_._i_=_([[0]]_I)_._i
let i be set ; ::_thesis: ( i in I implies ((union A) /\ B) . i = ([[0]] I) . i )
assume A2: i in I ; ::_thesis: ((union A) /\ B) . i = ([[0]] I) . i
for X9 being set st X9 in A . i holds
X9 misses B . i
proof
consider M being ManySortedSet of I such that
A3: M in A by PBOOLE:134;
let X9 be set ; ::_thesis: ( X9 in A . i implies X9 misses B . i )
assume A4: X9 in A . i ; ::_thesis: X9 misses B . i
dom (M +* (i .--> X9)) = I by A2, Lm1;
then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A5: dom (i .--> X9) = {i} by FUNCOP_1:13;
i in {i} by TARSKI:def_1;
then A6: K . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
K in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in A . j )
assume A7: j in I ; ::_thesis: K . j in A . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_A_._j_)_or_(_j_<>_i_&_K_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j in A . j
hence K . j in A . j by A4, A6; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j in A . j
then not j in dom (i .--> X9) by A5, TARSKI:def_1;
then K . j = M . j by FUNCT_4:11;
hence K . j in A . j by A3, A7, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence K . j in A . j ; ::_thesis: verum
end;
then K /\ B = [[0]] I by A1;
then (K . i) /\ (B . i) = ([[0]] I) . i by A2, PBOOLE:def_5;
then X9 /\ (B . i) = {} by A6, PBOOLE:5;
hence X9 misses B . i by XBOOLE_0:def_7; ::_thesis: verum
end;
then union (A . i) misses B . i by ZFMISC_1:80;
then (union (A . i)) /\ (B . i) = {} by XBOOLE_0:def_7;
then ((union A) . i) /\ (B . i) = {} by A2, Def2;
then ((union A) /\ B) . i = {} by A2, PBOOLE:def_5;
hence ((union A) /\ B) . i = ([[0]] I) . i by PBOOLE:5; ::_thesis: verum
end;
hence (union A) /\ B = [[0]] I by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:34
for I being set
for A, B being ManySortedSet of I st A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ) holds
union (A /\ B) = (union A) /\ (union B)
proof
let I be set ; ::_thesis: for A, B being ManySortedSet of I st A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ) holds
union (A /\ B) = (union A) /\ (union B)
let A, B be ManySortedSet of I; ::_thesis: ( A \/ B is V2() & ( for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ) implies union (A /\ B) = (union A) /\ (union B) )
assume A1: A \/ B is V2() ; ::_thesis: ( ex X, Y being ManySortedSet of I st
( X <> Y & X in A \/ B & Y in A \/ B & not X /\ Y = [[0]] I ) or union (A /\ B) = (union A) /\ (union B) )
assume A2: for X, Y being ManySortedSet of I st X <> Y & X in A \/ B & Y in A \/ B holds
X /\ Y = [[0]] I ; ::_thesis: union (A /\ B) = (union A) /\ (union B)
now__::_thesis:_for_i_being_set_st_i_in_I_holds_
(union_(A_/\_B))_._i_=_((union_A)_/\_(union_B))_._i
let i be set ; ::_thesis: ( i in I implies (union (A /\ B)) . i = ((union A) /\ (union B)) . i )
assume A3: i in I ; ::_thesis: (union (A /\ B)) . i = ((union A) /\ (union B)) . i
for X9, Y9 being set st X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) holds
X9 misses Y9
proof
consider M being ManySortedSet of I such that
A4: M in A \/ B by A1, PBOOLE:134;
A5: i in {i} by TARSKI:def_1;
let X9, Y9 be set ; ::_thesis: ( X9 <> Y9 & X9 in (A . i) \/ (B . i) & Y9 in (A . i) \/ (B . i) implies X9 misses Y9 )
assume that
A6: X9 <> Y9 and
A7: X9 in (A . i) \/ (B . i) and
A8: Y9 in (A . i) \/ (B . i) ; ::_thesis: X9 misses Y9
( dom (M +* (i .--> X9)) = I & dom (M +* (i .--> Y9)) = I ) by A3, Lm1;
then reconsider Kx = M +* (i .--> X9), Ky = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A9: dom (i .--> Y9) = {i} by FUNCOP_1:13;
then A10: Ky . i = (i .--> Y9) . i by A5, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
A11: Ky in A \/ B
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or Ky . j in (A \/ B) . j )
assume A12: j in I ; ::_thesis: Ky . j in (A \/ B) . j
now__::_thesis:_Ky_._j_in_(A_\/_B)_._j
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: Ky . j in (A \/ B) . j
hence Ky . j in (A \/ B) . j by A8, A10, A12, PBOOLE:def_4; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: Ky . j in (A \/ B) . j
then not j in dom (i .--> Y9) by A9, TARSKI:def_1;
then Ky . j = M . j by FUNCT_4:11;
hence Ky . j in (A \/ B) . j by A4, A12, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence Ky . j in (A \/ B) . j ; ::_thesis: verum
end;
A13: dom (i .--> X9) = {i} by FUNCOP_1:13;
then A14: Kx . i = (i .--> X9) . i by A5, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
Kx in A \/ B
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or Kx . j in (A \/ B) . j )
assume A15: j in I ; ::_thesis: Kx . j in (A \/ B) . j
now__::_thesis:_(_(_j_=_i_&_Kx_._j_in_(A_\/_B)_._j_)_or_(_j_<>_i_&_Kx_._j_in_(A_\/_B)_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: Kx . j in (A \/ B) . j
hence Kx . j in (A \/ B) . j by A7, A14, A15, PBOOLE:def_4; ::_thesis: verum
end;
case j <> i ; ::_thesis: Kx . j in (A \/ B) . j
then not j in dom (i .--> X9) by A13, TARSKI:def_1;
then Kx . j = M . j by FUNCT_4:11;
hence Kx . j in (A \/ B) . j by A4, A15, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence Kx . j in (A \/ B) . j ; ::_thesis: verum
end;
then Kx /\ Ky = [[0]] I by A2, A6, A14, A10, A11;
then (Kx /\ Ky) . i = {} by PBOOLE:5;
then X9 /\ Y9 = {} by A3, A14, A10, PBOOLE:def_5;
hence X9 misses Y9 by XBOOLE_0:def_7; ::_thesis: verum
end;
then union ((A . i) /\ (B . i)) = (union (A . i)) /\ (union (B . i)) by ZFMISC_1:83;
then union ((A . i) /\ (B . i)) = ((union A) . i) /\ (union (B . i)) by A3, Def2;
then union ((A . i) /\ (B . i)) = ((union A) . i) /\ ((union B) . i) by A3, Def2;
then union ((A . i) /\ (B . i)) = ((union A) /\ (union B)) . i by A3, PBOOLE:def_5;
hence (union (A /\ B)) . i = ((union A) /\ (union B)) . i by A3, Lm7; ::_thesis: verum
end;
hence union (A /\ B) = (union A) /\ (union B) by PBOOLE:3; ::_thesis: verum
end;
theorem :: MBOOLEAN:35
for I being set
for A, X being ManySortedSet of I
for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
proof
let I be set ; ::_thesis: for A, X being ManySortedSet of I
for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
let A, X be ManySortedSet of I; ::_thesis: for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
let B be V2() ManySortedSet of I; ::_thesis: ( X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) implies X c= union A )
assume that
A1: X c= union (A \/ B) and
A2: for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ; ::_thesis: X c= union A
let i be set ; :: according to PBOOLE:def_2 ::_thesis: ( not i in I or X . i c= (union A) . i )
assume A3: i in I ; ::_thesis: X . i c= (union A) . i
A4: for Y9 being set st Y9 in B . i holds
Y9 misses X . i
proof
consider M being ManySortedSet of I such that
A5: M in B by PBOOLE:134;
let Y9 be set ; ::_thesis: ( Y9 in B . i implies Y9 misses X . i )
assume A6: Y9 in B . i ; ::_thesis: Y9 misses X . i
dom (M +* (i .--> Y9)) = I by A3, Lm1;
then reconsider K = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
A7: dom (i .--> Y9) = {i} by FUNCOP_1:13;
i in {i} by TARSKI:def_1;
then A8: K . i = (i .--> Y9) . i by A7, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
K in B
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K . j in B . j )
assume A9: j in I ; ::_thesis: K . j in B . j
now__::_thesis:_(_(_j_=_i_&_K_._j_in_B_._j_)_or_(_j_<>_i_&_K_._j_in_B_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K . j in B . j
hence K . j in B . j by A6, A8; ::_thesis: verum
end;
case j <> i ; ::_thesis: K . j in B . j
then not j in dom (i .--> Y9) by A7, TARSKI:def_1;
then K . j = M . j by FUNCT_4:11;
hence K . j in B . j by A5, A9, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence K . j in B . j ; ::_thesis: verum
end;
then K /\ X = [[0]] I by A2;
then (K /\ X) . i = {} by PBOOLE:5;
then Y9 /\ (X . i) = {} by A3, A8, PBOOLE:def_5;
hence Y9 misses X . i by XBOOLE_0:def_7; ::_thesis: verum
end;
X . i c= (union (A \/ B)) . i by A1, A3, PBOOLE:def_2;
then X . i c= union ((A . i) \/ (B . i)) by A3, Lm6;
then X . i c= union (A . i) by A4, SETFAM_1:42;
hence X . i c= (union A) . i by A3, Def2; ::_thesis: verum
end;
theorem :: MBOOLEAN:36
for I being set
for A being V2() V26() ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) holds
union A in A
proof
let I be set ; ::_thesis: for A being V2() V26() ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) holds
union A in A
let A be V2() V26() ManySortedSet of I; ::_thesis: ( ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) implies union A in A )
assume A1: for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ; ::_thesis: union A in A
let i be set ; :: according to PBOOLE:def_1 ::_thesis: ( not i in I or (union A) . i in A . i )
assume A2: i in I ; ::_thesis: (union A) . i in A . i
then i in dom A by PARTFUN1:def_2;
then A . i in rng A by FUNCT_1:3;
then A3: A . i is finite by FINSET_1:def_2;
A4: for X9, Y9 being set st X9 in A . i & Y9 in A . i & not X9 c= Y9 holds
Y9 c= X9
proof
let X9, Y9 be set ; ::_thesis: ( X9 in A . i & Y9 in A . i & not X9 c= Y9 implies Y9 c= X9 )
assume that
A5: X9 in A . i and
A6: Y9 in A . i ; ::_thesis: ( X9 c= Y9 or Y9 c= X9 )
consider M being ManySortedSet of I such that
A7: M in A by PBOOLE:134;
( dom (M +* (i .--> Y9)) = I & dom (M +* (i .--> X9)) = I ) by A2, Lm1;
then reconsider K1 = M +* (i .--> X9), K2 = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
assume A8: not X9 c= Y9 ; ::_thesis: Y9 c= X9
A9: i in {i} by TARSKI:def_1;
A10: dom (i .--> Y9) = {i} by FUNCOP_1:13;
then A11: K2 . i = (i .--> Y9) . i by A9, FUNCT_4:13
.= Y9 by FUNCOP_1:72 ;
A12: K2 in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K2 . j in A . j )
assume A13: j in I ; ::_thesis: K2 . j in A . j
now__::_thesis:_(_(_j_=_i_&_K2_._j_in_A_._j_)_or_(_j_<>_i_&_K2_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K2 . j in A . j
hence K2 . j in A . j by A6, A11; ::_thesis: verum
end;
case j <> i ; ::_thesis: K2 . j in A . j
then not j in dom (i .--> Y9) by A10, TARSKI:def_1;
then K2 . j = M . j by FUNCT_4:11;
hence K2 . j in A . j by A7, A13, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence K2 . j in A . j ; ::_thesis: verum
end;
A14: dom (i .--> X9) = {i} by FUNCOP_1:13;
then A15: K1 . i = (i .--> X9) . i by A9, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
K1 in A
proof
let j be set ; :: according to PBOOLE:def_1 ::_thesis: ( not j in I or K1 . j in A . j )
assume A16: j in I ; ::_thesis: K1 . j in A . j
now__::_thesis:_(_(_j_=_i_&_K1_._j_in_A_._j_)_or_(_j_<>_i_&_K1_._j_in_A_._j_)_)
percases ( j = i or j <> i ) ;
case j = i ; ::_thesis: K1 . j in A . j
hence K1 . j in A . j by A5, A15; ::_thesis: verum
end;
case j <> i ; ::_thesis: K1 . j in A . j
then not j in dom (i .--> X9) by A14, TARSKI:def_1;
then K1 . j = M . j by FUNCT_4:11;
hence K1 . j in A . j by A7, A16, PBOOLE:def_1; ::_thesis: verum
end;
end;
end;
hence K1 . j in A . j ; ::_thesis: verum
end;
then ( K1 c= K2 or K2 c= K1 ) by A1, A12;
hence Y9 c= X9 by A2, A8, A15, A11, PBOOLE:def_2; ::_thesis: verum
end;
A . i <> {} by A2, PBOOLE:def_13;
then union (A . i) in A . i by A3, A4, CARD_2:62;
hence (union A) . i in A . i by A2, Def2; ::_thesis: verum
end;