:: Tarski {G}rothendieck Set Theory :: by Andrzej Trybulec :: :: Received January 1, 1989 :: Copyright (c) 1990-2018 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;