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