The abstract of the Mizar article:

Properties of ZF Models

by

Grzegorz Bancerek

Received July 5, 1989

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;