consider A being set such that
A2:
for x, y being Variable holds
( [(x '=' y),F1(x,y)] in A & [(x 'in' y),F2(x,y)] in A )
and
A3:
[F6(),F7(F6())] in A
and
A4:
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 ) ) )
by A1;
thus
( F6() is being_equality implies F7(F6()) = F1((Var1 F6()),(Var2 F6())) )
by A3, A4; ( ( F6() is being_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 a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
thus
( F6() is being_membership implies F7(F6()) = F2((Var1 F6()),(Var2 F6())) )
by A3, A4; ( ( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) ) & ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
thus
( F6() is negative implies F7(F6()) = F3(F7((the_argument_of F6()))) )
( ( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) ) & ( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) ) )
thus
( F6() is conjunctive implies for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b) )
( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) )proof
assume
F6() is
conjunctive
;
for a, b being set st a = F7((the_left_argument_of F6())) & b = F7((the_right_argument_of F6())) holds
F7(F6()) = F4(a,b)
then consider b,
c being
set such that A5:
F7(
F6())
= F4(
b,
c)
and A6:
[(the_left_argument_of F6()),b] in A
and A7:
[(the_right_argument_of F6()),c] in A
by A3, A4;
A8:
F7(
(the_left_argument_of F6()))
= b
by A1, A2, A4, A6;
let a1,
a2 be
set ;
( a1 = F7((the_left_argument_of F6())) & a2 = F7((the_right_argument_of F6())) implies F7(F6()) = F4(a1,a2) )
assume
(
a1 = F7(
(the_left_argument_of F6())) &
a2 = F7(
(the_right_argument_of F6())) )
;
F7(F6()) = F4(a1,a2)
hence
F7(
F6())
= F4(
a1,
a2)
by A1, A2, A4, A5, A7, A8;
verum
end;
thus
( F6() is universal implies F7(F6()) = F5((bound_in F6()),F7((the_scope_of F6()))) )
verum