defpred S1[ set ] means $1 is Subset of (VAL E);
deffunc H7( ZF-formula) -> set = St ($1,E);
deffunc H8( 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 H9( set , set ) -> set = $1 /\ $2;
deffunc H10( set ) -> Element of K27((VAL E)) = (VAL E) \ $1;
deffunc H11( 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 H12( 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 } ;
A1: for b being set st S1[b] holds
S1[H10(b)] ;
A2: for X, Y being set st S1[X] & S1[Y] holds
S1[H9(X,Y)]
proof
let X, Y be set ; :: thesis: ( S1[X] & S1[Y] implies S1[H9(X,Y)] )
assume that
A3: X is Subset of (VAL E) and
Y is Subset of (VAL E) ; :: thesis: S1[H9(X,Y)]
reconsider X = X as Subset of (VAL E) by A3;
X /\ Y c= VAL E ;
hence S1[H9(X,Y)] ; :: thesis: verum
end;
now :: thesis: for x, y being Variable holds
( { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) & { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) )
let x, y be Variable; :: thesis: ( { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) & { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) )
set X1 = { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } ;
set X2 = { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } ;
{ v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } c= VAL E
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } or a in VAL E )
assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } ; :: thesis: a in VAL E
then ex v1 being Element of VAL E st
( a = v1 & ( for f being Function of VAR,E st f = v1 holds
f . x = f . y ) ) ;
hence a in VAL E ; :: thesis: verum
end;
hence { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x = f . y } is Subset of (VAL E) ; :: thesis: { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E)
{ v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } c= VAL E
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } or a in VAL E )
assume a in { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } ; :: thesis: a in VAL E
then ex v1 being Element of VAL E st
( a = v1 & ( for f being Function of VAR,E st f = v1 holds
f . x in f . y ) ) ;
hence a in VAL E ; :: thesis: verum
end;
hence { v1 where v1 is Element of VAL E : for f being Function of VAR,E st f = v1 holds
f . x in f . y } is Subset of (VAL E) ; :: thesis: verum
end;
then A4: for x, y being Variable holds
( S1[H12(x,y)] & S1[H11(x,y)] ) ;
A5: for a being set
for x being Variable st S1[a] holds
S1[H8(x,a)]
proof
let a be set ; :: thesis: for x being Variable st S1[a] holds
S1[H8(x,a)]
let x be Variable; :: thesis: ( S1[a] implies S1[H8(x,a)] )
assume a is Subset of (VAL E) ; :: thesis: S1[H8(x,a)]
set Y = { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } ;
{ u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } c= VAL E
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } or b in VAL E )
assume b in { u5 where u5 is Element of VAL E : for X being set
for f being Function of VAR,E st X = a & f = u5 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) } ; :: thesis: b in VAL E
then ex v1 being Element of VAL E st
( b = v1 & ( for X being set
for f being Function of VAR,E st X = a & f = v1 holds
( f in X & ( for g being Function of VAR,E st ( for y being Variable st g . y <> f . y holds
x = y ) holds
g in X ) ) ) ) ;
hence b in VAL E ; :: thesis: verum
end;
hence S1[H8(x,a)] ; :: thesis: verum
end;
A6: for H being ZF-formula
for a being set holds
( a = H7(H) iff ex A being set st
( ( for x, y being Variable holds
( [(x '=' y),H12(x,y)] in A & [(x 'in' y),H11(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 = H12( Var1 H9, Var2 H9) ) & ( H9 is being_membership implies a = H11( 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 = H9(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 = H8( bound_in H9,b) & [(the_scope_of H9),b] in A ) ) ) ) ) ) by Def3;
thus S1[H7(H)] from ZF_MODEL:sch 4(A6, A4, A1, A2, A5); :: thesis: verum