begin
:: 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 = {} ) );
:: 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:
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 )
theorem Th2:
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 & {(x. 0 ),(x. 1),(x. 2)} misses Free H & 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) & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),((H / (x. 0 ),x) <=> ((x. 4) '=' (x. 0 ))))) & def_func' H,v = def_func' (H / (x. 0 ),x),v )
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 ))))) & not x. 4 in Free H holds
for m being Element of M holds (def_func' H,v) .: m = {}
Lm4:
for H being ZF-formula
for y, x being Variable st not y in variables_in H & x <> x. 0 & y <> x. 0 & y <> x. 4 holds
( x. 4 in Free H iff x. 0 in Free (Ex (x. 3),(((x. 3) 'in' x) '&' ((H / (x. 0 ),y) / (x. 4),(x. 0 )))) )
theorem Th3:
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))
theorem Th4:
theorem Th5:
theorem