:: ZF_FUND2 semantic presentation

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

:: deftheorem Def1 defines Section ZF_FUND2:def 1 :
for b1 being ZF-formula
for b2 being non empty set
for b3 being Function of VAR ,b2 holds
( ( x. 0 in Free b1 implies Section b1,b3 = { b4 where B is Element of b2 : b2,b3 / (x. 0),b4 |= b1 } ) & ( not x. 0 in Free b1 implies Section b1,b3 = {} ) );

definition
let c1 be non empty set ;
attr a1 is predicatively_closed means :Def2: :: ZF_FUND2:def 2
for b1 being ZF-formula
for b2 being non empty set
for b3 being Function of VAR ,b2 st b2 in a1 holds
Section b1,b3 in a1;
end;

:: deftheorem Def2 defines predicatively_closed ZF_FUND2:def 2 :
for b1 being non empty set holds
( b1 is predicatively_closed iff for b2 being ZF-formula
for b3 being non empty set
for b4 being Function of VAR ,b3 st b3 in b1 holds
Section b2,b4 in b1 );

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

Lemma4: for b1 being Function
for b2 being set st b2 in Union b1 holds
ex b3 being set st
( b3 in dom b1 & b2 in b1 . b3 )
proof end;

theorem Th2: :: ZF_FUND2:2
for b1 being Universe
for b2 being DOMAIN-Sequence of b1 st ( for b3, b4 being Ordinal of b1 st b3 in b4 holds
b2 . b3 c= b2 . b4 ) & ( for b3 being Ordinal of b1 holds
( b2 . b3 in Union b2 & b2 . b3 is epsilon-transitive ) ) & Union b2 is predicatively_closed holds
Union b2 |= the_axiom_of_power_sets
proof end;

Lemma6: for b1 being ZF-formula
for b2 being non empty set
for b3 being Function of VAR ,b2
for b4 being Variable st not b4 in variables_in b1 & {(x. 0),(x. 1),(x. 2)} misses Free b1 & b2,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b1 <=> ((x. 4) '=' (x. 0))))) holds
( {(x. 0),(x. 1),(x. 2)} misses Free (b1 / (x. 0),b4) & b2,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),((b1 / (x. 0),b4) <=> ((x. 4) '=' (x. 0))))) & def_func' b1,b3 = def_func' (b1 / (x. 0),b4),b3 )
proof end;

Lemma7: for b1, b2 being non empty set
for b3 being Element of b2
for b4 being Element of b1
for b5 being Function of VAR ,b1
for b6 being Function of VAR ,b2
for b7 being Variable st b5 = b6 & b4 = b3 holds
b5 / b7,b4 = b6 / b7,b3
proof end;

Lemma8: for b1 being ZF-formula
for b2 being non empty set
for b3 being Function of VAR ,b2 st b2,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b1 <=> ((x. 4) '=' (x. 0))))) & not x. 4 in Free b1 holds
for b4 being Element of b2 holds (def_func' b1,b3) .: b4 = {}
proof end;

Lemma9: for b1 being ZF-formula
for b2, b3 being Variable st not b2 in variables_in b1 & not b3 in variables_in b1 & b2 <> x. 0 & b3 <> x. 0 & b3 <> x. 4 holds
( x. 4 in Free b1 iff x. 0 in Free (Ex (x. 3),(((x. 3) 'in' b2) '&' ((b1 / (x. 0),b3) / (x. 4),(x. 0)))) )
proof end;

theorem Th3: :: ZF_FUND2:3
for b1 being Universe
for b2 being DOMAIN-Sequence of b1 st omega in b1 & ( for b3, b4 being Ordinal of b1 st b3 in b4 holds
b2 . b3 c= b2 . b4 ) & ( for b3 being Ordinal of b1 st b3 <> {} & b3 is_limit_ordinal holds
b2 . b3 = Union (b2 | b3) ) & ( for b3 being Ordinal of b1 holds
( b2 . b3 in Union b2 & b2 . b3 is epsilon-transitive ) ) & Union b2 is predicatively_closed holds
for b3 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free b3 holds
Union b2 |= the_axiom_of_substitution_for b3
proof end;

Lemma11: for b1 being ZF-formula
for b2 being non empty set
for b3 being Element of b2
for b4 being Function of VAR ,b2
for b5 being Nat st x. b5 in Free b1 holds
{[b5,b3]} \/ ((b4 * decode ) | ((code (Free b1)) \ {b5})) = ((b4 / (x. b5),b3) * decode ) | (code (Free b1))
proof end;

theorem Th4: :: ZF_FUND2:4
for b1 being ZF-formula
for b2 being non empty set
for b3 being Function of VAR ,b2 holds Section b1,b3 = { b4 where B is Element of b2 : {[{} ,b4]} \/ ((b3 * decode ) | ((code (Free b1)) \ {{} })) in Diagram b1,b2 }
proof end;

theorem Th5: :: ZF_FUND2:5
for b1 being Universe
for b2 being Subclass of b1 st b2 is closed_wrt_A1-A7 & b2 is epsilon-transitive holds
b2 is predicatively_closed
proof end;

theorem Th6: :: ZF_FUND2:6
for b1 being Universe
for b2 being DOMAIN-Sequence of b1 st omega in b1 & ( for b3, b4 being Ordinal of b1 st b3 in b4 holds
b2 . b3 c= b2 . b4 ) & ( for b3 being Ordinal of b1 st b3 <> {} & b3 is_limit_ordinal holds
b2 . b3 = Union (b2 | b3) ) & ( for b3 being Ordinal of b1 holds
( b2 . b3 in Union b2 & b2 . b3 is epsilon-transitive ) ) & Union b2 is closed_wrt_A1-A7 holds
Union b2 is_a_model_of_ZF
proof end;