:: ZF_MODEL semantic presentation

scheme :: ZF_MODEL:sch 1
s1{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula } :
ex b1, b2 being set st
( ( for b3, b4 being Variable holds
( [(b3 '=' b4),F1(b3,b4)] in b2 & [(b3 'in' b4),F2(b3,b4)] in b2 ) ) & [F6(),b1] in b2 & ( for b3 being ZF-formula
for b4 being set st [b3,b4] in b2 holds
( ( b3 is_equality implies b4 = F1((Var1 b3),(Var2 b3)) ) & ( b3 is_membership implies b4 = F2((Var1 b3),(Var2 b3)) ) & ( b3 is negative implies ex b5 being set st
( b4 = F3(b5) & [(the_argument_of b3),b5] in b2 ) ) & ( b3 is conjunctive implies ex b5, b6 being set st
( b4 = F4(b5,b6) & [(the_left_argument_of b3),b5] in b2 & [(the_right_argument_of b3),b6] in b2 ) ) & ( b3 is universal implies ex b5 being set st
( b4 = F5((bound_in b3),b5) & [(the_scope_of b3),b5] in b2 ) ) ) ) )
proof end;

scheme :: ZF_MODEL:sch 2
s2{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula, F7() -> set , F8() -> set } :
F7() = F8()
provided
E1: ex b1 being set st
( ( for b2, b3 being Variable holds
( [(b2 '=' b3),F1(b2,b3)] in b1 & [(b2 'in' b3),F2(b2,b3)] in b1 ) ) & [F6(),F7()] in b1 & ( for b2 being ZF-formula
for b3 being set st [b2,b3] in b1 holds
( ( b2 is_equality implies b3 = F1((Var1 b2),(Var2 b2)) ) & ( b2 is_membership implies b3 = F2((Var1 b2),(Var2 b2)) ) & ( b2 is negative implies ex b4 being set st
( b3 = F3(b4) & [(the_argument_of b2),b4] in b1 ) ) & ( b2 is conjunctive implies ex b4, b5 being set st
( b3 = F4(b4,b5) & [(the_left_argument_of b2),b4] in b1 & [(the_right_argument_of b2),b5] in b1 ) ) & ( b2 is universal implies ex b4 being set st
( b3 = F5((bound_in b2),b4) & [(the_scope_of b2),b4] in b1 ) ) ) ) ) and
E2: ex b1 being set st
( ( for b2, b3 being Variable holds
( [(b2 '=' b3),F1(b2,b3)] in b1 & [(b2 'in' b3),F2(b2,b3)] in b1 ) ) & [F6(),F8()] in b1 & ( for b2 being ZF-formula
for b3 being set st [b2,b3] in b1 holds
( ( b2 is_equality implies b3 = F1((Var1 b2),(Var2 b2)) ) & ( b2 is_membership implies b3 = F2((Var1 b2),(Var2 b2)) ) & ( b2 is negative implies ex b4 being set st
( b3 = F3(b4) & [(the_argument_of b2),b4] in b1 ) ) & ( b2 is conjunctive implies ex b4, b5 being set st
( b3 = F4(b4,b5) & [(the_left_argument_of b2),b4] in b1 & [(the_right_argument_of b2),b5] in b1 ) ) & ( b2 is universal implies ex b4 being set st
( b3 = F5((bound_in b2),b4) & [(the_scope_of b2),b4] in b1 ) ) ) ) )
proof end;

scheme :: ZF_MODEL:sch 3
s3{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6() -> ZF-formula, F7( ZF-formula) -> set } :
( ( F6() is_equality implies F7(F6()) = F1((Var1 F6()),(Var2 F6())) ) & ( F6() is_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) ) & ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for b1, b2 being set st b1 = F7((the_left_argument_of F6())) & b2 = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(b1,b2) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
provided
E1: for b1 being ZF-formula
for b2 being set holds
( b2 = F7(b1) iff ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),F1(b4,b5)] in b3 & [(b4 'in' b5),F2(b4,b5)] in b3 ) ) & [b1,b2] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = F1((Var1 b4),(Var2 b4)) ) & ( b4 is_membership implies b5 = F2((Var1 b4),(Var2 b4)) ) & ( b4 is negative implies ex b6 being set st
( b5 = F3(b6) & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = F4(b6,b7) & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = F5((bound_in b4),b6) & [(the_scope_of b4),b6] in b3 ) ) ) ) ) )
proof end;

