:: Tarski {G}rothendieck Set Theory
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users


theorem :: TARSKI:1
for x being object holds x is set by TARSKI_0:1;

theorem :: TARSKI:2
for X, Y being set st ( for x being object holds
( x in X iff x in Y ) ) holds
X = Y by TARSKI_0:2;

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

:: deftheorem defines { TARSKI:def 1 :
for y being object
for b2 being set holds
( b2 = {y} iff for x being object holds
( x in b2 iff x = y ) );

:: deftheorem Def2 defines { TARSKI:def 2 :
for y, z being object
for b3 being set holds
( b3 = {y,z} iff for x being object holds
( x in b3 iff ( x = y or x = z ) ) );

definition
let X, Y be set ;
pred X c= Y means :: TARSKI:def 3
 for x being object st x in X holds
x in Y;
reflexivity
for X being set
for x being object 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 object st x in X holds
x in Y );

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

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

theorem :: TARSKI:3
for x being object
for X being set st x in X holds
ex Y being set st
( Y in X & ( for x being object holds
( not x in X or not x in Y ) ) ) by TARSKI_0:5;

definition
let x, X be set ;
:: original: in
redefine pred x in X;
asymmetry
for x, X being set st R2(b1,b2) holds
not R2(b2,b1)
proof end;
end;

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

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

:: deftheorem defines [ TARSKI:def 5 :
for x, y being object holds [x,y] = {{x,y},{x}};

definition
let X, Y be set ;
pred X,Y are_equipotent means :: TARSKI:def 6
 ex Z being set st
( ( for x being object st x in X holds
ex y being object st
( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds
ex x being object st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object 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 object st x in X holds
ex y being object st
( y in Y & [x,y] in Z ) ) & ( for y being object st y in Y holds
ex x being object st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being object st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) ) );