:: TARSKI semantic presentation

theorem Th1: :: TARSKI:1
canceled;

theorem Th2: :: TARSKI:2
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 in b2 ) ) holds
b1 = b2 ;

definition
let c1 be set ;
func {c1} -> set means :: TARSKI:def 1
for b1 being set holds
( b1 in a2 iff b1 = a1 );
correctness
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 = c1 );
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 = c1 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 = c1 ) ) holds
b1 = b2;
;
let c2 be set ;
func {c1,c2} -> set means :: TARSKI:def 2
for b1 being set holds
( b1 in a3 iff ( b1 = a1 or b1 = a2 ) );
correctness
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ( b2 = c1 or b2 = c2 ) );
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ( b3 = c1 or b3 = c2 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ( b3 = c1 or b3 = c2 ) ) ) holds
b1 = b2;
;
commutativity
for b1 being set
for b2, b3 being set st ( for b4 being set holds
( b4 in b1 iff ( b4 = b2 or b4 = b3 ) ) ) holds
for b4 being set holds
( b4 in b1 iff ( b4 = b3 or b4 = b2 ) ) ;
end;

:: deftheorem Def1 defines { TARSKI:def 1 :
for b1 being set
for b2 being set holds
( b2 = {b1} iff for b3 being set holds
( b3 in b2 iff b3 = b1 ) );

:: deftheorem Def2 defines { TARSKI:def 2 :
for b1, b2 being set
for b3 being set holds
( b3 = {b1,b2} iff for b4 being set holds
( b4 in b3 iff ( b4 = b1 or b4 = b2 ) ) );

theorem Th3: :: TARSKI:3
canceled;

theorem Th4: :: TARSKI:4
canceled;

definition
let c1, c2 be set ;
pred c1 c= c2 means :: TARSKI:def 3
for b1 being set st b1 in a1 holds
b1 in a2;
reflexivity
for b1, b2 being set st b2 in b1 holds
b2 in b1 ;
end;

:: deftheorem Def3 defines c= TARSKI:def 3 :
for b1, b2 being set holds
( b1 c= b2 iff for b3 being set st b3 in b1 holds
b3 in b2 );

definition
let c1 be set ;
func union c1 -> set means :: TARSKI:def 4
for b1 being set holds
( b1 in a2 iff ex b2 being set st
( b1 in b2 & b2 in a1 ) );
correctness
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being set st
( b2 in b3 & b3 in c1 ) );
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being set st
( b3 in b4 & b4 in c1 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being set st
( b3 in b4 & b4 in c1 ) ) ) holds
b1 = b2;
;
end;

:: deftheorem Def4 defines union TARSKI:def 4 :
for b1 being set
for b2 being set holds
( b2 = union b1 iff for b3 being set holds
( b3 in b2 iff ex b4 being set st
( b3 in b4 & b4 in b1 ) ) );

theorem Th5: :: TARSKI:5
canceled;

theorem Th6: :: TARSKI:6
canceled;

theorem Th7: :: TARSKI:7
for b1, b2 being set st b1 in b2 holds
ex b3 being set st
( b3 in b2 & ( for b4 being set holds
( not b4 in b2 or not b4 in b3 ) ) ) ;

scheme :: TARSKI:sch 1
s1{ F1() -> set , P1[ set , set ] } :
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being set st
( b3 in F1() & P1[b3,b2] ) )
provided
for b1, b2, b3 being set st P1[b1,b2] & P1[b1,b3] holds
b2 = b3
proof end;

definition
let c1, c2 be set ;
func [c1,c2] -> set equals :Def5: :: TARSKI:def 5
{{a1,a2},{a1}};
coherence
{{c1,c2},{c1}} is set ;
end;

:: deftheorem Def5 defines [ TARSKI:def 5 :
for b1, b2 being set holds [b1,b2] = {{b1,b2},{b1}};

theorem Th8: :: TARSKI:8
canceled;

definition
let c1, c2 be set ;
pred c1,c2 are_equipotent means :: TARSKI:def 6
ex b1 being set st
( ( for b2 being set st b2 in a1 holds
ex b3 being set st
( b3 in a2 & [b2,b3] in b1 ) ) & ( for b2 being set st b2 in a2 holds
ex b3 being set st
( b3 in a1 & [b3,b2] in b1 ) ) & ( for b2, b3, b4, b5 being set st [b2,b3] in b1 & [b4,b5] in b1 holds
( b2 = b4 iff b3 = b5 ) ) );
end;

:: deftheorem Def6 defines are_equipotent TARSKI:def 6 :
for b1, b2 being set holds
( b1,b2 are_equipotent iff ex b3 being set st
( ( for b4 being set st b4 in b1 holds
ex b5 being set st
( b5 in b2 & [b4,b5] in b3 ) ) & ( for b4 being set st b4 in b2 holds
ex b5 being set st
( b5 in b1 & [b5,b4] in b3 ) ) & ( for b4, b5, b6, b7 being set st [b4,b5] in b3 & [b6,b7] in b3 holds
( b4 = b6 iff b5 = b7 ) ) ) );

theorem Th9: :: TARSKI:9
for b1 being set ex b2 being set st
( b1 in b2 & ( for b3, b4 being set st b3 in b2 & b4 c= b3 holds
b4 in b2 ) & ( for b3 being set st b3 in b2 holds
ex b4 being set st
( b4 in b2 & ( for b5 being set st b5 c= b3 holds
b5 in b4 ) ) ) & ( for b3 being set holds
( not b3 c= b2 or b3,b2 are_equipotent or b3 in b2 ) ) ) ;