:: TARSKI semantic presentation

begin


theorem :: TARSKI:1
for X, Y being set st ( for x being set holds
( x in X iff x in Y ) ) holds
X = Y ;

definition
let y be set ;
func{y} ->  set  means :: TARSKI:def 1
 for x being set holds
( x in it iff x = y );
correctness
existence
ex b1 being set st
for x being set holds
( x in b1 iff x = y );
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x = y ) ) & ( for x being set holds
( x in b2 iff x = y ) ) holds
b1 = b2;
;
let z be set ;
func{y,z} ->  set  means :: TARSKI:def 2
 for x being set holds
( x in it iff ( x = y or x = z ) );
correctness
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x = y or x = z ) );
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x = y or x = z ) ) ) & ( for x being set holds
( x in b2 iff ( x = y or x = z ) ) ) holds
b1 = b2;
;
commutativity
 for b1, y, z being set st ( for x being set holds
( x in b1 iff ( x = y or x = z ) ) ) holds
for x being set holds
( x in b1 iff ( x = z or x = y ) ) ;
end;

:: deftheorem  defines { TARSKI:def_1_:_
 for y, b2 being set holds
( b2 = {y} iff for x being set holds
( x in b2 iff x = y ) );

:: deftheorem  defines { TARSKI:def_2_:_
 for y, z, b3 being set holds
( b3 = {y,z} iff for x being set holds
( x in b3 iff ( x = y or x = z ) ) );

definition
let X, Y be set ;
predX c= Y means :: TARSKI:def 3
 for x being set st x in X holds
x in Y;
reflexivity
 for X, x being set st x in X holds
x in X ;
end;

:: deftheorem  defines c= TARSKI:def_3_:_
 for X, Y being set holds
( X c= Y iff for x being set st x in X holds
x in Y );

definition
let X be set ;
func union X ->  set  means :: TARSKI:def 4
 for x being set holds
( x in it iff ex Y being set st
( x in Y & Y in X ) );
correctness
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex Y being set st
( x in Y & Y in X ) );
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex Y being set st
( x in Y & Y in X ) ) ) & ( for x being set holds
( x in b2 iff ex Y being set st
( x in Y & Y in X ) ) ) holds
b1 = b2;
;
end;

:: deftheorem  defines union TARSKI:def_4_:_
 for X, b2 being set holds
( b2 = union X iff for x being set holds
( x in b2 iff ex Y being set st
( x in Y & Y in X ) ) );

theorem :: TARSKI:2
for x, X being set st x in X holds
ex Y being set st
( Y in X & ( for x being set holds
( not x in X or not x in Y ) ) ) ;

scheme :: TARSKI:sch 1
Fraenkel{ F1() ->  set , P1[ set , set ] } :
 ex X being set st
for x being set holds
( x in X iff ex y being set st
( y in F1() & P1[y,x] ) )
provided
 for x, y, z being set st P1[x,y] & P1[x,z] holds
y = z
proof
thus  ex X being set st
for x being set holds
( x in X iff ex y being set st
( y in F1() & P1[y,x] ) ) ; ::_thesis: verum
end;

definition
let x, y be set ;
func[x,y] ->  set  equals :: TARSKI:def 5
{{x,y},{x}};
correctness
coherence
{{x,y},{x}} is set ;
;
end;

:: deftheorem  defines [ TARSKI:def_5_:_
 for x, y being set holds [x,y] = {{x,y},{x}};

definition
let X, Y be set ;
predX,Y are_equipotent  means :: TARSKI:def 6
 ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in Y & [x,y] in Z ) ) & ( for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) );
end;

:: deftheorem  defines are_equipotent TARSKI:def_6_:_
 for X, Y being set holds
( X,Y are_equipotent iff ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in Y & [x,y] in Z ) ) & ( for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) ) );

theorem :: TARSKI:3
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
ex Z being set st
( Z in M & ( for Y being set st Y c= X holds
Y in Z ) ) ) & ( for X being set holds
( not X c= M or X,M are_equipotent or X in M ) ) ) ;