:: Tarski {G}rothendieck Set Theory -- Tarski's Axiom A :: by Andrzej Trybulec :: :: Received January 1, 1989 :: Copyright (c) 1990-2018 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; notations TARSKI; constructors TARSKI; begin reserve x,y,z,u for object; reserve N,M,X,Y,Z for set; :: Alfred Tarski :: Ueber unerreichbare Kardinalzahlen, :: Fundamenta Mathematicae, vol. 30 (1938), pp. 68--69 :: Axiom A. (Axiom der unerreichbaren Mengen). Zu jeder Menge N gibt es :: eine Menge M mit folgenden Eigenschaften: :: A1. N in M; :: A2. ist X in M und Y c= X, so ist Y in M; :: A3. ist X in M und ist Z die Menge, die alle Mengen Y c= X und keine :: andere Dinge als Element enthaelt, so,ist z in M; :: A4. ist X c= M und sind dabei die Menge X und M nicht gleichmaechtig, :: so ist X in M. :: Alfred Tarski :: On Well-ordered Subsets of any Set, :: Fundamenta Mathematicae, vol. 32 (1939), pp. 176--183 :: A. For every set N there exists a system M of sets which satisfies :: the following conditions: :: (i) N in M :: (ii) if X in M and Y c= X, then Y in M :: (iii) if X in M and Z is the system of all subsets of X, then Z in M :: (iv) if X c= M and X and M do not have the same potency, then X in M. theorem :: TARSKI_A:1 ex M st N in M & (for X,Y holds X in M & Y c= X implies Y in M) & (for X st X in M ex Z st Z in M & for Y st Y c= X holds Y in Z) & (for X holds X c= M implies X,M are_equipotent or X in M);