TARSKI_0

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