:: ZFMODEL1 semantic presentation

set c1 = x. 0;

set c2 = x. 1;

set c3 = x. 2;

set c4 = x. 3;

set c5 = x. 4;

theorem Th1: :: ZFMODEL1:1
for b1 being non empty set st b1 is epsilon-transitive holds
b1 |= the_axiom_of_extensionality
proof end;

theorem Th2: :: ZFMODEL1:2
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_pairs iff for b2, b3 being Element of b1 holds {b2,b3} in b1 )
proof end;

theorem Th3: :: ZFMODEL1:3
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_pairs iff for b2, b3 being set st b2 in b1 & b3 in b1 holds
{b2,b3} in b1 )
proof end;

theorem Th4: :: ZFMODEL1:4
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_unions iff for b2 being Element of b1 holds union b2 in b1 )
proof end;

theorem Th5: :: ZFMODEL1:5
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_unions iff for b2 being set st b2 in b1 holds
union b2 in b1 )
proof end;

theorem Th6: :: ZFMODEL1:6
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_infinity iff ex b2 being Element of b1 st
( b2 <> {} & ( for b3 being Element of b1 st b3 in b2 holds
ex b4 being Element of b1 st
( b3 c< b4 & b4 in b2 ) ) ) )
proof end;

theorem Th7: :: ZFMODEL1:7
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_infinity iff ex b2 being set st
( b2 in b1 & b2 <> {} & ( for b3 being set st b3 in b2 holds
ex b4 being set st
( b3 c< b4 & b4 in b2 ) ) ) )
proof end;

theorem Th8: :: ZFMODEL1:8
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_power_sets iff for b2 being Element of b1 holds b1 /\ (bool b2) in b1 )
proof end;

theorem Th9: :: ZFMODEL1:9
for b1 being non empty set st b1 is epsilon-transitive holds
( b1 |= the_axiom_of_power_sets iff for b2 being set st b2 in b1 holds
b1 /\ (bool b2) in b1 )
proof end;

defpred S1[ Nat] means for b1 being Variable
for b2 being non empty set
for b3 being ZF-formula
for b4 being Function of VAR ,b2 st len b3 = a1 & not b1 in Free b3 & b2,b4 |= b3 holds
b2,b4 |= All b1,b3;

Lemma5: for b1 being Nat st ( for b2 being Nat st b2 < b1 holds
S1[b2] ) holds
S1[b1]
proof end;

theorem Th10: :: ZFMODEL1:10
for b1 being Variable
for b2 being ZF-formula
for b3 being non empty set
for b4 being Function of VAR ,b3 st not b1 in Free b2 & b3,b4 |= b2 holds
b3,b4 |= All b1,b2
proof end;

Lemma7: for b1 being Variable
for b2 being ZF-formula holds
( the_scope_of (All b1,b2) = b2 & bound_in (All b1,b2) = b1 )
proof end;

theorem Th11: :: ZFMODEL1:11
for b1, b2 being Variable
for b3 being ZF-formula
for b4 being non empty set
for b5 being Function of VAR ,b4 st {b1,b2} misses Free b3 & b4,b5 |= b3 holds
b4,b5 |= All b1,b2,b3
proof end;

theorem Th12: :: ZFMODEL1:12
for b1, b2, b3 being Variable
for b4 being ZF-formula
for b5 being non empty set
for b6 being Function of VAR ,b5 st {b1,b2,b3} misses Free b4 & b5,b6 |= b4 holds
b5,b6 |= All b1,b2,b3,b4
proof end;