scheme :: ZF_MODEL:sch 4
s4{ F1( Variable, Variable) -> set , F2( Variable, Variable) -> set , F3( set ) -> set , F4( set , set ) -> set , F5( Variable, set ) -> set , F6( ZF-formula) -> set , F7() -> ZF-formula, P1[ set ] } :
P1[F6(F7())]
provided
E1: for b1 being ZF-formula
for b2 being set holds
( b2 = F6(b1) iff ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),F1(b4,b5)] in b3 & [(b4 'in' b5),F2(b4,b5)] in b3 ) ) & [b1,b2] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = F1((Var1 b4),(Var2 b4)) ) & ( b4 is_membership implies b5 = F2((Var1 b4),(Var2 b4)) ) & ( b4 is negative implies ex b6 being set st
( b5 = F3(b6) & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = F4(b6,b7) & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = F5((bound_in b4),b6) & [(the_scope_of b4),b6] in b3 ) ) ) ) ) ) and
E2: for b1, b2 being Variable holds
( P1[F1(b1,b2)] & P1[F2(b1,b2)] ) and
E3: for b1 being set st P1[b1] holds
P1[F3(b1)] and
E4: for b1, b2 being set st P1[b1] & P1[b2] holds
P1[F4(b1,b2)] and
E5: for b1 being set
for b2 being Variable st P1[b1] holds
P1[F5(b2,b1)]
proof end;

deffunc H1( Variable, Variable) -> set = {a1,a2};

deffunc H2( Variable, Variable) -> set = {a1,a2};

deffunc H3( set ) -> set = a1;

deffunc H4( set , set ) -> set = union {a1,a2};

deffunc H5( Variable, set ) -> set = (union {a2}) \ {a1};

definition
let c1 be ZF-formula;
func Free c1 -> set means :Def1: :: ZF_MODEL:def 1
ex b1 being set st
( ( for b2, b3 being Variable holds
( [(b2 '=' b3),{b2,b3}] in b1 & [(b2 'in' b3),{b2,b3}] in b1 ) ) & [a1,a2] in b1 & ( for b2 being ZF-formula
for b3 being set st [b2,b3] in b1 holds
( ( b2 is_equality implies b3 = {(Var1 b2),(Var2 b2)} ) & ( b2 is_membership implies b3 = {(Var1 b2),(Var2 b2)} ) & ( b2 is negative implies ex b4 being set st
( b3 = b4 & [(the_argument_of b2),b4] in b1 ) ) & ( b2 is conjunctive implies ex b4, b5 being set st
( b3 = union {b4,b5} & [(the_left_argument_of b2),b4] in b1 & [(the_right_argument_of b2),b5] in b1 ) ) & ( b2 is universal implies ex b4 being set st
( b3 = (union {b4}) \ {(bound_in b2)} & [(the_scope_of b2),b4] in b1 ) ) ) ) );
existence
ex b1, b2 being set st
( ( for b3, b4 being Variable holds
( [(b3 '=' b4),{b3,b4}] in b2 & [(b3 'in' b4),{b3,b4}] in b2 ) ) & [c1,b1] in b2 & ( for b3 being ZF-formula
for b4 being set st [b3,b4] in b2 holds
( ( b3 is_equality implies b4 = {(Var1 b3),(Var2 b3)} ) & ( b3 is_membership implies b4 = {(Var1 b3),(Var2 b3)} ) & ( b3 is negative implies ex b5 being set st
( b4 = b5 & [(the_argument_of b3),b5] in b2 ) ) & ( b3 is conjunctive implies ex b5, b6 being set st
( b4 = union {b5,b6} & [(the_left_argument_of b3),b5] in b2 & [(the_right_argument_of b3),b6] in b2 ) ) & ( b3 is universal implies ex b5 being set st
( b4 = (union {b5}) \ {(bound_in b3)} & [(the_scope_of b3),b5] in b2 ) ) ) ) )
proof end;
uniqueness
for b1, b2 being set st ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),{b4,b5}] in b3 & [(b4 'in' b5),{b4,b5}] in b3 ) ) & [c1,b1] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = {(Var1 b4),(Var2 b4)} ) & ( b4 is_membership implies b5 = {(Var1 b4),(Var2 b4)} ) & ( b4 is negative implies ex b6 being set st
( b5 = b6 & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = union {b6,b7} & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = (union {b6}) \ {(bound_in b4)} & [(the_scope_of b4),b6] in b3 ) ) ) ) ) & ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),{b4,b5}] in b3 & [(b4 'in' b5),{b4,b5}] in b3 ) ) & [c1,b2] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = {(Var1 b4),(Var2 b4)} ) & ( b4 is_membership implies b5 = {(Var1 b4),(Var2 b4)} ) & ( b4 is negative implies ex b6 being set st
( b5 = b6 & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = union {b6,b7} & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = (union {b6}) \ {(bound_in b4)} & [(the_scope_of b4),b6] in b3 ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines Free ZF_MODEL:def 1 :
for b1 being ZF-formula
for b2 being set holds
( b2 = Free b1 iff ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),{b4,b5}] in b3 & [(b4 'in' b5),{b4,b5}] in b3 ) ) & [b1,b2] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = {(Var1 b4),(Var2 b4)} ) & ( b4 is_membership implies b5 = {(Var1 b4),(Var2 b4)} ) & ( b4 is negative implies ex b6 being set st
( b5 = b6 & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = union {b6,b7} & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = (union {b6}) \ {(bound_in b4)} & [(the_scope_of b4),b6] in b3 ) ) ) ) ) );

