ZFMISC_1: Some Basic Properties of Sets

Lm19: for A, B being set st ( for z being set st z in A holds
ex x, y being set st z = [x,y] ) & ( for z being set st z in B holds
ex x, y being set st z = [x,y] ) & ( for x, y being set holds
( [x,y] in A iff [x,y] in B ) ) holds
A = B

proof end;

theorem Th90: :: ZFMISC_1:90

for X, Y being set holds
( [:X,Y:] = {} iff ( X = {} or Y = {} ) )

proof end;

theorem :: ZFMISC_1:91

for X, Y being set st X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] holds
X = Y

proof end;

theorem :: ZFMISC_1:92

for X, Y being set st [:X,X:] = [:Y,Y:] holds
X = Y

proof end;

Lm20: for z, X, Y being set st z in [:X,Y:] holds
ex x, y being set st [x,y] = z

proof end;

theorem :: ZFMISC_1:93

for X being set st X c= [:X,X:] holds
X = {}

proof end;

theorem :: ZFMISC_1:94

for Z, X, Y being set st Z <> {} & ( [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:] ) holds
X c= Y

proof end;

theorem Th95: :: ZFMISC_1:95

for X, Y, Z being set st X c= Y holds
( [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:] )

proof end;

theorem Th96: :: ZFMISC_1:96

for X1, Y1, X2, Y2 being set st X1 c= Y1 & X2 c= Y2 holds
[:X1,X2:] c= [:Y1,Y2:]

proof end;

theorem Th97: :: ZFMISC_1:97

for X, Y, Z being set holds
( [:(X \/ Y),Z:] = [:X,Z:] \/ [:Y,Z:] & [:Z,(X \/ Y):] = [:Z,X:] \/ [:Z,Y:] )

proof end;

theorem :: ZFMISC_1:98

for X1, X2, Y1, Y2 being set holds [:(X1 \/ X2),(Y1 \/ Y2):] = (([:X1,Y1:] \/ [:X1,Y2:]) \/ [:X2,Y1:]) \/ [:X2,Y2:]

proof end;

theorem :: ZFMISC_1:99

for X, Y, Z being set holds
( [:(X /\ Y),Z:] = [:X,Z:] /\ [:Y,Z:] & [:Z,(X /\ Y):] = [:Z,X:] /\ [:Z,Y:] )

proof end;

theorem Th100: :: ZFMISC_1:100

for X1, X2, Y1, Y2 being set holds [:(X1 /\ X2),(Y1 /\ Y2):] = [:X1,Y1:] /\ [:X2,Y2:]

proof end;

theorem :: ZFMISC_1:101

for A, X, B, Y being set st A c= X & B c= Y holds
[:A,Y:] /\ [:X,B:] = [:A,B:]

proof end;

theorem Th102: :: ZFMISC_1:102

for X, Y, Z being set holds
( [:(X \ Y),Z:] = [:X,Z:] \ [:Y,Z:] & [:Z,(X \ Y):] = [:Z,X:] \ [:Z,Y:] )

proof end;

theorem :: ZFMISC_1:103

for X1, X2, Y1, Y2 being set holds [:X1,X2:] \ [:Y1,Y2:] = [:(X1 \ Y1),X2:] \/ [:X1,(X2 \ Y2):]

proof end;

theorem Th104: :: ZFMISC_1:104

for X1, X2, Y1, Y2 being set st ( X1 misses X2 or Y1 misses Y2 ) holds
[:X1,Y1:] misses [:X2,Y2:]

proof end;

theorem :: ZFMISC_1:105

for x, y, z, Y being set holds
( [x,y] in [:{z},Y:] iff ( x = z & y in Y ) )

proof end;

theorem :: ZFMISC_1:106

for x, y, X, z being set holds
( [x,y] in [:X,{z}:] iff ( x in X & y = z ) )

proof end;

theorem :: ZFMISC_1:107

for X, x being set st X <> {} holds
( [:{x},X:] <> {} & [:X,{x}:] <> {} ) by Th90;

theorem :: ZFMISC_1:108

for x, y, X, Y being set st x <> y holds
( [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:] )

proof end;

theorem :: ZFMISC_1:109

for x, y, X being set holds
( [:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:] )

proof end;

theorem Th110: :: ZFMISC_1:110

for X1, Y1, X2, Y2 being set st X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] holds
( X1 = X2 & Y1 = Y2 )

proof end;

