Journal of Formalized Mathematics
Volume 7, 1995
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### Some Basic Properties of Many Sorted Sets

by
Artur Kornilowicz

MML identifier: PZFMISC1
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_1, PBOOLE, RELAT_1, FUNCT_4, CAT_1, BOOLE, MATRIX_1,
ZF_REFLE, PRE_CIRC, FINSET_1, CAT_4, TARSKI, PRALG_2;
notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, FUNCT_1, FUNCT_4, FINSET_1,
CQC_LANG, PBOOLE, PRE_CIRC, PRALG_2, MBOOLEAN;
constructors CQC_LANG, PRE_CIRC, PRALG_2, MBOOLEAN;
clusters FINSET_1, PBOOLE, CQC_LANG, XBOOLE_0;
requirements BOOLE;

begin :: Preliminaries

reserve i, I for set,
f for Function,
x, x1, x2, y, A, B, X, Y, Z for ManySortedSet of I,
J for non empty set,
NJ for ManySortedSet of J;

theorem :: PZFMISC1:1
for X be set 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 st i in I holds it.i = {A.i};
end;

definition let I, A;
cluster {A} -> non-empty locally-finite;
end;

definition let I, A, B;
func {A,B} -> ManySortedSet of I means
:: PZFMISC1:def 2
for i st i in I holds it.i = {A.i,B.i};
commutativity;
end;

definition let I, A, B;
cluster {A,B} -> non-empty locally-finite;
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
{ NJ } <> [0]I;

theorem :: PZFMISC1:8     :: ENUMSET1:3
x in { A } implies x = A;

theorem :: PZFMISC1:9     :: ENUMSET1:4
x in { x };

theorem :: PZFMISC1:10     :: ENUMSET1:9
x = A or x = B implies x in { A,B };

theorem :: PZFMISC1:11     ::ENUMSET1:41
{A} \/ {B} = {A,B};

theorem :: PZFMISC1:12     :: ENUMSET1:69
{ x,x } = { x };

canceled;

theorem :: PZFMISC1:14     :: SETWISEO:1
{A} c= {B} implies A = B;

theorem :: PZFMISC1:15     :: ZFMISC_1:6
{x} = {y} implies x = y;

theorem :: PZFMISC1:16     :: ZFMISC_1:8
{x} = {A,B} implies x = A & x = B;

theorem :: PZFMISC1:17     :: ZFMISC_1:9
{x} = {A,B} implies A = B;

theorem :: PZFMISC1:18     :: ZFMISC_1:12
{x} c= {x,y} & {y} c= {x,y};

theorem :: PZFMISC1:19     :: ZFMISC_1:13
{x} \/ {y} = {x} or {x} \/ {y} = {y} implies x = y;

theorem :: PZFMISC1:20     :: ZFMISC_1:14
{x} \/ {x,y} = {x,y};

canceled;

theorem :: PZFMISC1:22     :: ZFMISC_1:16
I is non empty & {x} /\ {y} = [0]I implies x <> y;

theorem :: PZFMISC1:23     :: ZFMISC_1:18
{x} /\ {y} = {x} or {x} /\ {y} = {y} implies x = y;

theorem :: PZFMISC1:24     :: ZFMISC_1:19
{x} /\ {x,y} = {x} & {y} /\ {x,y} = {y};

theorem :: PZFMISC1:25     :: ZFMISC_1:20
I is non empty & {x} \ {y} = {x} implies x <> y;

theorem :: PZFMISC1:26     :: ZFMISC_1:21
{x} \ {y} = [0]I implies x = y;

theorem :: PZFMISC1:27     :: ZFMISC_1:22
{x} \ {x,y} = [0]I & {y} \ {x,y} = [0]I;

theorem :: PZFMISC1:28     :: ZFMISC_1:24
{x} c= {y} implies {x} = {y};

theorem :: PZFMISC1:29     :: ZFMISC_1:26
{x,y} c= {A} implies x = A & y = A;

theorem :: PZFMISC1:30     :: ZFMISC_1:27
{x,y} c= {A} implies {x,y} = {A};