deffunc H6( ZF-formula) -> set = Free a1;

Lemma2: for b1 being ZF-formula
for b2 being set holds
( b2 = H6(b1) iff ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),H1(b4,b5)] in b3 & [(b4 'in' b5),H2(b4,b5)] in b3 ) ) & [b1,b2] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = H1( Var1 b4, Var2 b4) ) & ( b4 is_membership implies b5 = H2( Var1 b4, Var2 b4) ) & ( b4 is negative implies ex b6 being set st
( b5 = H3(b6) & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = H4(b6,b7) & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = H5( bound_in b4,b6) & [(the_scope_of b4),b6] in b3 ) ) ) ) ) )
by Def1;

E3: now
let c1 be ZF-formula;
thus ( ( c1 is_equality implies H6(c1) = H1( Var1 c1, Var2 c1) ) & ( c1 is_membership implies H6(c1) = H2( Var1 c1, Var2 c1) ) & ( c1 is negative implies H6(c1) = H3(H6( the_argument_of c1)) ) & ( c1 is conjunctive implies for b1, b2 being set st b1 = H6( the_left_argument_of c1) & b2 = H6( the_right_argument_of c1) holds
H6(c1) = H4(b1,b2) ) & ( c1 is universal implies H6(c1) = H5( bound_in c1,H6( the_scope_of c1)) ) ) from ZF_MODEL:sch 3(Lemma2);
end;

definition
let c1 be ZF-formula;
redefine func Free as Free c1 -> Subset of VAR ;
coherence
Free c1 is Subset of VAR
proof end;
end;

theorem Th1: :: ZF_MODEL:1
for b1 being ZF-formula holds
( ( b1 is_equality implies Free b1 = {(Var1 b1),(Var2 b1)} ) & ( b1 is_membership implies Free b1 = {(Var1 b1),(Var2 b1)} ) & ( b1 is negative implies Free b1 = Free (the_argument_of b1) ) & ( b1 is conjunctive implies Free b1 = (Free (the_left_argument_of b1)) \/ (Free (the_right_argument_of b1)) ) & ( b1 is universal implies Free b1 = (Free (the_scope_of b1)) \ {(bound_in b1)} ) )
proof end;

