:: ZF_FUND2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 ) )
proof end;
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 ;
attr M 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

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 )
proof end;

theorem Th2: :: ZF_FUND2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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 )
proof end;

Lm3: for M, E being non empty set
for e being Element of E
for m being Element of M
for v being Function of VAR ,M
for f being Function of VAR ,E
for x being Variable st v = f & m = e holds
v / x,m = f / x,e
proof end;

Lm4: 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 = {}
proof end;

Lm5: for H being ZF-formula
for x, y being Variable st not x in variables_in H & 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)))) )
proof end;

theorem Th3: :: ZF_FUND2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is_limit_ordinal holds
L . a = Union (L | a) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & 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
proof end;

Lm6: 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 Nat st x. i in Free H holds
{[i,m]} \/ ((v * decode ) | ((code (Free H)) \ {i})) = ((v / (x. i),m) * decode ) | (code (Free H))
proof end;

theorem Th4: :: ZF_FUND2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 }
proof end;

theorem Th5: :: ZF_FUND2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds
Y is predicatively_closed
proof end;

theorem :: ZF_FUND2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Universe
for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is_limit_ordinal holds
L . a = Union (L | a) ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is closed_wrt_A1-A7 holds
Union L is_a_model_of_ZF
proof end;