begin
scheme
ZFschex{
F1(
Variable,
Variable)
-> set ,
F2(
Variable,
Variable)
-> set ,
F3(
set )
-> set ,
F4(
set ,
set )
-> set ,
F5(
Variable,
set )
-> set ,
F6()
-> ZF-formula } :
ex
a,
A being
set st
( ( for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in A &
[(x 'in' y),F2(x,y)] in A ) ) &
[F6(),a] in A & ( for
H being
ZF-formula for
a being
set st
[H,a] in A holds
( (
H is
being_equality implies
a = F1(
(Var1 H),
(Var2 H)) ) & (
H is
being_membership implies
a = F2(
(Var1 H),
(Var2 H)) ) & (
H is
negative implies ex
b being
set st
(
a = F3(
b) &
[(the_argument_of H),b] in A ) ) & (
H is
conjunctive implies ex
b,
c being
set st
(
a = F4(
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 = F5(
(bound_in H),
b) &
[(the_scope_of H),b] in A ) ) ) ) )
scheme
ZFschuniq{
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 } :
provided
A1:
ex
A being
set st
( ( for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in A &
[(x 'in' y),F2(x,y)] in A ) ) &
[F6(),F7()] in A & ( for
H being
ZF-formula for
a being
set st
[H,a] in A holds
( (
H is
being_equality implies
a = F1(
(Var1 H),
(Var2 H)) ) & (
H is
being_membership implies
a = F2(
(Var1 H),
(Var2 H)) ) & (
H is
negative implies ex
b being
set st
(
a = F3(
b) &
[(the_argument_of H),b] in A ) ) & (
H is
conjunctive implies ex
b,
c being
set st
(
a = F4(
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 = F5(
(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),F1(x,y)] in A &
[(x 'in' y),F2(x,y)] in A ) ) &
[F6(),F8()] in A & ( for
H being
ZF-formula for
a being
set st
[H,a] in A holds
( (
H is
being_equality implies
a = F1(
(Var1 H),
(Var2 H)) ) & (
H is
being_membership implies
a = F2(
(Var1 H),
(Var2 H)) ) & (
H is
negative implies ex
b being
set st
(
a = F3(
b) &
[(the_argument_of H),b] in A ) ) & (
H is
conjunctive implies ex
b,
c being
set st
(
a = F4(
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 = F5(
(bound_in H),
b) &
[(the_scope_of H),b] in A ) ) ) ) )
scheme
ZFschresult{
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 } :
provided
A1:
for
H9 being
ZF-formula for
a being
set holds
(
a = F7(
H9) iff ex
A being
set st
( ( for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in A &
[(x 'in' y),F2(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 = F1(
(Var1 H),
(Var2 H)) ) & (
H is
being_membership implies
a = F2(
(Var1 H),
(Var2 H)) ) & (
H is
negative implies ex
b being
set st
(
a = F3(
b) &
[(the_argument_of H),b] in A ) ) & (
H is
conjunctive implies ex
b,
c being
set st
(
a = F4(
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 = F5(
(bound_in H),
b) &
[(the_scope_of H),b] in A ) ) ) ) ) )
scheme
ZFschproperty{
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 ] } :
provided
A1:
for
H9 being
ZF-formula for
a being
set holds
(
a = F6(
H9) iff ex
A being
set st
( ( for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in A &
[(x 'in' y),F2(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 = F1(
(Var1 H),
(Var2 H)) ) & (
H is
being_membership implies
a = F2(
(Var1 H),
(Var2 H)) ) & (
H is
negative implies ex
b being
set st
(
a = F3(
b) &
[(the_argument_of H),b] in A ) ) & (
H is
conjunctive implies ex
b,
c being
set st
(
a = F4(
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 = F5(
(bound_in H),
b) &
[(the_scope_of H),b] in A ) ) ) ) ) )
and A2:
for
x,
y being
Variable holds
(
P1[
F1(
x,
y)] &
P1[
F2(
x,
y)] )
and A3:
for
a being
set st
P1[
a] holds
P1[
F3(
a)]
and A4:
for
a,
b being
set st
P1[
a] &
P1[
b] holds
P1[
F4(
a,
b)]
and A5:
for
a being
set for
x being
Variable st
P1[
a] holds
P1[
F5(
x,
a)]
deffunc H1( Variable, Variable) -> set = {$1,$2};
deffunc H2( Variable, Variable) -> set = {$1,$2};
deffunc H3( set ) -> set = $1;
deffunc H4( set , set ) -> set = union {$1,$2};
deffunc H5( Variable, set ) -> Element of K27((union {$2})) = (union {$2}) \ {$1};
definition
let H be
ZF-formula;
func Free H -> set means :
Def1:
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 = (union {b}) \ {(bound_in H9)} &
[(the_scope_of H9),b] in A ) ) ) ) );
existence
ex b1, A being set st
( ( for x, y being Variable holds
( [(x '=' y),{x,y}] in A & [(x 'in' y),{x,y}] in A ) ) & [H,b1] 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 = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) )
uniqueness
for b1, b2 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,b1] 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 = (union {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,b2] 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 = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) holds
b1 = b2
end;
::
deftheorem Def1 defines
Free ZF_MODEL:def 1 :
for H being ZF-formula
for b2 being set holds
( b2 = 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,b2] 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 = (union {b}) \ {(bound_in H9)} & [(the_scope_of H9),b] in A ) ) ) ) ) );
deffunc H6( ZF-formula) -> set = Free $1;
Lm1:
for H being ZF-formula
for a1 being set holds
( a1 = H6(H) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H1(x,y)] in A & [(x 'in' y),H2(x,y)] in A ) ) & [H,a1] in A & ( for H9 being ZF-formula
for a being set st [H9,a] in A holds
( ( H9 is being_equality implies a = H1( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H2( Var1 H9, Var2 H9) ) & ( H9 is negative implies ex b being set st
( a = H3(b) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = H4(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 = H5( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) )
by Def1;
Lm2:
now for H being ZF-formula holds
( ( H is being_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is being_membership implies H6(H) = H2( Var1 H, Var2 H) ) & ( H is negative implies H6(H) = H3(H6( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H6( the_left_argument_of H) & b = H6( the_right_argument_of H) holds
H6(H) = H4(a,b) ) & ( H is universal implies H6(H) = H5( bound_in H,H6( the_scope_of H)) ) )
let H be
ZF-formula;
( ( H is being_equality implies H6(H) = H1( Var1 H, Var2 H) ) & ( H is being_membership implies H6(H) = H2( Var1 H, Var2 H) ) & ( H is negative implies H6(H) = H3(H6( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H6( the_left_argument_of H) & b = H6( the_right_argument_of H) holds
H6(H) = H4(a,b) ) & ( H is universal implies H6(H) = H5( bound_in H,H6( the_scope_of H)) ) )thus
( (
H is
being_equality implies
H6(
H)
= H1(
Var1 H,
Var2 H) ) & (
H is
being_membership implies
H6(
H)
= H2(
Var1 H,
Var2 H) ) & (
H is
negative implies
H6(
H)
= H3(
H6(
the_argument_of H)) ) & (
H is
conjunctive implies for
a,
b being
set st
a = H6(
the_left_argument_of H) &
b = H6(
the_right_argument_of H) holds
H6(
H)
= H4(
a,
b) ) & (
H is
universal implies
H6(
H)
= H5(
bound_in H,
H6(
the_scope_of H)) ) )
from ZF_MODEL:sch 3(Lm1); verum
end;
definition
deffunc H7(
set ,
set )
-> set =
(union {$1}) /\ (union {$2});
let H be
ZF-formula;
let E be non
empty set ;
deffunc H8(
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 H9(
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 H10(
set )
-> Element of
K27(
(VAL E)) =
(VAL E) \ (union {$1});
deffunc H11(
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 ) ) } ;
func St (
H,
E)
-> set means :
Def3:
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) \ (union {b}) &
[(the_argument_of H9),b] in A ) ) & (
H9 is
conjunctive implies ex
b,
c being
set st
(
a = (union {b}) /\ (union {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 b1, 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,b1] 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) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {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 ) ) ) ) )
uniqueness
for b1, b2 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,b1] 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) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {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,b2] 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) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {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
b1 = b2
end;
::
deftheorem Def3 defines
St ZF_MODEL:def 3 :
for H being ZF-formula
for E being non empty set
for b3 being set holds
( b3 = 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,b3] 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) \ (union {b}) & [(the_argument_of H9),b] in A ) ) & ( H9 is conjunctive implies ex b, c being set st
( a = (union {b}) /\ (union {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 for H being ZF-formula
for E being non empty set holds
( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds
H12(H) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) )
deffunc H7(
set ,
set )
-> set =
(union {$1}) /\ (union {$2});
let H be
ZF-formula;
for E being non empty set holds
( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds
H12(H) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) )let E be non
empty set ;
( ( H is being_equality implies H12(H) = H8( Var1 H, Var2 H) ) & ( H is being_membership implies H12(H) = H9( Var1 H, Var2 H) ) & ( H is negative implies H12(H) = H10(H12( the_argument_of H)) ) & ( H is conjunctive implies for a, b being set st a = H12( the_left_argument_of H) & b = H12( the_right_argument_of H) holds
H12(H) = H7(a,b) ) & ( H is universal implies H12(H) = H11( bound_in H,H12( the_scope_of H)) ) )deffunc H8(
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 H9(
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 H10(
set )
-> Element of
K27(
(VAL E)) =
(VAL E) \ (union {$1});
deffunc H11(
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 H12(
ZF-formula)
-> set =
St ($1,
E);
A1:
for
H being
ZF-formula for
a being
set holds
(
a = H12(
H) iff ex
A being
set st
( ( for
x,
y being
Variable holds
(
[(x '=' y),H8(x,y)] in A &
[(x 'in' y),H9(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 = H8(
Var1 H9,
Var2 H9) ) & (
H9 is
being_membership implies
a = H9(
Var1 H9,
Var2 H9) ) & (
H9 is
negative implies ex
b being
set st
(
a = H10(
b) &
[(the_argument_of H9),b] in A ) ) & (
H9 is
conjunctive implies ex
b,
c being
set st
(
a = H7(
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 = H11(
bound_in H9,
b) &
[(the_scope_of H9),b] in A ) ) ) ) ) )
by Def3;
thus
( (
H is
being_equality implies
H12(
H)
= H8(
Var1 H,
Var2 H) ) & (
H is
being_membership implies
H12(
H)
= H9(
Var1 H,
Var2 H) ) & (
H is
negative implies
H12(
H)
= H10(
H12(
the_argument_of H)) ) & (
H is
conjunctive implies for
a,
b being
set st
a = H12(
the_left_argument_of H) &
b = H12(
the_right_argument_of H) holds
H12(
H)
= H7(
a,
b) ) & (
H is
universal implies
H12(
H)
= H11(
bound_in H,
H12(
the_scope_of H)) ) )
from ZF_MODEL:sch 3(A1); verum
end;
definition
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;
;
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;
;
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;
;
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;
;
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;