definition
let c1 be non empty set ;
func VAL c1 -> set means :Def2: :: ZF_MODEL:def 2
for b1 being set holds
( b1 in a2 iff b1 is Function of VAR ,a1 );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff b2 is Function of VAR ,c1 )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff b3 is Function of VAR ,c1 ) ) & ( for b3 being set holds
( b3 in b2 iff b3 is Function of VAR ,c1 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines VAL ZF_MODEL:def 2 :
for b1 being non empty set
for b2 being set holds
( b2 = VAL b1 iff for b3 being set holds
( b3 in b2 iff b3 is Function of VAR ,b1 ) );

registration
let c1 be non empty set ;
cluster VAL a1 -> non empty ;
coherence
not VAL c1 is empty
proof end;
end;

definition
let c1 be ZF-formula;
let c2 be non empty set ;
deffunc H7( Variable, Variable) -> set = { b1 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b2 = b1 holds
b2 . a1 = b2 . a2 } ;
deffunc H8( Variable, Variable) -> set = { b1 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b2 = b1 holds
b2 . a1 in b2 . a2 } ;
deffunc H9( set ) -> set = (VAL c2) \ (union {a1});
deffunc H10( set , set ) -> set = (union {a1}) /\ (union {a2});
deffunc H11( Variable, set ) -> set = { b1 where B is Element of VAL c2 : for b1 being set
for b2 being Function of VAR ,c2 st b2 = a2 & b3 = b1 holds
( b3 in b2 & ( for b3 being Function of VAR ,c2 st ( for b4 being Variable st b4 . b5 <> b3 . b5 holds
a1 = b5 ) holds
b4 in b2 ) ) } ;
func St c1,c2 -> set means :Def3: :: ZF_MODEL:def 3
ex b1 being set st
( ( for b2, b3 being Variable holds
( [(b2 '=' b3),{ b4 where B is Element of VAL a2 : for b1 being Function of VAR ,a2 st b5 = b4 holds
b5 . b2 = b5 . b3 } ] in b1 & [(b2 'in' b3),{ b4 where B is Element of VAL a2 : for b1 being Function of VAR ,a2 st b5 = b4 holds
b5 . b2 in b5 . b3 } ] in b1 ) ) & [a1,a3] in b1 & ( for b2 being ZF-formula
for b3 being set st [b2,b3] in b1 holds
( ( b2 is_equality implies b3 = { b4 where B is Element of VAL a2 : for b1 being Function of VAR ,a2 st b5 = b4 holds
b5 . (Var1 b2) = b5 . (Var2 b2) } ) & ( b2 is_membership implies b3 = { b4 where B is Element of VAL a2 : for b1 being Function of VAR ,a2 st b5 = b4 holds
b5 . (Var1 b2) in b5 . (Var2 b2) } ) & ( b2 is negative implies ex b4 being set st
( b3 = (VAL a2) \ (union {b4}) & [(the_argument_of b2),b4] in b1 ) ) & ( b2 is conjunctive implies ex b4, b5 being set st
( b3 = (union {b4}) /\ (union {b5}) & [(the_left_argument_of b2),b4] in b1 & [(the_right_argument_of b2),b5] in b1 ) ) & ( b2 is universal implies ex b4 being set st
( b3 = { b5 where B is Element of VAL a2 : for b1 being set
for b2 being Function of VAR ,a2 st b6 = b4 & b7 = b5 holds
( b7 in b6 & ( for b3 being Function of VAR ,a2 st ( for b4 being Variable st b8 . b9 <> b7 . b9 holds
bound_in b2 = b9 ) holds
b8 in b6 ) ) } & [(the_scope_of b2),b4] in b1 ) ) ) ) );
existence
ex b1, b2 being set st
( ( for b3, b4 being Variable holds
( [(b3 '=' b4),{ b5 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b6 = b5 holds
b6 . b3 = b6 . b4 } ] in b2 & [(b3 'in' b4),{ b5 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b6 = b5 holds
b6 . b3 in b6 . b4 } ] in b2 ) ) & [c1,b1] in b2 & ( for b3 being ZF-formula
for b4 being set st [b3,b4] in b2 holds
( ( b3 is_equality implies b4 = { b5 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b6 = b5 holds
b6 . (Var1 b3) = b6 . (Var2 b3) } ) & ( b3 is_membership implies b4 = { b5 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b6 = b5 holds
b6 . (Var1 b3) in b6 . (Var2 b3) } ) & ( b3 is negative implies ex b5 being set st
( b4 = (VAL c2) \ (union {b5}) & [(the_argument_of b3),b5] in b2 ) ) & ( b3 is conjunctive implies ex b5, b6 being set st
( b4 = (union {b5}) /\ (union {b6}) & [(the_left_argument_of b3),b5] in b2 & [(the_right_argument_of b3),b6] in b2 ) ) & ( b3 is universal implies ex b5 being set st
( b4 = { b6 where B is Element of VAL c2 : for b1 being set
for b2 being Function of VAR ,c2 st b7 = b5 & b8 = b6 holds
( b8 in b7 & ( for b3 being Function of VAR ,c2 st ( for b4 being Variable st b9 . b10 <> b8 . b10 holds
bound_in b3 = b10 ) holds
b9 in b7 ) ) } & [(the_scope_of b3),b5] in b2 ) ) ) ) )
proof end;
uniqueness
for b1, b2 being set st ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),{ b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . b4 = b7 . b5 } ] in b3 & [(b4 'in' b5),{ b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . b4 in b7 . b5 } ] in b3 ) ) & [c1,b1] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = { b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . (Var1 b4) = b7 . (Var2 b4) } ) & ( b4 is_membership implies b5 = { b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . (Var1 b4) in b7 . (Var2 b4) } ) & ( b4 is negative implies ex b6 being set st
( b5 = (VAL c2) \ (union {b6}) & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = (union {b6}) /\ (union {b7}) & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = { b7 where B is Element of VAL c2 : for b1 being set
for b2 being Function of VAR ,c2 st b8 = b6 & b9 = b7 holds
( b9 in b8 & ( for b3 being Function of VAR ,c2 st ( for b4 being Variable st b10 . b11 <> b9 . b11 holds
bound_in b4 = b11 ) holds
b10 in b8 ) ) } & [(the_scope_of b4),b6] in b3 ) ) ) ) ) & ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),{ b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . b4 = b7 . b5 } ] in b3 & [(b4 'in' b5),{ b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . b4 in b7 . b5 } ] in b3 ) ) & [c1,b2] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = { b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . (Var1 b4) = b7 . (Var2 b4) } ) & ( b4 is_membership implies b5 = { b6 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b7 = b6 holds
b7 . (Var1 b4) in b7 . (Var2 b4) } ) & ( b4 is negative implies ex b6 being set st
( b5 = (VAL c2) \ (union {b6}) & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = (union {b6}) /\ (union {b7}) & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = { b7 where B is Element of VAL c2 : for b1 being set
for b2 being Function of VAR ,c2 st b8 = b6 & b9 = b7 holds
( b9 in b8 & ( for b3 being Function of VAR ,c2 st ( for b4 being Variable st b10 . b11 <> b9 . b11 holds
bound_in b4 = b11 ) holds
b10 in b8 ) ) } & [(the_scope_of b4),b6] in b3 ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines St ZF_MODEL:def 3 :
for b1 being ZF-formula
for b2 being non empty set
for b3 being set holds
( b3 = St b1,b2 iff ex b4 being set st
( ( for b5, b6 being Variable holds
( [(b5 '=' b6),{ b7 where B is Element of VAL b2 : for b1 being Function of VAR ,b2 st b8 = b7 holds
b8 . b5 = b8 . b6 } ] in b4 & [(b5 'in' b6),{ b7 where B is Element of VAL b2 : for b1 being Function of VAR ,b2 st b8 = b7 holds
b8 . b5 in b8 . b6 } ] in b4 ) ) & [b1,b3] in b4 & ( for b5 being ZF-formula
for b6 being set st [b5,b6] in b4 holds
( ( b5 is_equality implies b6 = { b7 where B is Element of VAL b2 : for b1 being Function of VAR ,b2 st b8 = b7 holds
b8 . (Var1 b5) = b8 . (Var2 b5) } ) & ( b5 is_membership implies b6 = { b7 where B is Element of VAL b2 : for b1 being Function of VAR ,b2 st b8 = b7 holds
b8 . (Var1 b5) in b8 . (Var2 b5) } ) & ( b5 is negative implies ex b7 being set st
( b6 = (VAL b2) \ (union {b7}) & [(the_argument_of b5),b7] in b4 ) ) & ( b5 is conjunctive implies ex b7, b8 being set st
( b6 = (union {b7}) /\ (union {b8}) & [(the_left_argument_of b5),b7] in b4 & [(the_right_argument_of b5),b8] in b4 ) ) & ( b5 is universal implies ex b7 being set st
( b6 = { b8 where B is Element of VAL b2 : for b1 being set
for b2 being Function of VAR ,b2 st b9 = b7 & b10 = b8 holds
( b10 in b9 & ( for b3 being Function of VAR ,b2 st ( for b4 being Variable st b11 . b12 <> b10 . b12 holds
bound_in b5 = b12 ) holds
b11 in b9 ) ) } & [(the_scope_of b5),b7] in b4 ) ) ) ) ) );

E6: now
let c1 be ZF-formula;
let c2 be non empty set ;
deffunc H7( Variable, Variable) -> set = { b1 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b2 = b1 holds
b2 . a1 = b2 . a2 } ;
deffunc H8( Variable, Variable) -> set = { b1 where B is Element of VAL c2 : for b1 being Function of VAR ,c2 st b2 = b1 holds
b2 . a1 in b2 . a2 } ;
deffunc H9( set ) -> set = (VAL c2) \ (union {a1});
deffunc H10( set , set ) -> set = (union {a1}) /\ (union {a2});
deffunc H11( Variable, set ) -> set = { b1 where B is Element of VAL c2 : for b1 being set
for b2 being Function of VAR ,c2 st b2 = a2 & b3 = b1 holds
( b3 in b2 & ( for b3 being Function of VAR ,c2 st ( for b4 being Variable st b4 . b5 <> b3 . b5 holds
a1 = b5 ) holds
b4 in b2 ) ) } ;
deffunc H12( ZF-formula) -> set = St a1,c2;
E7: for b1 being ZF-formula
for b2 being set holds
( b2 = H12(b1) iff ex b3 being set st
( ( for b4, b5 being Variable holds
( [(b4 '=' b5),H7(b4,b5)] in b3 & [(b4 'in' b5),H8(b4,b5)] in b3 ) ) & [b1,b2] in b3 & ( for b4 being ZF-formula
for b5 being set st [b4,b5] in b3 holds
( ( b4 is_equality implies b5 = H7( Var1 b4, Var2 b4) ) & ( b4 is_membership implies b5 = H8( Var1 b4, Var2 b4) ) & ( b4 is negative implies ex b6 being set st
( b5 = H9(b6) & [(the_argument_of b4),b6] in b3 ) ) & ( b4 is conjunctive implies ex b6, b7 being set st
( b5 = H10(b6,b7) & [(the_left_argument_of b4),b6] in b3 & [(the_right_argument_of b4),b7] in b3 ) ) & ( b4 is universal implies ex b6 being set st
( b5 = H11( bound_in b4,b6) & [(the_scope_of b4),b6] in b3 ) ) ) ) ) ) by Def3;
thus ( ( c1 is_equality implies H12(c1) = H7( Var1 c1, Var2 c1) ) & ( c1 is_membership implies H12(c1) = H8( Var1 c1, Var2 c1) ) & ( c1 is negative implies H12(c1) = H9(H12( the_argument_of c1)) ) & ( c1 is conjunctive implies for b1, b2 being set st b1 = H12( the_left_argument_of c1) & b2 = H12( the_right_argument_of c1) holds
H12(c1) = H10(b1,b2) ) & ( c1 is universal implies H12(c1) = H11( bound_in c1,H12( the_scope_of c1)) ) ) from ZF_MODEL:sch 3(E7);
end;

definition
let c1 be ZF-formula;
let c2 be non empty set ;
redefine func St as St c1,c2 -> Subset of (VAL a2);
coherence
St c1,c2 is Subset of (VAL c2)
proof end;
end;

theorem Th2: :: ZF_MODEL:2
for b1 being non empty set
for b2, b3 being Variable
for b4 being Function of VAR ,b1 holds
( b4 . b2 = b4 . b3 iff b4 in St (b2 '=' b3),b1 )
proof end;

theorem Th3: :: ZF_MODEL:3
for b1 being non empty set
for b2, b3 being Variable
for b4 being Function of VAR ,b1 holds
( b4 . b2 in b4 . b3 iff b4 in St (b2 'in' b3),b1 )
proof end;

theorem Th4: :: ZF_MODEL:4
for b1 being non empty set
for b2 being ZF-formula
for b3 being Function of VAR ,b1 holds
( not b3 in St b2,b1 iff b3 in St ('not' b2),b1 )
proof end;

theorem Th5: :: ZF_MODEL:5
for b1 being non empty set
for b2, b3 being ZF-formula
for b4 being Function of VAR ,b1 holds
( ( b4 in St b2,b1 & b4 in St b3,b1 ) iff b4 in St (b2 '&' b3),b1 )
proof end;

theorem Th6: :: ZF_MODEL:6
for b1 being non empty set
for b2 being Variable
for b3 being ZF-formula
for b4 being Function of VAR ,b1 holds
( ( b4 in St b3,b1 & ( for b5 being Function of VAR ,b1 st ( for b6 being Variable st b5 . b6 <> b4 . b6 holds
b2 = b6 ) holds
b5 in St b3,b1 ) ) iff b4 in St (All b2,b3),b1 )
proof end;

theorem Th7: :: ZF_MODEL:7
for b1 being ZF-formula
for b2 being non empty set st b1 is_equality holds
for b3 being Function of VAR ,b2 holds
( b3 . (Var1 b1) = b3 . (Var2 b1) iff b3 in St b1,b2 )
proof end;

theorem Th8: :: ZF_MODEL:8
for b1 being ZF-formula
for b2 being non empty set st b1 is_membership holds
for b3 being Function of VAR ,b2 holds
( b3 . (Var1 b1) in b3 . (Var2 b1) iff b3 in St b1,b2 )
proof end;

theorem Th9: :: ZF_MODEL:9
for b1 being ZF-formula
for b2 being non empty set st b1 is negative holds
for b3 being Function of VAR ,b2 holds
( not b3 in St (the_argument_of b1),b2 iff b3 in St b1,b2 )
proof end;

theorem Th10: :: ZF_MODEL:10
for b1 being ZF-formula
for b2 being non empty set st b1 is conjunctive holds
for b3 being Function of VAR ,b2 holds
( ( b3 in St (the_left_argument_of b1),b2 & b3 in St (the_right_argument_of b1),b2 ) iff b3 in St b1,b2 )
proof end;

theorem Th11: :: ZF_MODEL:11
for b1 being ZF-formula
for b2 being non empty set st b1 is universal holds
for b3 being Function of VAR ,b2 holds
( ( b3 in St (the_scope_of b1),b2 & ( for b4 being Function of VAR ,b2 st ( for b5 being Variable st b4 . b5 <> b3 . b5 holds
bound_in b1 = b5 ) holds
b4 in St (the_scope_of b1),b2 ) ) iff b3 in St b1,b2 )
proof end;

definition
let c1 be non empty set ;
let c2 be Function of VAR ,c1;
let c3 be ZF-formula;
pred c1,c2 |= c3 means :Def4: :: ZF_MODEL:def 4
a2 in St a3,a1;
end;

:: deftheorem Def4 defines |= ZF_MODEL:def 4 :
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being ZF-formula holds
( b1,b2 |= b3 iff b2 in St b3,b1 );

theorem Th12: :: ZF_MODEL:12
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3, b4 being Variable holds
( b1,b2 |= b3 '=' b4 iff b2 . b3 = b2 . b4 )
proof end;

theorem Th13: :: ZF_MODEL:13
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3, b4 being Variable holds
( b1,b2 |= b3 'in' b4 iff b2 . b3 in b2 . b4 )
proof end;

theorem Th14: :: ZF_MODEL:14
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being ZF-formula holds
( b1,b2 |= b3 iff not b1,b2 |= 'not' b3 )
proof end;

theorem Th15: :: ZF_MODEL:15
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3, b4 being ZF-formula holds
( b1,b2 |= b3 '&' b4 iff ( b1,b2 |= b3 & b1,b2 |= b4 ) )
proof end;

theorem Th16: :: ZF_MODEL:16
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being ZF-formula
for b4 being Variable holds
( b1,b2 |= All b4,b3 iff for b5 being Function of VAR ,b1 st ( for b6 being Variable st b5 . b6 <> b2 . b6 holds
b4 = b6 ) holds
b1,b5 |= b3 )
proof end;

theorem Th17: :: ZF_MODEL:17
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3, b4 being ZF-formula holds
( b1,b2 |= b3 'or' b4 iff ( b1,b2 |= b3 or b1,b2 |= b4 ) )
proof end;

theorem Th18: :: ZF_MODEL:18
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3, b4 being ZF-formula holds
( b1,b2 |= b3 => b4 iff ( b1,b2 |= b3 implies b1,b2 |= b4 ) )
proof end;

theorem Th19: :: ZF_MODEL:19
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3, b4 being ZF-formula holds
( b1,b2 |= b3 <=> b4 iff ( b1,b2 |= b3 iff b1,b2 |= b4 ) )
proof end;

theorem Th20: :: ZF_MODEL:20
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being ZF-formula
for b4 being Variable holds
( b1,b2 |= Ex b4,b3 iff ex b5 being Function of VAR ,b1 st
( ( for b6 being Variable st b5 . b6 <> b2 . b6 holds
b4 = b6 ) & b1,b5 |= b3 ) )
proof end;

theorem Th21: :: ZF_MODEL:21
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being Variable
for b4 being Element of b1 ex b5 being Function of VAR ,b1 st
( b5 . b3 = b4 & ( for b6 being Variable st b6 <> b3 holds
b5 . b6 = b2 . b6 ) )
proof end;

theorem Th22: :: ZF_MODEL:22
for b1 being ZF-formula
for b2, b3 being Variable
for b4 being non empty set
for b5 being Function of VAR ,b4 holds
( b4,b5 |= All b2,b3,b1 iff for b6 being Function of VAR ,b4 st ( for b7 being Variable holds
( not b6 . b7 <> b5 . b7 or b2 = b7 or b3 = b7 ) ) holds
b4,b6 |= b1 )
proof end;

theorem Th23: :: ZF_MODEL:23
for b1 being ZF-formula
for b2, b3 being Variable
for b4 being non empty set
for b5 being Function of VAR ,b4 holds
( b4,b5 |= Ex b2,b3,b1 iff ex b6 being Function of VAR ,b4 st
( ( for b7 being Variable holds
( not b6 . b7 <> b5 . b7 or b2 = b7 or b3 = b7 ) ) & b4,b6 |= b1 ) )
proof end;

definition
let c1 be non empty set ;
let c2 be ZF-formula;
pred c1 |= c2 means :Def5: :: ZF_MODEL:def 5
for b1 being Function of VAR ,a1 holds a1,b1 |= a2;
end;

:: deftheorem Def5 defines |= ZF_MODEL:def 5 :
for b1 being non empty set
for b2 being ZF-formula holds
( b1 |= b2 iff for b3 being Function of VAR ,b1 holds b1,b3 |= b2 );

theorem Th24: :: ZF_MODEL:24
canceled;

theorem Th25: :: ZF_MODEL:25
for b1 being ZF-formula
for b2 being Variable
for b3 being non empty set holds
( b3 |= All b2,b1 iff b3 |= b1 )
proof end;

definition
func the_axiom_of_extensionality -> ZF-formula equals :: ZF_MODEL:def 6
 All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1)));
