:: Some Basic Properties of Many Sorted Sets
:: by Artur Korni{\l}owicz
::
:: Received September 29, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, PBOOLE, RELAT_1, FUNCT_4, FUNCOP_1, XBOOLE_0, FINSET_1,
TARSKI, ZFMISC_1, PZFMISC1, SETLIM_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_4, FINSET_1,
FUNCOP_1, PBOOLE, MBOOLEAN;
constructors FUNCT_4, MBOOLEAN, PBOOLE, FINSET_1, RELSET_1;
registrations XBOOLE_0, FUNCOP_1, FINSET_1;
requirements BOOLE;
begin :: Preliminaries
reserve i for object, I for set,
f for Function,
x, x1, x2, y, A, B, X, Y, Z for ManySortedSet of I;
theorem :: PZFMISC1:1
for X be object for M be ManySortedSet of I st i in I
holds dom (M +* (i .--> X)) = I;
theorem :: PZFMISC1:2
f = {} implies f is ManySortedSet of {};
theorem :: PZFMISC1:3
I is non empty implies not ex X st X is empty-yielding & X is non-empty;
begin :: Singelton and unordered pairs
definition
let I, A;
func {A} -> ManySortedSet of I means
:: PZFMISC1:def 1
for i being object st i in I holds it.i = {A.i};
end;
registration
let I, A;
cluster {A} -> non-empty finite-yielding;
end;
definition
let I, A, B;
func {A,B} -> ManySortedSet of I means
:: PZFMISC1:def 2
for i being object st i in I holds it.i = {A.i,B.i};
commutativity;
end;
registration
let I, A, B;
cluster {A,B} -> non-empty finite-yielding;
end;
theorem :: PZFMISC1:4 :: Tarski:3
X = { y } iff for x holds x in X iff x = y;
theorem :: PZFMISC1:5 :: Tarski:4 a
(for x holds x in X iff x = x1 or x = x2) implies X = { x1,x2 };
theorem :: PZFMISC1:6 :: Tarski:4 b
X = { x1,x2 } implies for x holds x = x1 or x = x2 implies x in X;
theorem :: PZFMISC1:7 :: ENUMSET1:3
x in { A } implies x = A;
theorem :: PZFMISC1:8 :: ENUMSET1:4
x in { x };
theorem :: PZFMISC1:9 :: ENUMSET1:9
x = A or x = B implies x in { A,B };
theorem :: PZFMISC1:10 ::ENUMSET1:41
{A} (\/) {B} = {A,B};
theorem :: PZFMISC1:11 :: ENUMSET1:69
{ x,x } = { x };
theorem :: PZFMISC1:12 :: SETWISEO:1
{A} c= {B} implies A = B;
theorem :: PZFMISC1:13 :: ZFMISC_1:6
{x} = {y} implies x = y;
theorem :: PZFMISC1:14 :: ZFMISC_1:8
{x} = {A,B} implies x = A & x = B;
theorem :: PZFMISC1:15 :: ZFMISC_1:9
{x} = {A,B} implies A = B;
theorem :: PZFMISC1:16 :: ZFMISC_1:12
{x} c= {x,y} & {y} c= {x,y};
theorem :: PZFMISC1:17 :: ZFMISC_1:13
{x} (\/) {y} = {x} implies x = y;
theorem :: PZFMISC1:18 :: ZFMISC_1:14
{x} (\/) {x,y} = {x,y};
theorem :: PZFMISC1:19 :: ZFMISC_1:16
I is non empty & {x} (/\) {y} = EmptyMS I implies x <> y;
theorem :: PZFMISC1:20 :: ZFMISC_1:18
{x} (/\) {y} = {x} implies x = y;
theorem :: PZFMISC1:21 :: ZFMISC_1:19
{x} (/\) {x,y} = {x};
theorem :: PZFMISC1:22 :: ZFMISC_1:20
I is non empty & {x} (\) {y} = {x} implies x <> y;
theorem :: PZFMISC1:23 :: ZFMISC_1:21
{x} (\) {y} = EmptyMS I implies x = y;
theorem :: PZFMISC1:24 :: ZFMISC_1:22
{x} (\) {x,y} = EmptyMS I;
theorem :: PZFMISC1:25 :: ZFMISC_1:24
{x} c= {y} implies {x} = {y};
theorem :: PZFMISC1:26 :: ZFMISC_1:26
{x,y} c= {A} implies x = A & y = A;
theorem :: PZFMISC1:27 :: ZFMISC_1:27
{x,y} c= {A} implies {x,y} = {A};
theorem :: PZFMISC1:28 :: ZFMISC_1:30
bool { x } = { EmptyMS I, {x} };
theorem :: PZFMISC1:29 :: ZFMISC_1:80
{ A } c= bool A;
theorem :: PZFMISC1:30 :: ZFMISC_1:31
union { x } = x;
theorem :: PZFMISC1:31 :: ZFMISC_1:32
union { {x},{y} } = {x,y};
theorem :: PZFMISC1:32 :: ZFMISC_1:93
union { A,B } = A (\/) B;
theorem :: PZFMISC1:33 :: ZFMISC_1:37
{x} c= X iff x in X;
theorem :: PZFMISC1:34 :: ZFMISC_1:38
{x1,x2} c= X iff x1 in X & x2 in X;
theorem :: PZFMISC1:35 :: ZFMISC_1:42
A = EmptyMS I or A = {x1} or A = {x2} or A = {x1,x2} implies A c= {x1,x2};
begin :: Sum of an unordered pairs (or a singelton) and a set
theorem :: PZFMISC1:36 :: SETWISEO:6
x in A or x = B implies x in A (\/) {B};
theorem :: PZFMISC1:37 :: SETWISEO:8
A (\/) {x} c= B iff x in B & A c= B;
theorem :: PZFMISC1:38 :: ZFMISC_1:45
{x} (\/) X = X implies x in X;
theorem :: PZFMISC1:39 :: ZFMISC_1:46
x in X implies {x} (\/) X = X;
theorem :: PZFMISC1:40 :: ZFMISC_1:47, 48
{x,y} (\/) A = A iff x in A & y in A;
theorem :: PZFMISC1:41 :: ZFMISC_1:49
I is non empty implies {x} (\/) X <> EmptyMS I;
theorem :: PZFMISC1:42 :: ZFMISC_1:50
I is non empty implies {x,y} (\/) X <> EmptyMS I;
begin :: Intersection of an unordered pairs (or a singelton) and a set
theorem :: PZFMISC1:43 :: ZFMISC_1:51
X (/\) {x} = {x} implies x in X;
theorem :: PZFMISC1:44 :: ZFMISC_1:52
x in X implies X (/\) {x} = {x};
theorem :: PZFMISC1:45 :: ZFMISC_1:53, 63
x in X & y in X iff {x,y} (/\) X = {x,y};
theorem :: PZFMISC1:46 :: ZFMISC_1:54
I is non empty & {x} (/\) X = EmptyMS I implies not x in X;
theorem :: PZFMISC1:47 :: ZFMISC_1:55
I is non empty & {x,y} (/\) X = EmptyMS I implies not x in X & not y in X;
begin :: Difference of an unordered pairs (or a singelton) and a set
theorem :: PZFMISC1:48 :: ZFMISC_1:64 a
y in X (\) {x} implies y in X;
theorem :: PZFMISC1:49 :: ZFMISC_1:64 b
I is non empty & y in X (\) {x} implies y <> x;
theorem :: PZFMISC1:50 :: ZFMISC_1:65
I is non empty & X (\) {x} = X implies not x in X;
theorem :: PZFMISC1:51 :: ZFMISC_1:67
I is non empty & {x} (\) X = {x} implies not x in X;
theorem :: PZFMISC1:52 :: ZFMISC_1:68
{x} (\) X = EmptyMS I iff x in X;
theorem :: PZFMISC1:53 :: ZFMISC_1:70
I is non empty & {x,y} (\) X = {x} implies not x in X;
theorem :: PZFMISC1:54 :: ZFMISC_1:72
I is non empty & {x,y} (\) X = {x,y} implies not x in X & not y in X;
theorem :: PZFMISC1:55 :: ZFMISC_1:73
{x,y} (\) X = EmptyMS I iff x in X & y in X;
theorem :: PZFMISC1:56 :: ZFMISC_1:75
X = EmptyMS I or X = {x} or X = {y} or X = {x,y}
implies X (\) {x,y} = EmptyMS I;
begin :: Cartesian product
theorem :: PZFMISC1:57 :: ZFMISC_1:113
X = EmptyMS I or Y = EmptyMS I implies [|X,Y|] = EmptyMS I;
theorem :: PZFMISC1:58 :: ZFMISC_1:114
X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] implies X = Y;
theorem :: PZFMISC1:59 :: ZFMISC_1:115
[|X,X|] = [|Y,Y|] implies X = Y;
theorem :: PZFMISC1:60 :: ZFMISC_1:117
Z is non-empty & ([|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|]) implies X c= Y;
theorem :: PZFMISC1:61 :: ZFMISC_1:118
X c= Y implies [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|];
theorem :: PZFMISC1:62 :: ZFMISC_1:119
x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|];
theorem :: PZFMISC1:63 :: ZFMISC_1:120
[|X (\/) Y, Z|] = [|X, Z|] (\/) [|Y, Z|] &
[|Z, X (\/) Y|] = [|Z, X|] (\/) [|Z, Y|];
theorem :: PZFMISC1:64 :: ZFMISC_1:121
[|x1 (\/) x2, A (\/) B|] = [|x1,A|] (\/) [|x1,B|] (\/) [|x2,A|] (\/) [|x2,B|]
;
theorem :: PZFMISC1:65 :: ZFMISC_1:122
[|X (/\) Y, Z|] = [|X, Z|] (/\) [|Y, Z|] &
[|Z, X (/\) Y|] = [|Z, X|] (/\) [|Z, Y|];
theorem :: PZFMISC1:66 :: ZFMISC_1:123
[|x1 (/\) x2, A (/\) B|] = [|x1,A|] (/\) [|x2, B|];
theorem :: PZFMISC1:67 :: ZFMISC_1:124
A c= X & B c= Y implies [|A,Y|] (/\) [|X,B|] = [|A,B|];
theorem :: PZFMISC1:68 :: ZFMISC_1:125
[|X (\) Y, Z|] = [|X, Z|] (\) [|Y, Z|] &
[|Z, X (\) Y|] = [|Z, X|] (\) [|Z, Y|];
theorem :: PZFMISC1:69 :: ZFMISC_1:126
[|x1,x2|] (\) [|A,B|] = [|x1(\)A,x2|] (\/) [|x1,x2(\)B|];
theorem :: PZFMISC1:70 :: ZFMISC_1:127
x1 (/\) x2 = EmptyMS I or A (/\) B = EmptyMS I
implies [|x1,A|] (/\) [|x2,B|] = EmptyMS I;
theorem :: PZFMISC1:71 :: ZFMISC_1:130
X is non-empty implies [|{x},X|] is non-empty & [|X,{x}|] is non-empty;
theorem :: PZFMISC1:72 :: ZFMISC_1:132
[|{x,y},X|] = [|{x},X|] (\/) [|{y},X|] &
[|X,{x,y}|] = [|X,{x}|] (\/) [|X,{y}|];
theorem :: PZFMISC1:73 :: ZFMISC_1:134
x1 is non-empty & A is non-empty & [|x1,A|] = [|x2,B|]
implies x1 = x2 & A = B;
theorem :: PZFMISC1:74 :: ZFMISC_1:116, 135
X c= [|X,Y|] or X c= [|Y,X|] implies X = EmptyMS I;
theorem :: PZFMISC1:75 :: BORSUK_1:2
A in [|x,y|] & A in [|X,Y|] implies A in [|x (/\) X, y (/\) Y|];
theorem :: PZFMISC1:76 :: BORSUK_1:7
[|x,X|] c= [|y,Y|] & [|x,X|] is non-empty implies x c= y & X c= Y;
theorem :: PZFMISC1:77 :: REALSET1:4
A c= X implies [|A,A|] c= [|X,X|];
theorem :: PZFMISC1:78 :: SYSREL:17
X (/\) Y = EmptyMS I implies [|X,Y|] (/\) [|Y,X|] = EmptyMS I;
theorem :: PZFMISC1:79 :: ALTCAT_1:1
A is non-empty & ([|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|]) implies B c= Y;
theorem :: PZFMISC1:80 :: PARTFUN1:1
x c= [|A,B|] & y c= [|X,Y|] implies x (\/) y c= [|A (\/) X,B (\/) Y|];
begin :: Addenda
:: from AUTALG_1
definition
let I, A, B;
pred A is_transformable_to B means
:: PZFMISC1:def 3
for i be set st i in I holds B.i = {} implies A.i = {};
reflexivity;
end;