:: by Artur Korni{\l}owicz

::

:: Received September 29, 1995

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

theorem Th1: :: PZFMISC1:1

for i being object

for I being set

for X being object

for M being ManySortedSet of I st i in I holds

dom (M +* (i .--> X)) = I

for I being set

for X being object

for M being ManySortedSet of I st i in I holds

dom (M +* (i .--> X)) = I

proof end;

theorem :: PZFMISC1:2

for f being Function st f = {} holds

f is ManySortedSet of {} by PARTFUN1:def 2, RELAT_1:38, RELAT_1:def 18;

f is ManySortedSet of {} by PARTFUN1:def 2, RELAT_1:38, RELAT_1:def 18;

theorem :: PZFMISC1:3

for I being set st not I is empty holds

for X being ManySortedSet of I holds

( not X is V3() or not X is V2() )

for X being ManySortedSet of I holds

( not X is V3() or not X is V2() )

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 = {(A . i)}

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

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

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

b_{1} = b_{2}

end;
let A be ManySortedSet of I;

func {A} -> ManySortedSet of I means :Def1: :: PZFMISC1:def 1

for i being object st i in I holds

it . i = {(A . i)};

existence for i being object st i in I holds

it . i = {(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 { PZFMISC1:def 1 :

for I being set

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

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

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

for I being set

for A, b

( b

b

registration

let I be set ;

let A be ManySortedSet of I;

coherence

( {A} is non-empty & {A} is finite-yielding )

end;
let A be ManySortedSet of I;

coherence

( {A} is non-empty & {A} is finite-yielding )

proof end;

definition

let I be set ;

let A, B be ManySortedSet of I;

ex b_{1} being ManySortedSet of I st

for i being object st i in I holds

b_{1} . i = {(A . i),(B . i)}

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

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

b_{2} . i = {(A . i),(B . i)} ) holds

b_{1} = b_{2}

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

b_{1} . i = {(A . i),(B . i)} ) holds

for i being object st i in I holds

b_{1} . i = {(B . i),(A . i)}
;

end;
let A, B be ManySortedSet of I;

func {A,B} -> ManySortedSet of I means :Def2: :: PZFMISC1:def 2

for i being object st i in I holds

it . i = {(A . i),(B . i)};

existence for i being object st i in I holds

it . i = {(A . i),(B . i)};

ex b

for i being object st i in I holds

b

proof end;

uniqueness for b

b

b

b

proof end;

commutativity for b

b

for i being object st i in I holds

b

:: deftheorem Def2 defines { PZFMISC1:def 2 :

for I being set

for A, B, b_{4} being ManySortedSet of I holds

( b_{4} = {A,B} iff for i being object st i in I holds

b_{4} . i = {(A . i),(B . i)} );

for I being set

for A, B, b

( b

b

registration

let I be set ;

let A, B be ManySortedSet of I;

coherence

( {A,B} is non-empty & {A,B} is finite-yielding )

end;
let A, B be ManySortedSet of I;

coherence

( {A,B} is non-empty & {A,B} is finite-yielding )

proof end;

theorem :: PZFMISC1:4

for I being set

for y, X being ManySortedSet of I holds

( X = {y} iff for x being ManySortedSet of I holds

( x in X iff x = y ) )

for y, X being ManySortedSet of I holds

( X = {y} iff for x being ManySortedSet of I holds

( x in X iff x = y ) )

proof end;

theorem :: PZFMISC1:5

for I being set

for x1, x2, X being ManySortedSet of I st ( for x being ManySortedSet of I holds

( x in X iff ( x = x1 or x = x2 ) ) ) holds

X = {x1,x2}

for x1, x2, X being ManySortedSet of I st ( for x being ManySortedSet of I holds

( x in X iff ( x = x1 or x = x2 ) ) ) holds

X = {x1,x2}

proof end;

theorem :: PZFMISC1:6

for I being set

for x1, x2, X being ManySortedSet of I st X = {x1,x2} holds

for x being ManySortedSet of I st ( x = x1 or x = x2 ) holds

x in X

for x1, x2, X being ManySortedSet of I st X = {x1,x2} holds

for x being ManySortedSet of I st ( x = x1 or x = x2 ) holds

x in X

proof end;

theorem :: PZFMISC1:19

for I being set

for x, y being ManySortedSet of I st not I is empty & {x} (/\) {y} = EmptyMS I holds

x <> y

for x, y being ManySortedSet of I st not I is empty & {x} (/\) {y} = EmptyMS I holds

x <> y

proof end;

theorem :: PZFMISC1:22

for I being set

for x, y being ManySortedSet of I st not I is empty & {x} (\) {y} = {x} holds

x <> y

for x, y being ManySortedSet of I st not I is empty & {x} (\) {y} = {x} holds

x <> y

proof end;

theorem :: PZFMISC1:34

for I being set

for x1, x2, X being ManySortedSet of I holds

( {x1,x2} c= X iff ( x1 in X & x2 in X ) )

for x1, x2, X being ManySortedSet of I holds

( {x1,x2} c= X iff ( x1 in X & x2 in X ) )

proof end;

theorem :: PZFMISC1:35

for I being set

for x1, x2, A being ManySortedSet of I st ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) holds

A c= {x1,x2}

for x1, x2, A being ManySortedSet of I st ( A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} ) holds

A c= {x1,x2}

proof end;

theorem :: PZFMISC1:37

for I being set

for x, A, B being ManySortedSet of I holds

( A (\/) {x} c= B iff ( x in B & A c= B ) )

for x, A, B being ManySortedSet of I holds

( A (\/) {x} c= B iff ( x in B & A c= B ) )

proof end;

theorem :: PZFMISC1:40

for I being set

for x, y, A being ManySortedSet of I holds

( {x,y} (\/) A = A iff ( x in A & y in A ) )

for x, y, A being ManySortedSet of I holds

( {x,y} (\/) A = A iff ( x in A & y in A ) )

proof end;

theorem :: PZFMISC1:42

for I being set

for x, y, X being ManySortedSet of I st not I is empty holds

{x,y} (\/) X <> EmptyMS I

for x, y, X being ManySortedSet of I st not I is empty holds

{x,y} (\/) X <> EmptyMS I

proof end;

theorem :: PZFMISC1:45

for I being set

for x, y, X being ManySortedSet of I holds

( ( x in X & y in X ) iff {x,y} (/\) X = {x,y} )

for x, y, X being ManySortedSet of I holds

( ( x in X & y in X ) iff {x,y} (/\) X = {x,y} )

proof end;

theorem :: PZFMISC1:46

for I being set

for x, X being ManySortedSet of I st not I is empty & {x} (/\) X = EmptyMS I holds

not x in X

for x, X being ManySortedSet of I st not I is empty & {x} (/\) X = EmptyMS I holds

not x in X

proof end;

theorem :: PZFMISC1:47

for I being set

for x, y, X being ManySortedSet of I st not I is empty & {x,y} (/\) X = EmptyMS I holds

( not x in X & not y in X )

for x, y, X being ManySortedSet of I st not I is empty & {x,y} (/\) X = EmptyMS I holds

( not x in X & not y in X )

proof end;

theorem :: PZFMISC1:49

for I being set

for x, y, X being ManySortedSet of I st not I is empty & y in X (\) {x} holds

y <> x

for x, y, X being ManySortedSet of I st not I is empty & y in X (\) {x} holds

y <> x

proof end;

theorem :: PZFMISC1:50

for I being set

for x, X being ManySortedSet of I st not I is empty & X (\) {x} = X holds

not x in X

for x, X being ManySortedSet of I st not I is empty & X (\) {x} = X holds

not x in X

proof end;

theorem :: PZFMISC1:51

for I being set

for x, X being ManySortedSet of I st not I is empty & {x} (\) X = {x} holds

not x in X

for x, X being ManySortedSet of I st not I is empty & {x} (\) X = {x} holds

not x in X

proof end;

theorem :: PZFMISC1:53

for I being set

for x, y, X being ManySortedSet of I st not I is empty & {x,y} (\) X = {x} holds

not x in X

for x, y, X being ManySortedSet of I st not I is empty & {x,y} (\) X = {x} holds

not x in X

proof end;

theorem :: PZFMISC1:54

for I being set

for x, y, X being ManySortedSet of I st not I is empty & {x,y} (\) X = {x,y} holds

( not x in X & not y in X )

for x, y, X being ManySortedSet of I st not I is empty & {x,y} (\) X = {x,y} holds

( not x in X & not y in X )

proof end;

theorem :: PZFMISC1:55

for I being set

for x, y, X being ManySortedSet of I holds

( {x,y} (\) X = EmptyMS I iff ( x in X & y in X ) )

for x, y, X being ManySortedSet of I holds

( {x,y} (\) X = EmptyMS I iff ( x in X & y in X ) )

proof end;

theorem :: PZFMISC1:56

for I being set

for x, y, X being ManySortedSet of I st ( X = EmptyMS I or X = {x} or X = {y} or X = {x,y} ) holds

X (\) {x,y} = EmptyMS I

for x, y, X being ManySortedSet of I st ( X = EmptyMS I or X = {x} or X = {y} or X = {x,y} ) holds

X (\) {x,y} = EmptyMS I

proof end;

theorem :: PZFMISC1:57

for I being set

for X, Y being ManySortedSet of I st ( X = EmptyMS I or Y = EmptyMS I ) holds

[|X,Y|] = EmptyMS I

for X, Y being ManySortedSet of I st ( X = EmptyMS I or Y = EmptyMS I ) holds

[|X,Y|] = EmptyMS I

proof end;

theorem :: PZFMISC1:58

for I being set

for X, Y being ManySortedSet of I st X is V2() & Y is V2() & [|X,Y|] = [|Y,X|] holds

X = Y

for X, Y being ManySortedSet of I st X is V2() & Y is V2() & [|X,Y|] = [|Y,X|] holds

X = Y

proof end;

theorem :: PZFMISC1:60

for I being set

for X, Y, Z being ManySortedSet of I st Z is V2() & ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) holds

X c= Y

for X, Y, Z being ManySortedSet of I st Z is V2() & ( [|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|] ) holds

X c= Y

proof end;

theorem :: PZFMISC1:61

for I being set

for X, Y, Z being ManySortedSet of I st X c= Y holds

( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] )