correctness
coherence
All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1))) is ZF-formula;
;
func the_axiom_of_pairs -> ZF-formula equals :: ZF_MODEL:def 7
 All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))));
correctness
coherence
All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1)))))) is ZF-formula;
;
func the_axiom_of_unions -> ZF-formula equals :: ZF_MODEL:def 8
 All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))));
correctness
coherence
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0))))))) is ZF-formula;
;
func the_axiom_of_infinity -> ZF-formula equals :: ZF_MODEL:def 9
 Ex (x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All (x. 2),(((x. 2) 'in' (x. 0)) => (Ex (x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))));
correctness
coherence
Ex (x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All (x. 2),(((x. 2) 'in' (x. 0)) => (Ex (x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3))))))))) is ZF-formula;
;
func the_axiom_of_power_sets -> ZF-formula equals :: ZF_MODEL:def 10
 All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))));
correctness
coherence
All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0))))))) is ZF-formula;
;
end;

:: deftheorem Def6 defines the_axiom_of_extensionality ZF_MODEL:def 6 :
the_axiom_of_extensionality = All (x. 0),(x. 1),((All (x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1)))) => ((x. 0) '=' (x. 1)));

:: deftheorem Def7 defines the_axiom_of_pairs ZF_MODEL:def 7 :
the_axiom_of_pairs = All (x. 0),(x. 1),(Ex (x. 2),(All (x. 3),(((x. 3) 'in' (x. 2)) <=> (((x. 3) '=' (x. 0)) 'or' ((x. 3) '=' (x. 1))))));

