:: Models and Satisfiability. Defining by Structural Induction and
:: Free Variables in ZF-formulae
:: by Grzegorz Bancerek
::
:: Received April 14, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ZF_LANG, XXREAL_0, CLASSES2, XBOOLE_0, FUNCT_1, CARD_1, TARSKI,
SUBSET_1, XBOOLEAN, BVFUNC_2, FUNCT_4, ORDINAL1, ZF_MODEL, FUNCT_2;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, FUNCT_1, ZF_LANG, FUNCT_2,
ORDINAL1, NUMBERS, FUNCT_7;
constructors ENUMSET1, FUNCT_2, ZF_LANG, FUNCT_7, NUMBERS;
registrations XBOOLE_0, RELSET_1, ZF_LANG;
requirements NUMERALS, SUBSET, BOOLE;
definitions TARSKI, ZF_LANG;
equalities ZF_LANG;
expansions ZF_LANG;
theorems TARSKI, ZF_LANG, ZFMISC_1, XBOOLE_0, FUNCT_7, FUNCT_2, XTUPLE_0,
XBOOLE_1;
schemes ZF_LANG;
begin
reserve F,H,H9 for ZF-formula,
x,y,z,t for Variable,
a,b,c,d,A,X for set;
scheme
ZFschex { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3(set)->
set, F4(set,set)->set, F5(Variable,set)->set, H()->ZF-formula } : ex a,A st (
for x,y holds [x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)] in A) & [H(),a] in A
& for H,a 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 st a = F3(b) & [the_argument_of H,b] in A) & (H is conjunctive
implies ex b,c 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 st a = F5(
bound_in H,b) & [the_scope_of H,b] in A) proof
defpred Graph[set,ZF-formula,set] means (for x,y holds [x '=' y,F1(x,y)] in
$1 & [x 'in' y,F2(x,y)] in $1) & [$2,$3] in $1 & for H,a 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 st a = F3(b) & [
the_argument_of H,b] in $1) & (H is conjunctive implies ex b,c 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 st (a = F5(bound_in H,b) & [the_scope_of H,b] in $1));
defpred Ind[ZF-formula] means ex a,A st Graph[A,$1,a];
A1: H is atomic implies Ind[H]
proof
assume
A2: H is being_equality or H is being_membership;
then consider a 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, X = { [x '=' y,F1(x,y)] : x = x } \/ { [z 'in' t,F2(z,t)] : z = z
};
A4: now
assume H is being_membership;
then H.1 = 1 & H = (Var1 H) 'in' Var2 H by ZF_LANG:19,37;
then [H,a] in { [x 'in' y,F2(x,y)] : x = x } by A3,ZF_LANG:18;
hence [H,a] in X by XBOOLE_0:def 3;
end;
thus for x,y holds [x '=' y,F1(x,y)] in X & [x 'in' y,F2(x,y)] in X
proof
let x,y;
[x '=' y,F1(x,y)] in { [z '=' t,F1(z,t)] : z = z };
hence [x '=' y,F1(x,y)] in X by XBOOLE_0:def 3;
[x 'in' y,F2(x,y)] in { [z 'in' t,F2(z,t)] : z = z };
hence thesis by XBOOLE_0:def 3;
end;
now
assume H is being_equality;
then H.1 = 0 & H = (Var1 H) '=' Var2 H by ZF_LANG:18,36;
then [H,a] in { [x '=' y,F1(x,y)] : x = x } by A3,ZF_LANG:19;
hence [H,a] in X by XBOOLE_0:def 3;
end;
hence [H,a] in X by A2,A4;
let H,a;
A5: now
assume [H,a] in { [z 'in' t,F2(z,t)] : z = z };
then consider x,y 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;
end;
assume
A7: [H,a] in X;
then
A8: [H,a] in { [x '=' y,F1(x,y)] : x = x } or [H,a] in { [z 'in' t,F2(z,t
)] : z = z } by XBOOLE_0:def 3;
thus H is being_equality implies a = F1(Var1 H,Var2 H)
proof
assume
A9: H is being_equality;
then
A10: H = (Var1 H) '=' Var2 H by ZF_LANG:36;
A11: H.1 = 0 by A9,ZF_LANG:18;
[H,a] <> [x 'in' y,F2(x,y)]
proof
H <> x 'in' y by A11,ZF_LANG:15;
hence thesis by XTUPLE_0:1;
end;
then not ex x,y st [H,a] = [x 'in' y,F2(x,y)] & x = x;
then consider x,y 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 thesis by A12,XTUPLE_0:1;
end;
thus H is being_membership implies a = F2(Var1 H,Var2 H)
proof
assume
A13: H is being_membership;
then
A14: H = (Var1 H) 'in' Var2 H by ZF_LANG:37;
A15: H.1 = 1 by A13,ZF_LANG:19;
[H,a] <> [x '=' y,F1(x,y)]
proof
H <> x '=' y by A15,ZF_LANG:15;
hence thesis by XTUPLE_0:1;
end;
then not ex x,y st [H,a] = [x '=' y,F1(x,y)] & x = x;
then consider x,y 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 thesis by A16,XTUPLE_0:1;
end;
now
assume [H,a] in { [x '=' y,F1(x,y)] : x = x };
then consider x,y 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;
end;
hence thesis by A7,A5,XBOOLE_0:def 3,ZF_LANG:20,21,22;
end;
A18: for H st H is conjunctive & Ind[the_left_argument_of H] & Ind[
the_right_argument_of H] holds Ind[H]
proof
let H;
assume H is conjunctive;
then
A19: H.1 = 3 by ZF_LANG:21;
given a1 being set,A1 being set such that
A20: Graph[A1,the_left_argument_of H,a1];
given a2 being set,A2 being set such that
A21: Graph[A2,the_right_argument_of H,a2];
take a = F4(a1,a2) , X = A1 \/ A2 \/ { [H,a] };
thus for x,y holds [x '=' y,F1(x,y)] in X & [x 'in' y,F2(x,y)] in X
proof
let x,y;
[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 thesis by A22,XBOOLE_0:def 3;
end;
[H,a] in { [H,a] } by TARSKI:def 1;
hence [H,a] in X by XBOOLE_0:def 3;
let F,c;
A23: [F,c] = [H,a] implies F = H & c = a by XTUPLE_0:1;
assume [F,c] 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;
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;
thus F is negative implies ex b st c = F3(b) & [the_argument_of F,b] in X
proof
assume
A26: F is negative;
A27: now
assume [F,c] in A2;
then consider b 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 thesis by A28;
end;
now
assume [F,c] in A1;
then consider b 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 thesis by A30;
end;
hence thesis by A24,A23,A19,A26,A27,TARSKI:def 1,XBOOLE_0:def 3
,ZF_LANG:20;
end;
thus F is conjunctive implies ex b,d st c = F4(b,d) & [
the_left_argument_of F,b] in X & [the_right_argument_of F,d] in X
proof
assume
A32: F is conjunctive;
A33: now
assume [F,c] in A1;
then consider b,d 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 thesis by A34,A37;
end;
A38: now
assume [F,c] in A2;
then consider b,d 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 thesis by A39,A42;
end;
now
assume
A43: [F,c] = [H,a];
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 thesis by A23,A43,A44;
end;
hence thesis by A24,A33,A38,TARSKI:def 1,XBOOLE_0:def 3;
end;
thus F is universal implies ex b st c = F5(bound_in F,b) & [the_scope_of F
,b] in X
proof
assume
A45: F is universal;
A46: now
assume [F,c] in A2;
then consider b 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 thesis by A47;
end;
now
assume [F,c] in A1;
then consider b 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 thesis by A49;
end;
hence thesis by A24,A23,A19,A45,A46,TARSKI:def 1,XBOOLE_0:def 3
,ZF_LANG:22;
end;
end;
A51: for H st H is universal & Ind[the_scope_of H] holds Ind[H]
proof
let H;
assume H is universal;
then
A52: H.1 = 4 by ZF_LANG:22;
given a,A such that
A53: Graph[A,the_scope_of H,a];
take b = F5(bound_in H,a) , X = A \/ { [H,b] };
thus for x,y holds [x '=' y,F1(x,y)] in X & [x 'in' y,F2(x,y)] in X
proof
let x,y;
[x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)] in A by A53;
hence thesis by XBOOLE_0:def 3;
end;
[H,b] in { [H,b] } by TARSKI:def 1;
hence [H,b] in X by XBOOLE_0:def 3;
let F,c;
A54: [F,c] = [H,b] implies F = H & c = b by XTUPLE_0:1;
assume [F,c] 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;
thus F is being_membership implies c = F2(Var1 F,Var2 F) by A53,A55,A54,A52
,TARSKI:def 1,ZF_LANG:19;
thus F is negative implies ex b st c = F3(b) & [the_argument_of F,b] in X
proof
assume F is negative;
then consider b 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 thesis by A56;
end;
thus F is conjunctive implies ex b,d st c = F4(b,d) & [
the_left_argument_of F,b] in X & [the_right_argument_of F,d] in X
proof
assume F is conjunctive;
then consider b,d 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,d;
thus thesis by A58,XBOOLE_0:def 3;
end;
thus F is universal implies ex b st c = F5(bound_in F,b) & [the_scope_of F
,b] in X
proof
assume
A59: F is universal;
A60: now
assume [F,c] in A;
then consider b 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 thesis by A61;
end;
now
assume
A63: [F,c] = [H,b];
then [the_scope_of F,a] in X by A53,A54,XBOOLE_0:def 3;
hence thesis by A54,A63;
end;
hence thesis by A55,A60,TARSKI:def 1;
end;
end;
A64: for H st H is negative & Ind[the_argument_of H] holds Ind[H]
proof
let H;
assume H is negative;
then
A65: H.1 = 2 by ZF_LANG:20;
given a,A such that
A66: Graph[A,the_argument_of H,a];
take b = F3(a) , X = A \/ { [H,b] };
thus for x,y holds [x '=' y,F1(x,y)] in X & [x 'in' y,F2(x,y)] in X
proof
let x,y;
[x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)] in A by A66;
hence thesis by XBOOLE_0:def 3;
end;
[H,b] in { [H,b] } by TARSKI:def 1;
hence [H,b] in X by XBOOLE_0:def 3;
let F,c;
A67: [F,c] = [H,b] implies F = H & c = b by XTUPLE_0:1;
assume [F,c] 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;
thus F is being_membership implies c = F2(Var1 F,Var2 F) by A66,A68,A67,A65
,TARSKI:def 1,ZF_LANG:19;
thus F is negative implies ex b st c = F3(b) & [the_argument_of F,b] in X
proof
assume
A69: F is negative;
A70: now
assume [F,c] in A;
then consider d 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 thesis by A71;
end;
now
assume
A73: [F,c] = [H,b];
then [the_argument_of F,a] in X by A66,A67,XBOOLE_0:def 3;
hence thesis by A67,A73;
end;
hence thesis by A68,A70,TARSKI:def 1;
end;
thus F is conjunctive implies ex b,d st c = F4(b,d) & [
the_left_argument_of F,b] in X & [the_right_argument_of F,d] in X
proof
assume F is conjunctive;
then consider b,d 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,d;
thus thesis by A74,XBOOLE_0:def 3;
end;
thus F is universal implies ex b st c = F5(bound_in F,b) & [the_scope_of F
,b] in X
proof
assume F is universal;
then consider b 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;
thus thesis by A75,XBOOLE_0:def 3;
end;
end;
for H holds Ind[H] from ZF_LANG:sch 1(A1,A64,A18,A51);
hence thesis;
end;
scheme
ZFschuniq { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3(set)
->set, F4(set,set)->set, F5(Variable,set)->set, H()->ZF-formula, a()->set, b()
->set } : a() = b()
provided
A1: ex A st (for x,y holds [x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)]
in A) & [H(),a()] in A & for H,a 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 st a = F3(b) & [the_argument_of H,b] in
A) & (H is conjunctive implies ex b,c 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 st a
= F5(bound_in H,b) & [the_scope_of H,b] in A) and
A2: ex A st (for x,y holds [x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)]
in A) & [H(),b()] in A & for H,a 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 st a = F3(b) & [the_argument_of H,b] in
A) & (H is conjunctive implies ex b,c 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 st a
= F5(bound_in H,b) & [the_scope_of H,b] in A)
proof
consider A1 being set such that
for x,y holds [x '=' y,F1(x,y)] in A1 & [x 'in' y,F2(x,y)] in A1 and
A3: [H(),a()] in A1 and
A4: for H,a st [H,a] in A1 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 st a = F3(b) & [the_argument_of H,b] in A1) & (H is
conjunctive implies ex b,c st a = F4(b,c) & [the_left_argument_of H,b] in A1 &
[the_right_argument_of H,c] in A1) & (H is universal implies ex b st a = F5(
bound_in H,b) & [the_scope_of H,b] in A1) by A1;
consider A2 being set such that
for x,y holds [x '=' y,F1(x,y)] in A2 & [x 'in' y,F2(x,y)] in A2 and
A5: [H(),b()] in A2 and
A6: for H,a st [H,a] in A2 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 st a = F3(b) & [the_argument_of H,b] in A2) & (H is
conjunctive implies ex b,c st a = F4(b,c) & [the_left_argument_of H,b] in A2 &
[the_right_argument_of H,c] in A2) & (H is universal implies ex b st a = F5(
bound_in H,b) & [the_scope_of H,b] in A2) by A2;
defpred P[ZF-formula] means for a,b st [$1,a] in A1 & [$1,b] in A2 holds a =
b;
A7: for H st H is universal & P[the_scope_of H] holds P[H]
proof
let H such that
A8: H is universal and
A9: for a,b st [the_scope_of H,a] in A1 & [the_scope_of H,b] in A2 holds a = b;
let a,b;
assume [H,a] in A1 & [H,b] in A2;
then ( ex a1 being set st a = F5(bound_in H,a1) & [the_scope_of H,a1] in
A1)& ex b1 being set st b = F5(bound_in H,b1) & [the_scope_of H,b1] in A2 by A4
,A6,A8;
hence thesis by A9;
end;
A10: for H st H is atomic holds P[H]
proof
let H such that
A11: H is being_equality or H is being_membership;
let a,b such that
A12: [H,a] in A1 and
A13: [H,b] in A2;
A14: now
assume
A15: H is being_membership;
then a = F2(Var1 H,Var2 H) by A4,A12;
hence thesis by A6,A13,A15;
end;
now
assume
A16: H is being_equality;
then a = F1(Var1 H,Var2 H) by A4,A12;
hence thesis by A6,A13,A16;
end;
hence thesis by A11,A14;
end;
A17: for H st H is conjunctive & P[the_left_argument_of H] & P[
the_right_argument_of H] holds P[H]
proof
let H such that
A18: H is conjunctive and
A19: for a,b st [the_left_argument_of H,a] in A1 & [
the_left_argument_of H,b] in A2 holds a = b and
A20: for a,b st [the_right_argument_of H,a] in A1 & [
the_right_argument_of H,b] in A2 holds a = b;
let a,b;
assume that
A21: [H,a] in A1 and
A22: [H,b] in A2;
consider a1,a2 being set such that
A23: a = F4(a1,a2) and
A24: [the_left_argument_of H,a1] in A1 and
A25: [the_right_argument_of H,a2] in A1 by A4,A18,A21;
consider b1,b2 being set such that
A26: b = F4(b1,b2) and
A27: [the_left_argument_of H,b1] in A2 and
A28: [the_right_argument_of H,b2] in A2 by A6,A18,A22;
a1 = b1 by A19,A24,A27;
hence thesis by A20,A23,A25,A26,A28;
end;
A29: for H st H is negative & P[the_argument_of H] holds P[H]
proof
let H such that
A30: H is negative and
A31: for a,b st [the_argument_of H,a] in A1 & [the_argument_of H,b] in
A2 holds a = b;
let a,b;
assume [H,a] in A1 & [H,b] in A2;
then ( ex a1 being set st a = F3(a1) & [the_argument_of H,a1] in A1)& ex
b1 being set st b = F3(b1) & [the_argument_of H,b1] in A2 by A4,A6,A30;
hence thesis by A31;
end;
for H holds P[H] from ZF_LANG:sch 1 (A10,A29,A17,A7);
hence thesis by A3,A5;
end;
scheme
ZFschresult { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3(set
)->set, F4(set,set)->set, F5(Variable,set)->set, H()->ZF-formula, f(ZF-formula)
->set } : ( H() is being_equality implies f(H()) = F1(Var1 H(),Var2 H()) ) & (
H() is being_membership implies f(H()) = F2(Var1 H(),Var2 H()) ) & ( H() is
negative implies f(H()) = F3(f(the_argument_of H())) ) & ( H() is conjunctive
implies for a,b st a = f(the_left_argument_of H()) & b = f(
the_right_argument_of H()) holds f(H()) = F4(a,b) ) & ( H() is universal
implies f(H()) = F5(bound_in H(),f(the_scope_of H())) )
provided
A1: for H9,a holds a = f(H9) iff ex A st (for x,y holds [x '=' y,F1(x,y)
] in A & [x 'in' y,F2(x,y)] in A) & [H9,a] in A & for H,a 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 st a = F3(b) & [
the_argument_of H,b] in A) & (H is conjunctive implies ex b,c 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 st a = F5(bound_in H,b) & [the_scope_of H,b] in A)
proof
consider A such that
A2: for x,y holds [x '=' y,F1(x,y)] in A & [x 'in' y,F2(x,y)] in A and
A3: [H(),f(H())] in A and
A4: for H,a 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 st a = F3(b) & [the_argument_of H,b] in A) & (H is
conjunctive implies ex b,c 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 st a = F5(
bound_in H,b) & [the_scope_of H,b] in A) by A1;
thus H() is being_equality implies f(H()) = F1(Var1 H(),Var2 H()) by A3,A4;
thus H() is being_membership implies f(H()) = F2(Var1 H(),Var2 H()) by A3,A4;
thus H() is negative implies f(H()) = F3(f(the_argument_of H()))
proof
assume H() is negative;
then ex b st f(H()) = F3(b) & [the_argument_of H(),b] in A by A3,A4;
hence thesis by A1,A2,A4;
end;
thus H() is conjunctive implies for a,b st a = f(the_left_argument_of H()) &
b = f(the_right_argument_of H()) holds f(H()) = F4(a,b)
proof
assume H() is conjunctive;
then consider b,c such that
A5: f(H()) = F4(b,c) and
A6: [the_left_argument_of H(),b] in A and
A7: [the_right_argument_of H(),c] in A by A3,A4;
A8: f(the_left_argument_of H()) = b by A1,A2,A4,A6;
let a1,a2 be set;
assume
a1 = f(the_left_argument_of H()) & a2 = f(the_right_argument_of H ());
hence thesis by A1,A2,A4,A5,A7,A8;
end;
thus H() is universal implies f(H()) = F5(bound_in H(),f(the_scope_of H()))
proof
assume H() is universal;
then
ex b st f(H()) = F5(bound_in H(),b) & [the_scope_of H(),b] in A by A3,A4;
hence thesis by A1,A2,A4;
end;
end;
scheme
ZFschproperty { F1(Variable,Variable)->set, F2(Variable,Variable)->set, F3(
set)->set, F4(set,set)->set, F5(Variable,set)->set, f(ZF-formula)->set, H()->
ZF-formula, P[set] } : P[f(H())]
provided
A1: for H9,a holds a = f(H9) iff ex A st (for x,y holds [x '=' y,F1(x,y)
] in A & [x 'in' y,F2(x,y)] in A) & [H9,a] in A & for H,a 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 st a = F3(b) & [
the_argument_of H,b] in A) & (H is conjunctive implies ex b,c 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 st a = F5(bound_in H,b) & [the_scope_of H,b] in A) and
A2: for x,y holds P[F1(x,y)] & P[F2(x,y)] and
A3: for a st P[a] holds P[F3(a)] and
A4: for a,b st P[a] & P[b] holds P[F4(a,b)] and
A5: for a,x st P[a] holds P[F5(x,a)]
proof
defpred Pf[ZF-formula] means P[f($1)];
deffunc g(ZF-formula) = f($1);
deffunc f5(Variable,set) = F5($1,$2);
deffunc f4(set,set) = F4($1,$2);
deffunc f3(set) = F3($1);
deffunc f2(Variable,Variable) = F2($1,$2);
deffunc f1(Variable,Variable) = F1($1,$2);
A6: for H9,a holds a = g(H9) iff ex A st (for x,y holds [x '=' y,f1(x,y)] in
A & [x 'in' y,f2(x,y)] in A) & [H9,a] in A & for H,a 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 st a = f3(b) & [
the_argument_of H,b] in A) & (H is conjunctive implies ex b,c 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 st a = f5(bound_in H,b) & [the_scope_of H,b] in A) by A1
;
A7: now
let H;
thus ( H is being_equality implies g(H) = f1(Var1 H,Var2 H) ) & ( H is
being_membership implies g(H) = f2(Var1 H,Var2 H) ) & ( H is negative implies g
(H) = f3(g(the_argument_of H)) ) & ( H is conjunctive implies for a,b st a = g(
the_left_argument_of H) & b = g(the_right_argument_of H) holds g(H) = f4(a,b) )
& ( H is universal implies g(H) = f5(bound_in H,g(the_scope_of H)) ) from
ZFschresult (A6);
end;
A8: for H st H is negative & Pf[(the_argument_of H)] holds Pf[(H)]
proof
let H;
assume H is negative;
then f(H) = F3(f(the_argument_of H)) by A7;
hence thesis by A3;
end;
A9: for H st H is universal & Pf[(the_scope_of H)] holds Pf[(H)]
proof
let H;
assume H is universal;
then f(H) = F5(bound_in H,f(the_scope_of H)) by A7;
hence thesis by A5;
end;
A10: for H st H is conjunctive & Pf[(the_left_argument_of H)] & Pf[(
the_right_argument_of H)] holds Pf[(H)]
proof
let H;
assume H is conjunctive;
then
f(H) = F4(f(the_left_argument_of H),f(the_right_argument_of H)) by A7;
hence thesis by A4;
end;
A11: for H st H is atomic holds Pf[(H)]
proof
let H;
assume H is being_equality or H is being_membership;
then f(H) = F1(Var1 H,Var2 H) or f(H) = F2(Var1 H,Var2 H) by A7;
hence thesis by A2;
end;
for H holds Pf[(H)] from ZF_LANG:sch 1 (A11,A8,A10,A9);
hence thesis;
end;
:: The set of variables which have free occurrences in a ZF-formula
deffunc f1(Variable,Variable) = {$1,$2};
deffunc f2(Variable,Variable) = {$1,$2};
deffunc f3(set) = $1;
deffunc f4(set,set) = union {$1,$2};
deffunc f5(Variable,set) = $2 \ {$1};
definition
let H;
func Free H -> set means
:Def1:
ex A st (for x,y holds [x '=' y,{ x,y }] in
A & [x 'in' y,{ x,y }] in A) & [H,it] in A & for H9,a st [H9,a] in A holds (H9
is being_equality implies a = { Var1 H9,Var2 H9 }) & (H9 is being_membership
implies a = { Var1 H9,Var2 H9 }) & (H9 is negative implies ex b st a = b & [
the_argument_of H9,b] in A) & (H9 is conjunctive implies ex b,c st a = union {
b,c } & [the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) &
(H9 is universal implies ex b st a = b \ { bound_in H9 } & [
the_scope_of H9,b] in A);
existence
proof
thus ex a,A st (for x,y holds [x '=' y,f1(x,y)] in A & [x 'in' y,f2(x,y)]
in A) & [H,a] in A & for H9,a st [H9,a] in A holds (H9 is being_equality
implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership implies a = f2(Var1
H9,Var2 H9)) & (H9 is negative implies ex b st a = f3(b) & [the_argument_of H9,
b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c) & [
the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9 is
universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A)
from ZFschex;
end;
uniqueness
proof
let a1,a2 be set such that
A1: ex A st (for x,y holds [x '=' y,f1(x,y)] in A & [x 'in' y,f2(x,y)]
in A) & [H,a1] in A & for H9,a st [H9,a] in A holds (H9 is being_equality
implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership implies a = f2(Var1
H9,Var2 H9)) & (H9 is negative implies ex b st a = f3(b) & [the_argument_of H9,
b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c) & [
the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9 is
universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A)
and
A2: ex A st (for x,y holds [x '=' y,f1(x,y)] in A & [x 'in' y,f2(x,y)]
in A) & [H,a2] in A & for H9,a st [H9,a] in A holds (H9 is being_equality
implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership implies a = f2(Var1
H9,Var2 H9)) & (H9 is negative implies ex b st a = f3(b) & [the_argument_of H9,
b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c) & [
the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9 is
universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A);
thus a1 = a2 from ZFschuniq(A1,A2);
end;
end;
deffunc f(ZF-formula) = Free $1;
Lm1: for H for a1 being set holds a1 = f(H) iff ex A st (for x,y holds [x '='
y,f1(x,y)] in A & [x 'in' y,f2(x,y)] in A) & [H,a1] in A & for H9,a st [H9,a]
in A holds (H9 is being_equality implies a = f1(Var1 H9,Var2 H9)) & (H9 is
being_membership implies a = f2(Var1 H9,Var2 H9)) & (H9 is negative implies ex
b st a = f3(b) & [the_argument_of H9,b] in A) & (H9 is conjunctive implies ex b
,c st a = f4(b,c) & [the_left_argument_of H9,b] in A & [the_right_argument_of
H9,c] in A) & (H9 is universal implies ex b st a = f5(bound_in H9,b) & [
the_scope_of H9,b] in A) by Def1;
Lm2: now
let H;
thus (H is being_equality implies f(H) = f1(Var1 H,Var2 H)) & (H is
being_membership implies f(H) = f2(Var1 H,Var2 H)) & (H is negative implies f(H
) = f3(f(the_argument_of H))) & (H is conjunctive implies for a,b st a = f(
the_left_argument_of H) & b = f(the_right_argument_of H) holds f(H) = f4(a,b))
& (H is universal implies f(H) = f5(bound_in H, f(the_scope_of H))) from
ZFschresult(Lm1);
end;
definition
let H;
redefine func Free H -> Subset of VAR; :: redefines Free (ZF_MODEL, definition)
coherence
proof
defpred P[set] means $1 is Subset of VAR;
A1: P[f1(x,y)] & P[f2(x,y)]
proof
{ x,y } c= VAR
proof
let a be object;
assume a in { x,y };
then a = x or a = y by TARSKI:def 2;
hence thesis;
end;
hence thesis;
end;
A2: P[a] & P[b] implies P[f4(a,b)]
proof
assume
A3: a is Subset of VAR & b is Subset of VAR;
union { a,b } c= VAR
proof
let c be object;
assume c in union { a,b };
then consider X such that
A4: c in X and
A5: X in { a,b } by TARSKI:def 4;
X is Subset of VAR by A3,A5,TARSKI:def 2;
hence thesis by A4;
end;
hence thesis;
end;
A6: for a,x st P[a] holds P[f5(x,a)]
by XBOOLE_1:1;
A7: P[a] implies P[f3(a)];
thus P[f(H)] from ZFschproperty(Lm1,A1,A7,A2,A6);
end;
end;
theorem
for H holds (H is being_equality implies Free H = { Var1 H,Var2 H }) &
(H is being_membership implies Free H = { Var1 H,Var2 H }) & (H is negative
implies Free H = Free the_argument_of H) & (H is conjunctive implies Free H =
Free the_left_argument_of H \/ Free the_right_argument_of H) & (H is universal
implies Free H = (Free the_scope_of H) \ { bound_in H })
proof
let H;
thus (H is being_equality implies Free H = { Var1 H,Var2 H } ) & (H is
being_membership implies Free H = { Var1 H,Var2 H } ) & (H is negative implies
Free H = Free the_argument_of H ) by Lm2;
thus H is conjunctive implies Free H = Free the_left_argument_of H \/ Free
the_right_argument_of H
proof
assume H is conjunctive;
hence Free H = union { Free the_left_argument_of H,Free
the_right_argument_of H } by Lm2
.= Free the_left_argument_of H \/ Free the_right_argument_of H by
ZFMISC_1:75;
end;
assume H is universal;
hence thesis by Lm2;
end;
:: The set of all valuations of variables in a model
definition
let D be non empty set;
func VAL D -> set equals
Funcs(VAR,D);
coherence;
end;
registration
let D be non empty set;
cluster VAL D -> non empty;
coherence;
end;
reserve E for non empty set,
f,g,h for Function of VAR,E,
v1,v2,v3,v4,v5,u5 for Element of VAL E;
:: The set of all valuations which satisfy a ZF-formula in a model
definition
deffunc f4(set,set) = $1/\$2;
let H,E;
deffunc f1(Variable,Variable) = {v3: for f st f = v3 holds f.$1 = f.$2};
deffunc f2(Variable,Variable) = {v3: for f st f = v3 holds f.$1 in f.$2};
deffunc f3(set) = (VAL E) \ $1;
deffunc f5(Variable,set) = {v5: for X,f st X = $2 & f = v5 holds f in X &
for g st for y st g.y <> f.y holds $1 = y holds g in X};
func St(H,E) -> set means
:Def3:
ex A st (for x,y holds [x '=' y,{ v1 : for
f st f = v1 holds f.x = f.y }] in A & [x 'in' y,{ v2 : for f st f = v2 holds f.
x in f.y }] in A) & [H,it] in A & for H9,a st [H9,a] in A holds (H9 is
being_equality implies a = { v3 : for f st f = v3 holds f.(Var1 H9) = f.(Var2
H9) }) & (H9 is being_membership implies a = { v4 : for f st f = v4 holds f.(
Var1 H9) in f.(Var2 H9) }) & (H9 is negative implies
ex b st a = (VAL E) \ b & [the_argument_of H9,b] in A ) &
(H9 is conjunctive implies ex b,c
st a = b /\ c & [the_left_argument_of H9,b] in A & [
the_right_argument_of H9,c] in A) & (H9 is universal implies ex b st a = { v5 :
for X,f st X = b & f = v5 holds f in X & for g st for y st g.y <> f.y holds
bound_in H9 = y holds g in X } & [the_scope_of H9,b] in A);
existence
proof
thus ex a,A st (for x,y holds [x '=' y, f1(x,y)] in A & [x 'in' y, f2(x,y)
] in A) & [H,a] in A & for H9,a st [H9,a] in A holds (H9 is being_equality
implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership implies a = f2(Var1
H9, Var2 H9)) & (H9 is negative implies ex b st a = f3(b) & [the_argument_of H9
,b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c) & [
the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9 is
universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A)
from ZFschex;
end;
uniqueness
proof
let a1,a2 be set such that
A1: ex A st (for x,y holds [x '=' y, f1(x,y)] in A & [x 'in' y, f2(x,y
)] in A) & [H,a1] in A & for H9,a st [H9,a] in A holds (H9 is being_equality
implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership implies a = f2(Var1
H9, Var2 H9)) & (H9 is negative implies ex b st a = f3(b) & [the_argument_of H9
,b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c) & [
the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9 is
universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A)
and
A2: ex A st (for x,y holds [x '=' y, f1(x,y)] in A & [x 'in' y, f2(x,y
)] in A) & [H,a2] in A & for H9,a st [H9,a] in A holds (H9 is being_equality
implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership implies a = f2(Var1
H9, Var2 H9)) & (H9 is negative implies ex b st a = f3(b) & [the_argument_of H9
,b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c) & [
the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9 is
universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A);
thus a1 = a2 from ZFschuniq(A1,A2);
end;
end;
Lm3: now
deffunc f4(set,set) = $1/\$2;
let H,E;
deffunc f1(Variable,Variable) = {v3: for f st f = v3 holds f.$1 = f.$2};
deffunc f2(Variable,Variable) = {v3: for f st f = v3 holds f.$1 in f.$2};
deffunc f3(set) = (VAL E) \ $1;
deffunc f5(Variable,set) = {v5: for X,f st X = $2 & f = v5 holds f in X &
for g st for y st g.y <> f.y holds $1 = y holds g in X};
deffunc f(ZF-formula) = St($1,E);
A1: for H,a holds a = f(H) iff ex A st (for x,y holds [x '=' y, f1(x,y)] in
A & [x 'in' y, f2(x,y)] in A) & [H,a] in A & for H9,a st [H9,a] in A holds (H9
is being_equality implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership
implies a = f2(Var1 H9, Var2 H9)) & (H9 is negative implies ex b st a = f3(b) &
[the_argument_of H9,b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c)
& [the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9
is universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A)
by Def3;
thus (H is being_equality implies f(H) = f1(Var1 H,Var2 H) ) & (H is
being_membership implies f(H) = f2(Var1 H,Var2 H) ) & (H is negative implies f(
H) = f3(f(the_argument_of H)) ) & (H is conjunctive implies for a,b st a = f(
the_left_argument_of H) & b = f(the_right_argument_of H) holds f(H) = f4(a,b) )
& (H is universal implies f(H) = f5(bound_in H,f(the_scope_of H))) from
ZFschresult(A1);
end;
definition
let H,E;
redefine func St(H,E) -> Subset of VAL E; :: redefines St (ZF_MODEL, definition)
coherence
proof
defpred P[set] means $1 is Subset of VAL E;
deffunc f(ZF-formula) = St($1,E);
deffunc f5(Variable,set) = {v5: for X,f st X = $2 & f = v5 holds f in X &
for g st for y st g.y <> f.y holds $1 = y holds g in X};
deffunc f4(set,set) = $1/\$2;
deffunc f3(set) = (VAL E) \ $1;
deffunc f2(Variable,Variable) = {v3: for f st f = v3 holds f.$1 in f.$2};
deffunc f1(Variable,Variable) = {v3: for f st f = v3 holds f.$1 = f.$2};
A1: for b st P[b] holds P[f3(b)];
A2: for X,Y being set st P[X] & P[Y] holds P[f4(X,Y)]
proof
let X,Y be set;
assume that
A3: X is Subset of VAL E and
Y is Subset of VAL E;
reconsider X as Subset of VAL E by A3;
X /\ Y c= VAL E;
hence thesis;
end;
now
let x,y;
set X1 = { v1 : for f st f = v1 holds f.x = f.y };
set X2 = { v1 : for f st f = v1 holds f.x in f.y };
X1 c= VAL E
proof
let a be object;
assume a in X1;
then ex v1 st a = v1 & for f st f = v1 holds f.x = f.y;
hence thesis;
end;
hence { v1 : for f st f = v1 holds f.x = f.y } is Subset of VAL E;
X2 c= VAL E
proof
let a be object;
assume a in X2;
then ex v1 st a = v1 & for f st f = v1 holds f.x in f.y;
hence thesis;
end;
hence { v1 : for f st f = v1 holds f.x in f.y } is Subset of VAL E;
end;
then
A4: P[f1(x,y)] & P[f2(x,y)];
A5: for a,x st P[a] holds P[f5(x,a)]
proof
let a,x such that
a is Subset of VAL E;
set Y = { u5 : for X,f st X = a & f = u5 holds f in X & for g st for y
st g.y <> f.y holds x = y holds g in X };
Y c= VAL E
proof
let b be object;
assume b in Y;
then ex v1 st b = v1 & for X,f st X = a & f = v1 holds f in X & for g
st for y st g.y <> f.y holds x = y holds g in X;
hence thesis;
end;
hence thesis;
end;
A6: for H,a holds a = f(H) iff ex A st (for x,y holds [x '=' y, f1(x,y)]
in A & [x 'in' y, f2(x,y)] in A) & [H,a] in A & for H9,a st [H9,a] in A holds (
H9 is being_equality implies a = f1(Var1 H9,Var2 H9)) & (H9 is being_membership
implies a = f2(Var1 H9, Var2 H9)) & (H9 is negative implies ex b st a = f3(b) &
[the_argument_of H9,b] in A) & (H9 is conjunctive implies ex b,c st a = f4(b,c)
& [the_left_argument_of H9,b] in A & [the_right_argument_of H9,c] in A) & (H9
is universal implies ex b st a = f5(bound_in H9,b) & [the_scope_of H9,b] in A)
by Def3;
thus P[f(H)] from ZFschproperty(A6,A4,A1,A2,A5);
end;
end;
theorem Th2:
for x,y,f holds f.x = f.y iff f in St(x '=' y,E)
proof
let x,y,f;
A1: x '=' y is being_equality;
then
A2: x '=' y = (Var1(x '=' y)) '=' Var2(x '=' y) by ZF_LANG:36;
then
A3: x = Var1(x '=' y) by ZF_LANG:1;
A4: y = Var2(x '=' y) by A2,ZF_LANG:1;
A5: St(x '=' y,E) = { v1 : for f st f = v1 holds f.(Var1(x '=' y)) = f.(Var2
(x '=' y)) } by A1,Lm3;
thus f.x = f.y implies f in St(x '=' y,E)
proof
reconsider v = f as Element of VAL E by FUNCT_2:8;
assume f.x = f.y;
then for f st f = v holds f.(Var1(x '=' y)) = f.(Var2(x '=' y)) by A2,A3,
ZF_LANG:1;
hence thesis by A5;
end;
assume f in St(x '=' y,E);
then ex v1 st f = v1 & for f st f = v1 holds f.(Var1(x '=' y)) = f.(Var2(x
'=' y)) by A5;
hence thesis by A3,A4;
end;
theorem Th3:
for x,y,f holds f.x in f.y iff f in St(x 'in' y,E)
proof
let x,y,f;
A1: x 'in' y is being_membership;
then
A2: x 'in' y = (Var1(x 'in' y)) 'in' Var2(x 'in' y) by ZF_LANG:37;
then
A3: x = Var1(x 'in' y) by ZF_LANG:2;
A4: y = Var2(x 'in' y) by A2,ZF_LANG:2;
A5: St(x 'in' y,E) = { v1 : for f st f = v1 holds f.(Var1(x 'in' y)) in f.(
Var2(x 'in' y)) } by A1,Lm3;
thus f.x in f.y implies f in St(x 'in' y,E)
proof
reconsider v = f as Element of VAL E by FUNCT_2:8;
assume f.x in f.y;
then
for f st f = v holds f.(Var1(x 'in' y)) in f.(Var2(x 'in' y)) by A2,A3,
ZF_LANG:2;
hence thesis by A5;
end;
assume f in St(x 'in' y,E);
then
ex v1 st f = v1 & for f st f = v1 holds f.(Var1(x 'in' y)) in f.(Var2(x
'in' y)) by A5;
hence thesis by A3,A4;
end;
theorem Th4:
for H,f holds not f in St(H,E) iff f in St('not' H,E)
proof
let H,f;
A1: 'not' H is negative;
then H = the_argument_of 'not' H by ZF_LANG:def 30;
then
A2: St('not' H,E) = (VAL E) \ St(H,E) by A1,Lm3;
f in VAL E by FUNCT_2:8;
hence not f in St(H,E) implies f in St('not' H,E) by A2,XBOOLE_0:def 5;
assume f in St('not' H,E);
hence thesis by A2,XBOOLE_0:def 5;
end;
theorem Th5:
for H,H9,f holds f in St(H,E) & f in St(H9,E) iff f in St(H '&' H9,E)
proof
let H,H9,f;
A1: H '&' H9 is conjunctive;
then
A2: St(H '&' H9,E) = St(the_left_argument_of(H '&' H9),E) /\
St(the_right_argument_of(H '&' H9),E) by Lm3;
H '&' H9 = (the_left_argument_of(H '&' H9)) '&' the_right_argument_of(H
'&' H9) by A1,ZF_LANG:40;
then
A3: H = the_left_argument_of(H '&' H9) & H9 = the_right_argument_of(H '&' H9
) by ZF_LANG:30;
hence f in St(H,E) & f in St(H9,E) implies f in St(H '&' H9,E) by A2,
XBOOLE_0:def 4;
assume f in St(H '&' H9,E);
hence thesis by A2,A3,XBOOLE_0:def 4;
end;
theorem Th6:
for x,H,f holds ( f in St(H,E) & for g st for y st g.y <> f.y
holds x = y holds g in St(H,E) ) iff f in St(All(x,H),E)
proof
let x,H,f;
A1: All(x,H) is universal;
then
A2: St(All(x,H),E) = { v5 : for X,f st X = St(the_scope_of All(x,H),E) & f =
v5 holds f in X & for g st for y st g.y <> f.y holds bound_in All(x,H) = y
holds g in X } by Lm3;
A3: All(x,H) = All(bound_in All(x,H),the_scope_of All(x,H)) by A1,ZF_LANG:44;
then
A4: x = bound_in All(x,H) by ZF_LANG:3;
A5: H = the_scope_of All(x,H) by A3,ZF_LANG:3;
thus ( f in St(H,E) & for g st for y st g.y <> f.y holds x = y holds g in St
(H,E) ) implies f in St(All(x,H),E)
proof
reconsider v = f as Element of VAL E by FUNCT_2:8;
assume
f in St(H,E) & for g st for y st g.y <> f.y holds x = y holds g in St(H,E);
then
for X,h holds X = St(the_scope_of All(x,H),E) & h = v implies h in X &
for g holds ( for y st g.y <> h.y holds bound_in All(x,H) = y ) implies g in X
by A4,A5;
hence thesis by A2;
end;
assume f in St(All(x,H),E);
then
A6: ex v5 st f = v5 & for X,f st X = St(the_scope_of All(x,H),E) & f = v5
holds f in X & for g st for y st g.y <> f.y holds bound_in All(x,H) = y holds g
in X by A2;
hence f in St(H,E) by A5;
let g;
assume for y st g.y <> f.y holds x = y;
hence thesis by A4,A5,A6;
end;
theorem
H is being_equality implies for f holds f.(Var1 H) = f.(Var2 H) iff f
in St(H,E)
proof
assume H is being_equality;
then H = (Var1 H) '=' Var2 H by ZF_LANG:36;
hence thesis by Th2;
end;
theorem
H is being_membership implies for f holds f.(Var1 H) in f.(Var2 H) iff
f in St(H,E)
proof
assume H is being_membership;
then H = (Var1 H) 'in' Var2 H by ZF_LANG:37;
hence thesis by Th3;
end;
theorem
H is negative implies for f holds not f in St(the_argument_of H,E) iff
f in St(H,E)
proof
assume H is negative;
then H = 'not' the_argument_of H by ZF_LANG:def 30;
hence thesis by Th4;
end;
theorem
H is conjunctive implies for f holds f in St(the_left_argument_of H,E)
& f in St(the_right_argument_of H,E) iff f in St(H,E)
proof
assume H is conjunctive;
then H = (the_left_argument_of H) '&' the_right_argument_of H by ZF_LANG:40;
hence thesis by Th5;
end;
theorem
H is universal implies for f holds (f in St(the_scope_of H,E) & for g
st for y st g.y <> f.y holds bound_in H = y holds g in St(the_scope_of H,E) )
iff f in St(H,E)
proof
assume H is universal;
then H = All(bound_in H,the_scope_of H) by ZF_LANG:44;
hence thesis by Th6;
end;
:: The satisfaction of a ZF-formula in a model by a valuation
definition
let D be non empty set;
let f be Function of VAR,D;
let H;
pred D,f |= H means
:Def4:
f in St(H,D);
end;
theorem
for E,f,x,y holds E,f |= x '=' y iff f.x = f.y
by Th2;
theorem
for E,f,x,y holds E,f |= x 'in' y iff f.x in f.y
by Th3;
theorem Th14:
for E,f,H holds E,f |= H iff not E,f |= 'not' H
by Th4;
theorem Th15:
for E,f,H,H9 holds E,f |= H '&' H9 iff E,f |= H & E,f |= H9
by Th5;
theorem Th16:
for E,f,H,x holds E,f |= All(x,H) iff for g st for y st g.y <> f
.y holds x = y holds E,g |= H
proof
let E,f,H,x;
A1: (for g st for y st g.y <> f.y holds x = y holds E,g |= H) implies E,f |= H
proof
A2: for y st f.y <> f.y holds x = y;
assume for g st for y st g.y <> f.y holds x = y holds E,g |= H;
hence thesis by A2;
end;
A3: (for g st for y st g.y <> f.y holds x = y holds E,g |= H) implies for g
st for y st g.y <> f.y holds x = y holds g in St(H,E)
by Def4;
thus thesis by A3,A1,Th6;
end;
theorem
for E,f,H,H9 holds E,f |= H 'or' H9 iff E,f |= H or E,f |= H9
proof
let E,f,H,H9;
E,f |= 'not' H '&' 'not' H9 iff E,f |= 'not' H & E,f |= 'not' H9 by Th15;
hence thesis by Th14;
end;
theorem Th18:
for E,f,H,H9 holds E,f |= H => H9 iff (E,f |= H implies E,f |= H9)
proof
let E,f,H,H9;
E,f |= H '&' 'not' H9 iff E,f |= H & E,f |= 'not' H9 by Th15;
hence thesis by Th14;
end;
theorem
for E,f,H,H9 holds E,f |= H <=> H9 iff (E,f |= H iff E,f |= H9)
proof
let E,f,H,H9;
E,f |= (H => H9) '&' (H9 => H) iff E,f |= H => H9 & E,f |= H9 => H by Th15;
hence thesis by Th18;
end;
theorem Th20:
for E,f,H,x holds E,f |= Ex(x,H) iff ex g st (for y st g.y <> f.
y holds x = y) & E,g |= H
proof
let E,f,H,x;
thus E,f |= Ex(x,H) implies ex g st (for y st g.y <> f.y holds x = y) & E,g
|= H
proof
assume E,f |= Ex(x,H);
then consider g such that
A1: for y st g.y <> f.y holds x = y and
A2: not E,g |= 'not' H by Th14,Th16;
thus thesis by A1,A2,Th14;
end;
given g such that
A3: for y st g.y <> f.y holds x = y and
A4: E,g |= H;
not E,g |= 'not' H by A4,Th14;
hence thesis by Th14,A3,Th16;
end;
theorem
E,f |= All(x,y,H) iff for g st for z st g.z <> f.z holds x = z or y =
z holds E,g |= H
proof
thus E,f |= All(x,y,H) implies for g st for z st g.z <> f.z holds x = z or y
= z holds E,g |= H
proof
assume
A1: E,f |= All(x,y,H);
A2: for g st for z st g.z <> f.z holds x = z for h st for z st h.z <> g.z
holds y = z holds E,h |= H
proof
let g;
assume for z st g.z <> f.z holds x = z;
then E,g |= All(y,H) by A1,Th16;
hence thesis by Th16;
end;
let g such that
A3: for z st g.z <> f.z holds x = z or y = z;
set h = g+*(y,f.y);
for z st h.z <> f.z holds x = z
proof
let z such that
A4: h.z <> f.z and
A5: x <> z;
A6: y <> z by A4,FUNCT_7:128;
then g.z = f.z by A3,A5;
hence contradiction by A4,A6,FUNCT_7:32;
end;
then (for z st g.z <> h.z holds y = z) implies E,g |= H by A2;
hence thesis by FUNCT_7:32;
end;
assume
A7: for g st for z st g.z <> f.z holds x = z or y = z holds E,g |= H;
now
let g such that
A8: for z st g.z <> f.z holds x = z;
now
let h such that
A9: for z st h.z <> g.z holds y = z;
now
let z;
assume that
A10: h.z <> f.z & x <> z and
A11: y <> z;
h.z = g.z by A9,A11;
hence contradiction by A8,A10;
end;
hence E,h |= H by A7;
end;
hence E,g |= All(y,H) by Th16;
end;
hence thesis by Th16;
end;
theorem
E,f |= Ex(x,y,H) iff ex g st (for z st g.z <> f.z holds x = z or y = z
) & E,g |= H
proof
thus E,f |= Ex(x,y,H) implies ex g st (for z st g.z <> f.z holds x = z or y
= z) & E,g |= H
proof
assume E,f |= Ex(x,y,H);
then consider g such that
A1: for z st g.z <> f.z holds x = z and
A2: E,g |= Ex(y,H) by Th20;
consider h such that
A3: for z st h.z <> g.z holds y = z and
A4: E,h |= H by A2,Th20;
take h;
thus for z st h.z <> f.z holds x = z or y = z
proof
let z such that
A5: h.z <> f.z and
A6: x <> z and
A7: y <> z;
g.z = f.z by A1,A6;
hence contradiction by A3,A5,A7;
end;
thus thesis by A4;
end;
given g such that
A8: for z st g.z <> f.z holds x = z or y = z and
A9: E,g |= H;
set h = f+*(x,g.x);
now
let z;
assume that
A10: g.z <> h.z and
A11: y <> z;
A12: x <> z by A10,FUNCT_7:128;
then g.z = f.z by A8,A11;
hence contradiction by A10,A12,FUNCT_7:32;
end;
then
A13: E,h |= Ex(y,H) by A9,Th20;
for z st h.z <> f.z holds x = z by FUNCT_7:32;
hence thesis by A13,Th20;
end;
:: The satisfaction of a ZF-formula in a model
definition
let E,H;
pred E |= H means
for f holds E,f |= H;
end;
theorem
E |= All(x,H) iff E |= H
proof
thus E |= All(x,H) implies E |= H
proof
assume
A1: for f holds E,f |= All(x,H);
let f;
for y st f.y <> f.y holds x = y;
hence thesis by A1,Th16;
end;
assume
A2: E |= H;
let f;
for g st for y st g.y <> f.y holds x = y holds E,g |= H by A2;
hence thesis by Th16;
end;
:: The axioms of ZF-language
definition
func the_axiom_of_extensionality -> ZF-formula equals
All(x.0,x.1,All(x.2,x.
2 'in' x.0 <=> x.2 'in' x.1) => x.0 '=' x.1);
correctness;
func the_axiom_of_pairs -> ZF-formula equals
All(x.0,x.1,Ex(x.2,All(x.3, x.3
'in' x.2 <=> (x.3 '=' x.0 'or' x.3 '=' x.1) )));
correctness;
func the_axiom_of_unions -> ZF-formula equals
All(x.0,Ex(x.1,All(x.2, x.2
'in' x.1 <=> Ex(x.3,x.2 'in' x.3 '&' x.3 'in' x.0) )));
correctness;
func the_axiom_of_infinity -> ZF-formula equals
Ex(x.0,x.1,x.1 'in' x.0 '&'
All(x.2,x.2 'in' x.0 => Ex(x.3,x.3 'in' x.0 '&' 'not' x.3 '=' x.2 '&' All(x.4,
x.4 'in' x.2 => x.4 'in' x.3) )));
correctness;
func the_axiom_of_power_sets -> ZF-formula equals
All(x.0,Ex(x.1,All(x.2, x.
2 'in' x.1 <=> All(x.3,x.3 'in' x.2 => x.3 'in' x.0) )));
correctness;
end;
definition
let H be ZF-formula;
func the_axiom_of_substitution_for H -> ZF-formula equals
All(x.3,Ex(x.0,All
(x.4,H <=> x.4 '=' x.0))) => All(x.1,Ex(x.2,All(x.4,x.4 'in' x.2 <=> Ex(x.3,x.3
'in' x.1 '&' H))));
correctness;
end;
definition
let E;
attr E is being_a_model_of_ZF means
E is epsilon-transitive & E |=
the_axiom_of_pairs & E |= the_axiom_of_unions & E |= the_axiom_of_infinity & E
|= the_axiom_of_power_sets & for H st { x.0,x.1,x.2 } misses Free H holds E |=
the_axiom_of_substitution_for H;
end;