Volume 3, 1991

University of Bialystok

Copyright (c) 1991 Association of Mizar Users

**Grzegorz Bancerek**- Warsaw University, Bialystok
**Andrzej Kondracki**- Warsaw University

- The article consists of two parts. The first part is translation of chapter II.3 of [13]. A section of $D_{H}(a)$ determined by $f$ (symbolically $S_{H}(a,f)$) and a notion of predicative closure of a class are defined. It is proved that if following assumptions are satisfied: (o) $A=\bigcup_{\xi}A_{\xi}$, (i) $A_{\xi} \subset A_{\eta}$ for $\xi < \eta$, (ii) $A_{\lambda}=\bigcup_{\xi<\lambda}A_{\lambda}$ ($\lambda$ is a limit number), (iii) $A_{\xi}\in A$, (iv) $A_{\xi}$ is transitive, (v) $(x,y\in A) \rightarrow (x\cap y\in A)$, (vi) $A$ is predicatively closed, then the axiom of power sets and the axiom of substitution are valid in $A$. The second part is continuation of [12]. It is proved that if a non-void, transitive class is closed with respect to the operations $A_{1}-A_{7}$ then it is predicatively closed. At last sufficient criteria for a class to be a model of ZF-theory are formulated: if $A_{\xi}$ satisfies o - iv and $A$ is closed under the operations $A_{1}-A_{7}$ then $A$ is a model of ZF.

Contents (PDF format)

- [1]
Grzegorz Bancerek.
Cardinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
A model of ZF set theory language.
*Journal of Formalized Mathematics*, 1, 1989. - [3]
Grzegorz Bancerek.
Models and satisfiability.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Grzegorz Bancerek.
The ordinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Grzegorz Bancerek.
Sequences of ordinal numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Grzegorz Bancerek.
Increasing and continuous ordinal sequences.
*Journal of Formalized Mathematics*, 2, 1990. - [7]
Grzegorz Bancerek.
The reflection theorem.
*Journal of Formalized Mathematics*, 2, 1990. - [8]
Grzegorz Bancerek.
Replacing of variables in formulas of ZF theory.
*Journal of Formalized Mathematics*, 2, 1990. - [9]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [10]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [11]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
Andrzej Kondracki.
Mostowski's fundamental operations --- part I.
*Journal of Formalized Mathematics*, 2, 1990. - [13] Andrzej Mostowski. \em Constructible Sets with Applications. North Holland, 1969.
- [14]
Andrzej Nedzusiak.
$\sigma$-fields and probability.
*Journal of Formalized Mathematics*, 1, 1989. - [15]
Bogdan Nowak and Grzegorz Bancerek.
Universal classes.
*Journal of Formalized Mathematics*, 2, 1990. - [16]
Andrzej Trybulec.
Enumerated sets.
*Journal of Formalized Mathematics*, 1, 1989. - [17]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [18]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [19]
Andrzej Trybulec and Agata Darmochwal.
Boolean domains.
*Journal of Formalized Mathematics*, 1, 1989. - [20]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989. - [21]
Edmund Woronowicz.
Relations and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]