:: Properties of ZF Models
:: by Grzegorz Bancerek
::
:: Received July 5, 1989
:: Copyright (c) 1990-2011 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 :: ZFMODEL1:1

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

proof end;

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 )

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 )

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 )

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 )

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

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

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 )

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 )

proof end;

defpred S₁[ Nat] means for x being Variable
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₁[k] ) holds
S₁[n]

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)

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)

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)

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)))))))) ;
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
ex b₁ 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₁ . (g . (x. 3)) = g . (x. 4) )

proof end;

uniqueness
for b₁, b₂ 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₁ . (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₂ . (g . (x. 3)) = g . (x. 4) ) ) holds
b₁ = b₂

proof end;

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₄ being Function of E,E holds
( b₄ = 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₄ . (g . (x. 3)) = g . (x. 4) ) );

theorem :: ZFMODEL1:13

canceled;

theorem Th14: :: ZFMODEL1:14

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

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)))))))) ;
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
ex b₁ being Function of E,E st
for g being Function of VAR,E holds
( E,g |= H iff b₁ . (g . (x. 3)) = g . (x. 4) )

proof end;

uniqueness
for b₁, b₂ being Function of E,E st ( for g being Function of VAR,E holds
( E,g |= H iff b₁ . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E holds
( E,g |= H iff b₂ . (g . (x. 3)) = g . (x. 4) ) ) holds
b₁ = b₂

proof end;

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₃ being Function of E,E holds
( b₃ = def_func (H,E) iff for g being Function of VAR,E holds
( E,g |= H iff b₃ . (g . (x. 3)) = g . (x. 4) ) );

definition

let F be Function;
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) );
pred F is_parametrically_definable_in E means :Def4: :: ZFMODEL1:def 4
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) );

end;

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

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

theorem :: ZFMODEL1:15

canceled;

theorem :: ZFMODEL1:16

canceled;

theorem :: ZFMODEL1:17

canceled;

theorem :: ZFMODEL1:18

for E being non empty set
for F being Function st F is_definable_in E holds
F is_parametrically_definable_in E

proof end;

theorem Th19: :: ZFMODEL1:19

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 )

proof end;

theorem :: ZFMODEL1:20

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 )

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:21

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

proof end;

theorem :: ZFMODEL1:22

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

proof end;