:: by Grzegorz Bancerek

::

:: Received April 14, 1989

:: Copyright (c) 1990-2016 Association of Mizar Users

scheme :: ZF_MODEL:sch 1

ZFschex{ F_{1}( Variable, Variable) -> set , F_{2}( Variable, Variable) -> set , F_{3}( set ) -> set , F_{4}( set , set ) -> set , F_{5}( Variable, set ) -> set , F_{6}() -> ZF-formula } :

ZFschex{ F

ex a, A being set st

( ( for x, y being Variable holds

( [(x '=' y),F_{1}(x,y)] in A & [(x 'in' y),F_{2}(x,y)] in A ) ) & [F_{6}(),a] in A & ( for H being ZF-formula

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F_{1}((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F_{2}((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st

( a = F_{3}(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st

( a = F_{4}(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st

( a = F_{5}((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) )

( ( for x, y being Variable holds

( [(x '=' y),F

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F

( a = F

( a = F

( a = F

proof end;

scheme :: ZF_MODEL:sch 2

ZFschuniq{ F_{1}( Variable, Variable) -> set , F_{2}( Variable, Variable) -> set , F_{3}( set ) -> set , F_{4}( set , set ) -> set , F_{5}( Variable, set ) -> set , F_{6}() -> ZF-formula, F_{7}() -> set , F_{8}() -> set } :

provided

ZFschuniq{ F

provided

A1:
ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),F_{1}(x,y)] in A & [(x 'in' y),F_{2}(x,y)] in A ) ) & [F_{6}(),F_{7}()] in A & ( for H being ZF-formula

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F_{1}((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F_{2}((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st

( a = F_{3}(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st

( a = F_{4}(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st

( a = F_{5}((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) )
and

A2: ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),F_{1}(x,y)] in A & [(x 'in' y),F_{2}(x,y)] in A ) ) & [F_{6}(),F_{8}()] in A & ( for H being ZF-formula

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F_{1}((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F_{2}((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st

( a = F_{3}(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st

( a = F_{4}(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st

( a = F_{5}((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) )

( ( for x, y being Variable holds

( [(x '=' y),F

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F

( a = F

( a = F

( a = F

A2: ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),F

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F

( a = F

( a = F

( a = F

proof end;

scheme :: ZF_MODEL:sch 3

ZFschresult{ F_{1}( Variable, Variable) -> set , F_{2}( Variable, Variable) -> set , F_{3}( set ) -> set , F_{4}( set , set ) -> set , F_{5}( Variable, set ) -> set , F_{6}() -> ZF-formula, F_{7}( ZF-formula) -> set } :

ZFschresult{ F

( ( F_{6}() is being_equality implies F_{7}(F_{6}()) = F_{1}((Var1 F_{6}()),(Var2 F_{6}())) ) & ( F_{6}() is being_membership implies F_{7}(F_{6}()) = F_{2}((Var1 F_{6}()),(Var2 F_{6}())) ) & ( F_{6}() is negative implies F_{7}(F_{6}()) = F_{3}(F_{7}((the_argument_of F_{6}()))) ) & ( F_{6}() is conjunctive implies for a, b being set st a = F_{7}((the_left_argument_of F_{6}())) & b = F_{7}((the_right_argument_of F_{6}())) holds

F_{7}(F_{6}()) = F_{4}(a,b) ) & ( F_{6}() is universal implies F_{7}(F_{6}()) = F_{5}((bound_in F_{6}()),F_{7}((the_scope_of F_{6}()))) ) )

providedF

A1:
for H9 being ZF-formula

for a being set holds

( a = F_{7}(H9) iff ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),F_{1}(x,y)] in A & [(x 'in' y),F_{2}(x,y)] in A ) ) & [H9,a] in A & ( for H being ZF-formula

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F_{1}((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F_{2}((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st

( a = F_{3}(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st

( a = F_{4}(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st

( a = F_{5}((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) )

for a being set holds

( a = F

( ( for x, y being Variable holds

( [(x '=' y),F

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F

( a = F

( a = F

( a = F

proof end;

scheme :: ZF_MODEL:sch 4

ZFschproperty{ F_{1}( Variable, Variable) -> set , F_{2}( Variable, Variable) -> set , F_{3}( set ) -> set , F_{4}( set , set ) -> set , F_{5}( Variable, set ) -> set , F_{6}( ZF-formula) -> set , F_{7}() -> ZF-formula, P_{1}[ set ] } :

provided

ZFschproperty{ F

provided

A1:
for H9 being ZF-formula

for a being set holds

( a = F_{6}(H9) iff ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),F_{1}(x,y)] in A & [(x 'in' y),F_{2}(x,y)] in A ) ) & [H9,a] in A & ( for H being ZF-formula

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F_{1}((Var1 H),(Var2 H)) ) & ( H is being_membership implies a = F_{2}((Var1 H),(Var2 H)) ) & ( H is negative implies ex b being set st

( a = F_{3}(b) & [(the_argument_of H),b] in A ) ) & ( H is conjunctive implies ex b, c being set st

( a = F_{4}(b,c) & [(the_left_argument_of H),b] in A & [(the_right_argument_of H),c] in A ) ) & ( H is universal implies ex b being set st

( a = F_{5}((bound_in H),b) & [(the_scope_of H),b] in A ) ) ) ) ) )
and

A2: for x, y being Variable holds

( P_{1}[F_{1}(x,y)] & P_{1}[F_{2}(x,y)] )
and

A3: for a being set st P_{1}[a] holds

P_{1}[F_{3}(a)]
and

A4: for a, b being set st P_{1}[a] & P_{1}[b] holds

P_{1}[F_{4}(a,b)]
and

A5: for a being set

for x being Variable st P_{1}[a] holds

P_{1}[F_{5}(x,a)]

for a being set holds

( a = F

( ( for x, y being Variable holds

( [(x '=' y),F

for a being set st [H,a] in A holds

( ( H is being_equality implies a = F

( a = F

( a = F

( a = F

A2: for x, y being Variable holds

( P

A3: for a being set st P

P

A4: for a, b being set st P

P

A5: for a being set

for x being Variable st P

P

proof end;

deffunc H

deffunc H

deffunc H

deffunc H

deffunc H

definition

let H be ZF-formula;

ex b_{1}, A being set st

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b_{1}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) )

for b_{1}, b_{2} being set st ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b_{1}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b_{2}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) holds

b_{1} = b_{2}

end;
func Free H -> set means :Def1: :: ZF_MODEL:def 1

ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,it] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) );

existence ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,it] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) );

ex b

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) )

proof end;

uniqueness for b

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) holds

b

proof end;

:: deftheorem Def1 defines Free ZF_MODEL:def 1 :

for H being ZF-formula

for b_{2} being set holds

( b_{2} = Free H iff ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b_{2}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) );

for H being ZF-formula

for b

( b

( ( for x, y being Variable holds

( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is being_membership implies a = {(Var1 H9),(Var2 H9)} ) & ( H9 is negative implies ex b being set st

( a = b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = union {b,c} & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = b \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) );

deffunc H

Lm1: for H being ZF-formula

for a1 being set holds

( a1 = H

( ( for x, y being Variable holds

( [(x '=' y),H

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = H

( a = H

( a = H

( a = H

by Def1;

Lm2: now :: thesis: for H being ZF-formula holds

( ( H is being_equality implies H_{6}(H) = H_{1}( Var1 H, Var2 H) ) & ( H is being_membership implies H_{6}(H) = H_{2}( Var1 H, Var2 H) ) & ( H is negative implies H_{6}(H) = H_{3}(H_{6}( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H_{6}( the_left_argument_of H) & b = H_{6}( the_right_argument_of H) holds

H_{6}(H) = H_{4}(a,b) ) & ( H is universal implies H_{6}(H) = H_{5}( bound_in H,H_{6}( the_scope_of H)) ) )

( ( H is being_equality implies H

H

let H be ZF-formula; :: thesis: ( ( H is being_equality implies H_{6}(H) = H_{1}( Var1 H, Var2 H) ) & ( H is being_membership implies H_{6}(H) = H_{2}( Var1 H, Var2 H) ) & ( H is negative implies H_{6}(H) = H_{3}(H_{6}( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H_{6}( the_left_argument_of H) & b = H_{6}( the_right_argument_of H) holds

H_{6}(H) = H_{4}(a,b) ) & ( H is universal implies H_{6}(H) = H_{5}( bound_in H,H_{6}( the_scope_of H)) ) )

thus ( ( H is being_equality implies H_{6}(H) = H_{1}( Var1 H, Var2 H) ) & ( H is being_membership implies H_{6}(H) = H_{2}( Var1 H, Var2 H) ) & ( H is negative implies H_{6}(H) = H_{3}(H_{6}( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H_{6}( the_left_argument_of H) & b = H_{6}( the_right_argument_of H) holds

H_{6}(H) = H_{4}(a,b) ) & ( H is universal implies H_{6}(H) = H_{5}( bound_in H,H_{6}( the_scope_of H)) ) )
from ZF_MODEL:sch 3(Lm1); :: thesis: verum

end;
H

thus ( ( H is being_equality implies H

H

definition

let H be ZF-formula;

:: original: Free

redefine func Free H -> Subset of VAR;

coherence

Free H is Subset of VAR

end;
:: original: Free

redefine func Free H -> Subset of VAR;

coherence

Free H is Subset of VAR

proof end;

theorem :: ZF_MODEL:1

for H being ZF-formula holds

( ( H is being_equality implies Free H = {(Var1 H),(Var2 H)} ) & ( H is being_membership implies Free H = {(Var1 H),(Var2 H)} ) & ( H is negative implies Free H = Free (the_argument_of H) ) & ( H is conjunctive implies Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) ) & ( H is universal implies Free H = (Free (the_scope_of H)) \ {(bound_in H)} ) )

( ( H is being_equality implies Free H = {(Var1 H),(Var2 H)} ) & ( H is being_membership implies Free H = {(Var1 H),(Var2 H)} ) & ( H is negative implies Free H = Free (the_argument_of H) ) & ( H is conjunctive implies Free H = (Free (the_left_argument_of H)) \/ (Free (the_right_argument_of H)) ) & ( H is universal implies Free H = (Free (the_scope_of H)) \ {(bound_in H)} ) )

proof end;

:: The set of all valuations of variables in a model

registration
end;

:: The set of all valuations which satisfy a ZF-formula in a model

definition

deffunc H_{7}( set , set ) -> set = $1 /\ $2;

let H be ZF-formula;

let E be non empty set ;

deffunc H_{8}( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . $1 = f . $2 } ;

deffunc H_{9}( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . $1 in f . $2 } ;

deffunc H_{10}( set ) -> Element of K27((VAL E)) = (VAL E) \ $1;

deffunc H_{11}( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = $2 & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

$1 = y ) holds

g in X ) ) } ;

ex b_{1}, A being set st

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b_{1}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) )

for b_{1}, b_{2} being set st ex A being set st

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b_{1}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b_{2}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) holds

b_{1} = b_{2}

end;
let H be ZF-formula;

let E be non empty set ;

deffunc H

f . $1 = f . $2 } ;

deffunc H

f . $1 in f . $2 } ;

deffunc H

deffunc H

for f being Function of VAR,E st X = $2 & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

$1 = y ) holds

g in X ) ) } ;

func St (H,E) -> set means :Def3: :: ZF_MODEL:def 3

ex A being set st

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,it] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) );

existence ex A being set st

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,it] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) );

ex b

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) )

proof end;

uniqueness for b

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) & ex A being set st

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) holds

b

proof end;

:: deftheorem Def3 defines St ZF_MODEL:def 3 :

for H being ZF-formula

for E being non empty set

for b_{3} being set holds

( b_{3} = St (H,E) iff ex A being set st

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b_{3}] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) );

for H being ZF-formula

for E being non empty set

for b

( b

( ( for x, y being Variable holds

( [(x '=' y), { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds

f . x = f . y } ] in A & [(x 'in' y), { v2 where v2 is Element of VAL E : for f being Function of VAR,E st f = v2 holds

f . x in f . y } ] in A ) ) & [H,b

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . (Var1 H9) = f . (Var2 H9) } ) & ( H9 is being_membership implies a = { v4 where v4 is Element of VAL E : for f being Function of VAR,E st f = v4 holds

f . (Var1 H9) in f . (Var2 H9) } ) & ( H9 is negative implies ex b being set st

( a = (VAL E) \ b & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = b /\ c & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = b & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H9 = y ) holds

g in X ) ) } & [(the_scope_of H9),b] in A ) ) ) ) ) );

Lm3: now :: thesis: for H being ZF-formula

for E being non empty set holds

( ( H is being_equality implies H_{12}(H) = H_{8}( Var1 H, Var2 H) ) & ( H is being_membership implies H_{12}(H) = H_{9}( Var1 H, Var2 H) ) & ( H is negative implies H_{12}(H) = H_{10}(H_{12}( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H_{12}( the_left_argument_of H) & b = H_{12}( the_right_argument_of H) holds

H_{12}(H) = H_{7}(a,b) ) & ( H is universal implies H_{12}(H) = H_{11}( bound_in H,H_{12}( the_scope_of H)) ) )

for E being non empty set holds

( ( H is being_equality implies H

H

deffunc H_{7}( set , set ) -> set = $1 /\ $2;

let H be ZF-formula; :: thesis: for E being non empty set holds

( ( H is being_equality implies H_{12}(H) = H_{8}( Var1 H, Var2 H) ) & ( H is being_membership implies H_{12}(H) = H_{9}( Var1 H, Var2 H) ) & ( H is negative implies H_{12}(H) = H_{10}(H_{12}( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H_{12}( the_left_argument_of H) & b = H_{12}( the_right_argument_of H) holds

H_{12}(H) = H_{7}(a,b) ) & ( H is universal implies H_{12}(H) = H_{11}( bound_in H,H_{12}( the_scope_of H)) ) )

let E be non empty set ; :: thesis: ( ( H is being_equality implies H_{12}(H) = H_{8}( Var1 H, Var2 H) ) & ( H is being_membership implies H_{12}(H) = H_{9}( Var1 H, Var2 H) ) & ( H is negative implies H_{12}(H) = H_{10}(H_{12}( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H_{12}( the_left_argument_of H) & b = H_{12}( the_right_argument_of H) holds

H_{12}(H) = H_{7}(a,b) ) & ( H is universal implies H_{12}(H) = H_{11}( bound_in H,H_{12}( the_scope_of H)) ) )

deffunc H_{8}( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . $1 = f . $2 } ;

deffunc H_{9}( Variable, Variable) -> set = { v3 where v3 is Element of VAL E : for f being Function of VAR,E st f = v3 holds

f . $1 in f . $2 } ;

deffunc H_{10}( set ) -> Element of K27((VAL E)) = (VAL E) \ $1;

deffunc H_{11}( Variable, set ) -> set = { v5 where v5 is Element of VAL E : for X being set

for f being Function of VAR,E st X = $2 & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

$1 = y ) holds

g in X ) ) } ;

deffunc H_{12}( ZF-formula) -> set = St ($1,E);

A1: for H being ZF-formula

for a being set holds

( a = H_{12}(H) iff ex A being set st

( ( for x, y being Variable holds

( [(x '=' y),H_{8}(x,y)] in A & [(x 'in' y),H_{9}(x,y)] in A ) ) & [H,a] in A & ( for H9 being ZF-formula

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = H_{8}( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H_{9}( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st

( a = H_{10}(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st

( a = H_{7}(b,c) & [(the_left_argument_of H9),b] in A & [(the_right_argument_of H9),c] in A ) ) & ( H9 is universal implies ex b being set st

( a = H_{11}( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) )
by Def3;

thus ( ( H is being_equality implies H_{12}(H) = H_{8}( Var1 H, Var2 H) ) & ( H is being_membership implies H_{12}(H) = H_{9}( Var1 H, Var2 H) ) & ( H is negative implies H_{12}(H) = H_{10}(H_{12}( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H_{12}( the_left_argument_of H) & b = H_{12}( the_right_argument_of H) holds

H_{12}(H) = H_{7}(a,b) ) & ( H is universal implies H_{12}(H) = H_{11}( bound_in H,H_{12}( the_scope_of H)) ) )
from ZF_MODEL:sch 3(A1); :: thesis: verum

end;
let H be ZF-formula; :: thesis: for E being non empty set holds

( ( H is being_equality implies H

H

let E be non empty set ; :: thesis: ( ( H is being_equality implies H

H

deffunc H

f . $1 = f . $2 } ;

deffunc H

f . $1 in f . $2 } ;

deffunc H

deffunc H

for f being Function of VAR,E st X = $2 & f = v5 holds

( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

$1 = y ) holds

g in X ) ) } ;

deffunc H

A1: for H being ZF-formula

for a being set holds

( a = H

( ( for x, y being Variable holds

( [(x '=' y),H

for a being set st [H9,a] in A holds

( ( H9 is being_equality implies a = H

( a = H

( a = H

( a = H

thus ( ( H is being_equality implies H

H

definition

let H be ZF-formula;

let E be non empty set ;

:: original: St

redefine func St (H,E) -> Subset of (VAL E);

coherence

St (H,E) is Subset of (VAL E)

end;
let E be non empty set ;

:: original: St

redefine func St (H,E) -> Subset of (VAL E);

coherence

St (H,E) is Subset of (VAL E)

proof end;

theorem Th2: :: ZF_MODEL:2

for E being non empty set

for x, y being Variable

for f being Function of VAR,E holds

( f . x = f . y iff f in St ((x '=' y),E) )

for x, y being Variable

for f being Function of VAR,E holds

( f . x = f . y iff f in St ((x '=' y),E) )

proof end;

theorem Th3: :: ZF_MODEL:3

for E being non empty set

for x, y being Variable

for f being Function of VAR,E holds

( f . x in f . y iff f in St ((x 'in' y),E) )

for x, y being Variable

for f being Function of VAR,E holds

( f . x in f . y iff f in St ((x 'in' y),E) )

proof end;

theorem Th4: :: ZF_MODEL:4

for E being non empty set

for H being ZF-formula

for f being Function of VAR,E holds

( not f in St (H,E) iff f in St (('not' H),E) )

for H being ZF-formula

for f being Function of VAR,E holds

( not f in St (H,E) iff f in St (('not' H),E) )

proof end;

theorem Th5: :: ZF_MODEL:5

for E being non empty set

for H, H9 being ZF-formula

for f being Function of VAR,E holds

( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )

for H, H9 being ZF-formula

for f being Function of VAR,E holds

( ( f in St (H,E) & f in St (H9,E) ) iff f in St ((H '&' H9),E) )

proof end;

theorem Th6: :: ZF_MODEL:6

for E being non empty set

for x being Variable

for H being ZF-formula

for f being Function of VAR,E holds

( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

x = y ) holds

g in St (H,E) ) ) iff f in St ((All (x,H)),E) )

for x being Variable

for H being ZF-formula

for f being Function of VAR,E holds

( ( f in St (H,E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

x = y ) holds

g in St (H,E) ) ) iff f in St ((All (x,H)),E) )

proof end;

theorem :: ZF_MODEL:7

for H being ZF-formula

for E being non empty set st H is being_equality holds

for f being Function of VAR,E holds

( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) )

for E being non empty set st H is being_equality holds

for f being Function of VAR,E holds

( f . (Var1 H) = f . (Var2 H) iff f in St (H,E) )

proof end;

theorem :: ZF_MODEL:8

for H being ZF-formula

for E being non empty set st H is being_membership holds

for f being Function of VAR,E holds

( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) )

for E being non empty set st H is being_membership holds

for f being Function of VAR,E holds

( f . (Var1 H) in f . (Var2 H) iff f in St (H,E) )

proof end;

theorem :: ZF_MODEL:9

for H being ZF-formula

for E being non empty set st H is negative holds

for f being Function of VAR,E holds

( not f in St ((the_argument_of H),E) iff f in St (H,E) )

for E being non empty set st H is negative holds

for f being Function of VAR,E holds

( not f in St ((the_argument_of H),E) iff f in St (H,E) )

proof end;

theorem :: ZF_MODEL:10

for H being ZF-formula

for E being non empty set st H is conjunctive holds

for f being Function of VAR,E holds

( ( f in St ((the_left_argument_of H),E) & f in St ((the_right_argument_of H),E) ) iff f in St (H,E) )

for E being non empty set st H is conjunctive holds

for f being Function of VAR,E holds

( ( f in St ((the_left_argument_of H),E) & f in St ((the_right_argument_of H),E) ) iff f in St (H,E) )

proof end;

theorem :: ZF_MODEL:11

for H being ZF-formula

for E being non empty set st H is universal holds

for f being Function of VAR,E holds

( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H = y ) holds

g in St ((the_scope_of H),E) ) ) iff f in St (H,E) )

for E being non empty set st H is universal holds

for f being Function of VAR,E holds

( ( f in St ((the_scope_of H),E) & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

bound_in H = y ) holds

g in St ((the_scope_of H),E) ) ) iff f in St (H,E) )

proof end;

:: The satisfaction of a ZF-formula in a model by a valuation

:: deftheorem Def4 defines |= ZF_MODEL:def 4 :

for D being non empty set

for f being Function of VAR,D

for H being ZF-formula holds

( D,f |= H iff f in St (H,D) );

for D being non empty set

for f being Function of VAR,D

for H being ZF-formula holds

( D,f |= H iff f in St (H,D) );

theorem :: ZF_MODEL:12

theorem :: ZF_MODEL:13

theorem Th16: :: ZF_MODEL:16

for E being non empty set

for f being Function of VAR,E

for H being ZF-formula

for x being Variable holds

( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

x = y ) holds

E,g |= H )

for f being Function of VAR,E

for H being ZF-formula

for x being Variable holds

( E,f |= All (x,H) iff for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds

x = y ) holds

E,g |= H )

proof end;

theorem :: ZF_MODEL:17

for E being non empty set

for f being Function of VAR,E

for H, H9 being ZF-formula holds

( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) )

for f being Function of VAR,E

for H, H9 being ZF-formula holds

( E,f |= H 'or' H9 iff ( E,f |= H or E,f |= H9 ) )

proof end;

theorem Th18: :: ZF_MODEL:18

for E being non empty set

for f being Function of VAR,E

for H, H9 being ZF-formula holds

( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) )

for f being Function of VAR,E

for H, H9 being ZF-formula holds

( E,f |= H => H9 iff ( E,f |= H implies E,f |= H9 ) )

proof end;

theorem :: ZF_MODEL:19

for E being non empty set

for f being Function of VAR,E

for H, H9 being ZF-formula holds

( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) )

for f being Function of VAR,E

for H, H9 being ZF-formula holds

( E,f |= H <=> H9 iff ( E,f |= H iff E,f |= H9 ) )

proof end;

theorem Th20: :: ZF_MODEL:20

for E being non empty set

for f being Function of VAR,E

for H being ZF-formula

for x being Variable holds

( E,f |= Ex (x,H) iff ex g being Function of VAR,E st

( ( for y being Variable st g . y <> f . y holds

x = y ) & E,g |= H ) )

for f being Function of VAR,E

for H being ZF-formula

for x being Variable holds

( E,f |= Ex (x,H) iff ex g being Function of VAR,E st

( ( for y being Variable st g . y <> f . y holds

x = y ) & E,g |= H ) )

proof end;

theorem :: ZF_MODEL:21

for H being ZF-formula

for x, y being Variable

for E being non empty set

for f being Function of VAR,E holds

( E,f |= All (x,y,H) iff for g being Function of VAR,E st ( for z being Variable holds

( not g . z <> f . z or x = z or y = z ) ) holds

E,g |= H )

for x, y being Variable

for E being non empty set

for f being Function of VAR,E holds

( E,f |= All (x,y,H) iff for g being Function of VAR,E st ( for z being Variable holds

( not g . z <> f . z or x = z or y = z ) ) holds

E,g |= H )

proof end;

theorem :: ZF_MODEL:22

for H being ZF-formula

for x, y being Variable

for E being non empty set

for f being Function of VAR,E holds

( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st

( ( for z being Variable holds

( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )

for x, y being Variable

for E being non empty set

for f being Function of VAR,E holds

( E,f |= Ex (x,y,H) iff ex g being Function of VAR,E st

( ( for z being Variable holds

( not g . z <> f . z or x = z or y = z ) ) & E,g |= H ) )

proof end;

:: The satisfaction of a ZF-formula in a model

:: deftheorem defines |= ZF_MODEL:def 5 :

for E being non empty set

for H being ZF-formula holds

( E |= H iff for f being Function of VAR,E holds E,f |= H );

for E being non empty set

for H being ZF-formula holds

( E |= H iff for f being Function of VAR,E holds E,f |= H );

theorem :: ZF_MODEL:23

for H being ZF-formula

for x being Variable

for E being non empty set holds

( E |= All (x,H) iff E |= H )

for x being Variable

for E being non empty set holds

( E |= All (x,H) iff E |= H )

proof end;

:: The axioms of ZF-language

definition

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;

;

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;

;

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;

;

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;

;

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;

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 All ((x. 0),(x. 1),((All ((x. 2),(((x. 2) 'in' (x. 0)) <=> ((x. 2) 'in' (x. 1))))) => ((x. 0) '=' (x. 1))));

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

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

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

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

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;

;

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

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

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

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

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

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 H be ZF-formula;

coherence

(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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)) '&' H)))))))))) is ZF-formula;

;

end;
func the_axiom_of_substitution_for H -> ZF-formula equals :: ZF_MODEL:def 11

(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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)) '&' H))))))))));

correctness (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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)) '&' H))))))))));

coherence

(All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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)) '&' H)))))))))) is ZF-formula;

;

:: deftheorem defines the_axiom_of_substitution_for ZF_MODEL:def 11 :

for H being ZF-formula holds the_axiom_of_substitution_for H = (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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)) '&' H))))))))));

for H being ZF-formula holds the_axiom_of_substitution_for H = (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((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)) '&' H))))))))));

definition

let E be non empty set ;

end;
attr E is being_a_model_of_ZF means :: ZF_MODEL:def 12

( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) );

( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) );

:: deftheorem defines being_a_model_of_ZF ZF_MODEL:def 12 :

for E being non empty set holds

( E is being_a_model_of_ZF iff ( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) ) );

for E being non empty set holds

( E is being_a_model_of_ZF iff ( E is epsilon-transitive & E |= the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E |= the_axiom_of_power_sets & ( for H being ZF-formula st {(x. 0),(x. 1),(x. 2)} misses Free H holds

E |= the_axiom_of_substitution_for H ) ) );