defpred S1[ set , ZF-formula, set ] means ( ( for x, y being Variable holds
( [(x '=' y),F1(x,y)] in $1 & [(x 'in' y),F2(x,y)] in $1 ) ) & [$2,$3] in $1 & ( for H being ZF-formula
for a being set st [H,a] in $1 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 $1 ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in $1 & [(the_right_argument_of H),c] in $1 ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in $1 ) ) ) ) );
defpred S2[ ZF-formula] means ex a, A being set st S1[A,$1,a];
A1:
for H being ZF-formula st H is atomic holds
S2[H]
proof
let H be
ZF-formula;
( H is atomic implies S2[H] )
assume A2:
(
H is
being_equality or
H is
being_membership )
;
ZF_LANG:def 15 S2[H]
then consider a being
set such that A3:
( (
H is
being_equality &
a = F1(
(Var1 H),
(Var2 H)) ) or (
H is
being_membership &
a = F2(
(Var1 H),
(Var2 H)) ) )
;
take
a
;
ex A being set st S1[A,H,a]
take X =
{ [(x '=' y),F1(x,y)] where x, y is Variable : x = x } \/ { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } ;
S1[X,H,a]
thus
for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in X &
[(x 'in' y),F2(x,y)] in X )
( [H,a] in X & ( for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) )proof
let x,
y be
Variable;
( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X )
[(x '=' y),F1(x,y)] in { [(z '=' t),F1(z,t)] where z, t is Variable : z = z }
;
hence
[(x '=' y),F1(x,y)] in X
by XBOOLE_0:def 3;
[(x 'in' y),F2(x,y)] in X
[(x 'in' y),F2(x,y)] in { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z }
;
hence
[(x 'in' y),F2(x,y)] in X
by XBOOLE_0:def 3;
verum
end;
hence
[H,a] in X
by A2, A4;
for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )
let H be
ZF-formula;
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )let a be
set ;
( [H,a] in X implies ( ( 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) )
assume A7:
[H,a] in X
;
( ( 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )
then A8:
(
[H,a] in { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } or
[H,a] in { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } )
by XBOOLE_0:def 3;
thus
(
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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )proof
assume A9:
H is
being_equality
;
a = F1((Var1 H),(Var2 H))
then A10:
H = (Var1 H) '=' (Var2 H)
by ZF_LANG:36;
A11:
H . 1
= 0
by A9, ZF_LANG:18;
for
x,
y being
Variable holds
[H,a] <> [(x 'in' y),F2(x,y)]
then
for
x,
y being
Variable holds
( not
[H,a] = [(x 'in' y),F2(x,y)] or not
x = x )
;
then consider x,
y being
Variable such that A12:
[H,a] = [(x '=' y),F1(x,y)]
and
x = x
by A8;
H = x '=' y
by A12, XTUPLE_0:1;
then
(
Var1 H = x &
Var2 H = y )
by A10, ZF_LANG:1;
hence
a = F1(
(Var1 H),
(Var2 H))
by A12, XTUPLE_0:1;
verum
end;
thus
(
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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )proof
assume A13:
H is
being_membership
;
a = F2((Var1 H),(Var2 H))
then A14:
H = (Var1 H) 'in' (Var2 H)
by ZF_LANG:37;
A15:
H . 1
= 1
by A13, ZF_LANG:19;
for
x,
y being
Variable holds
[H,a] <> [(x '=' y),F1(x,y)]
then
for
x,
y being
Variable holds
( not
[H,a] = [(x '=' y),F1(x,y)] or not
x = x )
;
then consider x,
y being
Variable such that A16:
[H,a] = [(x 'in' y),F2(x,y)]
and
x = x
by A8;
H = x 'in' y
by A16, XTUPLE_0:1;
then
(
Var1 H = x &
Var2 H = y )
by A14, ZF_LANG:2;
hence
a = F2(
(Var1 H),
(Var2 H))
by A16, XTUPLE_0:1;
verum
end;
hence
( (
H is
negative implies ex
b being
set st
(
a = F3(
b) &
[(the_argument_of H),b] in X ) ) & (
H is
conjunctive implies ex
b,
c being
set st
(
a = F4(
b,
c) &
[(the_left_argument_of H),b] in X &
[(the_right_argument_of H),c] in X ) ) & (
H is
universal implies ex
b being
set st
(
a = F5(
(bound_in H),
b) &
[(the_scope_of H),b] in X ) ) )
by A7, A5, XBOOLE_0:def 3, ZF_LANG:20, ZF_LANG:21, ZF_LANG:22;
verum
end;
A18:
for H being ZF-formula st H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] holds
S2[H]
proof
let H be
ZF-formula;
( H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] implies S2[H] )
assume
H is
conjunctive
;
( not S2[ the_left_argument_of H] or not S2[ the_right_argument_of H] or S2[H] )
then A19:
H . 1
= 3
by ZF_LANG:21;
given a1,
A1 being
set such that A20:
S1[
A1,
the_left_argument_of H,
a1]
;
( not S2[ the_right_argument_of H] or S2[H] )
given a2,
A2 being
set such that A21:
S1[
A2,
the_right_argument_of H,
a2]
;
S2[H]
take a =
F4(
a1,
a2);
ex A being set st S1[A,H,a]
take X =
(A1 \/ A2) \/ {[H,a]};
S1[X,H,a]
thus
for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in X &
[(x 'in' y),F2(x,y)] in X )
( [H,a] in X & ( for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) )proof
let x,
y be
Variable;
( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X )
[(x 'in' y),F2(x,y)] in A1
by A20;
then A22:
[(x 'in' y),F2(x,y)] in A1 \/ A2
by XBOOLE_0:def 3;
[(x '=' y),F1(x,y)] in A1
by A20;
then
[(x '=' y),F1(x,y)] in A1 \/ A2
by XBOOLE_0:def 3;
hence
(
[(x '=' y),F1(x,y)] in X &
[(x 'in' y),F2(x,y)] in X )
by A22, XBOOLE_0:def 3;
verum
end;
[H,a] in {[H,a]}
by TARSKI:def 1;
hence
[H,a] in X
by XBOOLE_0:def 3;
for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )
let F be
ZF-formula;
for a being set st [F,a] in X holds
( ( F is being_equality implies a = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies a = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( a = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( a = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )let c be
set ;
( [F,c] in X implies ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) )
A23:
(
[F,c] = [H,a] implies (
F = H &
c = a ) )
by XTUPLE_0:1;
assume
[F,c] in X
;
( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
then A24:
(
[F,c] in A1 \/ A2 or
[F,c] in {[H,a]} )
by XBOOLE_0:def 3;
then A25:
(
[F,c] in A1 or
[F,c] in A2 or
[F,c] = [H,a] )
by TARSKI:def 1, XBOOLE_0:def 3;
hence
(
F is
being_equality implies
c = F1(
(Var1 F),
(Var2 F)) )
by A20, A21, A23, A19, ZF_LANG:18;
( ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
not
H is
being_membership
by A19, ZF_LANG:19;
hence
(
F is
being_membership implies
c = F2(
(Var1 F),
(Var2 F)) )
by A20, A21, A25, XTUPLE_0:1;
( ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
thus
(
F is
negative implies ex
b being
set st
(
c = F3(
b) &
[(the_argument_of F),b] in X ) )
( ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
thus
(
F is
conjunctive implies ex
b,
d being
set st
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X ) )
( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) )proof
assume A32:
F is
conjunctive
;
ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )
A33:
now ( [F,c] in A1 implies ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) )assume
[F,c] in A1
;
ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )then consider b,
d being
set such that A34:
c = F4(
b,
d)
and A35:
[(the_left_argument_of F),b] in A1
and A36:
[(the_right_argument_of F),d] in A1
by A20, A32;
[(the_right_argument_of F),d] in A1 \/ A2
by A36, XBOOLE_0:def 3;
then A37:
[(the_right_argument_of F),d] in X
by XBOOLE_0:def 3;
[(the_left_argument_of F),b] in A1 \/ A2
by A35, XBOOLE_0:def 3;
then
[(the_left_argument_of F),b] in X
by XBOOLE_0:def 3;
hence
ex
b,
d being
set st
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X )
by A34, A37;
verum end;
A38:
now ( [F,c] in A2 implies ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) )assume
[F,c] in A2
;
ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )then consider b,
d being
set such that A39:
c = F4(
b,
d)
and A40:
[(the_left_argument_of F),b] in A2
and A41:
[(the_right_argument_of F),d] in A2
by A21, A32;
[(the_right_argument_of F),d] in A1 \/ A2
by A41, XBOOLE_0:def 3;
then A42:
[(the_right_argument_of F),d] in X
by XBOOLE_0:def 3;
[(the_left_argument_of F),b] in A1 \/ A2
by A40, XBOOLE_0:def 3;
then
[(the_left_argument_of F),b] in X
by XBOOLE_0:def 3;
hence
ex
b,
d being
set st
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X )
by A39, A42;
verum end;
now ( [F,c] = [H,a] implies ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X ) )assume A43:
[F,c] = [H,a]
;
ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )then
[(the_right_argument_of F),a2] in A1 \/ A2
by A21, A23, XBOOLE_0:def 3;
then A44:
[(the_right_argument_of F),a2] in X
by XBOOLE_0:def 3;
[(the_left_argument_of F),a1] in A1 \/ A2
by A20, A23, A43, XBOOLE_0:def 3;
then
[(the_left_argument_of F),a1] in X
by XBOOLE_0:def 3;
hence
ex
b,
d being
set st
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X )
by A23, A43, A44;
verum end;
hence
ex
b,
d being
set st
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X )
by A24, A33, A38, TARSKI:def 1, XBOOLE_0:def 3;
verum
end;
thus
(
F is
universal implies ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X ) )
verumproof
assume A45:
F is
universal
;
ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
A46:
now ( [F,c] in A2 implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) )assume
[F,c] in A2
;
ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )then consider b being
set such that A47:
c = F5(
(bound_in F),
b)
and A48:
[(the_scope_of F),b] in A2
by A21, A45;
[(the_scope_of F),b] in A1 \/ A2
by A48, XBOOLE_0:def 3;
then
[(the_scope_of F),b] in X
by XBOOLE_0:def 3;
hence
ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X )
by A47;
verum end;
now ( [F,c] in A1 implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) )assume
[F,c] in A1
;
ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )then consider b being
set such that A49:
c = F5(
(bound_in F),
b)
and A50:
[(the_scope_of F),b] in A1
by A20, A45;
[(the_scope_of F),b] in A1 \/ A2
by A50, XBOOLE_0:def 3;
then
[(the_scope_of F),b] in X
by XBOOLE_0:def 3;
hence
ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X )
by A49;
verum end;
hence
ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X )
by A24, A23, A19, A45, A46, TARSKI:def 1, XBOOLE_0:def 3, ZF_LANG:22;
verum
end;
end;
A51:
for H being ZF-formula st H is universal & S2[ the_scope_of H] holds
S2[H]
proof
let H be
ZF-formula;
( H is universal & S2[ the_scope_of H] implies S2[H] )
assume
H is
universal
;
( not S2[ the_scope_of H] or S2[H] )
then A52:
H . 1
= 4
by ZF_LANG:22;
given a,
A being
set such that A53:
S1[
A,
the_scope_of H,
a]
;
S2[H]
take b =
F5(
(bound_in H),
a);
ex A being set st S1[A,H,b]
take X =
A \/ {[H,b]};
S1[X,H,b]
thus
for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in X &
[(x 'in' y),F2(x,y)] in X )
( [H,b] in X & ( for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) )proof
let x,
y be
Variable;
( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X )
(
[(x '=' y),F1(x,y)] in A &
[(x 'in' y),F2(x,y)] in A )
by A53;
hence
(
[(x '=' y),F1(x,y)] in X &
[(x 'in' y),F2(x,y)] in X )
by XBOOLE_0:def 3;
verum
end;
[H,b] in {[H,b]}
by TARSKI:def 1;
hence
[H,b] in X
by XBOOLE_0:def 3;
for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )
let F be
ZF-formula;
for a being set st [F,a] in X holds
( ( F is being_equality implies a = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies a = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( a = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( a = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )let c be
set ;
( [F,c] in X implies ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) )
A54:
(
[F,c] = [H,b] implies (
F = H &
c = b ) )
by XTUPLE_0:1;
assume
[F,c] in X
;
( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
then A55:
(
[F,c] in A or
[F,c] in {[H,b]} )
by XBOOLE_0:def 3;
hence
(
F is
being_equality implies
c = F1(
(Var1 F),
(Var2 F)) )
by A53, A54, A52, TARSKI:def 1, ZF_LANG:18;
( ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
thus
(
F is
being_membership implies
c = F2(
(Var1 F),
(Var2 F)) )
by A53, A55, A54, A52, TARSKI:def 1, ZF_LANG:19;
( ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
thus
(
F is
negative implies ex
b being
set st
(
c = F3(
b) &
[(the_argument_of F),b] in X ) )
( ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )proof
assume
F is
negative
;
ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
then consider b being
set such that A56:
c = F3(
b)
and A57:
[(the_argument_of F),b] in A
by A53, A55, A54, A52, TARSKI:def 1, ZF_LANG:20;
[(the_argument_of F),b] in X
by A57, XBOOLE_0:def 3;
hence
ex
b being
set st
(
c = F3(
b) &
[(the_argument_of F),b] in X )
by A56;
verum
end;
thus
(
F is
conjunctive implies ex
b,
d being
set st
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X ) )
( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) )proof
assume
F is
conjunctive
;
ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )
then consider b,
d being
set such that A58:
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in A &
[(the_right_argument_of F),d] in A )
by A53, A55, A54, A52, TARSKI:def 1, ZF_LANG:21;
take
b
;
ex d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )
take
d
;
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )
thus
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X )
by A58, XBOOLE_0:def 3;
verum
end;
thus
(
F is
universal implies ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X ) )
verumproof
assume A59:
F is
universal
;
ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
A60:
now ( [F,c] in A implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) )assume
[F,c] in A
;
ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )then consider b being
set such that A61:
c = F5(
(bound_in F),
b)
and A62:
[(the_scope_of F),b] in A
by A53, A59;
[(the_scope_of F),b] in X
by A62, XBOOLE_0:def 3;
hence
ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X )
by A61;
verum end;
now ( [F,c] = [H,b] implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) )assume A63:
[F,c] = [H,b]
;
ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )then
[(the_scope_of F),a] in X
by A53, A54, XBOOLE_0:def 3;
hence
ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X )
by A54, A63;
verum end;
hence
ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X )
by A55, A60, TARSKI:def 1;
verum
end;
end;
A64:
for H being ZF-formula st H is negative & S2[ the_argument_of H] holds
S2[H]
proof
let H be
ZF-formula;
( H is negative & S2[ the_argument_of H] implies S2[H] )
assume
H is
negative
;
( not S2[ the_argument_of H] or S2[H] )
then A65:
H . 1
= 2
by ZF_LANG:20;
given a,
A being
set such that A66:
S1[
A,
the_argument_of H,
a]
;
S2[H]
take b =
F3(
a);
ex A being set st S1[A,H,b]
take X =
A \/ {[H,b]};
S1[X,H,b]
thus
for
x,
y being
Variable holds
(
[(x '=' y),F1(x,y)] in X &
[(x 'in' y),F2(x,y)] in X )
( [H,b] in X & ( for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) ) ) )proof
let x,
y be
Variable;
( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X )
(
[(x '=' y),F1(x,y)] in A &
[(x 'in' y),F2(x,y)] in A )
by A66;
hence
(
[(x '=' y),F1(x,y)] in X &
[(x 'in' y),F2(x,y)] in X )
by XBOOLE_0:def 3;
verum
end;
[H,b] in {[H,b]}
by TARSKI:def 1;
hence
[H,b] in X
by XBOOLE_0:def 3;
for H being ZF-formula
for a being set st [H,a] in X 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 X ) ) & ( H is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of H),b] in X & [(the_right_argument_of H),c] in X ) ) & ( H is universal implies ex b being set st
( a = F5((bound_in H),b) & [(the_scope_of H),b] in X ) ) )
let F be
ZF-formula;
for a being set st [F,a] in X holds
( ( F is being_equality implies a = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies a = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( a = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( a = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( a = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )let c be
set ;
( [F,c] in X implies ( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) ) )
A67:
(
[F,c] = [H,b] implies (
F = H &
c = b ) )
by XTUPLE_0:1;
assume
[F,c] in X
;
( ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) & ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
then A68:
(
[F,c] in A or
[F,c] in {[H,b]} )
by XBOOLE_0:def 3;
hence
(
F is
being_equality implies
c = F1(
(Var1 F),
(Var2 F)) )
by A66, A67, A65, TARSKI:def 1, ZF_LANG:18;
( ( F is being_membership implies c = F2((Var1 F),(Var2 F)) ) & ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
thus
(
F is
being_membership implies
c = F2(
(Var1 F),
(Var2 F)) )
by A66, A68, A67, A65, TARSKI:def 1, ZF_LANG:19;
( ( F is negative implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) ) & ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
thus
(
F is
negative implies ex
b being
set st
(
c = F3(
b) &
[(the_argument_of F),b] in X ) )
( ( F is conjunctive implies ex b, c being set st
( c = F4(b,c) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),c] in X ) ) & ( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) ) )
thus
(
F is
conjunctive implies ex
b,
d being
set st
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X ) )
( F is universal implies ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) )proof
assume
F is
conjunctive
;
ex b, d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )
then consider b,
d being
set such that A74:
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in A &
[(the_right_argument_of F),d] in A )
by A66, A68, A67, A65, TARSKI:def 1, ZF_LANG:21;
take
b
;
ex d being set st
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )
take
d
;
( c = F4(b,d) & [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] in X )
thus
(
c = F4(
b,
d) &
[(the_left_argument_of F),b] in X &
[(the_right_argument_of F),d] in X )
by A74, XBOOLE_0:def 3;
verum
end;
thus
(
F is
universal implies ex
b being
set st
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X ) )
verumproof
assume
F is
universal
;
ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
then consider b being
set such that A75:
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in A )
by A66, A68, A67, A65, TARSKI:def 1, ZF_LANG:22;
take
b
;
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
thus
(
c = F5(
(bound_in F),
b) &
[(the_scope_of F),b] in X )
by A75, XBOOLE_0:def 3;
verum
end;
end;
for H being ZF-formula holds S2[H]
from ZF_LANG:sch 1(A1, A64, A18, A51);
hence
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 ) ) ) ) )
; verum