Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Properties of ZF Models

by
Grzegorz Bancerek

MML identifier: ZFMODEL1
[ Mizar article, MML identifier index ]

```environ

vocabulary ZF_LANG, FUNCT_1, ORDINAL1, ZF_MODEL, TARSKI, BOOLE, FINSEQ_1,
MCART_1, RELAT_1, ZFMODEL1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, XREAL_0, NAT_1,
RELAT_1, FUNCT_1, FINSEQ_1, ZF_LANG, RELSET_1, FUNCT_2, ORDINAL1,
ZF_MODEL, MCART_1;
constructors NAT_1, ENUMSET1, ZF_MODEL, MCART_1, XREAL_0, MEMBERED, XBOOLE_0;
clusters ZF_LANG, RELSET_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM;

begin

reserve x,y,z for Variable,
H for ZF-formula,
E for non empty set,
a,b,c,X,Y,Z for set,
u,v,w for Element of E,
f,g,h,i,j for Function of VAR,E,
k,n for Nat;

theorem :: ZFMODEL1:1
E is epsilon-transitive implies E |= the_axiom_of_extensionality;

theorem :: ZFMODEL1:2
E is epsilon-transitive implies
(E |= the_axiom_of_pairs iff for u,v holds { u,v } in E);

theorem :: ZFMODEL1:3
E is epsilon-transitive implies
(E |= the_axiom_of_pairs iff for X,Y st X in E & Y in E holds { X,Y } in E);

theorem :: ZFMODEL1:4
E is epsilon-transitive implies
(E |= the_axiom_of_unions iff for u holds union u in E);

theorem :: ZFMODEL1:5
E is epsilon-transitive implies
(E |= the_axiom_of_unions iff for X st X in E holds union X in E);

theorem :: ZFMODEL1:6
E is epsilon-transitive implies
(E |= the_axiom_of_infinity iff
ex u st u <> {} & for v st v in u ex w st v c< w & w in u);

theorem :: ZFMODEL1:7
E is epsilon-transitive implies
(E |= the_axiom_of_infinity iff
ex X st X in E & X <> {} & for Y st Y in X ex Z st Y c< Z & Z in X);

theorem :: ZFMODEL1:8
E is epsilon-transitive implies
(E |= the_axiom_of_power_sets iff for u holds E /\ bool u in E);

theorem :: ZFMODEL1:9
E is epsilon-transitive implies
(E |= the_axiom_of_power_sets iff for X st X in E holds E /\ bool X in E);

theorem :: ZFMODEL1:10
not x in Free H & E,f |= H implies E,f |= All(x,H);

theorem :: ZFMODEL1:11
{ x,y } misses Free H & E,f |= H implies E,f |= All(x,y,H);

theorem :: ZFMODEL1:12
{ x,y,z } misses Free H & E,f |= H implies E,f |= All(x,y,z,H);

definition let H,E; let val be Function of VAR,E;
assume
not x.0 in Free H &
E,val |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
func def_func'(H,val) -> Function of E,E means
:: ZFMODEL1:def 1
for g st for y st g.y <> val.y holds x.0 = y or x.3 = y or x.4 = y
holds E,g |= H iff it.(g.x.3) = g.x.4;
end;

canceled;

theorem :: ZFMODEL1:14
for H,f,g st (for x st f.x <> g.x holds not x in Free H) & E,f |= H
holds E,g |= H;

definition let H,E;
assume
Free H c= { x.3,x.4 } &
E |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
func def_func(H,E) -> Function of E,E means
:: ZFMODEL1:def 2
for g holds E,g |= H iff it.(g.x.3) = g.x.4;
end;

definition let F be Function; let E;
pred F is_definable_in E means
:: ZFMODEL1:def 3
ex H st Free H c= { x.3,x.4 } &
E |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) &
F = def_func(H,E);

pred F is_parametrically_definable_in E means
:: ZFMODEL1:def 4
ex H,f st { x.0,x.1,x.2 } misses Free H &
E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) &
F = def_func'(H,f);
end;

canceled 3;

theorem :: ZFMODEL1:18
for F being Function st F is_definable_in E holds
F is_parametrically_definable_in E;

theorem :: ZFMODEL1:19
E is epsilon-transitive implies
((for H st { x.0,x.1,x.2 } misses Free H holds
E |= the_axiom_of_substitution_for H) iff
for H,f st { x.0,x.1,x.2 } misses Free H &
E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
for u holds def_func'(H,f).:u in E );

theorem :: ZFMODEL1:20
E is epsilon-transitive implies
((for H st { x.0,x.1,x.2 } misses Free H holds
E |= the_axiom_of_substitution_for H) iff
for F being Function st F is_parametrically_definable_in E
for X st X in E holds F.:X in E );

theorem :: ZFMODEL1:21
E is_a_model_of_ZF implies
E is epsilon-transitive &
(for u,v st for w holds w in u iff w in v holds u = v) &
(for u,v holds { u,v } in E) &
(for u holds union u in E) &
(ex u st u <> {} & for v st v in u ex w st v c< w & w in u) &
(for u holds E /\ bool u in E) &
(for H,f st { x.0,x.1,x.2 } misses Free H &
E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
for u holds def_func'(H,f).:u in E );

theorem :: ZFMODEL1:22

E is epsilon-transitive &
(for u,v holds { u,v } in E) &
(for u holds union u in E) &
(ex u st u <> {} & for v st v in u ex w st v c< w & w in u) &
(for u holds E /\ bool u in E) &
(for H,f st { x.0,x.1,x.2 } misses Free H &
E,f |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
for u holds def_func'(H,f).:u in E )
implies E is_a_model_of_ZF;
```