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; :: thesis: ( H is atomic implies S2[H] )
assume A2: ( H is being_equality or H is being_membership ) ; :: according to ZF_LANG:def 15 :: thesis: 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 ; :: thesis: 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 } ; :: thesis: S1[X,H,a]
A4: now :: thesis: ( H is being_membership implies [H,a] in X )
assume H is being_membership ; :: thesis: [H,a] in X
then ( H . 1 = 1 & H = (Var1 H) 'in' (Var2 H) ) by ZF_LANG:19, ZF_LANG:37;
then [H,a] in { [(x 'in' y),F2(x,y)] where x, y is Variable : x = x } by A3, ZF_LANG:18;
hence [H,a] in X by XBOOLE_0:def 3; :: thesis: verum
end;
thus for x, y being Variable holds
( [(x '=' y),F1(x,y)] in X & [(x 'in' y),F2(x,y)] in X ) :: thesis: ( [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; :: thesis: ( [(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; :: thesis: [(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; :: thesis: verum
end;
now :: thesis: ( H is being_equality implies [H,a] in X )
assume H is being_equality ; :: thesis: [H,a] in X
then ( H . 1 = 0 & H = (Var1 H) '=' (Var2 H) ) by ZF_LANG:18, ZF_LANG:36;
then [H,a] in { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } by A3, ZF_LANG:19;
hence [H,a] in X by XBOOLE_0:def 3; :: thesis: verum
end;
hence [H,a] in X by A2, A4; :: thesis: 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; :: thesis: 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 ; :: thesis: ( [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 ) ) ) )
A5: now :: thesis: ( [H,a] in { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } implies H . 1 = 1 )
assume [H,a] in { [(z 'in' t),F2(z,t)] where z, t is Variable : z = z } ; :: thesis: H . 1 = 1
then consider x, y being Variable such that
A6: [H,a] = [(x 'in' y),F2(x,y)] and
x = x ;
H = x 'in' y by A6, XTUPLE_0:1;
hence H . 1 = 1 by ZF_LANG:15; :: thesis: verum
end;
assume A7: [H,a] in X ; :: thesis: ( ( 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)) ) :: thesis: ( ( 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 ; :: thesis: 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)]
proof
let x, y be Variable; :: thesis: [H,a] <> [(x 'in' y),F2(x,y)]
H <> x 'in' y by A11, ZF_LANG:15;
hence [H,a] <> [(x 'in' y),F2(x,y)] by XTUPLE_0:1; :: thesis: verum
end;
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; :: thesis: verum
end;
thus ( H is being_membership implies a = F2((Var1 H),(Var2 H)) ) :: thesis: ( ( 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 ; :: thesis: 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)]
proof
let x, y be Variable; :: thesis: [H,a] <> [(x '=' y),F1(x,y)]
H <> x '=' y by A15, ZF_LANG:15;
hence [H,a] <> [(x '=' y),F1(x,y)] by XTUPLE_0:1; :: thesis: verum
end;
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; :: thesis: verum
end;
now :: thesis: ( [H,a] in { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } implies H . 1 = 0 )
assume [H,a] in { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } ; :: thesis: H . 1 = 0
then consider x, y being Variable such that
A17: [H,a] = [(x '=' y),F1(x,y)] and
x = x ;
H = x '=' y by A17, XTUPLE_0:1;
hence H . 1 = 0 by ZF_LANG:15; :: thesis: 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; :: thesis: 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; :: thesis: ( H is conjunctive & S2[ the_left_argument_of H] & S2[ the_right_argument_of H] implies S2[H] )
assume H is conjunctive ; :: thesis: ( 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] ; :: thesis: ( 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] ; :: thesis: S2[H]
take a = F4(a1,a2); :: thesis: ex A being set st S1[A,H,a]
take X = (A1 \/ A2) \/ {[H,a]}; :: thesis: 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 ) :: thesis: ( [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; :: thesis: ( [(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; :: thesis: verum
end;
[H,a] in {[H,a]} by TARSKI:def 1;
hence [H,a] in X by XBOOLE_0:def 3; :: thesis: 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; :: thesis: 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 ; :: thesis: ( [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 ; :: thesis: ( ( 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; :: thesis: ( ( 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; :: thesis: ( ( 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 ) ) :: thesis: ( ( 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 A26: F is negative ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
A27: now :: thesis: ( [F,c] in A2 implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) )
assume [F,c] in A2 ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
then consider b being set such that
A28: c = F3(b) and
A29: [(the_argument_of F),b] in A2 by A21, A26;
[(the_argument_of F),b] in A1 \/ A2 by A29, XBOOLE_0:def 3;
then [(the_argument_of F),b] in X by XBOOLE_0:def 3;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A28; :: thesis: verum
end;
now :: thesis: ( [F,c] in A1 implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) )
assume [F,c] in A1 ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
then consider b being set such that
A30: c = F3(b) and
A31: [(the_argument_of F),b] in A1 by A20, A26;
[(the_argument_of F),b] in A1 \/ A2 by A31, XBOOLE_0:def 3;
then [(the_argument_of F),b] in X by XBOOLE_0:def 3;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A30; :: thesis: verum
end;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A24, A23, A19, A26, A27, TARSKI:def 1, XBOOLE_0:def 3, ZF_LANG:20; :: thesis: 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 ) ) :: thesis: ( 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 ; :: thesis: 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 :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum
end;
A38: now :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum
end;
now :: thesis: ( [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] ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ) ) :: thesis: verum
proof
assume A45: F is universal ; :: thesis: ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
A46: now :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum
end;
now :: thesis: ( [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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( H is universal & S2[ the_scope_of H] implies S2[H] )
assume H is universal ; :: thesis: ( 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] ; :: thesis: S2[H]
take b = F5((bound_in H),a); :: thesis: ex A being set st S1[A,H,b]
take X = A \/ {[H,b]}; :: thesis: 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 ) :: thesis: ( [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; :: thesis: ( [(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; :: thesis: verum
end;
[H,b] in {[H,b]} by TARSKI:def 1;
hence [H,b] in X by XBOOLE_0:def 3; :: thesis: 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; :: thesis: 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 ; :: thesis: ( [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 ; :: thesis: ( ( 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; :: thesis: ( ( 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; :: thesis: ( ( 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 ) ) :: thesis: ( ( 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 ; :: thesis: 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; :: thesis: 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 ) ) :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 ) ) :: thesis: verum
proof
assume A59: F is universal ; :: thesis: ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
A60: now :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum
end;
now :: thesis: ( [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] ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( H is negative & S2[ the_argument_of H] implies S2[H] )
assume H is negative ; :: thesis: ( 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] ; :: thesis: S2[H]
take b = F3(a); :: thesis: ex A being set st S1[A,H,b]
take X = A \/ {[H,b]}; :: thesis: 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 ) :: thesis: ( [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; :: thesis: ( [(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; :: thesis: verum
end;
[H,b] in {[H,b]} by TARSKI:def 1;
hence [H,b] in X by XBOOLE_0:def 3; :: thesis: 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; :: thesis: 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 ; :: thesis: ( [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 ; :: thesis: ( ( 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; :: thesis: ( ( 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; :: thesis: ( ( 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 ) ) :: thesis: ( ( 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 A69: F is negative ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
A70: now :: thesis: ( [F,c] in A implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) )
assume [F,c] in A ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
then consider d being set such that
A71: c = F3(d) and
A72: [(the_argument_of F),d] in A by A66, A69;
[(the_argument_of F),d] in X by A72, XBOOLE_0:def 3;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A71; :: thesis: verum
end;
now :: thesis: ( [F,c] = [H,b] implies ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) )
assume A73: [F,c] = [H,b] ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
then [(the_argument_of F),a] in X by A66, A67, XBOOLE_0:def 3;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A67, A73; :: thesis: verum
end;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A68, A70, TARSKI:def 1; :: thesis: 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 ) ) :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 ) ) :: thesis: verum
proof
assume F is universal ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: 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 ) ) ) ) ) ; :: thesis: verum