:: by Grzegorz Bancerek and Andrzej Kondracki

::

:: Received February 15, 1991

:: Copyright (c) 1991-2016 Association of Mizar Users

definition

let H be ZF-formula;

let M be non empty set ;

let v be Function of VAR,M;

( ( 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 ) )

for b_{1} being Subset of M holds verum
;

end;
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 { m where m is Element of M : M,v / ((x. 0),m) |= H } if x. 0 in Free H

otherwise {} ;

( ( 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 b

:: 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) = {} ) );

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 ;

end;
attr M is predicatively_closed means :: 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;

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;

:: deftheorem 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 );

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)

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

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

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 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;

Lm4: for H being ZF-formula

for x, y 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)))))) )

proof end;

theorem Th3: :: ZF_FUND2:3

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

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;

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))

proof end;

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) }

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

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

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

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 being_a_model_of_ZF

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 being_a_model_of_ZF

proof end;