:: Definitions and Basic Properties of Boolean & Union of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received April 27, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users

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 object st i in I holds
it . i = bool (A . i);

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = bool (A . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = bool (A . i) ) & ( for i being object st i in I holds
b₂ . i = bool (A . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def1 defines bool MBOOLEAN:def 1 :
for I being set
for A, b₃ being ManySortedSet of I holds
( b₃ = bool A iff for i being object st i in I holds
b₃ . 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 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 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 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 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 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 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 end;

theorem :: MBOOLEAN:2

for I being set holds bool (EmptyMS I) = I --> {{}}

proof end;

theorem :: MBOOLEAN:3

for I, x being set holds bool (I --> x) = I --> (bool x)

proof end;

theorem :: MBOOLEAN:4

for x being object
for I being set holds bool (I --> {x}) = I --> {{},{x}}

proof end;

theorem :: MBOOLEAN:5

for I being set
for A being ManySortedSet of I holds EmptyMS I c= A

proof 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 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 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 end;

theorem :: MBOOLEAN:9

for I being set
for A, B being ManySortedSet of I holds bool (A (/\) B) = (bool A) (/\) (bool B)

proof 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 end;

theorem :: MBOOLEAN:11

for I being set
for A, B, X being ManySortedSet of I holds
( X c= A (\) B iff ( X c= A & X misses B ) )

proof 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 end;

theorem :: MBOOLEAN:13

for I being set
for A, B, X being ManySortedSet of I holds
( X c= A (\+\) B iff ( X c= A (\/) B & X misses A (/\) B ) )

proof end;

theorem :: MBOOLEAN:14

for I being set
for A, X, Y being ManySortedSet of I st ( X c= A or Y c= A ) holds
X (/\) Y c= A

proof end;

theorem :: MBOOLEAN:15

for I being set
for A, X, Y being ManySortedSet of I st X c= A holds
X (\) Y c= A

proof end;

theorem :: MBOOLEAN:16

for I being set
for A, X, Y being ManySortedSet of I st X c= A & Y c= A holds
X (\+\) Y c= A

proof end;

theorem :: MBOOLEAN:17

for I being set
for X, Y being ManySortedSet of I holds [|X,Y|] c= bool (bool (X (\/) Y))

proof end;

theorem :: MBOOLEAN:18

for I being set
for A, X being ManySortedSet of I holds
( X c= A iff X in bool A )

proof end;

theorem :: MBOOLEAN:19

for I being set
for A, B being ManySortedSet of I holds (Funcs) (A,B) c= bool [|A,B|]

proof end;

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 object st i in I holds
it . i = union (A . i);

existence
ex b₁ being ManySortedSet of I st
for i being object st i in I holds
b₁ . i = union (A . i)

proof end;

uniqueness
for b₁, b₂ being ManySortedSet of I st ( for i being object st i in I holds
b₁ . i = union (A . i) ) & ( for i being object st i in I holds
b₂ . i = union (A . i) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines union MBOOLEAN:def 2 :
for I being set
for A, b₃ being ManySortedSet of I holds
( b₃ = union A iff for i being object st i in I holds
b₃ . i = union (A . i) );

registration

let I be set ;

cluster union (EmptyMS I) -> V3() ;

coherence
union (EmptyMS I) is empty-yielding

proof 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 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 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 end;

theorem :: MBOOLEAN:21

for I being set holds union (EmptyMS I) = EmptyMS I

proof end;

theorem :: MBOOLEAN:22

for I, x being set holds union (I --> x) = I --> (union x)

proof end;

theorem :: MBOOLEAN:23

for x being object
for I being set holds union (I --> {x}) = I --> x

proof end;

theorem :: MBOOLEAN:24

for x, y being object
for I being set holds union (I --> {{x},{y}}) = I --> {x,y}

proof end;

theorem :: MBOOLEAN:25

for I being set
for A, X being ManySortedSet of I st X in A holds
X c= union A

proof 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 end;

theorem :: MBOOLEAN:27

for I being set
for A, B being ManySortedSet of I holds union (A (\/) B) = (union A) (\/) (union B)

proof 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 end;

theorem :: MBOOLEAN:29

for I being set
for A being ManySortedSet of I holds union (bool A) = A

proof end;

theorem :: MBOOLEAN:30

for I being set
for A being ManySortedSet of I holds A c= bool (union A)

proof end;

theorem :: MBOOLEAN:31

for I being set
for A, X, Y being ManySortedSet of I st union Y c= A & X in Y holds
X c= A

proof 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 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 = EmptyMS I ) holds
(union A) (/\) B = EmptyMS I

proof 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 = EmptyMS I ) holds
union (A (/\) B) = (union A) (/\) (union B)

proof 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 = EmptyMS I ) holds
X c= union A

proof 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 end;