for X, Y, Z being ManySortedSet of I st X c= Y holds

( [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|] )

proof end;

theorem :: PZFMISC1:62

for I being set

for x1, x2, A, B being ManySortedSet of I st x1 c= A & x2 c= B holds

[|x1,x2|] c= [|A,B|]

for x1, x2, A, B being ManySortedSet of I st x1 c= A & x2 c= B holds

[|x1,x2|] c= [|A,B|]

proof end;

theorem :: PZFMISC1:63

for I being set

for X, Y, Z being ManySortedSet of I holds

( [|(X (\/) Y),Z|] = [|X,Z|] (\/) [|Y,Z|] & [|Z,(X (\/) Y)|] = [|Z,X|] (\/) [|Z,Y|] )

for X, Y, Z being ManySortedSet of I holds

( [|(X (\/) Y),Z|] = [|X,Z|] (\/) [|Y,Z|] & [|Z,(X (\/) Y)|] = [|Z,X|] (\/) [|Z,Y|] )

proof end;

theorem :: PZFMISC1:64

for I being set

for x1, x2, A, B being ManySortedSet of I holds [|(x1 (\/) x2),(A (\/) B)|] = (([|x1,A|] (\/) [|x1,B|]) (\/) [|x2,A|]) (\/) [|x2,B|]

