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]
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;
A4: now
assume H is being_equality ; :: thesis: [H,a] in X
then H . 1 = 0 by ZF_LANG:35;
then ( a = F1((Var1 H),(Var2 H)) & H = (Var1 H) '=' (Var2 H) ) by A3, ZF_LANG:36, ZF_LANG:53;
then [H,a] in { [(x '=' y),F1(x,y)] where x, y is Variable : x = x } ;
hence [H,a] in X by XBOOLE_0:def 3; :: thesis: verum
end;
now
assume H is being_membership ; :: thesis: [H,a] in X
then H . 1 = 1 by ZF_LANG:36;
then ( a = F2((Var1 H),(Var2 H)) & H = (Var1 H) 'in' (Var2 H) ) by A3, ZF_LANG:35, ZF_LANG:54;
then [H,a] in { [(x 'in' y),F2(x,y)] where x, y is Variable : x = x } ;
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 ) ) ) )
assume A5: [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 A6: ( [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 A7: H is being_equality ; :: thesis: a = F1((Var1 H),(Var2 H))
then A8: H . 1 = 0 by ZF_LANG:35;
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 A8, ZF_LANG:31;
hence [H,a] <> [(x 'in' y),F2(x,y)] by ZFMISC_1:33; :: 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
A9: ( [H,a] = [(x '=' y),F1(x,y)] & x = x ) by A6;
A10: ( H = x '=' y & a = F1(x,y) ) by A9, ZFMISC_1:33;
H = (Var1 H) '=' (Var2 H) by A7, ZF_LANG:53;
then ( Var1 H = x & Var2 H = y ) by A10, ZF_LANG:6;
hence a = F1((Var1 H),(Var2 H)) by A9, ZFMISC_1:33; :: 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 A11: H is being_membership ; :: thesis: a = F2((Var1 H),(Var2 H))
then A12: H . 1 = 1 by ZF_LANG:36;
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 A12, ZF_LANG:31;
hence [H,a] <> [(x '=' y),F1(x,y)] by ZFMISC_1:33; :: 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
A13: ( [H,a] = [(x 'in' y),F2(x,y)] & x = x ) by A6;
A14: ( H = x 'in' y & a = F2(x,y) ) by A13, ZFMISC_1:33;
H = (Var1 H) 'in' (Var2 H) by A11, ZF_LANG:54;
then ( Var1 H = x & Var2 H = y ) by A14, ZF_LANG:7;
hence a = F2((Var1 H),(Var2 H)) by A13, ZFMISC_1:33; :: thesis: verum
end;
A15: now
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
A16: ( [H,a] = [(x '=' y),F1(x,y)] & x = x ) ;
H = x '=' y by A16, ZFMISC_1:33;
hence H . 1 = 0 by ZF_LANG:31; :: thesis: verum
end;
now
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
A17: ( [H,a] = [(x 'in' y),F2(x,y)] & x = x ) ;
H = x 'in' y by A17, ZFMISC_1:33;
hence H . 1 = 1 by ZF_LANG:31; :: 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 A5, A15, XBOOLE_0:def 3, ZF_LANG:37, ZF_LANG:38, ZF_LANG:39; :: thesis: verum
end;
A18: 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 A19: H is negative ; :: thesis: ( not S2[ the_argument_of H] or S2[H] )
given a, A being set such that A20: 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 A20;
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 ) ) ) )
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 A21: ( [F,c] in A or [F,c] in {[H,b]} ) by XBOOLE_0:def 3;
A22: ( [F,c] = [H,b] implies ( F = H & c = b ) ) by ZFMISC_1:33;
A23: H . 1 = 2 by A19, ZF_LANG:37;
hence ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) by A20, A21, A22, TARSKI:def 1, ZF_LANG:35; :: 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 A20, A21, A22, A23, TARSKI:def 1, ZF_LANG:36; :: 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 A24: F is negative ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
A25: now
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
A26: ( c = F3(d) & [(the_argument_of F),d] in A ) by A20, A24;
[(the_argument_of F),d] in X by A26, XBOOLE_0:def 3;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A26; :: thesis: verum
end;
now
assume A27: [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 A20, A22, XBOOLE_0:def 3;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A22, A27; :: thesis: verum
end;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A21, A25, 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
A28: ( c = F4(b,d) & [(the_left_argument_of F),b] in A & [(the_right_argument_of F),d] in A ) by A20, A21, A22, A23, TARSKI:def 1, ZF_LANG:38;
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 A28, 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
A29: ( c = F5((bound_in F),b) & [(the_scope_of F),b] in A ) by A20, A21, A22, A23, TARSKI:def 1, ZF_LANG:39;
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 A29, XBOOLE_0:def 3; :: thesis: verum
end;
end;
A30: 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 A31: H is conjunctive ; :: thesis: ( not S2[ the_left_argument_of H] or not S2[ the_right_argument_of H] or S2[H] )
given a1, A1 being set such that A32: 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 A33: 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 '=' y),F1(x,y)] in A1 & [(x 'in' y),F2(x,y)] in A1 ) by A32;
then ( [(x '=' y),F1(x,y)] in A1 \/ A2 & [(x 'in' y),F2(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 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 ) ) ) )
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 A34: ( [F,c] in A1 \/ A2 or [F,c] in {[H,a]} ) by XBOOLE_0:def 3;
then A35: ( [F,c] in A1 or [F,c] in A2 or [F,c] = [H,a] ) by TARSKI:def 1, XBOOLE_0:def 3;
A36: ( [F,c] = [H,a] implies ( F = H & c = a ) ) by ZFMISC_1:33;
A37: H . 1 = 3 by A31, ZF_LANG:38;
then A38: ( not H is being_equality & not H is being_membership & not H is negative & not H is universal ) by ZF_LANG:35, ZF_LANG:36, ZF_LANG:37, ZF_LANG:39;
thus ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) by A32, A33, A35, A36, A37, ZF_LANG:35; :: 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 A32, A33, A35, A38, ZFMISC_1:33; :: 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 A39: F is negative ; :: thesis: ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X )
A40: now
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
A41: ( c = F3(b) & [(the_argument_of F),b] in A1 ) by A32, A39;
[(the_argument_of F),b] in A1 \/ A2 by A41, 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 A41; :: thesis: verum
end;
now
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
A42: ( c = F3(b) & [(the_argument_of F),b] in A2 ) by A33, A39;
[(the_argument_of F),b] in A1 \/ A2 by A42, 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 A42; :: thesis: verum
end;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A34, A36, A37, A39, A40, TARSKI:def 1, XBOOLE_0:def 3, ZF_LANG:37; :: 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 A43: 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 )
A44: now
assume A45: [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_left_argument_of F),a1] in A1 \/ A2 & [(the_right_argument_of F),a2] in A1 \/ A2 ) by A32, A33, A36, XBOOLE_0:def 3;
then ( [(the_left_argument_of F),a1] in X & [(the_right_argument_of F),a2] 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 A36, A45; :: thesis: verum
end;
A46: now
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
A47: ( c = F4(b,d) & [(the_left_argument_of F),b] in A1 & [(the_right_argument_of F),d] in A1 ) by A32, A43;
( [(the_left_argument_of F),b] in A1 \/ A2 & [(the_right_argument_of F),d] in A1 \/ A2 ) by A47, XBOOLE_0:def 3;
then ( [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] 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 A47; :: thesis: verum
end;
now
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
A48: ( c = F4(b,d) & [(the_left_argument_of F),b] in A2 & [(the_right_argument_of F),d] in A2 ) by A33, A43;
( [(the_left_argument_of F),b] in A1 \/ A2 & [(the_right_argument_of F),d] in A1 \/ A2 ) by A48, XBOOLE_0:def 3;
then ( [(the_left_argument_of F),b] in X & [(the_right_argument_of F),d] 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 A48; :: 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 A34, A44, A46, 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 A49: F is universal ; :: thesis: ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
A50: now
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
A51: ( c = F5((bound_in F),b) & [(the_scope_of F),b] in A1 ) by A32, A49;
[(the_scope_of F),b] in A1 \/ A2 by A51, 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 A51; :: thesis: verum
end;
now
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
A52: ( c = F5((bound_in F),b) & [(the_scope_of F),b] in A2 ) by A33, A49;
[(the_scope_of F),b] in A1 \/ A2 by A52, 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 A52; :: thesis: verum
end;
hence ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A34, A36, A37, A49, A50, TARSKI:def 1, XBOOLE_0:def 3, ZF_LANG:39; :: thesis: verum
end;
end;
A53: 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 A54: H is universal ; :: thesis: ( not S2[ the_scope_of H] or S2[H] )
given a, A being set such that A55: 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 A55;
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 ) ) ) )
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 A56: ( [F,c] in A or [F,c] in {[H,b]} ) by XBOOLE_0:def 3;
A57: ( [F,c] = [H,b] implies ( F = H & c = b ) ) by ZFMISC_1:33;
A58: H . 1 = 4 by A54, ZF_LANG:39;
hence ( F is being_equality implies c = F1((Var1 F),(Var2 F)) ) by A55, A56, A57, TARSKI:def 1, ZF_LANG:35; :: 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 A55, A56, A57, A58, TARSKI:def 1, ZF_LANG:36; :: 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
A59: ( c = F3(b) & [(the_argument_of F),b] in A ) by A55, A56, A57, A58, TARSKI:def 1, ZF_LANG:37;
[(the_argument_of F),b] in X by A59, XBOOLE_0:def 3;
hence ex b being set st
( c = F3(b) & [(the_argument_of F),b] in X ) by A59; :: 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
A60: ( c = F4(b,d) & [(the_left_argument_of F),b] in A & [(the_right_argument_of F),d] in A ) by A55, A56, A57, A58, TARSKI:def 1, ZF_LANG:38;
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 A60, 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 A61: F is universal ; :: thesis: ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X )
A62: now
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
A63: ( c = F5((bound_in F),b) & [(the_scope_of F),b] in A ) by A55, A61;
[(the_scope_of F),b] in X by A63, XBOOLE_0:def 3;
hence ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A63; :: thesis: verum
end;
now
assume A64: [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 A55, A57, XBOOLE_0:def 3;
hence ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A57, A64; :: thesis: verum
end;
hence ex b being set st
( c = F5((bound_in F),b) & [(the_scope_of F),b] in X ) by A56, A62, TARSKI:def 1; :: thesis: verum
end;
end;
for H being ZF-formula holds S2[H] from ZF_LANG:sch 1(A1, A18, A30, A53);
 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