:: Mostowski's Fundamental Operations - Part II
:: by Grzegorz Bancerek and Andrzej Kondracki
::
:: Received February 15, 1991
:: Copyright (c) 1991-2012 Association of Mizar Users


begin

definition
let H be ZF-formula;
let M be non empty set ;
let v be Function of VAR,M;
func Section (H,v) ->  Subset of M equals :Def1: :: ZF_FUND2:def 1
 {  m where m is Element of M : M,v / ((x. 0),m) |= H  }   if  x. 0 in Free H
otherwise  {} ;
coherence
 ( ( x. 0 in Free H implies  {  m where m is Element of M : M,v / ((x. 0),m) |= H  }  is Subset of M ) & ( not x. 0 in Free H implies {} is Subset of M ) )
proofend;
consistency
 for b1 being Subset of M holds verum ;
end;

:: deftheorem Def1 defines Section ZF_FUND2:def_1_:_
 for H being ZF-formula
for M being non empty set
for v being Function of VAR,M holds
( ( x. 0 in Free H implies Section (H,v) =  {  m where m is Element of M : M,v / ((x. 0),m) |= H  }  ) & ( not x. 0 in Free H implies Section (H,v) = {} ) );

definition
let M be non empty set ;
attrM is predicatively_closed  means :Def2: :: ZF_FUND2:def 2
 for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st E in M holds
Section (H,f) in M;
end;

:: deftheorem Def2 defines predicatively_closed ZF_FUND2:def_2_:_
 for M being non empty set holds
( M is predicatively_closed iff for H being ZF-formula
for E being non empty set
for f being Function of VAR,E st E in M holds
Section (H,f) in M );

theorem Th1: :: ZF_FUND2:1
for E being non empty set
for e being Element of E
for f being Function of VAR,E st E is epsilon-transitive holds
Section ((All ((x. 2),(((x. 2) 'in' (x. 0)) => ((x. 2) 'in' (x. 1))))),(f / ((x. 1),e))) = E /\ (bool e)
proofend;

Lm1:  for g being Function
for u1 being set st u1 in Union g holds
ex u2 being set st
( u2 in dom g & u1 in g . u2 )
proofend;

theorem Th2: :: ZF_FUND2:2
for W being Universe
for L being DOMAIN-Sequence of W st ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
Union L |= the_axiom_of_power_sets
proofend;

Lm2:  for H being ZF-formula
for M being non empty set
for v being Function of VAR,M
for x being Variable st not x in variables_in H &amp; {(x. 0),(x. 1),(x. 2)} misses Free H &amp; M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (H / ((x. 0),x)) &amp; M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / ((x. 0),x)) <=> ((x. 4) '=' (x. 0)))))))) &amp; def_func' (H,v) = def_func' ((H / ((x. 0),x)),v) )
proofend;

Lm3:  for H being ZF-formula
for M being non empty set
for v being Function of VAR,M st M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) &amp; not x. 4 in Free H holds
for m being Element of M holds (def_func' (H,v)) .: m = {}
proofend;

Lm4:  for H being ZF-formula
for y, x being Variable st not y in variables_in H &amp; x <> x. 0 &amp; y <> x. 0 &amp; y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex ((x. 3),(((x. 3) 'in' x) '&amp;' ((H / ((x. 0),y)) / ((x. 4),(x. 0)))))) )
proofend;

theorem Th3: :: ZF_FUND2:3
for W being Universe
for L being DOMAIN-Sequence of W st omega in W &amp; ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) &amp; ( for a being Ordinal of W st a <> {} &amp; a is limit_ordinal holds
L . a = Union (L | a) ) &amp; ( for a being Ordinal of W holds
( L . a in Union L &amp; L . a is epsilon-transitive ) ) &amp; Union L is predicatively_closed holds
for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds
Union L |= the_axiom_of_substitution_for H
proofend;

Lm5:  for H being ZF-formula
for M being non empty set
for m being Element of M
for v being Function of VAR,M
for i being Element of NAT st x. i in Free H holds
{[i,m]} \/ ((v * decode) | ((code (Free H)) \ {i})) = ((v / ((x. i),m)) * decode) | (code (Free H))
proofend;

theorem Th4: :: ZF_FUND2:4
for H being ZF-formula
for M being non empty set
for v being Function of VAR,M holds Section (H,v) =  {  m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M)  }
proofend;

theorem Th5: :: ZF_FUND2:5
for W being Universe
for Y being Subclass of W st Y is closed_wrt_A1-A7 &amp; Y is epsilon-transitive holds
Y is predicatively_closed
proofend;

theorem :: ZF_FUND2:6
for W being Universe
for L being DOMAIN-Sequence of W st omega in W &amp; ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) &amp; ( for a being Ordinal of W st a <> {} &amp; a is limit_ordinal holds
L . a = Union (L | a) ) &amp; ( for a being Ordinal of W holds
( L . a in Union L &amp; L . a is epsilon-transitive ) ) &amp; Union L is closed_wrt_A1-A7 holds
Union L is being_a_model_of_ZF
proofend;