for x1, x2, A, B being ManySortedSet of I holds [|(x1 (\/) x2),(A (\/) B)|] = (([|x1,A|] (\/) [|x1,B|]) (\/) [|x2,A|]) (\/) [|x2,B|]

proof end;

theorem :: PZFMISC1:65

for I being set

for X, Y, Z being ManySortedSet of I holds

( [|(X (/\) Y),Z|] = [|X,Z|] (/\) [|Y,Z|] & [|Z,(X (/\) Y)|] = [|Z,X|] (/\) [|Z,Y|] )

for X, Y, Z being ManySortedSet of I holds

( [|(X (/\) Y),Z|] = [|X,Z|] (/\) [|Y,Z|] & [|Z,(X (/\) Y)|] = [|Z,X|] (/\) [|Z,Y|] )

proof end;

theorem :: PZFMISC1:66

for I being set

for x1, x2, A, B being ManySortedSet of I holds [|(x1 (/\) x2),(A (/\) B)|] = [|x1,A|] (/\) [|x2,B|]

for x1, x2, A, B being ManySortedSet of I holds [|(x1 (/\) x2),(A (/\) B)|] = [|x1,A|] (/\) [|x2,B|]

proof end;

theorem :: PZFMISC1:67

for I being set

for A, B, X, Y being ManySortedSet of I st A c= X & B c= Y holds

[|A,Y|] (/\) [|X,B|] = [|A,B|]

for A, B, X, Y being ManySortedSet of I st A c= X & B c= Y holds

[|A,Y|] (/\) [|X,B|] = [|A,B|]

proof end;

theorem :: PZFMISC1:68

for I being set

for X, Y, Z being ManySortedSet of I holds

( [|(X (\) Y),Z|] = [|X,Z|] (\) [|Y,Z|] & [|Z,(X (\) Y)|] = [|Z,X|] (\) [|Z,Y|] )

for X, Y, Z being ManySortedSet of I holds

( [|(X (\) Y),Z|] = [|X,Z|] (\) [|Y,Z|] & [|Z,(X (\) Y)|] = [|Z,X|] (\) [|Z,Y|] )

proof end;

theorem :: PZFMISC1:69

for I being set

for x1, x2, A, B being ManySortedSet of I holds [|x1,x2|] (\) [|A,B|] = [|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]