theorem :: ZFMISC_1:111

for X, Y being set st ( X c= [:X,Y:] or X c= [:Y,X:] ) holds
X = {}

proof end;

theorem :: ZFMISC_1:112

for N being set ex M being set st
( N in M & ( for X, Y being set st X in M & Y c= X holds
Y in M ) & ( for X being set st X in M holds
bool X in M ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) )

proof end;

theorem :: ZFMISC_1:113

for e, X1, Y1, X2, Y2 being set st e in [:X1,Y1:] & e in [:X2,Y2:] holds
e in [:(X1 /\ X2),(Y1 /\ Y2):]

proof end;

begin

:: from BORSUK_1

theorem Th114: :: ZFMISC_1:114

for X1, X2, Y1, Y2 being set st [:X1,X2:] c= [:Y1,Y2:] & [:X1,X2:] <> {} holds
( X1 c= Y1 & X2 c= Y2 )

proof end;

:: from ALTCAT_1

theorem :: ZFMISC_1:115

for A being non empty set
for B, C, D being set st ( [:A,B:] c= [:C,D:] or [:B,A:] c= [:D,C:] ) holds
B c= D

proof end;

theorem :: ZFMISC_1:116

for x, X being set st x in X holds
(X \ {x}) \/ {x} = X

proof end;

theorem :: ZFMISC_1:117

for x, X being set st not x in X holds
(X \/ {x}) \ {x} = X

proof end;

:: from WAYBEL18, 2006.01.06, A.T.

theorem :: ZFMISC_1:118

for x, y, z, Z being set holds
( Z c= {x,y,z} iff ( Z = {} or Z = {x} or Z = {y} or Z = {z} or Z = {x,y} or Z = {y,z} or Z = {x,z} or Z = {x,y,z} ) )

proof end;

:: from PARTFUN1, 2006.12.05, A.T.

theorem :: ZFMISC_1:119

for N, M, X1, Y1, X2, Y2 being set st N c= [:X1,Y1:] & M c= [:X2,Y2:] holds
N \/ M c= [:(X1 \/ X2),(Y1 \/ Y2):]

proof end;

Lm21: for x, y, X being set st not x in X & not y in X holds
{x,y} misses X

proof end;

theorem Th120: :: ZFMISC_1:120

for x, y, X being set st not x in X & not y in X holds
X = X \ {x,y}

proof end;

theorem :: ZFMISC_1:121

for x, y, X being set st not x in X & not y in X holds
X = (X \/ {x,y}) \ {x,y}

proof end;

:: from INCPROJ, 2007.01.18. AK

definition

let x1, x2, x3 be set ;

pred x1,x2,x3 are_mutually_different means :: ZFMISC_1:def 5
( x1 <> x2 & x1 <> x3 & x2 <> x3 );

end;

:: deftheorem defines are_mutually_different ZFMISC_1:def 5 :

definition

let x1, x2, x3, x4 be set ;

pred x1,x2,x3,x4 are_mutually_different means :: ZFMISC_1:def 6
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 );

end;

:: deftheorem defines are_mutually_different ZFMISC_1:def 6 :

:: from CARD_2, 2007.01.18. AK

definition

let x1, x2, x3, x4, x5 be set ;

pred x1,x2,x3,x4,x5 are_mutually_different means :: ZFMISC_1:def 7
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 );

end;

:: deftheorem defines are_mutually_different ZFMISC_1:def 7 :

:: from BORSUK_5, 2007.01.18. AK

definition

let x1, x2, x3, x4, x5, x6 be set ;

pred x1,x2,x3,x4,x5,x6 are_mutually_different means :: ZFMISC_1:def 8
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x4 <> x5 & x4 <> x6 & x5 <> x6 );

end;

:: deftheorem defines are_mutually_different ZFMISC_1:def 8 :

definition

let x1, x2, x3, x4, x5, x6, x7 be set ;

pred x1,x2,x3,x4,x5,x6,x7 are_mutually_different means :: ZFMISC_1:def 9
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x1 <> x6 & x1 <> x7 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x2 <> x6 & x2 <> x7 & x3 <> x4 & x3 <> x5 & x3 <> x6 & x3 <> x7 & x4 <> x5 & x4 <> x6 & x4 <> x7 & x5 <> x6 & x5 <> x7 & x6 <> x7 );

end;

:: deftheorem defines are_mutually_different ZFMISC_1:def 9 :