xboole_0.miz
begin
reserve X,Y,Z for
set,
x,y,z for
object;
scheme ::
XBOOLE_0:sch1
Separation { A() ->
set , P[
object] } :
ex X be
set st for x holds x
in X iff x
in A() & P[x];
defpred
Q[
object,
object] means $1
= $2 & P[$2];
A1: for x,y,z be
object 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
TARSKI:sch 1(
A1);
take X;
let x;
thus x
in X implies x
in A() & P[x]
proof
assume x
in X;
then ex y st y
in A() &
Q[y, x] by
A2;
hence thesis;
end;
assume x
in A() & P[x];
then ex y st y
in A() &
Q[y, x];
hence x
in X by
A2;
end;
definition
let X be
set;
::
XBOOLE_0:def1
attr X is
empty means
:
Def1: not ex x st x
in X;
end
registration
cluster
empty for
set;
existence
proof
defpred
P[
object] means contradiction;
consider Y such that
A1: for x holds x
in Y iff x
in the
set &
P[x] from
Separation;
take Y;
thus not ex x st x
in Y by
A1;
end;
end
definition
::
XBOOLE_0:def2
func
{} ->
set equals the
empty
set;
coherence ;
let X,Y be
set;
::
XBOOLE_0:def3
func X
\/ Y ->
set means
:
Def3: for x holds 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 Z be
set 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;
uniqueness
proof
let A1,A2 be
set such that
A1: for x holds x
in A1 iff x
in X or x
in Y and
A2: for x holds 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
A1;
hence x
in A1 iff x
in A2 by
A2;
end;
hence thesis by
TARSKI: 2;
end;
commutativity ;
idempotence ;
::
XBOOLE_0:def4
func X
/\ Y ->
set means
:
Def4: for x holds x
in it iff x
in X & x
in Y;
existence
proof
defpred
P[
object] means $1
in Y;
thus ex Z be
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
A3: for x holds x
in A1 iff x
in X & x
in Y and
A4: for x holds x
in A2 iff x
in X & x
in Y;
now
let x;
x
in A1 iff x
in X & x
in Y by
A3;
hence x
in A1 iff x
in A2 by
A4;
end;
hence thesis by
TARSKI: 2;
end;
commutativity ;
idempotence ;
::
XBOOLE_0:def5
func X
\ Y ->
set means
:
Def5: for x holds x
in it iff x
in X & not x
in Y;
existence
proof
defpred
P[
object] means not $1
in Y;
thus ex Z be
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
A5: for x holds x
in A1 iff x
in X & not x
in Y and
A6: for x holds 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
A5;
hence x
in A1 iff x
in A2 by
A6;
end;
hence thesis by
TARSKI: 2;
end;
end
definition
let X,Y be
set;
::
XBOOLE_0:def6
func X
\+\ Y ->
set equals ((X
\ Y)
\/ (Y
\ X));
correctness ;
commutativity ;
::
XBOOLE_0:def7
pred X
misses Y means (X
/\ Y)
=
{} ;
symmetry ;
::
XBOOLE_0:def8
pred X
c< Y means
:
Def8: X
c= Y & X
<> Y;
irreflexivity ;
asymmetry by
TARSKI: 2;
::
XBOOLE_0:def9
pred X,Y
are_c=-comparable means X
c= Y or Y
c= X;
reflexivity ;
symmetry ;
:: original:
=
redefine
::
XBOOLE_0:def10
pred X
= Y means X
c= Y & Y
c= X;
compatibility by
TARSKI: 2;
end
notation
let X,Y be
set;
antonym X
meets Y for X
misses Y;
end
theorem ::
XBOOLE_0:1
x
in (X
\+\ Y) iff not (x
in X iff x
in Y)
proof
x
in (X
\+\ Y) iff x
in (X
\ Y) or x
in (Y
\ X) by
Def3;
hence thesis by
Def5;
end;
theorem ::
XBOOLE_0:2
(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
Def5;
hence x
in X iff x
in (Y
\+\ Z) by
Def3;
end;
hence thesis by
TARSKI: 2;
end;
registration
cluster
{} ->
empty;
coherence ;
end
registration
let x;
cluster
{x} -> non
empty;
coherence
proof
x
in
{x} by
TARSKI:def 1;
hence ex z st z
in
{x};
end;
let y;
cluster
{x, y} -> non
empty;
coherence
proof
x
in
{x, y} by
TARSKI:def 2;
hence ex z st z
in
{x, y};
end;
end
registration
cluster non
empty for
set;
existence
proof
take
{ the
set};
thus thesis;
end;
end
registration
let D be non
empty
set, X be
set;
cluster (D
\/ X) -> non
empty;
coherence
proof
consider x such that
A1: x
in D by
Def1;
x
in (D
\/ X) by
A1,
Def3;
hence ex x st x
in (D
\/ X);
end;
cluster (X
\/ D) -> non
empty;
coherence ;
end
Lm1: X is
empty implies X
=
{}
proof
assume not ex x st x
in X;
then for x holds x
in
{} iff x
in X by
Def1;
hence thesis by
TARSKI: 2;
end;
theorem ::
XBOOLE_0:3
Th3: X
meets Y iff ex x st x
in X & x
in Y
proof
hereby
assume X
meets Y;
then (X
/\ Y)
<>
{} ;
then not (X
/\ Y) is
empty by
Lm1;
then
consider x such that
A1: x
in (X
/\ Y);
take x;
thus x
in X & x
in Y by
A1,
Def4;
end;
given x such that
A2: x
in X & x
in Y;
x
in (X
/\ Y) by
A2,
Def4;
then (X
/\ Y)
<>
{} by
Def1;
hence thesis;
end;
theorem ::
XBOOLE_0:4
X
meets Y iff ex x st x
in (X
/\ Y)
proof
hereby
assume X
meets Y;
then (X
/\ Y)
<>
{} ;
then not (X
/\ Y) is
empty by
Lm1;
then
consider x such that
A1: x
in (X
/\ Y);
take x;
thus x
in (X
/\ Y) by
A1;
end;
assume ex x st x
in (X
/\ Y);
then (X
/\ Y)
<>
{} by
Def1;
hence thesis;
end;
theorem ::
XBOOLE_0:5
X
misses Y & x
in (X
\/ Y) implies x
in X & not x
in Y or x
in Y & not x
in X by
Def3,
Th3;
scheme ::
XBOOLE_0:sch2
Extensionality { X,Y() ->
set , P[
object] } :
X()
= Y()
provided
A1: for x holds x
in X() iff P[x]
and
A2: for x holds x
in Y() iff P[x];
A3: for x holds x
in Y() implies x
in X() by
A1,
A2;
for x holds x
in X() implies x
in Y() by
A1,
A2;
hence thesis by
A3,
TARSKI: 2;
end;
scheme ::
XBOOLE_0:sch3
SetEq { P[
object] } :
for X1,X2 be
set st (for x holds x
in X1 iff P[x]) & (for x holds x
in X2 iff P[x]) holds X1
= X2;
let X1,X2 be
set such that
A1: for x holds x
in X1 iff P[x] and
A2: for x holds x
in X2 iff P[x];
thus thesis from
Extensionality(
A1,
A2);
end;
begin
theorem ::
XBOOLE_0:6
Th6: X
c< Y implies ex x st x
in Y & not x
in X by
Def8,
TARSKI:def 3;
theorem ::
XBOOLE_0:7
X
<>
{} implies ex x st x
in X by
Def1,
Lm1;
theorem ::
XBOOLE_0:8
X
c< Y implies ex x st x
in Y & X
c= (Y
\
{x})
proof
assume
A1: X
c< Y;
then
consider x such that
A2: x
in Y and
A3: not x
in X by
Th6;
take x;
thus x
in Y by
A2;
let y;
assume
A4: y
in X;
then y
<> x by
A3;
then
A5: not y
in
{x} by
TARSKI:def 1;
X
c= Y by
A1;
then y
in Y by
A4;
hence thesis by
Def5,
A5;
end;
notation
let x,y be
set;
antonym x
c/= y for x
c= y;
end
notation
let x be
object, y be
set;
antonym x
nin y for x
in y;
end