:: by Grzegorz Bancerek

::

:: Received July 5, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

set x0 = x. 0;

set x1 = x. 1;

set x2 = x. 2;

set x3 = x. 3;

set x4 = x. 4;

theorem Th2: :: ZFMODEL1:2

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} in E )

( E |= the_axiom_of_pairs iff for u, v being Element of E holds {u,v} in E )

proof end;

theorem :: ZFMODEL1:3

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_pairs iff for X, Y being set st X in E & Y in E holds

{X,Y} in E )

( E |= the_axiom_of_pairs iff for X, Y being set st X in E & Y in E holds

{X,Y} in E )

proof end;

theorem Th4: :: ZFMODEL1:4

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_unions iff for u being Element of E holds union u in E )

( E |= the_axiom_of_unions iff for u being Element of E holds union u in E )

proof end;

theorem :: ZFMODEL1:5

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_unions iff for X being set st X in E holds

union X in E )

( E |= the_axiom_of_unions iff for X being set st X in E holds

union X in E )

proof end;

theorem Th6: :: ZFMODEL1:6

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_infinity iff ex u being Element of E st

( u <> {} & ( for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u ) ) ) )

( E |= the_axiom_of_infinity iff ex u being Element of E st

( u <> {} & ( for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u ) ) ) )

proof end;

theorem :: ZFMODEL1:7

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_infinity iff ex X being set st

( X in E & X <> {} & ( for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X ) ) ) )

( E |= the_axiom_of_infinity iff ex X being set st

( X in E & X <> {} & ( for Y being set st Y in X holds

ex Z being set st

( Y c< Z & Z in X ) ) ) )

proof end;

theorem Th8: :: ZFMODEL1:8

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E )

( E |= the_axiom_of_power_sets iff for u being Element of E holds E /\ (bool u) in E )

proof end;

theorem :: ZFMODEL1:9

for E being non empty set st E is epsilon-transitive holds

( E |= the_axiom_of_power_sets iff for X being set st X in E holds

E /\ (bool X) in E )

( E |= the_axiom_of_power_sets iff for X being set st X in E holds

E /\ (bool X) in E )

proof end;

defpred S

for E being non empty set

for H being ZF-formula

for f being Function of VAR,E st len H = $1 & not x in Free H & E,f |= H holds

E,f |= All (x,H);

Lm1: for n being Nat st ( for k being Nat st k < n holds

S

S

proof end;

theorem Th10: :: ZFMODEL1:10

for x being Variable

for H being ZF-formula

for E being non empty set

for f being Function of VAR,E st not x in Free H & E,f |= H holds

E,f |= All (x,H)

for H being ZF-formula

for E being non empty set

for f being Function of VAR,E st not x in Free H & E,f |= H holds

E,f |= All (x,H)

proof end;

Lm2: for x being Variable

for H being ZF-formula holds

( the_scope_of (All (x,H)) = H & bound_in (All (x,H)) = x )

proof end;

theorem Th11: :: ZFMODEL1:11

for x, y being Variable

for H being ZF-formula

for E being non empty set

for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

for H being ZF-formula

for E being non empty set

for f being Function of VAR,E st {x,y} misses Free H & E,f |= H holds

E,f |= All (x,y,H)

proof end;

theorem :: ZFMODEL1:12

for x, y, z being Variable

for H being ZF-formula

for E being non empty set

for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds

E,f |= All (x,y,z,H)

for H being ZF-formula

for E being non empty set

for f being Function of VAR,E st {x,y,z} misses Free H & E,f |= H holds

E,f |= All (x,y,z,H)

proof end;

definition

let H be ZF-formula;

let E be non empty set ;

let val be Function of VAR,E;

assume that

A1: not x. 0 in Free H and

A2: E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ;

ex b_{1} being Function of E,E st

for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b_{1} . (g . (x. 3)) = g . (x. 4) )

for b_{1}, b_{2} being Function of E,E st ( for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b_{1} . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b_{2} . (g . (x. 3)) = g . (x. 4) ) ) holds

b_{1} = b_{2}

end;
let E be non empty set ;

let val be Function of VAR,E;

assume that

A1: not x. 0 in Free H and

A2: E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ;

func def_func' (H,val) -> Function of E,E means :Def1: :: ZFMODEL1:def 1

for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff it . (g . (x. 3)) = g . (x. 4) );

existence for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff it . (g . (x. 3)) = g . (x. 4) );

ex b

for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b

proof end;

uniqueness for b

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b

b

proof end;

:: deftheorem Def1 defines def_func' ZFMODEL1:def 1 :

for H being ZF-formula

for E being non empty set

for val being Function of VAR,E st not x. 0 in Free H & E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for b_{4} being Function of E,E holds

( b_{4} = def_func' (H,val) iff for g being Function of VAR,E st ( for y being Variable holds

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b_{4} . (g . (x. 3)) = g . (x. 4) ) );

for H being ZF-formula

for E being non empty set

for val being Function of VAR,E st not x. 0 in Free H & E,val |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for b

( b

( not g . y <> val . y or x. 0 = y or x. 3 = y or x. 4 = y ) ) holds