definition
let c6 be ZF-formula;
let c7 be non empty set ;
let c8 be Function of VAR ,c7;
assume E9: ( not x. 0 in Free c6 & c7,c8 |= All (x. 3),(Ex (x. 0),(All (x. 4),(c6 <=> ((x. 4) '=' (x. 0))))) ) ;
func def_func' c1,c3 -> Function of a2,a2 means :Def1: :: ZFMODEL1:def 1
for b1 being Function of VAR ,a2 st ( for b2 being Variable holds
( not b1 . b2 <> a3 . b2 or x. 0 = b2 or x. 3 = b2 or x. 4 = b2 ) ) holds
( a2,b1 |= a1 iff a4 . (b1 . (x. 3)) = b1 . (x. 4) );
existence
ex b1 being Function of c7,c7 st
for b2 being Function of VAR ,c7 st ( for b3 being Variable holds
( not b2 . b3 <> c8 . b3 or x. 0 = b3 or x. 3 = b3 or x. 4 = b3 ) ) holds
( c7,b2 |= c6 iff b1 . (b2 . (x. 3)) = b2 . (x. 4) )
proof end;
uniqueness
for b1, b2 being Function of c7,c7 st ( for b3 being Function of VAR ,c7 st ( for b4 being Variable holds
( not b3 . b4 <> c8 . b4 or x. 0 = b4 or x. 3 = b4 or x. 4 = b4 ) ) holds
( c7,b3 |= c6 iff b1 . (b3 . (x. 3)) = b3 . (x. 4) ) ) & ( for b3 being Function of VAR ,c7 st ( for b4 being Variable holds
( not b3 . b4 <> c8 . b4 or x. 0 = b4 or x. 3 = b4 or x. 4 = b4 ) ) holds
( c7,b3 |= c6 iff b2 . (b3 . (x. 3)) = b3 . (x. 4) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines def_func' ZFMODEL1:def 1 :
for b1 being ZF-formula
for b2 being non empty set
for b3 being Function of VAR ,b2 st not x. 0 in Free b1 & b2,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b1 <=> ((x. 4) '=' (x. 0))))) holds
for b4 being Function of b2,b2 holds
( b4 = def_func' b1,b3 iff for b5 being Function of VAR ,b2 st ( for b6 being Variable holds
( not b5 . b6 <> b3 . b6 or x. 0 = b6 or x. 3 = b6 or x. 4 = b6 ) ) holds
( b2,b5 |= b1 iff b4 . (b5 . (x. 3)) = b5 . (x. 4) ) );

theorem Th13: :: ZFMODEL1:13
canceled;

theorem Th14: :: ZFMODEL1:14
for b1 being non empty set
for b2 being ZF-formula
for b3, b4 being Function of VAR ,b1 st ( for b5 being Variable st b3 . b5 <> b4 . b5 holds
not b5 in Free b2 ) & b1,b3 |= b2 holds
b1,b4 |= b2
proof end;

definition
let c6 be ZF-formula;
let c7 be non empty set ;
assume E11: ( Free c6 c= {(x. 3),(x. 4)} & c7 |= All (x. 3),(Ex (x. 0),(All (x. 4),(c6 <=> ((x. 4) '=' (x. 0))))) ) ;
func def_func c1,c2 -> Function of a2,a2 means :Def2: :: ZFMODEL1:def 2
for b1 being Function of VAR ,a2 holds
( a2,b1 |= a1 iff a3 . (b1 . (x. 3)) = b1 . (x. 4) );
existence
ex b1 being Function of c7,c7 st
for b2 being Function of VAR ,c7 holds
( c7,b2 |= c6 iff b1 . (b2 . (x. 3)) = b2 . (x. 4) )
proof end;
uniqueness
for b1, b2 being Function of c7,c7 st ( for b3 being Function of VAR ,c7 holds
( c7,b3 |= c6 iff b1 . (b3 . (x. 3)) = b3 . (x. 4) ) ) & ( for b3 being Function of VAR ,c7 holds
( c7,b3 |= c6 iff b2 . (b3 . (x. 3)) = b3 . (x. 4) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines def_func ZFMODEL1:def 2 :
for b1 being ZF-formula
for b2 being non empty set st Free b1 c= {(x. 3),(x. 4)} & b2 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b1 <=> ((x. 4) '=' (x. 0))))) holds
for b3 being Function of b2,b2 holds
( b3 = def_func b1,b2 iff for b4 being Function of VAR ,b2 holds
( b2,b4 |= b1 iff b3 . (b4 . (x. 3)) = b4 . (x. 4) ) );

definition
let c6 be Function;
let c7 be non empty set ;
pred c1 is_definable_in c2 means :: ZFMODEL1:def 3
ex b1 being ZF-formula st
( Free b1 c= {(x. 3),(x. 4)} & a2 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b1 <=> ((x. 4) '=' (x. 0))))) & a1 = def_func b1,a2 );
pred c1 is_parametrically_definable_in c2 means :Def4: :: ZFMODEL1:def 4
ex b1 being ZF-formulaex b2 being Function of VAR ,a2 st
( {(x. 0),(x. 1),(x. 2)} misses Free b1 & a2,b2 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b1 <=> ((x. 4) '=' (x. 0))))) & a1 = def_func' b1,b2 );
end;