theorem :: PZFMISC1:31     :: ZFMISC_1:30
bool { x } = { [0]I, {x} };

theorem :: PZFMISC1:32     :: ZFMISC_1:80
{ A } c= bool A;

theorem :: PZFMISC1:33     :: ZFMISC_1:31
union { x } = x;

theorem :: PZFMISC1:34     :: ZFMISC_1:32
union { {x},{y} } = {x,y};

theorem :: PZFMISC1:35     :: ZFMISC_1:93
union { A,B } = A \/ B;

theorem :: PZFMISC1:36     :: ZFMISC_1:37
{x} c= X iff x in X;

theorem :: PZFMISC1:37     :: ZFMISC_1:38
{x1,x2} c= X iff x1 in X & x2 in X;

theorem :: PZFMISC1:38     :: ZFMISC_1:42
A = [0]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:39     :: SETWISEO:6
x in A or x = B implies x in A \/ {B};

theorem :: PZFMISC1:40     :: SETWISEO:8
A \/ {x} c= B iff x in B & A c= B;

theorem :: PZFMISC1:41     :: ZFMISC_1:45
{x} \/ X = X implies x in X;

theorem :: PZFMISC1:42     :: ZFMISC_1:46
x in X implies {x} \/ X = X;

theorem :: PZFMISC1:43     :: ZFMISC_1:47, 48
{x,y} \/ A = A iff x in A & y in A;

theorem :: PZFMISC1:44     :: ZFMISC_1:49
I is non empty implies {x} \/ X <> [0]I;

theorem :: PZFMISC1:45     :: ZFMISC_1:50
I is non empty implies {x,y} \/ X <> [0]I;

begin :: Intersection of an unordered pairs (or a singelton) and a set

theorem :: PZFMISC1:46     :: ZFMISC_1:51
X /\ {x} = {x} implies x in X;

theorem :: PZFMISC1:47     :: ZFMISC_1:52
x in X implies X /\ {x} = {x};

theorem :: PZFMISC1:48     :: ZFMISC_1:53, 63
x in X & y in X iff {x,y} /\ X = {x,y};

theorem :: PZFMISC1:49     :: ZFMISC_1:54
I is non empty & {x} /\ X = [0]I implies not x in X;

theorem :: PZFMISC1:50     :: ZFMISC_1:55
I is non empty & {x,y} /\ X = [0]I implies not x in X & not y in X;

begin :: Difference of an unordered pairs (or a singelton) and a set

theorem :: PZFMISC1:51     :: ZFMISC_1:64 a
y in X \ {x} implies y in X;

theorem :: PZFMISC1:52     :: ZFMISC_1:64 b
I is non empty & y in X \ {x} implies y <> x;

theorem :: PZFMISC1:53     :: ZFMISC_1:65
I is non empty & X \ {x} = X implies not x in X;

theorem :: PZFMISC1:54     :: ZFMISC_1:67
I is non empty & {x} \ X = {x} implies not x in X;

theorem :: PZFMISC1:55     :: ZFMISC_1:68
{x} \ X = [0]I iff x in X;

theorem :: PZFMISC1:56     :: ZFMISC_1:70
I is non empty & {x,y} \ X = {x} implies not x in X;

canceled;

theorem :: PZFMISC1:58     :: ZFMISC_1:72
I is non empty & {x,y} \ X = {x,y} implies not x in X & not y in X;

theorem :: PZFMISC1:59     :: ZFMISC_1:73
{x,y} \ X = [0]I iff x in X & y in X;

theorem :: PZFMISC1:60     :: ZFMISC_1:75
X = [0]I or X = {x} or X = {y} or X = {x,y} implies X \ {x,y} = [0]I;

begin :: Cartesian product

theorem :: PZFMISC1:61     :: ZFMISC_1:113
X = [0]I or Y = [0]I implies [|X,Y|] = [0]I;

theorem :: PZFMISC1:62     :: ZFMISC_1:114
X is non-empty & Y is non-empty & [|X,Y|] = [|Y,X|] implies X = Y;

theorem :: PZFMISC1:63     :: ZFMISC_1:115
[|X,X|] = [|Y,Y|] implies X = Y;