( E,g |= H iff b

theorem Th13: :: ZFMODEL1:13

for E being non empty set

for H being ZF-formula

for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H holds

E,g |= H

for H being ZF-formula

for f, g being Function of VAR,E st ( for x being Variable st f . x <> g . x holds

not x in Free H ) & E,f |= H holds

E,g |= H

proof end;

definition

let H be ZF-formula;

let E be non empty set ;

assume that

A1: Free H c= {(x. 3),(x. 4)} and

A2: E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ;

ex b_{1} being Function of E,E st

for g being Function of VAR,E holds

( E,g |= H iff b_{1} . (g . (x. 3)) = g . (x. 4) )

for b_{1}, b_{2} being Function of E,E st ( for g being Function of VAR,E holds

( E,g |= H iff b_{1} . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E holds

( E,g |= H iff b_{2} . (g . (x. 3)) = g . (x. 4) ) ) holds

b_{1} = b_{2}

end;
let E be non empty set ;

assume that

A1: Free H c= {(x. 3),(x. 4)} and

A2: E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ;

func def_func (H,E) -> Function of E,E means :Def2: :: ZFMODEL1:def 2

for g being Function of VAR,E holds

( E,g |= H iff it . (g . (x. 3)) = g . (x. 4) );

existence for g being Function of VAR,E holds

( E,g |= H iff it . (g . (x. 3)) = g . (x. 4) );

ex b

for g being Function of VAR,E holds

( E,g |= H iff b

proof end;

uniqueness for b

( E,g |= H iff b

( E,g |= H iff b

b

proof end;

:: deftheorem Def2 defines def_func ZFMODEL1:def 2 :

for H being ZF-formula

for E being non empty set st Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for b_{3} being Function of E,E holds

( b_{3} = def_func (H,E) iff for g being Function of VAR,E holds

( E,g |= H iff b_{3} . (g . (x. 3)) = g . (x. 4) ) );

for H being ZF-formula

for E being non empty set st Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for b

( b

( E,g |= H iff b

definition

let F be Function;

let E be non empty set ;

end;
let E be non empty set ;

pred F is_definable_in E means :: ZFMODEL1:def 3

ex H being ZF-formula st

( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) );

ex H being ZF-formula st

( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) );

:: deftheorem defines is_definable_in ZFMODEL1:def 3 :

for F being Function

for E being non empty set holds

( F is_definable_in E iff ex H being ZF-formula st

( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) ) );

for F being Function

for E being non empty set holds

( F is_definable_in E iff ex H being ZF-formula st

( Free H c= {(x. 3),(x. 4)} & E |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func (H,E) ) );

:: deftheorem Def4 defines is_parametrically_definable_in ZFMODEL1:def 4 :

for F being Function

for E being non empty set holds

( F is_parametrically_definable_in E iff ex H being ZF-formula ex f being Function of VAR,E st

( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H,f) ) );

for F being Function

for E being non empty set holds

( F is_parametrically_definable_in E iff ex H being ZF-formula ex f being Function of VAR,E st

( {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F = def_func' (H,f) ) );

theorem :: ZFMODEL1:14

for E being non empty set

for F being Function st F is_definable_in E holds

F is_parametrically_definable_in E

for F being Function st F is_definable_in E holds

F is_parametrically_definable_in E

proof end;

theorem Th15: :: ZFMODEL1:15

for E being non empty set st E is epsilon-transitive holds

( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula

for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for u being Element of E holds (def_func' (H,f)) .: u in E )

( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) iff for H being ZF-formula

for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for u being Element of E holds (def_func' (H,f)) .: u in E )

proof end;

theorem :: ZFMODEL1:16

for E being non empty set st E is epsilon-transitive holds

( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds

for X being set st X in E holds

F .: X in E )

( ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) iff for F being Function st F is_parametrically_definable_in E holds

for X being set st X in E holds

F .: X in E )

proof end;

Lm3: for E being non empty set st E is epsilon-transitive holds

for u, v being Element of E st ( for w being Element of E holds

( w in u iff w in v ) ) holds

u = v

proof end;

theorem :: ZFMODEL1:17

for E being non empty set st E is being_a_model_of_ZF holds

( E is epsilon-transitive & ( for u, v being Element of E st ( for w being Element of E holds

( w in u iff w in v ) ) holds

u = v ) & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st

( u <> {} & ( for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula

for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for u being Element of E holds (def_func' (H,f)) .: u in E ) )

( E is epsilon-transitive & ( for u, v being Element of E st ( for w being Element of E holds

( w in u iff w in v ) ) holds

u = v ) & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st

( u <> {} & ( for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula

for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for u being Element of E holds (def_func' (H,f)) .: u in E ) )

proof end;

theorem :: ZFMODEL1:18

for E being non empty set st E is epsilon-transitive & ( for u, v being Element of E holds {u,v} in E ) & ( for u being Element of E holds union u in E ) & ex u being Element of E st

( u <> {} & ( for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula

for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for u being Element of E holds (def_func' (H,f)) .: u in E ) holds

E is being_a_model_of_ZF

( u <> {} & ( for v being Element of E st v in u holds

ex w being Element of E st

( v c< w & w in u ) ) ) & ( for u being Element of E holds E /\ (bool u) in E ) & ( for H being ZF-formula

for f being Function of VAR,E st {(x. 0),(x. 1),(x. 2)} misses Free H & E,f |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) holds

for u being Element of E holds (def_func' (H,f)) .: u in E ) holds

E is being_a_model_of_ZF

proof end;