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 [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.

#### MML Identifier: ZF_FUND2

The terminology and notation used in this paper have been introduced in the following articles [17] [16] [11] [20] [18] [21] [9] [10] [4] [2] [3] [5] [1] [14] [8] [15] [6] [7] [12] [19]

Contents (PDF format)

#### Bibliography

[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.