theorem :: PZFMISC1:64     :: ZFMISC_1:117
Z is non-empty & ([|X,Z|] c= [|Y,Z|] or [|Z,X|] c= [|Z,Y|]) implies X c= Y;

theorem :: PZFMISC1:65     :: ZFMISC_1:118
X c= Y implies [|X,Z|] c= [|Y,Z|] & [|Z,X|] c= [|Z,Y|];

theorem :: PZFMISC1:66     :: ZFMISC_1:119
x1 c= A & x2 c= B implies [|x1,x2|] c= [|A,B|];

theorem :: PZFMISC1:67     :: ZFMISC_1:120
[|X \/ Y, Z|] = [|X, Z|] \/ [|Y, Z|]
& [|Z, X \/ Y|] = [|Z, X|] \/ [|Z, Y|];

theorem :: PZFMISC1:68     :: ZFMISC_1:121
[|x1 \/ x2, A \/ B|] = [|x1,A|] \/ [|x1,B|] \/ [|x2,A|] \/ [|x2,B|];

theorem :: PZFMISC1:69     :: ZFMISC_1:122
[|X /\ Y, Z|] = [|X, Z|] /\ [|Y, Z|]
& [|Z, X /\ Y|] = [|Z, X|] /\ [|Z, Y|];

theorem :: PZFMISC1:70     :: ZFMISC_1:123
[|x1 /\ x2, A /\ B|] = [|x1,A|] /\ [|x2, B|];

theorem :: PZFMISC1:71     :: ZFMISC_1:124
A c= X & B c= Y implies [|A,Y|] /\ [|X,B|] = [|A,B|];

theorem :: PZFMISC1:72     :: ZFMISC_1:125
[|X \ Y, Z|] = [|X, Z|] \ [|Y, Z|]
& [|Z, X \ Y|] = [|Z, X|] \ [|Z, Y|];

theorem :: PZFMISC1:73     :: ZFMISC_1:126
[|x1,x2|] \ [|A,B|] = [|x1\A,x2|] \/ [|x1,x2\B|];

theorem :: PZFMISC1:74     :: ZFMISC_1:127
x1 /\ x2 = [0]I or A /\ B = [0]I implies [|x1,A|] /\ [|x2,B|] = [0]I;

theorem :: PZFMISC1:75     :: ZFMISC_1:130
X is non-empty implies [|{x},X|] is non-empty & [|X,{x}|] is non-empty;

theorem :: PZFMISC1:76     :: ZFMISC_1:132
[|{x,y},X|] = [|{x},X|] \/ [|{y},X|]
& [|X,{x,y}|] = [|X,{x}|] \/ [|X,{y}|];

theorem :: PZFMISC1:77     :: ZFMISC_1:134
x1 is non-empty & A is non-empty & [|x1,A|] = [|x2,B|]
implies x1 = x2 & A = B;

theorem :: PZFMISC1:78     :: ZFMISC_1:116, 135
X c= [|X,Y|] or X c= [|Y,X|] implies X = [0]I;

theorem :: PZFMISC1:79     :: BORSUK_1:2
A in [|x,y|] & A in [|X,Y|] implies A in [|x /\ X, y /\ Y|];

theorem :: PZFMISC1:80     :: BORSUK_1:7
[|x,X|] c= [|y,Y|] & [|x,X|] is non-empty implies x c= y & X c= Y;

theorem :: PZFMISC1:81     :: REALSET1:4
A c= X implies [|A,A|] c= [|X,X|];

theorem :: PZFMISC1:82     :: SYSREL:17
X /\ Y = [0]I implies [|X,Y|] /\ [|Y,X|] = [0]I;

theorem :: PZFMISC1:83     :: ALTCAT_1:1
A is non-empty & ([|A,B|] c= [|X,Y|] or [|B,A|] c= [|Y,X|]) implies B c= Y;

theorem :: PZFMISC1:84     :: PARTFUN1:1
x c= [|A,B|] & y c= [|X,Y|] implies x \/ y c= [|A \/ X,B \/ Y|];
```