for x1, x2, A, B being ManySortedSet of I holds [|x1,x2|] (\) [|A,B|] = [|(x1 (\) A),x2|] (\/) [|x1,(x2 (\) B)|]

proof end;

theorem :: PZFMISC1:70

for I being set

for x1, x2, A, B being ManySortedSet of I st ( x1 (/\) x2 = EmptyMS I or A (/\) B = EmptyMS I ) holds

[|x1,A|] (/\) [|x2,B|] = EmptyMS I

for x1, x2, A, B being ManySortedSet of I st ( x1 (/\) x2 = EmptyMS I or A (/\) B = EmptyMS I ) holds

[|x1,A|] (/\) [|x2,B|] = EmptyMS I

proof end;

theorem :: PZFMISC1:71

for I being set

for x, X being ManySortedSet of I st X is V2() holds

( [|{x},X|] is V2() & [|X,{x}|] is V2() )

for x, X being ManySortedSet of I st X is V2() holds

( [|{x},X|] is V2() & [|X,{x}|] is V2() )

proof end;

theorem :: PZFMISC1:72

for I being set

for x, y, X being ManySortedSet of I holds

( [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|] )

for x, y, X being ManySortedSet of I holds

( [|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] & [|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|] )

proof end;

theorem :: PZFMISC1:73

for I being set

for x1, x2, A, B being ManySortedSet of I st x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] holds

( x1 = x2 & A = B )

for x1, x2, A, B being ManySortedSet of I st x1 is V2() & A is V2() & [|x1,A|] = [|x2,B|] holds

( x1 = x2 & A = B )

proof end;

theorem :: PZFMISC1:74

for I being set

for X, Y being ManySortedSet of I st ( X c= [|X,Y|] or X c= [|Y,X|] ) holds

X = EmptyMS I

for X, Y being ManySortedSet of I st ( X c= [|X,Y|] or X c= [|Y,X|] ) holds

X = EmptyMS I

proof end;

theorem :: PZFMISC1:75

for I being set

for x, y, A, X, Y being ManySortedSet of I st A in [|x,y|] & A in [|X,Y|] holds

A in [|(x (/\) X),(y (/\) Y)|]

for x, y, A, X, Y being ManySortedSet of I st A in [|x,y|] & A in [|X,Y|] holds

A in [|(x (/\) X),(y (/\) Y)|]

proof end;

theorem :: PZFMISC1:76

for I being set

for x, y, X, Y being ManySortedSet of I st [|x,X|] c= [|y,Y|] & [|x,X|] is V2() holds

( x c= y & X c= Y )

for x, y, X, Y being ManySortedSet of I st [|x,X|] c= [|y,Y|] & [|x,X|] is V2() holds

( x c= y & X c= Y )

proof end;

theorem :: PZFMISC1:78

for I being set

for X, Y being ManySortedSet of I st X (/\) Y = EmptyMS I holds

[|X,Y|] (/\) [|Y,X|] = EmptyMS I

for X, Y being ManySortedSet of I st X (/\) Y = EmptyMS I holds

[|X,Y|] (/\) [|Y,X|] = EmptyMS I

proof end;

theorem :: PZFMISC1:79

for I being set

for A, B, X, Y being ManySortedSet of I st A is V2() & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) holds

B c= Y

for A, B, X, Y being ManySortedSet of I st A is V2() & ( [|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|] ) holds

B c= Y

proof end;

theorem :: PZFMISC1:80

for I being set

for x, y, A, B, X, Y being ManySortedSet of I st x c= [|A,B|] & y c= [|X,Y|] holds

x (\/) y c= [|(A (\/) X),(B (\/) Y)|]

for x, y, A, B, X, Y being ManySortedSet of I st x c= [|A,B|] & y c= [|X,Y|] holds

x (\/) y c= [|(A (\/) X),(B (\/) Y)|]

proof end;

:: from AUTALG_1

definition

let I be set ;

let A, B be ManySortedSet of I;

for A being ManySortedSet of I

for i being set st i in I & A . i = {} holds

A . i = {} ;

end;
let A, B be ManySortedSet of I;

pred A is_transformable_to B means :: PZFMISC1:def 3

for i being set st i in I & B . i = {} holds

A . i = {} ;

reflexivity for i being set st i in I & B . i = {} holds

A . i = {} ;

for A being ManySortedSet of I

for i being set st i in I & A . i = {} holds

A . i = {} ;

:: deftheorem defines is_transformable_to PZFMISC1:def 3 :

for I being set

for A, B being ManySortedSet of I holds

( A is_transformable_to B iff for i being set st i in I & B . i = {} holds

A . i = {} );

for I being set

for A, B being ManySortedSet of I holds

( A is_transformable_to B iff for i being set st i in I & B . i = {} holds

A . i = {} );