:: by Artur Korni{\l}owicz

::

:: Received April 27, 1995

:: Copyright (c) 1995-2016 Association of Mizar Users

definition

let I be set ;

let A be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = bool (A . i)

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = bool (A . i) ) & ( for i being object st i in I holds

b_{2} . i = bool (A . i) ) holds

b_{1} = b_{2}

end;
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 for i being object st i in I holds

it . i = bool (A . i);

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines bool MBOOLEAN:def 1 :

for I being set

for A, b_{3} being ManySortedSet of I holds

( b_{3} = bool A iff for i being object st i in I holds

b_{3} . i = bool (A . i) );

for I being set

for A, b

( b

b

registration
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 ) )

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: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

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:10

for I being set

for A, B being ManySortedSet of I holds bool (A (\) B) c= (I --> {{}}) (\/) ((bool A) (\) (bool B))

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 ) )

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)

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 ) )

for A, B, X being ManySortedSet of I holds

( X c= A (\+\) B iff ( X c= A (\/) B & X misses A (/\) B ) )

proof end;

definition

let I be set ;

let A be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = union (A . i)

for b_{1}, b_{2} being ManySortedSet of I st ( for i being object st i in I holds

b_{1} . i = union (A . i) ) & ( for i being object st i in I holds

b_{2} . i = union (A . i) ) holds

b_{1} = b_{2}

end;
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 for i being object st i in I holds

it . i = union (A . i);

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def2 defines union MBOOLEAN:def 2 :

for I being set

for A, b_{3} being ManySortedSet of I holds

( b_{3} = union A iff for i being object st i in I holds

b_{3} . i = union (A . i) );

for I being set

for A, b

( b

b

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 ) )

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:28

for I being set

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

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

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

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

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)

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

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

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;