:: Tarski {G}rothendieck Set Theory
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI;
begin
reserve x,y,z,u for object;
reserve N,M,X,Y,Z for set;
theorem :: TARSKI:1 :: Everything is a set
for x being object holds x is set;
theorem :: TARSKI:2 :: Extensionality
(for x being object holds x in X iff x in Y) implies X = Y;
definition let y be object;
func { y } -> set means
:: TARSKI:def 1
for x being object holds x in it iff x = y;
let z be object;
func { y, z } -> set means
:: TARSKI:def 2
x in it iff x = y or x = z;
commutativity;
end;
definition let X,Y;
pred X c= Y means
:: TARSKI:def 3
for x being object holds x in X implies x in Y;
reflexivity;
end;
definition let X;
func union X -> set means
:: TARSKI:def 4
x in it iff ex Y st x in Y & Y in X;
end;
theorem :: TARSKI:3 :: Regularity
x in X implies
ex Y st Y in X & not ex x st x in X & x in Y;
definition let x, X be set;
redefine pred x in X;
asymmetry;
end;
scheme :: TARSKI:sch 1
Replacement{ A() -> set, P[object,object] }:
ex X st for x being object holds x in X iff
ex y being object st y in A() & P[y,x]
provided
for x,y,z being object st P[x,y] & P[x,z] holds y = z;
definition let x,y be object;
func [x,y] -> object equals
:: TARSKI:def 5
{ { x,y }, { x } };
end;
definition let X,Y;
pred X,Y are_equipotent means
:: TARSKI:def 6
ex Z st
(for x st x in X ex y st y in Y & [x,y] in Z) &
(for y st y in Y 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;