:: ZFMODEL1 semantic presentation

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 A1: ( not x. 0 in Free H & 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

proof end;

uniqueness

proof end;

end;

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

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 A1: ( Free H c= {(x. 3),(x. 4)} & 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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines def_func ZFMODEL1:def 2 :

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 :

:: deftheorem Def4 defines is_parametrically_definable_in ZFMODEL1:def 4 :

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_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_a_model_of_ZF

proof end;