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