:: Properties of ZF Models
::  by Grzegorz Bancerek
::
:: Received July 5, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies ZF_LANG, XBOOLE_0, SUBSET_1, FUNCT_1, CARD_1, ORDINAL1, ZF_MODEL,
      TARSKI, BVFUNC_2, XBOOLEAN, FUNCT_4, ZFMISC_1, NAT_1, FINSEQ_1, ARYTM_3,
      CLASSES2, XXREAL_0, MCART_1, RELAT_1, ZFMODEL1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, XXREAL_0,
      ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, FINSEQ_1, ZF_LANG, RELSET_1,
      FUNCT_2, FUNCT_7, NAT_1, ZF_MODEL, MCART_1;
 constructors ENUMSET1, XXREAL_0, NAT_1, MEMBERED, ZF_MODEL, FUNCT_7, RELSET_1,
      XTUPLE_0, NUMBERS;
 registrations SUBSET_1, MEMBERED, ZF_LANG, RELAT_1, XXREAL_0, RELSET_1,
      XTUPLE_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;

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 that
 not x.0 in Free H and
 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;

theorem :: ZFMODEL1:13
  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 that
 Free H c= { x.3,x.4 } and
 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;

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

theorem :: ZFMODEL1:15
  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:16
  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:17
  E is being_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:18
  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 being_a_model_of_ZF;