Copyright (c) 2002 Association of Mizar Users
environ
vocabulary TARSKI, BOOLE, ZFMISC_1;
notation TARSKI;
constructors TARSKI;
theorems TARSKI;
schemes TARSKI;
begin
reserve X, Y, Z, x, y, z for set;
scheme Separation { A()-> set, P[set] } :
ex X being set st for x being set holds x in X iff x in A() & P[x]
proof
defpred Q[set,set] means $1 = $2 & P[$2];
A1: for x,y,z st Q[x,y] & Q[x,z] holds y = z;
consider X such that
A2: for x holds x in X iff ex y st y in A() & Q[y,x] from Fraenkel(A1);
take X;
let x;
x in X iff ex y st y in A() & y = x & P[x] by A2;
hence thesis;
end;
definition
func {} -> set means
:Def1: not ex x being set st x in it;
existence
proof
consider X;
defpred P[set] means contradiction;
consider Y such that
A1: x in Y iff x in X & P[x] from Separation;
take Y;
thus thesis by A1;
end;
uniqueness
proof
let X,Y;
assume (not ex x st x in X) & (not ex x st x in Y);
then x in Y iff x in X;
hence thesis by TARSKI:2;
end;
let X,Y be set;
func X \/ Y -> set means
:Def2: x in it iff x in X or x in Y;
existence
proof
take union {X,Y};
let x;
thus x in union {X,Y} implies x in X or x in Y
proof
assume x in union {X,Y};
then ex X0 being set st x in X0 & X0 in {X,Y} by TARSKI:def 4;
hence thesis by TARSKI:def 2;
end;
assume x in X or x in Y;
then consider X0 being set such that
A2: X0 = X or X0 = Y and
A3: x in X0;
X0 in {X,Y} by A2,TARSKI:def 2;
hence x in union {X,Y} by A3,TARSKI:def 4;
end;
uniqueness
proof
let A1, A2 be set such that
A4: x in A1 iff x in X or x in Y and
A5: x in A2 iff x in X or x in Y;
now
let x;
x in A1 iff x in X or x in Y by A4;
hence x in A1 iff x in A2 by A5;
end;
hence A1 = A2 by TARSKI:2;
end;
commutativity;
idempotence;
func X /\ Y -> set means
:Def3: x in it iff x in X & x in Y;
existence
proof defpred P[set] means $1 in Y;
thus ex Z being set st for x holds x in Z iff x in X & P[x]
from Separation;
end;
uniqueness
proof
let A1, A2 be set such that
A6: x in A1 iff x in X & x in Y and
A7: x in A2 iff x in X & x in Y;
now
let x;
x in A1 iff x in X & x in Y by A6;
hence x in A1 iff x in A2 by A7;
end;
hence A1 = A2 by TARSKI:2;
end;
commutativity;
idempotence;
func X \ Y -> set means
:Def4: x in it iff x in X & not x in Y;
existence
proof defpred P[set] means not $1 in Y;
thus ex Z being set st for x holds x in Z iff x in X & P[x]
from Separation;
end;
uniqueness
proof
let A1, A2 be set such that
A8: x in A1 iff x in X & not x in Y and
A9: x in A2 iff x in X & not x in Y;
now
let x;
x in A1 iff x in X & not x in Y by A8;
hence x in A1 iff x in A2 by A9;
end;
hence A1 = A2 by TARSKI:2;
end;
end;
definition let X be set;
attr X is empty means
:Def5: X = {};
let Y be set;
func X \+\ Y -> set equals
:Def6: (X \ Y) \/ (Y \ X);
correctness;
commutativity;
pred X misses Y means :Def7:
X /\ Y = {};
symmetry;
antonym X meets Y;
pred X c< Y means
X c= Y & X <> Y;
irreflexivity;
pred X,Y are_c=-comparable means
X c= Y or Y c= X;
reflexivity;
symmetry;
redefine pred X = Y means
X c= Y & Y c= X;
compatibility
proof
thus X = Y implies X c= Y & Y c= X;
assume X c= Y & Y c= X;
then for x holds x in X iff x in Y by TARSKI:def 3;
hence X = Y by TARSKI:2;
end;
end;
theorem
x in X \+\ Y iff not (x in X iff x in Y)
proof
X \+\ Y = (X \ Y) \/ (Y \ X) by Def6;
then x in X \+\ Y iff x in X \ Y or x in Y \ X by Def2;
hence thesis by Def4;
end;
theorem :: BOOLE'25:
(for x holds not x in X iff (x in Y iff x in Z)) implies X = Y \+\ Z
proof
assume A1: not x in X iff (x in Y iff x in Z);
now let x;
x in X iff x in Y & not x in Z or x in Z & not x in Y by A1;
then x in X iff x in Y \ Z or x in Z \ Y by Def4;
then x in X iff x in (Y \ Z) \/ (Z \ Y) by Def2;
hence x in X iff x in Y \+\ Z by Def6;
end;
hence thesis by TARSKI:2;
end;
definition
cluster {} -> empty;
coherence by Def5;
cluster empty set;
existence
proof {} is empty by Def5; hence thesis; end;
cluster non empty set;
existence
proof consider x;
x in {x} by TARSKI:def 1;
then {x} <> {} by Def1;
then {x} is non empty by Def5;
hence thesis;
end;
end;
definition let D be non empty set, X be set;
cluster D \/ X -> non empty;
coherence
proof
consider x being set such that
A1: x in D by Def1;
x in D \/ X by A1,Def2;
then D \/ X <> {} by Def1;
hence thesis by Def5;
end;
cluster X \/ D -> non empty;
coherence
proof
consider x being set such that
A2: x in D by Def1;
x in X \/ D by A2,Def2;
then X \/ D <> {} by Def1;
hence thesis by Def5;
end;
end;
theorem Th3: :: BOOLE'1:
X meets Y iff ex x st x in X & x in Y
proof
hereby assume X meets Y;
then X /\ Y <> {} by Def7;
then consider x such that
A1: x in X /\ Y by Def1;
take x;
thus x in X & x in Y by A1,Def3;
end;
given x such that
A2: x in X & x in Y;
x in X /\ Y by A2,Def3;
then X /\ Y <> {} by Def1;
hence thesis by Def7;
end;
theorem :: BOOLE'2:
X meets Y iff ex x st x in X /\ Y
proof
hereby assume X meets Y;
then X /\ Y <> {} by Def7;
then consider x such that
A1: x in X /\ Y by Def1;
take x;
thus x in X /\ Y by A1;
end;
given x such that
A2: x in X /\ Y;
X /\ Y <> {} by A2,Def1;
hence thesis by Def7;
end;
theorem :: SYSREL'1:
X misses Y & x in X \/ Y implies
((x in X & not x in Y) or (x in Y & not x in X))
by Def2,Th3;
scheme Extensionality { X,Y() -> set, P[set] } :
X() = Y() provided
A1: for x holds x in X() iff P[x] and
A2: for x holds x in Y() iff P[x]
proof
A3: x in X() implies x in Y()
proof assume x in X(); then P[x] by A1; hence x in Y() by A2; end;
x in Y() implies x in X()
proof assume x in Y(); then P[x] by A2; hence x in X() by A1; end;
hence thesis by A3,TARSKI:2;
end;
scheme SetEq { P[set] } :
for X1,X2 being set st
(for x being set holds x in X1 iff P[x]) &
(for x being set holds x in X2 iff P[x]) holds X1 = X2
proof defpred p[set] means P[$1];
let X1,X2 be set such that
A1: for x being set holds x in X1 iff p[x] and
A2: for x being set holds x in X2 iff p[x];
thus thesis from Extensionality(A1,A2);
end;