:: Tarski {G}rothendieck Set Theory :: by Andrzej Trybulec :: :: Received January 1, 1989 :: Copyright (c) 1990-2016 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; theorems TARSKI_0; schemes TARSKI_0; begin reserve x,y,z,u for object; reserve N,M,X,Y,Z for set; theorem :: Everything is a set for x being object holds x is set by TARSKI_0:1; theorem :: Extensionality (for x being object holds x in X iff x in Y) implies X = Y by TARSKI_0:2; definition let y be object; func { y } -> set means for x being object holds x in it iff x = y; existence proof consider X being set such that A1: for x being object holds x in X iff x = y or x = y by TARSKI_0:3; take X; thus thesis by A1; end; uniqueness proof let X1, X2 be set such that A1: for z being object holds z in X1 iff z = y and A2: for z being object holds z in X2 iff z = y; now let z be object; z in X1 iff z = y by A1; hence z in X1 iff z in X2 by A2; end; hence thesis by TARSKI_0:2; end; let z be object; func { y, z } -> set means :Def2: x in it iff x = y or x = z; existence proof consider X being set such that A1: for x being object holds x in X iff x = y or x = z by TARSKI_0:3; take X; thus thesis by A1; end; uniqueness proof let X1, X2 be set such that A1: for x being object holds x in X1 iff x = y or x = z and A2: for x being object holds x in X2 iff x = y or x = z; now let x be object; x in X1 iff x = y or x = z by A1; hence x in X1 iff x in X2 by A2; end; hence thesis by TARSKI_0:2; end; commutativity; end; definition let X,Y; pred X c= Y means for x being object holds x in X implies x in Y; reflexivity; end; definition let X; func union X -> set means x in it iff ex Y st x in Y & Y in X; existence proof consider Z being set such that A1: for x being object holds x in Z iff ex Y being set st x in Y & Y in X by TARSKI_0:4; take Z; thus thesis by A1; end; uniqueness proof let X1, X2 be set such that A1: for x being object holds x in X1 iff ex Y being set st x in Y & Y in X and A2: for x being object holds x in X2 iff ex Y being set st x in Y & Y in X; now let x be object; x in X1 iff ex Y being set st x in Y & Y in X by A1; hence x in X1 iff x in X2 by A2; end; hence thesis by TARSKI_0:2; end; end; theorem :: Regularity x in X implies ex Y st Y in X & not ex x st x in X & x in Y by TARSKI_0:5; definition let x, X be set; redefine pred x in X; asymmetry proof let a,b be set; assume A1: a in b & b in a; set X = {a,b}; A3: a in X & b in X by Def2; consider Y being set such that A4: Y in X & not ex x being object st x in X & x in Y by A3,TARSKI_0:5; Y = a or Y = b by A4,Def2; hence thesis by A1,A3,A4; end; end; scheme 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 A1: for x,y,z being object st P[x,y] & P[x,z] holds y = z proof thus thesis from TARSKI_0:sch 1(A1); end; definition let x,y be object; func [x,y] -> object equals { { x,y }, { x } }; coherence; end; definition let X,Y; pred X,Y are_equipotent means 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;