TARSKI

:: 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

 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;
    for z being object holds z in X1 iff z in X2 by A1,A2;
    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 by TARSKI_0:3;
  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 by TARSKI_0:4;
  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;  :: redefines in (HIDDEN, definition)
  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;