:: Properties of ZF Models
:: 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 :: 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 S1[ 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
S1[k] ) holds
S1[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 b1 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 b1 . (g . (x. 3)) = g . (x. 4) )
proof end;
uniqueness
for b1, b2 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 b1 . (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 b2 . (g . (x. 3)) = g . (x. 4) ) ) holds
b1 = b2
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 b4 being Function of E,E holds
( b4 = 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 b4 . (g . (x. 3)) = g . (x. 4) ) );

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
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 b1 being Function of E,E st
for g being Function of VAR,E holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) )
proof end;
uniqueness
for b1, b2 being Function of E,E st ( for g being Function of VAR,E holds
( E,g |= H iff b1 . (g . (x. 3)) = g . (x. 4) ) ) & ( for g being Function of VAR,E holds
( E,g |= H iff b2 . (g . (x. 3)) = g . (x. 4) ) ) holds
b1 = b2
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 b3 being Function of E,E holds
( b3 = def_func (H,E) iff for g being Function of VAR,E holds
( E,g |= H iff b3 . (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:14
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 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 )
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 )
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 ) )
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
proof end;