Copyright (c) 1989 Association of Mizar Users
environ
vocabulary BOOLE, TARSKI, ZFMISC_1;
notation TARSKI, XBOOLE_0;
constructors TARSKI, XBOOLE_0;
clusters XBOOLE_0;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0, ENUMSET1, XBOOLE_1;
schemes XBOOLE_0;
begin
reserve v,x,x1,x2,y,y1,y2,z,A,B,X,X1,X2,X3,X4,Y,Y1,Y2,Z,N,M for set;
definition
let x, y be set;
cluster [x,y] -> non empty;
coherence proof
A1:[x, y] = {{x,y}, {x}} by TARSKI:def 5;
{x} in [x,y] by A1,TARSKI:def 2; then
[x,y] <> {} by XBOOLE_0:def 1;
hence thesis by XBOOLE_0:def 5;
end;
end;
Lm1: {x} <> {}
proof x in {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 1;
end;
Lm2:
{x} c= X iff x in X
proof
thus {x} c= X implies x in X
proof x in {x} by TARSKI:def 1; hence thesis by TARSKI:def 3; end;
assume
A1: x in X;
let y;
thus thesis by A1,TARSKI:def 1;
end;
Lm3:
Y c= X & not x in Y implies Y c= X \ { x }
proof assume
A1: Y c= X & not x in Y;
let y;
assume y in Y;
then y in X & not y in { x } by A1,TARSKI:def 1,def 3;
hence thesis by XBOOLE_0:def 4;
end;
Lm4:
Y c= { x } iff Y = {} or Y = { x }
proof
thus Y c= { x } implies Y = {} or Y = { x }
proof assume
A1: Y c= { x };
x in Y or not x in Y;
then { x } c= Y or Y c= { x } \ { x } by A1,Lm2,Lm3;
then { x } = Y or Y c= {} by A1,XBOOLE_0:def 10,XBOOLE_1:37;
hence Y = {} or Y = { x } by XBOOLE_1:3;
end;
thus thesis by XBOOLE_1:2;
end;
definition let X;
defpred IT[set] means $1 c= X;
func bool X means
:Def1: Z in it iff Z c= X;
existence
proof
consider M such that
A1: X in M and
A2: for X,Y holds X in M & Y c= X implies Y in M and
for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z and
for X holds X c= M implies X,M are_equipotent or X in M by TARSKI:9;
consider IT being set such that
A3: Y in IT iff Y in M & IT[Y] from Separation;
take IT; let Y;
thus Y in IT implies Y c= X by A3;
assume
A4: Y c= X;
then Y in M by A1,A2;
hence Y in IT by A3,A4;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being set holds x in X1 iff IT[x]) &
(for x being set holds x in X2 iff IT[x]) holds X1 = X2
from SetEq;
end;
end;
definition let X1,X2;
defpred X[set] means ex x,y st x in X1 & y in X2 & $1 = [x,y];
func [: X1,X2 :] means
:Def2: z in it iff ex x,y st x in X1 & y in X2 & z = [x,y];
existence
proof
consider X such that
A1: for z holds z in X iff z in bool(bool(X1 \/ X2)) & X[z]
from Separation;
take X;
let z;
thus z in X implies ex x,y st x in X1 & y in X2 & z = [x,y] by A1;
given x,y such that
A2: x in X1 and
A3: y in X2 and
A4: z = [x,y];
{x} c= X1 & X1 c= X1 \/ X2 by A2,Lm2,XBOOLE_1:7;
then {x} c= X1 \/ X2 by XBOOLE_1:1;
then A5: {x} in bool(X1 \/ X2) by Def1;
{x,y} c= X1 \/ X2
proof
let z;
assume z in {x,y};
then z = x or z = y by TARSKI:def 2;
hence thesis by A2,A3,XBOOLE_0:def 2;
end;
then A6: {x,y} in bool(X1 \/ X2) by Def1;
{{x,y},{x}} c= bool(X1 \/ X2)
proof let z;
assume z in {{x,y},{x}};
hence thesis by A5,A6,TARSKI:def 2;
end;
then {{x,y},{x}} in bool(bool(X1 \/ X2)) by Def1;
then z in bool(bool(X1 \/ X2)) by A4,TARSKI:def 5;
hence thesis by A1,A2,A3,A4;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being set holds x in X1 iff X[x]) &
(for x being set holds x in X2 iff X[x]) holds X1 = X2
from SetEq;
end;
end;
definition let X1,X2,X3;
func [: X1,X2,X3 :] equals [:[:X1,X2:],X3:];
coherence;
end;
definition let X1,X2,X3,X4;
func [: X1,X2,X3,X4 :] equals [:[:X1,X2,X3:],X4:];
coherence;
end;
begin
::
:: Empty set.
::
theorem
bool {} = { {} }
proof
now let x be set;
x c= {} iff x = {} by XBOOLE_1:3;
hence x in bool {} iff x in { {} } by Def1,TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem
union {} = {}
proof
now given x such that
A1: x in union {};
ex X being set st x in X & X in {} by A1,TARSKI:def 4;
hence contradiction by XBOOLE_0:def 1;
end;
hence thesis by XBOOLE_0:def 1;
end;
::
:: Singleton and unordered pairs.
::
canceled 3;
theorem Th6:
{x} c= {y} implies x = y
proof
A1: {x} = {y} implies x = y
proof x in { x } by TARSKI:def 1; hence thesis by TARSKI:def 1; end;
assume {x} c= {y};
then {x} = {} or {x} = {y} by Lm4;
hence thesis by A1,Lm1;
end;
canceled;
theorem Th8:
{x} = {y1,y2} implies x = y1
proof assume { x } = { y1,y2 };
then y1 in { x } & y2 in { x } by TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
theorem Th9:
{x} = {y1,y2} implies y1 = y2
proof assume { x } = { y1,y2 };
then x = y1 & x = y2 by Th8;
hence thesis;
end;
theorem Th10:
{ x1,x2 } = { y1,y2 } implies x1 = y1 or x1 = y2
proof x1 in { x1,x2 } & x2 in { x1,x2 } by TARSKI:def 2;
hence thesis by TARSKI:def 2;
end;
canceled;
theorem Th12:
{x} c= {x,y}
proof
thus {x} c= {x,y}
proof let z; assume z in {x};
then z=x by TARSKI:def 1;
hence thesis by TARSKI:def 2;
end;
end;
Lm5:
{x} \/ X c= X implies x in X
proof
assume
A1: {x} \/ X c= X;
assume not x in X;
then not x in {x} \/ X by A1,TARSKI:def 3;
then not x in {x} by XBOOLE_0:def 2;
hence thesis by TARSKI:def 1;
end;
theorem
{x} \/ {y} = {x} implies x = y
proof assume {x} \/ {y} = {x};
then y in {x} or x in {y} by Lm5;
hence thesis by TARSKI:def 1;
end;
Lm6:
x in X implies {x} \/ X = X
proof assume x in X; then {x} c= X by Lm2; hence thesis by XBOOLE_1:12; end;
theorem
{x} \/ {x,y} = {x,y}
proof x in {x,y} by TARSKI:def 2; hence thesis by Lm6; end;
Lm7:
{x} misses X implies not x in X
proof assume that
A1: {x} /\ X = {} and
A2: x in X;
x in {x} by TARSKI:def 1;
then x in {x} /\ X by A2,XBOOLE_0:def 3;
hence contradiction by A1,XBOOLE_0:def 1;
end;
canceled;
theorem
{x} misses {y} implies x <> y
proof assume {x} misses {y};
then not x in {y} by Lm7;
hence thesis by TARSKI:def 1;
end;
Lm8:
not x in X implies {x} misses X
proof assume
A1: not x in X;
thus {x} /\ X c= {}
proof let y;
assume y in {x} /\ X;
then y in {x} & y in X by XBOOLE_0:def 3;
hence thesis by A1,TARSKI:def 1;
end;
thus {} c= {x} /\ X by XBOOLE_1:2;
end;
theorem Th17:
x <> y implies {x} misses {y}
proof assume x <> y;
then not x in {y} by TARSKI:def 1;
hence {x} misses {y} by Lm8;
end;
Lm9:
X /\ {x} = {x} implies x in X
proof assume X /\ {x} = {x};
then x in X /\ {x} by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
theorem
{x} /\ {y} = {x} implies x = y
proof assume {x} /\ {y} = {x};
then x in {y} or y in {x} by Lm9;
hence thesis by TARSKI:def 1;
end;
Lm10:
x in X implies X /\ {x} = {x}
proof assume x in X;
then {x} c= X by Lm2;
hence thesis by XBOOLE_1:28;
end;
theorem
{x} /\ {x,y} = {x}
proof x in {x,y} & y in {x,y} by TARSKI:def 2; hence thesis by Lm10; end;
Lm11:
{x} \ X = {x} iff not x in X
proof {x} \ X = {x} iff {x} misses X by XBOOLE_1:83;
hence thesis by Lm7,Lm8;
end;
theorem
{x} \ {y} = {x} iff x <> y
proof {x} \ {y} = {x} iff not x in {y} by Lm11; hence thesis by TARSKI:def 1;
end;
Lm12:
{x} \ X = {} iff x in X
proof {x} \ X = {} iff {x} c= X by XBOOLE_1:37; hence thesis by Lm2; end;
theorem
{x} \ {y} = {} implies x = y
proof assume {x} \ {y} = {}; then x in {y} by Lm12;
hence thesis by TARSKI:def 1;
end;
theorem
{x} \ {x,y} = {}
proof x in {x,y} & y in {x,y} by TARSKI:def 2;
hence thesis by Lm12;
end;
Lm13:
{x,y} \ X = {x} iff not x in X & (y in X or x = y)
proof
thus {x,y} \ X = {x} implies not x in X & (y in X or x = y)
proof assume
A1: {x,y} \ X = {x};
then x in {x,y} \ X by TARSKI:def 1;
hence not x in X by XBOOLE_0:def 4;
assume
A2: not y in X;
y in {x,y} by TARSKI:def 2;
then y in {x} by A1,A2,XBOOLE_0:def 4;
hence thesis by TARSKI:def 1;
end;
assume that
A3: not x in X and
A4: y in X or x=y;
z in {x,y} \ X iff z=x
proof
(z in {x,y} \ X iff z in {x,y} & not z in X) &
(z in {x,y} iff z=x or z=y) by TARSKI:def 2,XBOOLE_0:def 4;
hence thesis by A3,A4;
end;
hence thesis by TARSKI:def 1;
end;
theorem
x <> y implies { x,y } \ { y } = { x }
proof assume x <> y;
then not x in {y} & y in {y} & not y in {x} & x in {x} & {x,y} = {y,x}
by TARSKI:def 1;
hence thesis by Lm13;
end;
theorem
{x} c= {y} implies x = y by Th6;
theorem
{z} c= {x,y} implies z = x or z = y
proof assume
A1: {z} c= {x,y};
z in {z} by TARSKI:def 1;
then z in {x,y} by A1,TARSKI:def 3;
hence thesis by TARSKI:def 2;
end;
theorem Th26:
{x,y} c= {z} implies x = z
proof assume
A1: {x,y} c= {z};
x in {x,y} & y in {x,y} by TARSKI:def 2;
then x in {z} & y in {z} by A1,TARSKI:def 3;
hence thesis by TARSKI:def 1;
end;
theorem
{x,y} c= {z} implies {x,y} = {z}
proof assume {x,y} c= {z};
then x=z & y=z by Th26;
hence thesis by ENUMSET1:69;
end;
Lm14:
X <> {x} & X <> {} implies ex y st y in X & y <> x
proof assume that
A1: X <> {x} and
A2: X <> {};
per cases;
suppose
A3: not x in X;
consider y being set such that
A4: y in X by A2,XBOOLE_0:def 1;
take y;
thus thesis by A3,A4;
suppose
A5: x in X;
consider y such that
A6: y in X & not y in {x} or y in {x} & not y in X by A1,TARSKI:2;
take y;
thus thesis by A5,A6,TARSKI:def 1;
end;
Lm15:
Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2}
proof
thus Z c= {x1,x2} implies Z={} or Z={x1} or Z={x2} or Z={x1,x2}
proof assume that
A1: Z c= {x1,x2} and
A2: Z <> {} and
A3: Z <> {x1} and
A4: Z <> {x2};
now let z;
thus z in Z implies z in {x1,x2} by A1,TARSKI:def 3;
A5: now assume
A6: not x1 in Z;
consider y such that
A7: y in Z and
A8: y<>x2 by A2,A4,Lm14;
y in {x1,x2} by A1,A7,TARSKI:def 3;
hence contradiction by A6,A7,A8,TARSKI:def 2;
end;
A9: now assume
A10: not x2 in Z;
consider y such that
A11: y in Z and
A12: y<>x1 by A2,A3,Lm14;
y in {x1,x2} by A1,A11,TARSKI:def 3;
hence contradiction by A10,A11,A12,TARSKI:def 2;
end;
assume z in {x1,x2};
hence z in Z by A5,A9,TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
thus thesis by Th12,XBOOLE_1:2;
end;
theorem
{x1,x2} c= {y1,y2} implies x1 = y1 or x1 = y2
proof
assume {x1,x2} c= {y1,y2};
then A1: {x1,x2}={} or {x1,x2}={y1} or {x1,x2}={y2} or {x1,x2}={y1,y2} by
Lm15;
x1 in {x1,x2} by TARSKI:def 2;
hence thesis by A1,Th8,Th10,XBOOLE_0:def 1;
end;
theorem
x <> y implies { x } \+\ { y } = { x,y }
proof assume
A1: x <> y;
z in { x } \+\ { y } iff z=x or z=y
proof
(z in {x} iff z=x) & (z in {y} iff z=y)
& (z in {x} \+\
{y} iff not ( z in {x} iff z in {y})) by TARSKI:def 1,XBOOLE_0:1;
hence thesis by A1;
end;
hence thesis by TARSKI:def 2;
end;
theorem
bool { x } = { {} , { x }}
proof
now let y;
y c= { x } iff y = {} or y = { x } by Lm4;
hence y in bool { x } iff y in { {}, { x }} by Def1,TARSKI:def 2;
end;
hence thesis by TARSKI:2;
end;
Lm16:
X in A implies X c= union A
proof assume
A1: X in A;
let x; thus thesis by A1,TARSKI:def 4;
end;
theorem
union { x } = x
proof
x in { x } by TARSKI:def 1;
then A1: x c= union { x } by Lm16;
union { x } c= x
proof let y;
assume y in union { x };
then ex Y being set st y in Y & Y in { x } by TARSKI:def 4;
hence thesis by TARSKI:def 1;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
Lm17:
union { X,Y } = X \/ Y
proof
x in union {X,Y} iff x in X or x in Y
proof
thus x in union {X,Y} implies x in X or x in Y
proof assume x in union {X,Y};
then ex Z st x in Z & Z in {X,Y} by TARSKI:def 4;
hence thesis by TARSKI:def 2;
end;
X in {X,Y} & Y in {X,Y} by TARSKI:def 2;
hence thesis by TARSKI:def 4;
end;
hence thesis by XBOOLE_0:def 2;
end;
theorem
union {{x},{y}} = {x,y}
proof
thus union {{x},{y}} = {x} \/ {y} by Lm17
.= {x,y} by ENUMSET1:41;
end;
::
:: Ordered pairs.
::
theorem Th33:
[x1,x2] = [y1,y2] implies x1 = y1 & x2 = y2
proof
A1: [x1,x2] = { {x1,x2}, {x1} } &
[y1,y2] = { {y1,y2}, {y1} } by TARSKI:def 5;
assume
A2: [x1,x2] = [y1,y2];
A3: now assume
A4: y1 = y2;
then { { y1 } } = { {y1}, {y1} } & { {y1}, {y1} } = { {x1,x2},{x1} }
by A1,A2,ENUMSET1:69;
then { y1 } = { x1,x2 } by Th8;
hence thesis by A4,Th8;
end;
now assume
A5: y1 <> y2;
then A6: {x1} <> {y1,y2} by Th9;
then {x1} = {y1} by A1,A2,Th10;
hence
A7: x1 = y1 by Th6;
{y1,y2} = {x1,x2} by A1,A2,A6,Th10;
hence x2 = y2 by A5,A7,Th10;
end;
hence thesis by A3;
end;
Lm18:
[x,y] in [:X,Y:] iff x in X & y in Y
proof
thus [x,y] in [:X,Y:] implies x in X & y in Y
proof assume [x,y] in [:X,Y:];
then ex x1,y1 st x1 in X & y1 in Y & [x,y]=[x1,y1] by Def2;
hence x in X & y in Y by Th33;
end;
thus thesis by Def2;
end;
theorem
[x,y] in [:{x1},{y1}:] iff x = x1 & y = y1
proof x=x1 & y=y1 iff x in {x1} & y in {y1} by TARSKI:def 1;
hence thesis by Lm18;
end;
theorem
[:{x},{y}:] = {[x,y]}
proof
now let z;
thus z in [:{x},{y}:] implies z in {[x,y]}
proof assume z in [:{x},{y}:];
then consider x1,y1 such that
A1: x1 in {x} & y1 in {y} and
A2: z=[x1,y1] by Def2;
x1=x & y1=y by A1,TARSKI:def 1;
hence thesis by A2,TARSKI:def 1;
end;
assume z in {[x,y]};
then z=[x,y] & x in {x} & y in {y} by TARSKI:def 1;
hence z in [:{x},{y}:] by Lm18;
end;
hence thesis by TARSKI:2;
end;
theorem
[:{x},{y,z}:] = {[x,y],[x,z]} & [:{x,y},{z}:] = {[x,z],[y,z]}
proof
thus [:{x},{y,z}:] = {[x,y],[x,z]}
proof
now let v;
thus v in [:{x},{y,z}:] implies v in {[x,y],[x,z]}
proof assume v in [:{x},{y,z}:];
then consider x1,y1 such that
A1: x1 in {x} & y1 in {y,z} and
A2: v=[x1,y1] by Def2;
x1=x & (y1=y or y1=z) by A1,TARSKI:def 1,def 2;
hence v in {[x,y],[x,z]} by A2,TARSKI:def 2;
end;
assume v in {[x,y],[x,z]};
then (v=[x,y] or v=[x,z]) & x in{x} & y in{y,z} & z in{y,z}
by TARSKI:def 1,def 2;
hence v in [:{x},{y,z}:] by Lm18;
end;
hence thesis by TARSKI:2;
end;
now let v;
thus v in [:{x,y},{z}:] implies v in {[x,z],[y,z]}
proof assume v in [:{x,y},{z}:];
then consider x1,y1 such that
A3: x1 in {x,y} & y1 in {z} and
A4: v=[x1,y1] by Def2;
y1=z & (x1=x or x1=y) by A3,TARSKI:def 1,def 2;
hence v in {[x,z],[y,z]} by A4,TARSKI:def 2;
end;
assume v in {[x,z],[y,z]};
then (v=[x,z] or v=[y,z]) & x in{x,y} & y in{x,y} & z in{z}
by TARSKI:def 1,def 2;
hence v in [:{x,y},{z}:] by Lm18;
end;
hence thesis by TARSKI:2;
end;
::
:: Singleton and unordered pairs included in a set.
::
theorem
{x} c= X iff x in X by Lm2;
theorem Th38:
{x1,x2} c= Z iff x1 in Z & x2 in Z
proof
thus {x1,x2} c= Z implies x1 in Z & x2 in Z
proof x1 in {x1,x2} & x2 in {x1,x2} by TARSKI:def 2;
hence thesis by TARSKI:def 3;
end;
assume
A1: x1 in Z & x2 in Z;
let z;
assume z in {x1,x2};
hence thesis by A1,TARSKI:def 2;
end;
::
:: Set included in a singleton (or unordered pair).
::
theorem
Y c= { x } iff Y = {} or Y = { x } by Lm4;
theorem
Y c= X & not x in Y implies Y c= X \ { x } by Lm3;
theorem
X <> {x} & X <> {} implies ex y st y in X & y <> x by Lm14;
theorem
Z c= {x1,x2} iff Z = {} or Z = {x1} or Z = {x2} or Z = {x1,x2} by Lm15;
::
:: Sum of an unordered pair (or a singleton) and a set.
::
theorem Th43:
{z} = X \/ Y implies
X = {z} & Y = {z} or X = {} & Y = {z} or X = {z} & Y = {}
proof
assume {z} = X \/ Y;
then (X <> {} or Y <> {}) & X c= {z} & Y c= {z} by Lm1,XBOOLE_1:7;
hence thesis by Lm4;
end;
theorem
{z} = X \/ Y & X <> Y implies X = {} or Y = {}
proof assume {z} = X \/ Y;
then X={z} & Y={z} or X={} & Y={z} or X={z} & Y={} by Th43;
hence thesis;
end;
theorem
{x} \/ X c= X implies x in X by Lm5;
theorem
x in X implies {x} \/ X = X by Lm6;
theorem
{x,y} \/ Z c= Z implies x in Z
proof assume
A1: {x,y} \/ Z c= Z;
assume not x in Z;
then not x in {x,y} \/ Z by A1,TARSKI:def 3;
then not x in {x,y} by XBOOLE_0:def 2;
hence thesis by TARSKI:def 2;
end;
theorem
x in Z & y in Z implies {x,y} \/ Z = Z
proof assume x in Z & y in Z;
then {x,y} c= Z by Th38;
hence thesis by XBOOLE_1:12;
end;
theorem
{x} \/ X <> {}
proof x in {x} by TARSKI:def 1;
then x in {x} \/ X by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 1;
end;
theorem
{x,y} \/ X <> {}
proof x in {x,y} by TARSKI:def 2;
then x in {x,y} \/ X by XBOOLE_0:def 2;
hence thesis by XBOOLE_0:def 1;
end;
::
:: Intersection of an unordered pair (or a singleton) and a set.
::
theorem
X /\ {x} = {x} implies x in X by Lm9;
theorem
x in X implies X /\ {x} = {x} by Lm10;
theorem
x in Z & y in Z implies {x,y} /\ Z = {x,y}
proof assume x in Z & y in Z;
then {x,y} c= Z by Th38;
hence thesis by XBOOLE_1:28;
end;
theorem
{x} misses X implies not x in X by Lm7;
theorem Th55:
{x,y} misses Z implies not x in Z
proof assume that
A1: {x,y} /\ Z = {} and
A2: x in Z;
x in {x,y} & y in {x,y} by TARSKI:def 2;
then x in {x,y} /\ Z or y in {x,y} /\ Z by A2,XBOOLE_0:def 3;
hence contradiction by A1,XBOOLE_0:def 1;
end;
theorem
not x in X implies {x} misses X by Lm8;
theorem Th57:
not x in Z & not y in Z implies {x,y} misses Z
proof assume
A1: not x in Z & not y in Z;
assume {x,y} meets Z;
then consider z such that
A2: z in {x,y} /\ Z by XBOOLE_0:4;
z in {x,y} & z in Z by A2,XBOOLE_0:def 3;
hence contradiction by A1,TARSKI:def 2;
end;
theorem
{x} misses X or {x} /\ X = {x}
proof assume {x} meets X; then x in X by Lm8; hence thesis by Lm10; end;
theorem
{x,y} /\ X = {x} implies not y in X or x = y
proof assume that
A1: {x,y} /\ X = {x} and
A2: y in X;
y in {x,y} by TARSKI:def 2;
then y in {x} by A1,A2,XBOOLE_0:def 3;
hence y=x by TARSKI:def 1;
end;
theorem
x in X & (not y in X or x = y) implies {x,y} /\ X = {x}
proof assume that
A1: x in X and
A2: not y in X or x=y;
z in {x,y} /\ X iff z=x
proof
(z in {x,y} /\ X iff z in {x,y} & z in X) & (z in {x,y} iff z=x or z=y)
by TARSKI:def 2,XBOOLE_0:def 3;
hence thesis by A1,A2;
end;
hence {x,y} /\ X = {x} by TARSKI:def 1;
end;
canceled 2;
theorem
{x,y} /\ X = {x,y} implies x in X
proof assume {x,y} /\ X = {x,y};
then x in {x,y} /\ X & y in {x,y} /\ X or x in X /\ {x,y} & y in X /\ {x,y}
by TARSKI:def 2;
hence thesis by XBOOLE_0:def 3;
end;
::
:: Difference of an unordered pair (or a singleton) and a set.
::
theorem
z in X \ {x} iff z in X & z <> x
proof z in X \ {x} iff z in X & not z in {x} by XBOOLE_0:def 4;
hence thesis by TARSKI:def 1;
end;
theorem
X \ {x} = X iff not x in X
proof X \ {x} = X iff X misses {x} by XBOOLE_1:83;
hence thesis by Lm7,Lm8;
end;
theorem
X \ {x} = {} implies X = {} or X = {x}
proof assume X \ {x} = {};
then X c= {x} by XBOOLE_1:37;
hence thesis by Lm4;
end;
theorem
{x} \ X = {x} iff not x in X by Lm11;
theorem
{x} \ X = {} iff x in X by Lm12;
theorem
{x} \ X = {} or {x} \ X = {x}
proof assume {x} \ X <> {}; then not x in X by Lm12; hence thesis by Lm11;
end;
theorem
{x,y} \ X = {x} iff not x in X & (y in X or x = y) by Lm13;
canceled;
theorem Th72:
{x,y} \ X = {x,y} iff not x in X & not y in X
proof {x,y} \ X = {x,y} iff {x,y} misses X by XBOOLE_1:83;
hence thesis by Th55,Th57;
end;
theorem Th73:
{x,y} \ X = {} iff x in X & y in X
proof {x,y} \ X = {} iff {x,y} c= X by XBOOLE_1:37; hence thesis by Th38;
end;
theorem
{x,y} \ X = {} or {x,y} \ X = {x} or {x,y} \ X = {y} or {x,y} \ X = {x,y}
proof assume {x,y} \ X <> {} & {x,y} \ X <> {x} & {x,y} \ X <> {y};
then (not x in X or not y in X) & (x in X or not y in X & x<>y)
& (not x in X & x<>y or y in X) by Lm13,Th73;
hence {x,y} \ X = {x,y} by Th72;
end;
theorem
X \ {x,y} = {} iff X = {} or X = {x} or X = {y} or X = {x,y}
proof X \ {x,y} = {} iff X c= {x,y} by XBOOLE_1:37;
hence thesis by Lm15;
end;
::
:: Power Set.
::
canceled 3;
theorem
A c= B implies bool A c= bool B
proof assume
A1: A c= B;
let x;
assume x in bool A;
then x c= A by Def1;
then x c= B by A1,XBOOLE_1:1;
hence x in bool B by Def1;
end;
theorem
{ A } c= bool A
proof A in bool A by Def1; hence thesis by Lm2; end;
theorem
bool A \/ bool B c= bool (A \/ B)
proof let x;
assume x in bool A \/ bool B;
then x in bool A or x in bool B by XBOOLE_0:def 2;
then (x c= A or x c= B) & A c= A \/ B & B c= A \/ B by Def1,XBOOLE_1:7;
then x c= A \/ B by XBOOLE_1:1;
hence thesis by Def1;
end;
theorem
bool A \/ bool B = bool (A \/ B) implies A,B are_c=-comparable
proof assume
A1: bool A \/ bool B = bool (A \/ B);
A \/ B in bool (A \/ B) by Def1;
then A \/ B in bool A or A \/ B in bool B by A1,XBOOLE_0:def 2;
then (A \/ B c= A or A \/ B c= B) & A c= A \/ B & B c= A \/ B
by Def1,XBOOLE_1:7;
hence A c= B or B c= A by XBOOLE_0:def 10;
end;
theorem
bool (A /\ B) = bool A /\ bool B
proof
now let x;
A /\ B c= A & A /\ B c= B by XBOOLE_1:17;
then x c= A & x c= B iff x c= A /\ B by XBOOLE_1:1,19;
then x in bool A & x in bool B iff x in bool (A /\ B) by Def1;
hence x in bool (A /\ B) iff x in bool A /\ bool B by XBOOLE_0:def 3;
end;
hence thesis by TARSKI:2;
end;
theorem
bool (A \ B) c= { {} } \/ (bool A \ bool B)
proof let x;
assume x in bool (A \ B);
then A1: x c= A \ B by Def1;
A \ B c= A & (A \ B) misses B by XBOOLE_1:36,79;
then x c= A & x misses B by A1,XBOOLE_1:1,63;
then x c= A & x /\ B = {} by XBOOLE_0:def 7;
then x = {} or x c= A & not x c= B by XBOOLE_1:28;
then x in { {} } or x in bool A & not x in bool B by Def1,TARSKI:def 1;
then x in { {} } or x in bool A \ bool B by XBOOLE_0:def 4;
hence x in { {} } \/ (bool A \ bool B) by XBOOLE_0:def 2;
end;
canceled;
theorem
bool (A \ B) \/ bool (B \ A) c= bool (A \+\ B)
proof let x;
assume x in bool (A \ B) \/ bool (B \ A);
then x in bool (A \ B) or x in bool (B \ A) by XBOOLE_0:def 2;
then A1: x c= A \ B or x c= B \ A by Def1;
x c= (A \ B) \/ (B \ A)
proof let z;
assume z in x;
then z in A \ B or z in B \ A by A1,TARSKI:def 3;
hence thesis by XBOOLE_0:def 2;
end;
then x c= A \+\ B by XBOOLE_0:def 6;
hence thesis by Def1;
end;
::
:: Union of a set.
::
canceled 5;
theorem
X in A implies X c= union A by Lm16;
theorem
union { X,Y } = X \/ Y by Lm17;
theorem
(for X st X in A holds X c= Z) implies union A c= Z
proof assume
A1: for X st X in A holds X c= Z;
let y;
assume y in union A;
then consider Y such that
A2: y in Y and
A3: Y in A by TARSKI:def 4;
Y c= Z by A1,A3;
hence y in Z by A2,TARSKI:def 3;
end;
theorem Th95:
A c= B implies union A c= union B
proof assume
A1: A c= B;
let x;
assume x in union A;
then consider Y such that
A2: x in Y and
A3: Y in A by TARSKI:def 4;
Y in B by A1,A3,TARSKI:def 3;
hence x in union B by A2,TARSKI:def 4;
end;
theorem
union (A \/ B) = union A \/ union B
proof
A1: union (A \/ B) c= union A \/ union B
proof let x;
assume x in union (A \/ B);
then consider Y such that
A2: x in Y and
A3: Y in A \/ B by TARSKI:def 4;
Y in A or Y in B by A3,XBOOLE_0:def 2;
then x in union A or x in union B by A2,TARSKI:def 4;
hence x in union A \/ union B by XBOOLE_0:def 2;
end;
A c= A \/ B & B c= A \/ B by XBOOLE_1:7;
then union A c= union (A \/ B) & union B c= union (A \/ B) by Th95;
then union A \/ union B c= union (A \/ B) by XBOOLE_1:8;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th97:
union (A /\ B) c= union A /\ union B
proof let x;
assume x in union (A /\ B);
then consider Y such that
A1: x in Y and
A2: Y in A /\ B by TARSKI:def 4;
Y in A & Y in B by A2,XBOOLE_0:def 3;
then x in union A & x in union B by A1,TARSKI:def 4;
hence thesis by XBOOLE_0:def 3;
end;
theorem
(for X st X in A holds X misses B) implies union A misses B
proof assume
A1: for X st X in A holds X misses B;
assume union(A) meets B;
then consider z being set such that
A2: z in union(A) /\ B by XBOOLE_0:4;
A3: z in union(A) & z in B by A2,XBOOLE_0:def 3;
then consider X such that
A4: z in X and
A5: X in A by TARSKI:def 4;
z in X /\ B & X misses B by A1,A3,A4,A5,XBOOLE_0:def 3;
hence contradiction by XBOOLE_0:4;
end;
theorem
union bool A = A
proof
now let x;
thus x in union bool A implies x in A
proof assume x in union bool A;
then consider X such that
A1: x in X and
A2: X in bool A by TARSKI:def 4;
X c= A by A2,Def1;
hence x in A by A1,TARSKI:def 3;
end;
assume x in A;
then { x } c= A by Lm2;
then { x } in bool A & x in { x } by Def1,TARSKI:def 1;
hence x in union bool A by TARSKI:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
A c= bool union A
proof let x;
assume x in A;
then x c= union A by Lm16;
hence x in bool union A by Def1;
end;
theorem
(for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y)
implies union(A /\ B) = union A /\ union B
proof assume
A1: for X,Y st X<>Y & X in A \/ B & Y in A \/ B holds X misses Y;
A2: union (A /\ B) c= union A /\ union B by Th97;
union A /\ union B c= union (A /\ B)
proof let x;
assume x in union A /\ union B;
then A3: x in union A & x in union B by XBOOLE_0:def 3;
then consider X such that
A4: x in X and
A5: X in A by TARSKI:def 4;
consider Y such that
A6: x in Y and
A7: Y in B by A3,TARSKI:def 4;
now assume
A8: X<>Y;
x in X /\ Y by A4,A6,XBOOLE_0:def 3;
then X meets Y & X in A \/ B & Y in A \/ B
by A5,A7,XBOOLE_0:4,def 2;
hence contradiction by A1,A8;
end;
then Y in A /\ B by A5,A7,XBOOLE_0:def 3;
hence thesis by A6,TARSKI:def 4;
end;
hence thesis by A2,XBOOLE_0:def 10;
end;
::
:: Cartesian product.
::
theorem Th102:
z in [:X,Y:] implies ex x,y st [x,y] = z
proof assume z in [:X,Y:];
then ex x,y st x in X & y in Y & [x,y]=z by Def2;
hence thesis;
end;
theorem Th103:
A c= [:X,Y:] & z in A implies ex x,y st x in X & y in Y & z = [x,y]
proof assume A c= [:X,Y:] & z in A;
then z in [:X,Y:] by TARSKI:def 3;
hence thesis by Def2;
end;
theorem Th104:
z in [:X1, Y1:] /\ [:X2, Y2:]
implies ex x,y st z = [x,y] & x in X1 /\ X2 & y in Y1 /\ Y2
proof assume z in [:X1, Y1:] /\ [:X2, Y2:];
then A1: z in [:X1, Y1:] & z in [:X2, Y2:] by XBOOLE_0:def 3;
then consider x1,y1 such that
A2: x1 in X1 & y1 in Y1 and
A3: z=[x1,y1] by Def2;
consider x2,y2 such that
A4: x2 in X2 & y2 in Y2 and
A5: z=[x2,y2] by A1,Def2;
x1=x2 & y1=y2 by A3,A5,Th33;
then x1 in X1 /\ X2 & y1 in Y1 /\ Y2 by A2,A4,XBOOLE_0:def 3;
hence thesis by A3;
end;
theorem
[:X,Y:] c= bool bool (X \/ Y)
proof let z;
assume z in [:X,Y:];
then consider x,y such that
A1: x in X and
A2: y in Y and
A3: z = [x,y] by Def2;
A4: z = {{x,y},{x}} by A3,TARSKI:def 5;
z c= bool (X \/ Y)
proof let u be set;
assume
A5: u in z;
X c= X \/ Y & {x} c= X & x in X \/ Y & y in X \/ Y
by A1,A2,Lm2,XBOOLE_0:def 2,XBOOLE_1:7;
then {x} c= X \/ Y & {x,y} c= X \/ Y & (u = {x,y} or u = {x})
by A4,A5,Th38,TARSKI:def 2,XBOOLE_1:1;
hence u in bool (X \/ Y) by Def1;
end;
hence thesis by Def1;
end;
theorem
[x,y] in [:X,Y:] iff x in X & y in Y by Lm18;
theorem Th107:
[x,y] in [:X,Y:] implies [y,x] in [:Y,X:]
proof
([x,y] in [:X,Y:] implies x in X & y in Y)
& (y in Y & x in X implies [y,x] in [:Y,X:]) by Lm18;
hence thesis;
end;
theorem
(for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:])
implies [:X1,Y1:]=[:X2,Y2:]
proof assume
A1: for x,y holds [x,y] in [:X1,Y1:] iff [x,y] in [:X2,Y2:];
now let z;
thus z in [:X1,Y1:] implies z in [:X2,Y2:]
proof assume
A2: z in [:X1,Y1:];
then ex x,y st x in X1 & y in Y1 & [x,y]=z by Def2;
hence thesis by A1,A2;
end;
assume
A3: z in [:X2,Y2:];
then ex x,y st x in X2 & y in Y2 & [x,y]=z by Def2;
hence z in [:X1,Y1:] by A1,A3;
end;
hence thesis by TARSKI:2;
end;
theorem
A c= [:X,Y:] & (for x,y st [x,y] in A holds [x,y] in B) implies A c= B
proof assume that
A1: A c= [:X,Y:] and
A2: for x,y st [x,y] in A holds [x,y] in B;
let z;
z in A implies ex x,y st x in X & y in Y & [x,y]=z by A1,Th103;
hence thesis by A2;
end;
theorem Th110:
A c= [:X1,Y1:] & B c= [:X2,Y2:] & (for x,y holds [x,y] in A iff [x,y] in B)
implies A = B
proof assume that
A1: A c= [:X1,Y1:] & B c= [:X2,Y2:] and
A2: for x,y holds [x,y] in A iff [x,y] in B;
now let z;
(z in A implies ex x,y st x in X1 & y in Y1 & z=[x,y])
& (z in B implies ex x,y st x in X2 & y in Y2 & z=[x,y]) by A1,Th103;
hence z in A iff z in B by A2;
end;
hence thesis by TARSKI:2;
end;
theorem
(for z st z in A ex x,y st z=[x,y]) &
(for x,y st [x,y] in A holds [x,y] in B)
implies A c= B
proof assume that
A1: for z st z in A ex x,y st z=[x,y] and
A2: for x,y st [x,y] in A holds [x,y] in B;
let z;
z in A implies ex x,y st z=[x,y] by A1;
hence thesis by A2;
end;
theorem Th112:
(for z st z in A ex x,y st z = [x,y]) & (for z st z in B ex x,y st z=[x,y]) &
(for x,y holds [x,y] in A iff [x,y] in B)
implies A = B
proof assume that
A1: (for z st z in A ex x,y st z=[x,y]) &
(for z st z in B ex x,y st z=[x,y]) and
A2: for x,y holds [x,y] in A iff [x,y] in B;
now let z;
(z in A implies ex x,y st z=[x,y]) & (z in B implies ex x,y st z=[x,y])
by A1;
hence z in A iff z in B by A2;
end;
hence thesis by TARSKI:2;
end;
theorem Th113:
[:X,Y:] = {} iff X = {} or Y = {}
proof
thus [:X,Y:] = {} implies X={} or Y={}
proof assume A1: [:X,Y:] = {};
assume X<>{};
then consider x being set such that
A2: x in X by XBOOLE_0:def 1;
assume Y<>{};
then consider y being set such that
A3: y in Y by XBOOLE_0:def 1;
[x,y] in [:X,Y:] by A2,A3,Def2;
hence contradiction by A1,XBOOLE_0:def 1;
end;
assume
A4: not thesis;
then consider z being set such that
A5: z in [:X,Y:] by XBOOLE_0:def 1;
A6: now assume
A7: X={};
ex x,y st x in X & y in Y & [x,y]=z by A5,Def2;
hence contradiction by A7,XBOOLE_0:def 1;
end;
now assume
A8: Y={};
ex x,y st x in X & y in Y & [x,y]=z by A5,Def2;
hence contradiction by A8,XBOOLE_0:def 1;
end;
hence contradiction by A4,A6;
end;
theorem
X <> {} & Y <> {} & [:X,Y:] = [:Y,X:] implies X = Y
proof assume X<>{};
then consider x being set such that
A1: x in X by XBOOLE_0:def 1;
assume Y<>{};
then consider y being set such that
A2: y in Y by XBOOLE_0:def 1;
assume
A3: [:X,Y:]=[:Y,X:];
z in X iff z in Y
proof
thus z in X implies z in Y
proof assume z in X;
then [z,y] in [:Y,X:] by A2,A3,Lm18;
hence z in Y by Lm18;
end;
assume z in Y;
then [z,x] in [:X,Y:] by A1,A3,Lm18;
hence z in X by Lm18;
end;
hence thesis by TARSKI:2;
end;
theorem
[:X,X:] = [:Y,Y:] implies X = Y
proof assume
A1: [:X,X:] = [:Y,Y:];
x in X iff x in Y
proof
(x in X iff [x,x] in [:X,X:]) & (x in Y iff [x,x] in [:Y,Y:]) by Lm18;
hence thesis by A1;
end;
hence thesis by TARSKI:2;
end;
theorem
X c= [:X,X:] implies X = {}
proof assume
A1: X c= [:X,X:];
assume X <> {};
then consider z being set such that
A2: z in X by XBOOLE_0:def 1;
z in X \/ union X by A2,XBOOLE_0:def 2;
then consider Y such that
A3: Y in X \/ union X and
A4: not ex x st x in X \/ union X & x in Y by TARSKI:7;
now assume
A5: Y in X;
then Y in [:X,X:] by A1,TARSKI:def 3;
then consider x,y such that
A6: Y=[x,y] by Th102;
Y={{x,y},{x}} by A6,TARSKI:def 5;
then A7: {x} in Y by TARSKI:def 2;
Y c= union X by A5,Lm16;
then {x} in union X by A7,TARSKI:def 3;
then {x} in X \/ union X by XBOOLE_0:def 2;
hence contradiction by A4,A7;
end;
then Y in union X by A3,XBOOLE_0:def 2;
then consider Z such that
A8: Y in Z and
A9: Z in X by TARSKI:def 4;
Z in [:X,X:] by A1,A9,TARSKI:def 3;
then consider x,y such that
A10: x in X & y in X and
A11: Z=[x,y] by Def2;
Z={{x,y},{x}} by A11,TARSKI:def 5;
then Y={x} or Y={x,y} by A8,TARSKI:def 2;
then x in Y & x in X \/
union X by A10,TARSKI:def 1,def 2,XBOOLE_0:def 2;
hence contradiction by A4;
end;
theorem
Z <> {} & ([:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:]) implies X c= Y
proof assume Z<>{};
then consider z being set such that
A1: z in Z by XBOOLE_0:def 1;
assume
A2: [:X,Z:] c= [:Y,Z:] or [:Z,X:] c= [:Z,Y:];
let x;
assume x in X;
then [x,z] in [:X,Z:] & [z,x] in [:Z,X:] by A1,Def2;
then [x,z] in [:Y,Z:] or [z,x] in [:Z,Y:] by A2,TARSKI:def 3;
hence x in Y by Lm18;
end;
theorem Th118:
X c= Y implies [:X,Z:] c= [:Y,Z:] & [:Z,X:] c= [:Z,Y:]
proof assume
A1: X c= Y;
thus [:X,Z:] c= [:Y,Z:]
proof let z;
assume z in [:X,Z:];
then consider x,y such that
A2: x in X & y in Z and
A3: z=[x,y] by Def2;
x in Y by A1,A2,TARSKI:def 3;
hence thesis by A2,A3,Def2;
end;
let z;
assume z in [:Z,X:];
then consider y,x such that
A4: y in Z & x in X and
A5: z=[y,x] by Def2;
x in Y by A1,A4,TARSKI:def 3;
hence z in [:Z,Y:] by A4,A5,Def2;
end;
theorem Th119:
X1 c= Y1 & X2 c= Y2 implies [:X1,X2:] c= [:Y1,Y2:]
proof assume X1 c= Y1 & X2 c= Y2;
then [:X1,X2:] c= [:Y1,X2:] & [:Y1,X2:] c= [:Y1,Y2:] by Th118;
hence thesis by XBOOLE_1:1;
end;
theorem Th120:
[:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:] & [:Z, X \/ Y:] = [:Z, X:] \/ [:Z, Y:]
proof
A1: z in [:X1,X2:] \/ [:Y1,Y2:] implies ex x,y st z=[x,y]
proof assume z in [:X1,X2:] \/ [:Y1,Y2:];
then z in [:X1,X2:] or z in [:Y1,Y2:] by XBOOLE_0:def 2;
hence ex x,y st z=[x,y] by Th102;
end;
thus
A2: [:X \/ Y, Z:] = [:X, Z:] \/ [:Y, Z:]
proof
A3: (for z st z in [:X,Z:] \/ [:Y,Z:] ex x,y st z=[x,y])
& (for z st z in [:X \/ Y, Z:] ex x,y st z=[x,y])
by A1,Th102;
for x,y holds [x,y] in [:X \/ Y, Z:] iff [x,y] in [:X, Z:] \/ [:Y, Z:]
proof let x,y;
thus [x,y] in [:X \/ Y, Z:] implies [x,y] in [:X, Z:] \/ [:Y, Z:]
proof assume [x,y] in [:X \/ Y, Z:];
then x in X \/ Y & y in Z by Lm18;
then (x in X or x in Y) & y in Z by XBOOLE_0:def 2;
then [x,y] in [:X,Z:] or [x,y] in [:Y,Z:] by Lm18;
hence [x,y] in [:X, Z:] \/ [:Y, Z:] by XBOOLE_0:def 2;
end;
assume [x,y] in [:X, Z:] \/ [:Y, Z:];
then [x,y] in [:X, Z:] or [x,y] in [:Y, Z:] by XBOOLE_0:def 2;
then (x in X & y in Z) or (x in Y & y in Z) by Lm18;
then x in X \/ Y & y in Z by XBOOLE_0:def 2;
hence [x,y] in [:X \/ Y,Z:] by Lm18;
end;
hence thesis by A3,Th112;
end;
A4: (for z st z in [:Z,X:] \/ [:Z,Y:] ex x,y st z=[x,y])
& (for z st z in [:Z,X \/ Y:] ex x,y st z=[x,y])
by A1,Th102;
for y,x holds [y,x] in [:Z, X \/ Y:] iff [y,x] in [:Z, X:] \/ [:Z, Y:]
proof let y,x;
([y,x] in [:Z, X \/ Y:] iff [x,y] in [:X \/ Y, Z:])
& ([x,y] in [:X, Z:] \/ [:Y,Z:]
iff [x,y] in [:X, Z:] or [x,y] in [:Y,Z:])
& ([x,y]in[:X, Z:] or [x,y]in[:Y,Z:]
iff [y,x]in[:Z,X:] or [y,x]in[:Z,Y:])
by Th107,XBOOLE_0:def 2;
hence thesis by A2,XBOOLE_0:def 2;
end;
hence thesis by A4,Th112;
end;
theorem
[:X1 \/ X2, Y1 \/ Y2:] = [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2,Y2:]
proof
thus [:X1 \/ X2, Y1 \/ Y2:]
= [:X1, Y1 \/ Y2:] \/ [:X2, Y1 \/ Y2:] by Th120
.= [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1 \/ Y2:] by Th120
.= [:X1,Y1:] \/ [:X1,Y2:] \/ ([:X2,Y1:] \/ [:X2,Y2:]) by Th120
.= [:X1,Y1:] \/ [:X1,Y2:] \/ [:X2,Y1:] \/ [:X2,Y2:] by XBOOLE_1:4;
end;
theorem
[:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:] & [:Z, X /\ Y:] = [:Z, X:] /\ [:Z, Y:]
proof
thus
A1: [:X /\ Y, Z:] = [:X, Z:] /\ [:Y, Z:]
proof
A2: [:X /\ Y, Z:] c= [:X /\ Y, Z:] & [:X, Z:] /\ [:Y, Z:] c= [:X, Z:]
by XBOOLE_1:17;
for x,y holds [x,y] in [:X /\ Y, Z:] iff [x,y] in [:X, Z:] /\ [:Y, Z:]
proof let x,y;
thus [x,y] in [:X /\ Y, Z:] implies [x,y] in [:X, Z:] /\ [:Y, Z:]
proof assume [x,y] in [:X /\ Y, Z:];
then x in X /\ Y & y in Z by Lm18;
then (x in X & x in Y) & y in Z by XBOOLE_0:def 3;
then [x,y] in [:X,Z:] & [x,y] in [:Y,Z:] by Lm18;
hence [x,y] in [:X, Z:] /\ [:Y, Z:] by XBOOLE_0:def 3;
end;
assume [x,y] in [:X, Z:] /\ [:Y, Z:];
then [x,y] in [:X, Z:] & [x,y] in [:Y, Z:] by XBOOLE_0:def 3;
then (x in X & y in Z) & (x in Y & y in Z) by Lm18;
then x in X /\ Y & y in Z by XBOOLE_0:def 3;
hence [x,y] in [:X /\ Y,Z:] by Lm18;
end;
hence thesis by A2,Th110;
end;
A3: [:Z, X /\ Y:] c= [:Z, X /\ Y:] & [:Z, X:] /\ [:Z, Y:] c= [:Z, X:]
by XBOOLE_1:17;
for y,x holds [y,x] in [:Z, X /\ Y:] iff [y,x] in [:Z, X:] /\ [:Z, Y:]
proof let y,x;
([y,x] in [:Z, X /\ Y:] iff [x,y] in [:X /\ Y, Z:])
& ([x,y] in [:X, Z:] /\
[:Y,Z:] iff [x,y] in [:X, Z:] & [x,y] in [:Y,Z:])
& ([x,y]in[:X, Z:] & [x,y]in[:Y,Z:] iff [y,x]in[:Z,X:] & [y,x]in[:Z,Y:])
by Th107,XBOOLE_0:def 3;
hence thesis by A1,XBOOLE_0:def 3;
end;
hence thesis by A3,Th110;
end;
theorem Th123:
[:X1 /\ X2, Y1 /\ Y2:] = [:X1,Y1:] /\ [:X2, Y2:]
proof
Y1 /\ Y2 c= Y1 & Y1 /\ Y2 c= Y2 & X1 /\ X2 c= X1 & X1 /\
X2 c= X2 by XBOOLE_1:17;
then [:X1 /\ X2, Y1 /\ Y2:] c= [:X1, Y1:]
& [:X1 /\ X2, Y1 /\ Y2:] c= [:X2, Y2:] by Th119;
then A1: [:X1 /\ X2, Y1 /\ Y2:] c= [:X1, Y1:] /\ [:X2, Y2:] by XBOOLE_1:19;
[:X1, Y1:] /\ [:X2, Y2:] c= [:X1 /\ X2, Y1 /\ Y2:]
proof let z;
assume z in [:X1, Y1:] /\ [:X2, Y2:];
then ex x,y st z=[x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 by Th104;
hence thesis by Def2;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem
A c= X & B c= Y implies [:A,Y:] /\ [:X,B:] = [:A,B:]
proof assume A c= X & B c= Y;
then [:A,Y:] /\ [:X,B:] = [:A /\ X, Y /\ B:] & A /\ X = A & Y /\ B = B
by Th123,XBOOLE_1:28;
hence thesis;
end;
theorem Th125:
[:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:] & [:Z, X \ Y:] = [:Z, X:] \ [:Z, Y:]
proof
thus
A1: [:X \ Y, Z:] = [:X, Z:] \ [:Y, Z:]
proof
A2: [:X \ Y, Z:] c= [:X \ Y, Z:] & [:X, Z:] \ [:Y, Z:] c= [:X, Z:]
by XBOOLE_1:36;
for x,y holds [x,y] in [:X \ Y, Z:] iff [x,y] in [:X, Z:] \ [:Y, Z:]
proof let x,y;
thus [x,y] in [:X \ Y, Z:] implies [x,y] in [:X, Z:] \ [:Y, Z:]
proof assume [x,y] in [:X \ Y, Z:];
then x in X \ Y & y in Z by Lm18;
then (x in X & not x in Y) & y in Z by XBOOLE_0:def 4;
then [x,y] in [:X,Z:] & not [x,y] in [:Y,Z:] by Lm18;
hence [x,y] in [:X, Z:] \ [:Y, Z:] by XBOOLE_0:def 4;
end;
assume [x,y] in [:X, Z:] \ [:Y, Z:];
then [x,y] in [:X, Z:] & not [x,y] in [:Y, Z:] by XBOOLE_0:def 4;
then (x in X & y in Z) & not (x in Y & y in Z) by Lm18;
then x in X \ Y & y in Z by XBOOLE_0:def 4;
hence [x,y] in [:X \ Y,Z:] by Lm18;
end;
hence thesis by A2,Th110;
end;
A3: [:Z, X \ Y:] c= [:Z, X \ Y:] & [:Z, X:] \ [:Z, Y:] c= [:Z, X:]
by XBOOLE_1:36;
for y,x holds [y,x] in [:Z, X \ Y:] iff [y,x] in [:Z, X:] \ [:Z, Y:]
proof let y,x;
([y,x] in [:Z, X \ Y:] iff [x,y] in [:X \ Y, Z:])
& ([x,y] in [:X, Z:] \ [:Y,Z:]
iff [x,y] in [:X, Z:] & not [x,y]in[:Y,Z:])
& ([x,y]in[:X, Z:]& not[x,y]in[:Y,Z:]
iff [y,x]in[:Z,X:]& not[y,x]in[:Z,Y:])
by Th107,XBOOLE_0:def 4;
hence thesis by A1,XBOOLE_0:def 4;
end;
hence thesis by A3,Th110;
end;
theorem
[:X1,X2:] \ [:Y1,Y2:] = [:X1\Y1,X2:] \/ [:X1,X2\Y2:]
proof
[:X1\Y1,X2:] = [:X1,X2:] \ [:Y1,X2:] & [:X1,X2\Y2:] = [:X1,X2:] \ [:X1,Y2:]
& [:Y1,X2:] /\ [:X1,Y2:] = [:Y1 /\ X1, X2 /\ Y2:]
& Y1 /\ X1 c= Y1 & X2 /\ Y2 c= Y2 by Th123,Th125,XBOOLE_1:17;
then [:X1\Y1,X2:] \/ [:X1,X2\Y2:] = [:X1,X2:] \ [:Y1 /\ X1, X2 /\ Y2:] &
[:Y1 /\ X1, X2 /\ Y2:] c= [:Y1,Y2:] by Th119,XBOOLE_1:54;
then A1: [:X1,X2:] \ [:Y1,Y2:] c= [:X1\Y1,X2:] \/ [:X1,X2\Y2:] by XBOOLE_1:
34;
[:X1\Y1,X2:] \/ [:X1,X2\Y2:] c= [:X1,X2:] \ [:Y1, Y2:]
proof let z;
assume
A2: z in [:X1\Y1,X2:] \/ [:X1,X2\Y2:];
A3: now assume z in [:X1\Y1,X2:];
then consider x,y such that
A4: x in X1\Y1 and
A5: y in X2 and
A6: z=[x,y] by Def2;
x in X1 & not x in Y1 by A4,XBOOLE_0:def 4;
then z in [:X1,X2:] & not z in [:Y1,Y2:] by A5,A6,Lm18;
hence z in [:X1,X2:] \ [:Y1, Y2:] by XBOOLE_0:def 4;
end;
now assume z in [:X1,X2\Y2:];
then consider x,y such that
A7: x in X1 and
A8: y in X2\Y2 and
A9: z=[x,y] by Def2;
y in X2 & not y in Y2 by A8,XBOOLE_0:def 4;
then z in [:X1,X2:] & not z in [:Y1,Y2:] by A7,A9,Lm18;
hence z in [:X1,X2:] \ [:Y1, Y2:] by XBOOLE_0:def 4;
end;
hence z in [:X1,X2:] \ [:Y1, Y2:] by A2,A3,XBOOLE_0:def 2;
end;
hence thesis by A1,XBOOLE_0:def 10;
end;
theorem Th127:
X1 misses X2 or Y1 misses Y2 implies [:X1,Y1:] misses [:X2,Y2:]
proof assume
A1: X1 misses X2 or Y1 misses Y2;
assume not thesis;
then consider z being set such that
A2: z in [:X1,Y1:] /\ [:X2,Y2:] by XBOOLE_0:4;
ex x,y st z=[x,y] & x in X1 /\ X2 & y in Y1 /\ Y2 by A2,Th104;
hence contradiction by A1,XBOOLE_0:4;
end;
theorem Th128:
[x,y] in [:{z},Y:] iff x = z & y in Y
proof A1: x in {z} iff x=z by TARSKI:def 1;
hence [x,y] in [:{z},Y:] implies x=z & y in Y by Lm18;
thus thesis by A1,Lm18;
end;
theorem Th129:
[x,y] in [:X,{z}:] iff x in X & y = z
proof A1: y in {z} iff y=z by TARSKI:def 1;
hence [x,y] in [:X,{z}:] implies x in X & y=z by Lm18;
thus thesis by A1,Lm18;
end;
theorem
X <> {} implies [:{x},X:] <> {} & [:X,{x}:] <> {}
proof assume X <> {};
then consider y being set such that
A1: y in X by XBOOLE_0:def 1;
[x,y] in [:{x},X:] & [y,x] in [:X,{x}:] by A1,Th128,Th129;
hence thesis by XBOOLE_0:def 1;
end;
theorem
x <> y implies [:{x},X:] misses [:{y},Y:] & [:X,{x}:] misses [:Y,{y}:]
proof assume x<>y;
then {x} misses {y} & {y} misses {x} by Th17;
hence thesis by Th127;
end;
theorem
[:{x,y},X:] = [:{x},X:] \/ [:{y},X:] & [:X,{x,y}:] = [:X,{x}:] \/ [:X,{y}:]
proof {x,y}={x} \/ {y} by ENUMSET1:41; hence thesis by Th120; end;
canceled;
theorem
X1 <> {} & Y1 <> {} & [:X1,Y1:] = [:X2,Y2:] implies X1 = X2 & Y1 = Y2
proof assume
A1: X1<>{};
then consider x being set such that
A2: x in X1 by XBOOLE_0:def 1;
assume
A3: Y1<>{};
then consider y being set such that
A4: y in Y1 by XBOOLE_0:def 1;
assume
A5: [:X1,Y1:] = [:X2,Y2:];
then [:X2,Y2:] <> {} by A1,A3,Th113;
then A6: X2 <> {} & Y2 <> {} by Th113;
z in X1 iff z in X2
proof
thus z in X1 implies z in X2
proof assume z in X1;
then [z,y] in [:X2,Y2:] by A4,A5,Lm18;
hence z in X2 by Lm18;
end;
consider y2 being set such that
A7: y2 in Y2 by A6,XBOOLE_0:def 1;
assume z in X2;
then [z,y2] in [:X2,Y2:] by A7,Lm18;
hence z in X1 by A5,Lm18;
end;
hence X1 = X2 by TARSKI:2;
z in Y1 iff z in Y2
proof
thus z in Y1 implies z in Y2
proof assume z in Y1;
then [x,z] in [:X2,Y2:] by A2,A5,Lm18;
hence z in Y2 by Lm18;
end;
consider x2 being set such that
A8: x2 in X2 by A6,XBOOLE_0:def 1;
assume z in Y2;
then [x2,z] in [:X2,Y2:] by A8,Lm18;
hence z in Y1 by A5,Lm18;
end;
hence Y1 = Y2 by TARSKI:2;
end;
theorem
X c= [:X,Y:] or X c= [:Y,X:] implies X = {}
proof assume
A1: X c= [:X,Y:] or X c= [:Y,X:];
assume
A2: X <> {};
A3: now assume
A4: X c= [:X,Y:];
consider z being set such that
A5: z in X by A2,XBOOLE_0:def 1;
z in X \/ union X by A5,XBOOLE_0:def 2;
then consider Y1 such that
A6: Y1 in X \/ union X and
A7: not ex x st x in X \/ union X & x in Y1 by TARSKI:7;
now assume
A8: Y1 in X;
then Y1 in [:X,Y:] by A4,TARSKI:def 3;
then consider x,y such that
A9: Y1 = [x,y] by Th102;
Y1={{x,y},{x}} by A9,TARSKI:def 5;
then A10: {x} in Y1 by TARSKI:def 2;
Y1 c= union X by A8,Lm16;
then {x} in union X by A10,TARSKI:def 3;
then {x} in X \/ union X by XBOOLE_0:def 2;
hence contradiction by A7,A10;
end;
then Y1 in union X by A6,XBOOLE_0:def 2;
then consider Y2 such that
A11: Y1 in Y2 and
A12: Y2 in X by TARSKI:def 4;
Y2 in [:X,Y:] by A4,A12,TARSKI:def 3;
then consider x,y such that
A13: x in X & y in Y and
A14: Y2=[x,y] by Def2;
Y2={{x,y},{x}} by A14,TARSKI:def 5;
then Y1={x} or Y1={x,y} by A11,TARSKI:def 2;
then x in Y1 & x in X \/ union X
by A13,TARSKI:def 1,def 2,XBOOLE_0:def 2;
hence contradiction by A7;
end;
now assume
A15: X c= [:Y,X:];
defpred P[set] means ex Y st $1=Y & ex z st z in Y & z in X;
consider Z such that
A16: for y holds y in Z iff y in union X & P[y] from Separation;
X \/ Z <> {} by A2,XBOOLE_1:15;
then consider x being set such that
A17: x in X \/ Z by XBOOLE_0:def 1;
consider Y2 such that
A18: Y2 in X \/ Z and
A19: not ex x st x in X \/ Z & x in Y2 by A17,TARSKI:7;
now assume
A20: not ex Y2 st Y2 in X & for Y1 st Y1 in Y2 holds
for z holds not z in Y1 or not z in X;
now assume
A21: Y2 in X;
then consider Y1 such that
A22: Y1 in Y2 and
A23: ex z st z in Y1 & z in X by A20;
Y1 in union X by A21,A22,TARSKI:def 4;
then Y1 in Z by A16,A23;
then Y1 in X \/ Z by XBOOLE_0:def 2;
hence contradiction by A19,A22;
end;
then Y2 in Z by A18,XBOOLE_0:def 2;
then ex X2 st Y2=X2 & ex z st z in X2 & z in X by A16;
then consider z such that
A24: z in Y2 and
A25: z in X;
z in X \/ Z by A25,XBOOLE_0:def 2;
hence contradiction by A19,A24;
end;
then consider Y1 such that
A26: Y1 in X and
A27: not ex Y2 st Y2 in Y1 & ex z st z in Y2 & z in X;
A28: now
given y,x such that
A29: x in X and
A30: Y1 = [y,x];
Y1 = {{y,x},{y}} by A30,TARSKI:def 5;
then {y,x} in Y1 & x in {y,x} by TARSKI:def 2;
hence contradiction by A27,A29;
end;
Y1 in [:Y,X:] by A15,A26,TARSKI:def 3;
then ex y,x st y in Y & x in X & Y1 = [y,x] by Def2;
hence contradiction by A28;
end;
hence thesis by A1,A3;
end;
theorem
ex M st N in M &
(for X,Y holds X in M & Y c= X implies Y in M) &
(for X holds X in M implies bool X in M) &
(for X holds X c= M implies X,M are_equipotent or X in M)
proof
consider M such that
A1: N in M and
A2: for X,Y holds X in M & Y c= X implies Y in M and
A3: for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z and
A4: for X holds X c= M implies X,M are_equipotent or X in M by TARSKI:9;
take M;
thus N in M by A1;
thus for X,Y holds X in M & Y c= X implies Y in M by A2;
thus for X holds X in M implies bool X in M
proof let X;
assume X in M;
then consider Z such that
A5: Z in M and
A6: for Y st Y c= X holds Y in Z by A3;
now let Y;
assume Y in bool X;
then Y c= X by Def1;
hence Y in Z by A6;
end;
then bool X c= Z by TARSKI:def 3;
hence thesis by A2,A5;
end;
thus thesis by A4;
end;