Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

## Mostowski's Fundamental Operations --- Part II

Grzegorz Bancerek
Warsaw University, Bialystok
Andrzej Kondracki
Warsaw University

### Summary.

The article consists of two parts. The first part is translation of chapter II.3 of . 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 . 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.

#### MML Identifier: ZF_FUND2

The terminology and notation used in this paper have been introduced in the following articles                    

Contents (PDF format)

#### Bibliography

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