:: deftheorem Def8 defines the_axiom_of_unions ZF_MODEL:def 8 :
the_axiom_of_unions = All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (Ex (x. 3),(((x. 2) 'in' (x. 3)) '&' ((x. 3) 'in' (x. 0)))))));

:: deftheorem Def9 defines the_axiom_of_infinity ZF_MODEL:def 9 :
the_axiom_of_infinity = Ex (x. 0),(x. 1),(((x. 1) 'in' (x. 0)) '&' (All (x. 2),(((x. 2) 'in' (x. 0)) => (Ex (x. 3),((((x. 3) 'in' (x. 0)) '&' ('not' ((x. 3) '=' (x. 2)))) '&' (All (x. 4),(((x. 4) 'in' (x. 2)) => ((x. 4) 'in' (x. 3)))))))));

:: deftheorem Def10 defines the_axiom_of_power_sets ZF_MODEL:def 10 :
the_axiom_of_power_sets = All (x. 0),(Ex (x. 1),(All (x. 2),(((x. 2) 'in' (x. 1)) <=> (All (x. 3),(((x. 3) 'in' (x. 2)) => ((x. 3) 'in' (x. 0)))))));

definition
let c1 be ZF-formula;
func the_axiom_of_substitution_for c1 -> ZF-formula equals :: ZF_MODEL:def 11
(All (x. 3),(Ex (x. 0),(All (x. 4),(a1 <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' a1))))));
correctness
coherence
(All (x. 3),(Ex (x. 0),(All (x. 4),(c1 <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' c1)))))) is ZF-formula;
;
end;

:: deftheorem Def11 defines the_axiom_of_substitution_for ZF_MODEL:def 11 :
for b1 being ZF-formula holds the_axiom_of_substitution_for b1 = (All (x. 3),(Ex (x. 0),(All (x. 4),(b1 <=> ((x. 4) '=' (x. 0)))))) => (All (x. 1),(Ex (x. 2),(All (x. 4),(((x. 4) 'in' (x. 2)) <=> (Ex (x. 3),(((x. 3) 'in' (x. 1)) '&' b1))))));

definition
let c1 be non empty set ;
attr a1 is being_a_model_of_ZF means :: ZF_MODEL:def 12
( a1 is epsilon-transitive & a1 |= the_axiom_of_pairs & a1 |= the_axiom_of_unions & a1 |= the_axiom_of_infinity & a1 |= the_axiom_of_power_sets & ( for b1 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free b1 holds
a1 |= the_axiom_of_substitution_for b1 ) );
end;

:: deftheorem Def12 defines being_a_model_of_ZF ZF_MODEL:def 12 :
for b1 being non empty set holds
( b1 is being_a_model_of_ZF iff ( b1 is epsilon-transitive & b1 |= the_axiom_of_pairs & b1 |= the_axiom_of_unions & b1 |= the_axiom_of_infinity & b1 |= the_axiom_of_power_sets & ( for b2 being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free b2 holds
b1 |= the_axiom_of_substitution_for b2 ) ) );

notation
let c1 be non empty set ;
synonym c1 is_a_model_of_ZF for being_a_model_of_ZF c1;
end;