:: Axioms of 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
begin
reserve x,y,z,a for object;
reserve X,Y,Z for set;
:: Set axiom
theorem
for x being object holds x is set;
:: Extensionality axiom
theorem
(for x being object holds x in X iff x in Y) implies X = Y;
:: Axiom of pair
theorem
for x,y being object ex z being set st
for a being object holds
a in z iff a = x or a = y;
:: Axiom of union
theorem
for X being set
ex Z being set st
for x being object holds
x in Z iff ex Y being set st x in Y & Y in X;
:: Axiom of regularity
theorem
x in X implies ex Y st Y in X & not ex x st x in X & x in Y;
:: Fraenkel's scheme
scheme Replacement { A() -> set, P[object, object] }:
ex X st for x holds x in X iff ex y st y in A() & P[y,x]
provided
for x,y,z being object st P[x,y] & P[x,z] holds y = z
proof
thus thesis;
end;