tarski.miz
begin
reserve x,y,z,u for
object;
reserve N,M,X,Y,Z for
set;
theorem ::
TARSKI:1
for x be
object holds x is
set by
TARSKI_0: 1;
theorem ::
TARSKI:2
(for x be
object holds x
in X iff x
in Y) implies X
= Y by
TARSKI_0: 2;
definition
let y be
object;
::
TARSKI:def1
func
{y} ->
set means for x be
object holds x
in it iff x
= y;
existence
proof
consider X be
set such that
A1: for x be
object holds x
in X iff x
= y or x
= y by
TARSKI_0: 3;
take X;
thus thesis by
A1;
end;
uniqueness
proof
let X1,X2 be
set such that
A1: for z be
object holds z
in X1 iff z
= y and
A2: for z be
object holds z
in X2 iff z
= y;
for z be
object holds z
in X1 iff z
in X2 by
A1,
A2;
hence thesis by
TARSKI_0: 2;
end;
let z be
object;
::
TARSKI:def2
func
{y,z} ->
set means
:
Def2: x
in it iff x
= y or x
= z;
existence by
TARSKI_0: 3;
uniqueness
proof
let X1,X2 be
set such that
A1: for x be
object holds x
in X1 iff x
= y or x
= z and
A2: for x be
object holds x
in X2 iff x
= y or x
= z;
now
let x be
object;
x
in X1 iff x
= y or x
= z by
A1;
hence x
in X1 iff x
in X2 by
A2;
end;
hence thesis by
TARSKI_0: 2;
end;
commutativity ;
end
definition
let X, Y;
::
TARSKI:def3
pred X
c= Y means for x be
object holds x
in X implies x
in Y;
reflexivity ;
end
definition
let X;
::
TARSKI:def4
func
union X ->
set means x
in it iff ex Y st x
in Y & Y
in X;
existence by
TARSKI_0: 4;
uniqueness
proof
let X1,X2 be
set such that
A1: for x be
object holds x
in X1 iff ex Y be
set st x
in Y & Y
in X and
A2: for x be
object holds x
in X2 iff ex Y be
set st x
in Y & Y
in X;
now
let x be
object;
x
in X1 iff ex Y be
set st x
in Y & Y
in X by
A1;
hence x
in X1 iff x
in X2 by
A2;
end;
hence thesis by
TARSKI_0: 2;
end;
end
theorem ::
TARSKI:3
x
in X implies ex Y st Y
in X & not ex x st x
in X & x
in Y by
TARSKI_0: 5;
definition
let x,X be
set;
:: original:
in
redefine
pred x
in X;
asymmetry
proof
let a,b be
set;
assume
A1: a
in b & b
in a;
set X =
{a, b};
A3: a
in X & b
in X by
Def2;
consider Y be
set such that
A4: Y
in X & not ex x be
object st x
in X & x
in Y by
A3,
TARSKI_0: 5;
Y
= a or Y
= b by
A4,
Def2;
hence thesis by
A1,
A3,
A4;
end;
end
scheme ::
TARSKI:sch1
Replacement { A() ->
set , P[
object,
object] } :
ex X st for x be
object holds x
in X iff ex y be
object st y
in A() & P[y, x]
provided
A1: for x,y,z be
object st P[x, y] & P[x, z] holds y
= z;
thus thesis from
TARSKI_0:sch 1(
A1);
end;
definition
let x,y be
object;
::
TARSKI:def5
func
[x,y] ->
object equals
{
{x, y},
{x}};
coherence ;
end
definition
let X, Y;
::
TARSKI:def6
pred X,Y
are_equipotent means ex Z st (for x st x
in X holds ex y st y
in Y &
[x, y]
in Z) & (for y st y
in Y holds ex x st x
in X &
[x, y]
in Z) & for x, y, z, u st
[x, y]
in Z &
[z, u]
in Z holds x
= z iff y
= u;
end