:: deftheorem Def3 defines is_definable_in ZFMODEL1:def 3 :
for b1 being Function
for b2 being non empty set holds
( b1 is_definable_in b2 iff ex b3 being ZF-formula st
( Free b3 c= {(x. 3),(x. 4)} & b2 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b3 <=> ((x. 4) '=' (x. 0))))) & b1 = def_func b3,b2 ) );

:: deftheorem Def4 defines is_parametrically_definable_in ZFMODEL1:def 4 :
for b1 being Function
for b2 being non empty set holds
( b1 is_parametrically_definable_in b2 iff ex b3 being ZF-formulaex b4 being Function of VAR ,b2 st
( {(x. 0),(x. 1),(x. 2)} misses Free b3 & b2,b4 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b3 <=> ((x. 4) '=' (x. 0))))) & b1 = def_func' b3,b4 ) );

theorem Th15: :: ZFMODEL1:15
canceled;

theorem Th16: :: ZFMODEL1:16
canceled;

theorem Th17: :: ZFMODEL1:17
canceled;

theorem Th18: :: ZFMODEL1:18
for b1 being non empty set
for b2 being Function st b2 is_definable_in b1 holds
b2 is_parametrically_definable_in b1
proof end;

theorem Th19: :: ZFMODEL1:19
for b1 being non empty set st b1 is epsilon-transitive holds
( ( for b2 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free b2 holds
b1 |= the_axiom_of_substitution_for b2 ) iff for b2 being ZF-formula
for b3 being Function of VAR ,b1 st {(x. 0),(x. 1),(x. 2)} misses Free b2 & b1,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) holds
for b4 being Element of b1 holds (def_func' b2,b3) .: b4 in b1 )
proof end;

theorem Th20: :: ZFMODEL1:20
for b1 being non empty set st b1 is epsilon-transitive holds
( ( for b2 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free b2 holds
b1 |= the_axiom_of_substitution_for b2 ) iff for b2 being Function st b2 is_parametrically_definable_in b1 holds
for b3 being set st b3 in b1 holds
b2 .: b3 in b1 )
proof end;

Lemma14: for b1 being non empty set st b1 is epsilon-transitive holds
for b2, b3 being Element of b1 st ( for b4 being Element of b1 holds
( b4 in b2 iff b4 in b3 ) ) holds
b2 = b3
proof end;

theorem Th21: :: ZFMODEL1:21
for b1 being non empty set st b1 is_a_model_of_ZF holds
( b1 is epsilon-transitive & ( for b2, b3 being Element of b1 st ( for b4 being Element of b1 holds
( b4 in b2 iff b4 in b3 ) ) holds
b2 = b3 ) & ( for b2, b3 being Element of b1 holds {b2,b3} in b1 ) & ( for b2 being Element of b1 holds union b2 in b1 ) & ex b2 being Element of b1 st
( b2 <> {} & ( for b3 being Element of b1 st b3 in b2 holds
ex b4 being Element of b1 st
( b3 c< b4 & b4 in b2 ) ) ) & ( for b2 being Element of b1 holds b1 /\ (bool b2) in b1 ) & ( for b2 being ZF-formula
for b3 being Function of VAR ,b1 st {(x. 0),(x. 1),(x. 2)} misses Free b2 & b1,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) holds
for b4 being Element of b1 holds (def_func' b2,b3) .: b4 in b1 ) )
proof end;

theorem Th22: :: ZFMODEL1:22
for b1 being non empty set st b1 is epsilon-transitive & ( for b2, b3 being Element of b1 holds {b2,b3} in b1 ) & ( for b2 being Element of b1 holds union b2 in b1 ) & ex b2 being Element of b1 st
( b2 <> {} & ( for b3 being Element of b1 st b3 in b2 holds
ex b4 being Element of b1 st
( b3 c< b4 & b4 in b2 ) ) ) & ( for b2 being Element of b1 holds b1 /\ (bool b2) in b1 ) & ( for b2 being ZF-formula
for b3 being Function of VAR ,b1 st {(x. 0),(x. 1),(x. 2)} misses Free b2 & b1,b3 |= All (x. 3),(Ex (x. 0),(All (x. 4),(b2 <=> ((x. 4) '=' (x. 0))))) holds
for b4 being Element of b1 holds (def_func' b2,b3) .: b4 in b1 ) holds
b1 is_a_model_of_ZF
proof end;