:: Definable Functions
:: by Grzegorz Bancerek
::
:: Received September 26, 1990
:: 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 NUMBERS, ZF_LANG, XBOOLE_0, SUBSET_1, FUNCT_1, ZF_MODEL, ARYTM_3,
TARSKI, XBOOLEAN, BVFUNC_2, ZF_LANG1, FINSET_1, RELAT_1, CARD_1,
XXREAL_0, ZFMODEL1, NAT_1;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, FUNCT_1, FINSET_1, PARTFUN1, FUNCT_2, ZF_LANG, ZF_MODEL,
ZFMODEL1, ZF_LANG1, XXREAL_0;
constructors ENUMSET1, PARTFUN1, XXREAL_0, XREAL_0, NAT_1, ZF_MODEL, ZFMODEL1,
ZF_LANG1, RELSET_1, NUMBERS;
registrations FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, XREAL_0, FINSEQ_1,
ZF_LANG, ORDINAL1, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, ZF_MODEL, ZFMODEL1, XBOOLE_0, FUNCT_2;
equalities XBOOLE_0;
expansions TARSKI, ZF_MODEL, FUNCT_2;
theorems TARSKI, ZFMISC_1, ENUMSET1, NAT_1, FUNCT_1, FUNCT_2, ZF_MODEL,
ZFMODEL1, ZF_LANG1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0,
FUNCT_7, ORDINAL1;
schemes NAT_1, PARTFUN1, ZF_LANG1;
begin
reserve x,y,z,x1,x2,x3,x4,y1,y2,s for Variable,
M for non empty set,
a,b for set,
i,j,k for Element of NAT,
m,m1,m2,m3,m4 for Element of M,
H,H1,H2 for ZF-formula,
v,v9,v1,v2 for Function of VAR,M;
theorem Th1:
Free (H/(x,y)) c= (Free H \ {x}) \/ {y}
proof
defpred P[ZF-formula] means Free ($1/(x,y)) c= (Free $1 \ {x}) \/ {y};
A1: for x1,x2 holds P[x1 '=' x2] & P[x1 'in' x2]
proof
let x1,x2;
A2: x2 = x or x2 <> x;
x1 = x or x1 <> x;
then consider y1,y2 such that
A3: x1 <> x & x2 <> x & y1 = x1 & y2 = x2 or x1 = x & x2 <> x & y1 = y
& y2 = x2 or x1 <> x & x2 = x & y1 = x1 & y2 = y or x1 = x & x2 = x & y1 = y &
y2 = y by A2;
A4: {y1,y2} c= ({x1,x2} \ {x}) \/ {y}
proof
let a be object;
assume a in {y1,y2};
then (a = x1 or a = x2) & a <> x or a = y by A3,TARSKI:def 2;
then a in {x1,x2} & not a in {x} or a in {y} by TARSKI:def 1,def 2;
then a in {x1,x2} \ {x} or a in {y} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
(x1 'in' x2)/(x,y) = y1 'in' y2 by A3,ZF_LANG1:154;
then
A5: Free ((x1 'in' x2)/(x,y)) = {y1,y2} by ZF_LANG1:59;
(x1 '=' x2)/(x,y) = y1 '=' y2 by A3,ZF_LANG1:152;
then Free ((x1 '=' x2)/(x,y)) = {y1,y2} by ZF_LANG1:58;
hence thesis by A5,A4,ZF_LANG1:58,59;
end;
A6: for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2]
proof
let H1,H2;
assume that
A7: P[H1] and
A8: P[H2];
A9: Free ((H1/(x,y)) '&' (H2/(x,y))) = Free (H1/(x,y)) \/ Free (H2/(x, y
)) by ZF_LANG1:61;
A10: ((Free H1 \ {x}) \/ {y}) \/ ((Free H2 \ {x}) \/ {y}) c= ((Free H1 \/
Free H2) \ {x}) \/ {y}
proof
let a be object;
assume a in ((Free H1 \ {x}) \/ {y}) \/ ((Free H2 \ {x}) \/ {y});
then a in (Free H1 \ {x}) \/ {y} or a in (Free H2 \ {x}) \/ {y} by
XBOOLE_0:def 3;
then a in Free H1 \ {x} or a in Free H2 \ {x} or a in {y} by
XBOOLE_0:def 3;
then (a in Free H1 or a in Free H2) & not a in {x} or a in {y} by
XBOOLE_0:def 5;
then a in Free H1 \/ Free H2 & not a in {x} or a in {y} by XBOOLE_0:def 3
;
then a in (Free H1 \/ Free H2) \ {x} or a in {y} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
A11: (H1 '&' H2)/(x,y) = (H1/(x,y)) '&' (H2/(x,y)) by ZF_LANG1:158;
A12: Free (H1 '&' H2) = Free H1 \/ Free H2 by ZF_LANG1:61;
Free (H1/(x,y)) \/ Free (H2/(x,y)) c= ((Free H1 \ {x}) \/ {y}) \/ ((
Free H2 \ {x}) \/ {y}) by A7,A8,XBOOLE_1:13;
hence thesis by A9,A12,A11,A10,XBOOLE_1:1;
end;
A13: for H,z st P[H] holds P[All(z,H)]
proof
let H,z;
A14: Free All(z,H) = Free H \ {z} by ZF_LANG1:62;
z = x or z <> x;
then consider s such that
A15: z = x & s = y or z <> x & s = z;
A16: ((Free H \ {x}) \/ {y}) \ {s} c= ((Free H \ {z}) \ {x}) \/ {y}
proof
let a be object;
assume
A17: a in ((Free H \ {x}) \/ {y}) \ {s};
then a in Free H \ {x} or a in {y} by XBOOLE_0:def 3;
then a in Free H & not a in {z} & not a in {x} or a in {y} by A15,A17,
XBOOLE_0:def 5;
then a in Free H \ {z} & not a in {x} or a in {y} by XBOOLE_0:def 5;
then a in (Free H \ {z}) \ {x} or a in {y} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
assume P[H];
then
A18: Free (H/(x,y)) \ {s} c= ((Free H \ {x}) \/ {y}) \ {s} by XBOOLE_1:33;
A19: Free All(s,H/(x,y)) = Free (H/(x,y)) \ {s} by ZF_LANG1:62;
All(z,H)/(x,y) = All(s,H/(x,y)) by A15,ZF_LANG1:159,160;
hence thesis by A19,A14,A18,A16,XBOOLE_1:1;
end;
A20: for H st P[H] holds P['not' H]
proof
let H;
A21: Free 'not' H = Free H by ZF_LANG1:60;
Free 'not'(H/(x,y)) = Free (H/(x,y)) by ZF_LANG1:60;
hence thesis by A21,ZF_LANG1:156;
end;
for H holds P[H] from ZF_LANG1:sch 1(A1,A20,A6,A13);
hence thesis;
end;
theorem Th2:
not y in variables_in H implies (x in Free H implies Free (H/(x,y
)) = (Free H \ {x}) \/ {y}) & (not x in Free H implies Free (H/(x,y)) = Free H)
proof
defpred P[ZF-formula] means not y in variables_in $1 implies (x in Free $1
implies Free ($1/(x,y)) = (Free $1 \ {x}) \/ {y}) & (not x in Free $1 implies
Free ($1/(x,y)) = Free $1);
A1: for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2]
proof
let H1,H2;
assume that
A2: P[H1] and
A3: P[H2] and
A4: not y in variables_in (H1 '&' H2);
A5: Free ((H1/(x,y)) '&' (H2/(x,y))) = Free (H1/(x,y)) \/ Free (H2/(x,y))
by ZF_LANG1:61;
set H = H1 '&' H2;
A6: Free (H1 '&' H2) = Free H1 \/ Free H2 by ZF_LANG1:61;
A7: variables_in (H1 '&' H2) = variables_in H1 \/ variables_in H2 by
ZF_LANG1:141;
A8: H/(x,y) = (H1/(x,y)) '&' (H2/(x,y)) by ZF_LANG1:158;
thus x in Free H implies Free (H/(x,y)) = (Free H \ {x}) \/ {y}
proof
assume
A9: x in Free H;
A10: now
assume
A11: not x in Free H1;
then Free H1 = Free H1 \ { x} by ZFMISC_1:57;
hence
Free (H/(x,y)) = (Free H1 \ {x}) \/ (Free H2 \ {x}) \/ {y} by A2,A3,A4
,A6,A5,A7,A8,A9,A11,XBOOLE_0:def 3,XBOOLE_1:4
.= (Free H \ {x}) \/ {y} by A6,XBOOLE_1:42;
end;
A12: now
assume
A13: not x in Free H2;
then Free H2 = Free H2 \ { x} by ZFMISC_1:57;
hence
Free (H/(x,y)) = (Free H1 \ {x}) \/ (Free H2 \ {x}) \/ {y} by A2,A3,A4
,A6,A5,A7,A8,A9,A13,XBOOLE_0:def 3,XBOOLE_1:4
.= (Free H \ {x}) \/ {y} by A6,XBOOLE_1:42;
end;
now
assume that
A14: x in Free H1 and
A15: x in Free H2;
thus Free (H/(x,y)) = {y} \/ (Free H1 \ {x}) \/ (Free H2 \ {x}) \/ {y}
by A2,A3,A4,A5,A7,A8,A14,A15,XBOOLE_0:def 3,XBOOLE_1:4
.= {y} \/ ((Free H1 \ {x}) \/ (Free H2 \ {x})) \/ {y} by XBOOLE_1:4
.= (Free H \ {x}) \/ {y} \/ {y} by A6,XBOOLE_1:42
.= (Free H \ {x}) \/ ({y} \/ {y}) by XBOOLE_1:4
.= (Free H \ {x}) \/ {y};
end;
hence thesis by A10,A12;
end;
assume not x in Free (H1 '&' H2);
hence thesis by A2,A3,A4,A6,A5,A7,XBOOLE_0:def 3,ZF_LANG1:158;
end;
A16: for H,z st P[H] holds P[All(z,H)]
proof
let H,z;
assume that
A17: P[H] and
A18: not y in variables_in All(z,H);
set G = All(z,H)/(x,y);
A19: Free All(z,H) = Free H \ {z} by ZF_LANG1:62;
z = x or z <> x;
then consider s such that
A20: z = x & s = y or z <> x & s = z;
A21: G = All(s,H/(x,y)) by A20,ZF_LANG1:159,160;
A22: Free All(s,H/(x,y)) = Free (H/(x,y)) \ {s} by ZF_LANG1:62;
A23: variables_in All(z,H) = variables_in H \/ {z} by ZF_LANG1:142;
thus x in Free All(z,H) implies Free G = (Free All(z,H) \ {x}) \/ {y}
proof
assume
A24: x in Free All(z,H);
then
A25: not x in {z} by A19,XBOOLE_0:def 5;
thus Free G c= (Free All(z,H) \ {x}) \/ {y}
proof
let a be object;
assume
A26: a in Free G;
then a in (Free H \ {x}) \/ {y} by A17,A18,A19,A22,A23,A21,A24,
XBOOLE_0:def 3,def 5;
then a in Free H \ {x} or a in {y} by XBOOLE_0:def 3;
then
A27: a in Free H & not a in {x} or a in {y} by XBOOLE_0:def 5;
not a in {z} by A20,A22,A21,A25,A26,TARSKI:def 1,XBOOLE_0:def 5;
then a in Free All(z,H) & not a in {x} or a in {y} by A19,A27,
XBOOLE_0:def 5;
then a in Free All(z,H) \ {x} or a in {y} by XBOOLE_0:def 5;
hence thesis by XBOOLE_0:def 3;
end;
let a be object;
assume a in (Free All(z,H) \ {x}) \/ {y};
then a in Free All(z,H) \ {x} or a in {y} by XBOOLE_0:def 3;
then
A28: a in Free All(z,H) & not a in {x} or a in {y} & a = y by TARSKI:def 1
,XBOOLE_0:def 5;
then a in Free H & not a in {x} or a in {y} by A19,XBOOLE_0:def 5;
then a in Free H \ {x} or a in {y} by XBOOLE_0:def 5;
then
A29: a in (Free H \ {x}) \/ {y} by XBOOLE_0:def 3;
not a in {z} by A18,A19,A23,A28,XBOOLE_0:def 3,def 5;
hence thesis by A20,A17,A18,A19,A22,A23,A21,A24,A25,A29,TARSKI:def 1
,XBOOLE_0:def 3,def 5;
end;
assume not x in Free All(z,H);
then
A30: not x in Free H or x in {z} by A19,XBOOLE_0:def 5;
A31: Free All(z,H) c= variables_in All(z,H) by ZF_LANG1:151;
A32: now
assume
A33: x in Free H;
thus Free G = Free All(z,H)
proof
thus Free G c= Free All(z,H)
proof
let a be object;
assume
A34: a in Free G;
then
A35: not a in {y} by A20,A22,A21,A30,A33,TARSKI:def 1,XBOOLE_0:def 5;
a in (Free H \ {z}) \/ {y} by A20,A17,A18,A22,A23,A21,A30,A33,A34,
TARSKI:def 1,XBOOLE_0:def 3,def 5;
hence thesis by A19,A35,XBOOLE_0:def 3;
end;
let a be object;
assume
A36: a in Free All(z,H);
then a <> y by A18,A31;
then
A37: not a in {y} by TARSKI:def 1;
a in (Free H \ {x}) \/ {y} by A20,A19,A30,A33,A36,TARSKI:def 1
,XBOOLE_0:def 3;
hence thesis by A20,A17,A18,A22,A23,A21,A30,A33,A37,TARSKI:def 1
,XBOOLE_0:def 3,def 5;
end;
end;
now
assume not x in Free H;
then Free G = (Free H \ {z}) \ {y} & not y in Free All(z,H) or Free G =
Free H \ {z} by A20,A17,A18,A22,A23,A21,A31,XBOOLE_0:def 3,ZFMISC_1:57;
hence thesis by A19,ZFMISC_1:57;
end;
hence thesis by A32;
end;
A38: for x1,x2 holds P[x1 '=' x2] & P[x1 'in' x2]
proof
let x1,x2;
A39: x2 = x or x2 <> x;
x1 = x or x1 <> x;
then consider y1,y2 such that
A40: x1 <> x & x2 <> x & y1 = x1 & y2 = x2 or x1 = x & x2 <> x & y1 = y
& y2 = x2 or x1 <> x & x2 = x & y1 = x1 & y2 = y or x1 = x & x2 = x & y1 = y &
y2 = y by A39;
(x1 '=' x2)/(x,y) = y1 '=' y2 by A40,ZF_LANG1:152;
then
A41: Free ((x1 '=' x2)/(x,y)) = {y1,y2} by ZF_LANG1:58;
A42: Free (x1 '=' x2) = {x1,x2} by ZF_LANG1:58;
A43: variables_in (x1 '=' x2) = {x1,x2} by ZF_LANG1:138;
thus P[x1 '=' x2]
proof
assume not y in variables_in (x1 '=' x2);
thus x in Free (x1 '=' x2) implies Free ((x1 '=' x2)/(x,y)) = (Free (x1
'=' x2) \ {x}) \/ {y}
proof
assume
A44: x in Free (x1 '=' x2);
thus Free ((x1 '=' x2)/(x,y)) c= (Free (x1 '=' x2) \ {x}) \/ {y} by Th1
;
let a be object;
assume a in (Free (x1 '=' x2) \ {x}) \/ {y};
then a in Free (x1 '=' x2) \ {x} or a in {y} by XBOOLE_0:def 3;
then a in Free (x1 '=' x2) & not a in {x} or a in {y} by XBOOLE_0:def 5
;
then (a = x1 or a = x2) & a <> x or a = y by A42,TARSKI:def 1,def 2;
hence thesis by A40,A41,A42,A44,TARSKI:def 2;
end;
assume not x in Free (x1 '=' x2);
hence thesis by A42,A43,ZF_LANG1:182;
end;
A45: Free (x1 'in' x2) = {x1,x2} by ZF_LANG1:59;
assume not y in variables_in (x1 'in' x2);
(x1 'in' x2)/(x,y) = y1 'in' y2 by A40,ZF_LANG1:154;
then
A46: Free ((x1 'in' x2)/(x,y)) = {y1,y2} by ZF_LANG1:59;
thus x in Free (x1 'in' x2) implies Free ((x1 'in' x2)/(x,y)) = (Free (x1
'in' x2) \ {x}) \/ {y}
proof
assume
A47: x in Free (x1 'in' x2);
thus Free ((x1 'in' x2)/(x,y)) c= (Free (x1 'in' x2) \ {x}) \/ {y} by Th1
;
let a be object;
assume a in (Free (x1 'in' x2) \ {x}) \/ {y};
then a in Free (x1 'in' x2) \ {x} or a in {y} by XBOOLE_0:def 3;
then a in Free (x1 'in' x2) & not a in {x} or a in {y} by XBOOLE_0:def 5;
then (a = x1 or a = x2) & a <> x or a = y by A45,TARSKI:def 1,def 2;
hence thesis by A40,A46,A45,A47,TARSKI:def 2;
end;
assume not x in Free (x1 'in' x2);
hence thesis by A41,A42,A46,A45,A43,ZF_LANG1:182;
end;
A48: for H st P[H] holds P['not' H]
proof
let H;
A49: Free 'not' H = Free H by ZF_LANG1:60;
Free 'not'(H/(x,y)) = Free (H/(x,y)) by ZF_LANG1:60;
hence thesis by A49,ZF_LANG1:140,156;
end;
for H holds P[H] from ZF_LANG1:sch 1(A38,A48,A1,A16);
hence thesis;
end;
registration
let H;
cluster variables_in H -> finite;
coherence
proof
variables_in H = rng H \ {0,1,2,3,4} by ZF_LANG1:def 2;
hence thesis;
end;
end;
theorem Th3:
(ex i st for j st x.j in variables_in H holds j < i) &
ex x st not x in variables_in H
proof
defpred P[ZF-formula] means ex i st for j st x.j in variables_in $1 holds j
< i;
A1: for x,y holds P[x '=' y] & P[x 'in' y]
proof
let x,y;
consider i such that
A2: x = x.i by ZF_LANG1:77;
consider j such that
A3: y = x.j by ZF_LANG1:77;
j <= j+i by NAT_1:11;
then
A4: j < i+j+1 by NAT_1:13;
i <= i+j by NAT_1:11;
then
A5: i < i+j+1 by NAT_1:13;
A6: variables_in (x '=' y) = {x,y} by ZF_LANG1:138;
thus P[x '=' y]
proof
take i+j+1;
let k be Element of NAT;
assume x.k in variables_in (x '=' y);
then x.k = x.i or x.k = x.j by A2,A3,A6,TARSKI:def 2;
hence thesis by A5,A4,ZF_LANG1:76;
end;
take i+j+1;
let k be Element of NAT;
A7: variables_in (x 'in' y) = {x,y} by ZF_LANG1:139;
assume x.k in variables_in (x 'in' y);
then x.k = x.i or x.k = x.j by A2,A3,A7,TARSKI:def 2;
hence thesis by A5,A4,ZF_LANG1:76;
end;
A8: for H1,H2 st P[H1] & P[H2] holds P[H1 '&' H2]
proof
let H1,H2;
given i1 being Element of NAT such that
A9: for j st x.j in variables_in H1 holds j < i1;
given i2 being Element of NAT such that
A10: for j st x.j in variables_in H2 holds j < i2;
i1 <= i2 or i1 > i2;
then consider i such that
A11: i1 <= i2 & i = i2 or i1 > i2 & i = i1;
take i;
let j;
assume x.j in variables_in (H1 '&' H2);
then x.j in variables_in H1 \/ variables_in H2 by ZF_LANG1:141;
then x.j in variables_in H1 or x.j in variables_in H2 by XBOOLE_0:def 3;
then j < i1 or j < i2 by A9,A10;
hence thesis by A11,XXREAL_0:2;
end;
A12: for H,x st P[H] holds P[All(x,H)]
proof
let H,x;
given i1 being Element of NAT such that
A13: for j st x.j in variables_in H holds j < i1;
consider i2 be Element of NAT such that
A14: x = x.i2 by ZF_LANG1:77;
i1 <= i2+1 or i1 > i2+1;
then consider i such that
A15: i1 <= i2+1 & i = i2+1 or i1 > i2+1 & i = i1;
take i;
let j;
assume x.j in variables_in All(x,H);
then x.j in variables_in H \/ {x} by ZF_LANG1:142;
then x.j in variables_in H or x.j in {x} & i2+0 = i2 & 0 < 1 by
XBOOLE_0:def 3;
then j < i1 or x.j = x.i2 & i2 < i2+1 by A13,A14,TARSKI:def 1,XREAL_1:6;
then j < i1 or j < i2+1 by ZF_LANG1:76;
hence thesis by A15,XXREAL_0:2;
end;
A16: for H st P[H] holds P['not' H]
proof
let H;
variables_in 'not' H = variables_in H by ZF_LANG1:140;
hence thesis;
end;
for H holds P[H] from ZF_LANG1:sch 1(A1,A16,A8,A12);
then consider i such that
A17: for j st x.j in variables_in H holds j < i;
thus ex i st for j st x.j in variables_in H holds j < i by A17;
take x.i;
thus thesis by A17;
end;
theorem Th4:
not x in variables_in H implies (M,v |= H iff M,v |= All(x,H))
proof
Free H c= variables_in H by ZF_LANG1:151;
then
A1: x in Free H implies x in variables_in H;
v/(x,v.x) = v by FUNCT_7:35;
hence thesis by A1,ZFMODEL1:10,ZF_LANG1:71;
end;
theorem Th5:
not x in variables_in H implies (M,v |= H iff M,v/(x,m) |= H)
proof
A1: M,v/(x,m) |= All(x,H) implies M,(v/(x,m))/(x,v.x) |= H by ZF_LANG1:71;
A2: (v/(x,m))/(x,v.x) = v/(x,v.x) by FUNCT_7:34;
M,v |= All(x,H) implies M,v/(x,m) |= H by ZF_LANG1:71;
hence thesis by A1,A2,Th4,FUNCT_7:35;
end;
theorem Th6:
x <> y & y <> z & z <> x implies v/(x,m1)/(y,m2)/(z,m3) = v/(z,m3
)/(y,m2)/(x,m1) & v/(x,m1)/(y,m2)/(z,m3) = v/(y,m2)/(z,m3)/(x,m1)
proof
assume that
A1: x <> y and
A2: y <> z and
A3: z <> x;
A4: v/(z,m3)/(y,m2) = v/(y,m2)/(z,m3) by A2,FUNCT_7:33;
v/(x,m1)/(y,m2) = v/(y,m2)/(x,m1) by A1,FUNCT_7:33;
hence thesis by A3,A4,FUNCT_7:33;
end;
theorem Th7:
x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4
implies v/(x1,m1)/(x2,m2)/(x3,m3)/(x4,m4) = v/(x2,m2)/(x3,m3)/(x4,m4)/(x1,m1) &
v/(x1,m1)/(x2,m2)/(x3,m3)/(x4,m4) = v/(x3,m3)/(x4,m4)/(x1,m1)/(x2,m2) & v/(x1,
m1)/(x2,m2)/(x3,m3)/(x4,m4) = v/(x4,m4)/(x2,m2)/(x3,m3)/(x1,m1)
proof
assume that
A1: x1 <> x2 and
A2: x1 <> x3 and
A3: x1 <> x4 and
A4: x2 <> x3 and
A5: x2 <> x4 and
A6: x3 <> x4;
A7: v/(x1,m1)/(x3,m3)/(x4,m4)/(x2,m2) = v/(x3,m3)/(x4,m4)/(x1,m1)/(x2,m2) by A2
,A3,A6,Th6;
A8: v/(x2,m2)/(x3,m3)/(x1,m1)/(x4,m4) = v/(x2,m2)/(x3,m3)/(x4,m4)/(x1,m1) by A3
,FUNCT_7:33;
v/(x1,m1)/(x2,m2)/(x3,m3) = v/(x2,m2)/(x3,m3)/(x1,m1) by A1,A2,A4,Th6;
hence thesis by A4,A5,A6,A8,A7,Th6;
end;
theorem Th8:
v/(x1,m1)/(x2,m2)/(x1,m) = v/(x2,m2)/(x1,m) & v/(x1,m1)/(x2,m2)/(
x3,m3)/(x1,m) = v/(x2,m2)/(x3,m3)/(x1,m) & v/(x1,m1)/(x2,m2)/(x3,m3)/(x4,m4)/(
x1,m) = v/(x2,m2)/(x3,m3)/(x4,m4)/(x1,m)
proof
A1: v/(x1,m1)/(x2,m2)/(x1,m) = v/(x2,m2)/(x1,m1)/(x1,m) or x1 = x2 by
FUNCT_7:33;
hence v/(x1,m1)/(x2,m2)/(x1,m) = v/(x2,m2)/(x1,m) by FUNCT_7:34;
x1 = x3 or x1 <> x3;
then
A2: v/(x1,m1)/(x2,m2)/(x3,m3)/(x1,m) = v/(x1,m1)/(x2,m2)/(x1,m)/(x3,m3 ) & v
/(x2,m2)/(x3,m3)/(x1,m) = v/(x2,m2)/(x1,m)/(x3,m3) or v/(x1,m1)/(x2,m2)/(x3,m3)
/(x1,m) = v/(x1,m1)/(x2,m2)/(x1,m) & v/(x2,m2)/(x3,m3)/(x1,m) = v/(x2,m2)/(x1,m
) by FUNCT_7:33,34;
hence v/(x1,m1)/(x2,m2)/(x3,m3)/(x1,m) = v/(x2,m2)/(x3,m3)/(x1,m) by A1,
FUNCT_7:34;
x1 = x4 or x1 <> x4;
then
v/(x1,m1)/(x2,m2)/(x3,m3)/(x4,m4)/(x1,m) = v/(x1,m1)/(x2,m2)/(x3,m3)/(x1
,m)/(x4,m4) & v/(x2,m2)/(x3,m3)/(x1,m)/(x4,m4) = v/(x2,m2)/(x3,m3)/(x4,m4)/(x1,
m) or v/(x1,m1)/(x2,m2)/(x3,m3)/(x4,m4)/(x1,m) = v/(x1,m1)/(x2,m2)/(x3,m3)/(x1,
m) & v/(x2,m2)/(x3,m3)/(x4,m4)/(x1,m) = v/(x2,m2)/(x3,m3)/(x1,m) by
FUNCT_7:33,34;
hence thesis by A1,A2,FUNCT_7:34;
end;
theorem Th9:
not x in Free H implies (M,v |= H iff M,v/(x,m) |= H)
proof
A1: v/(x,v.x) = v by FUNCT_7:35;
assume
A2: not x in Free H;
then M,v |= H implies M,v |= All(x,H) by ZFMODEL1:10;
hence M,v |= H implies M,v/(x,m) |= H by ZF_LANG1:71;
assume M,v/(x,m) |= H;
then
A3: M,v/(x,m) |= All(x,H) by A2,ZFMODEL1:10;
v/(x,m)/(x,v.x) = v/(x,v.x) by FUNCT_7:34;
hence thesis by A3,A1,ZF_LANG1:71;
end;
theorem Th10:
not x.0 in Free H & M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '='
x.0))) implies for m1,m2 holds def_func'(H,v).m1 = m2 iff M,v/(x.3,m1)/(x.4,m2)
|= H
proof
assume that
A1: not x.0 in Free H and
A2: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
let m1,m2;
A3: v/(x.3,m1).(x.3) = m1 by FUNCT_7:128;
A4: now
let y;
assume
A5: v/(x.3,m1)/(x.4,m2).y <> v.y;
assume that
x.0 <> y and
A6: x.3 <> y and
A7: x.4 <> y;
v/(x.3,m1)/(x.4,m2).y = v/(x.3,m1).y by A7,FUNCT_7:32;
hence contradiction by A5,A6,FUNCT_7:32;
end;
A8: v/(x.3,m1)/(x.4,m2).(x.3) = v/(x.3,m1).(x.3) by FUNCT_7:32,ZF_LANG1:76;
v/(x.3,m1)/(x.4,m2).(x.4) = m2 by FUNCT_7:128;
hence thesis by A1,A2,A3,A8,A4,ZFMODEL1:def 1;
end;
Lm1: x.0 <> x.3 by ZF_LANG1:76;
Lm2: x.0 <> x.4 by ZF_LANG1:76;
Lm3: x.3 <> x.4 by ZF_LANG1:76;
theorem Th11:
Free H c= {x.3,x.4} & M |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '='
x.0))) implies def_func'(H,v) = def_func(H,M)
proof
assume that
A1: Free H c= {x.3,x.4} and
A2: M |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
A3: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0) )) by A2;
let a be Element of M;
set r = def_func'(H,v).a;
A4: v/(x.3,a)/(x.4,r).(x.3) = v/(x.3,a).(x.3) by FUNCT_7:32,ZF_LANG1:76;
not x.0 in Free H by A1,Lm1,Lm2,TARSKI:def 2;
then
A5: M,v/(x.3,a)/(x.4,r) |= H by A3,Th10;
A6: v/(x.3,a).(x.3) = a by FUNCT_7:128;
v/(x.3,a)/(x.4,r).(x.4) = r by FUNCT_7:128;
hence def_func'(H,v).a = def_func(H,M).a by A1,A2,A5,A4,A6,ZFMODEL1:def 2;
end;
theorem Th12:
not x in variables_in H implies (M,v |= H/(y,x) iff M,v/(y,v.x) |= H)
proof
defpred V[ZF-formula] means not x in variables_in $1 implies for v holds M,v
|= $1/(y,x) iff M,v/(y,v.x) |= $1;
A1: for x1,x2 holds V[x1 '=' x2] & V[x1 'in' x2]
proof
let x1,x2;
A2: x2 = y or x2 <> y;
A3: x1 = y or x1 <> y;
thus V[x1 '=' x2]
proof
assume not x in variables_in (x1 '=' x2);
let v;
consider y1,y2 such that
A4: x1 <> y & x2 <> y & y1 = x1 & y2 = x2 or x1 = y & x2 <> y & y1 =
x & y2 = x2 or x1 <> y & x2 = y & y1 = x1 & y2 = x or x1 = y & x2 = y & y1 = x
& y2 = x by A3,A2;
A5: v/(y,v.x).x2 = v.y2 by A4,FUNCT_7:32,128;
A6: v/(y,v.x).x1 = v.y1 by A4,FUNCT_7:32,128;
A7: (x1 '=' x2)/(y,x) = y1 '=' y2 by A4,ZF_LANG1:152;
thus M,v |= (x1 '=' x2)/(y,x) implies M,v/(y,v.x) |= x1 '=' x2
proof
assume M,v |= (x1 '=' x2)/(y,x);
then v.y1 = v.y2 by A7,ZF_MODEL:12;
hence thesis by A6,A5,ZF_MODEL:12;
end;
assume M,v/(y,v.x) |= x1 '=' x2;
then v/(y,v.x).x1 = v/(y,v.x).x2 by ZF_MODEL:12;
hence thesis by A7,A6,A5,ZF_MODEL:12;
end;
consider y1,y2 such that
A8: x1 <> y & x2 <> y & y1 = x1 & y2 = x2 or x1 = y & x2 <> y & y1 =
x & y2 = x2 or x1 <> y & x2 = y & y1 = x1 & y2 = x or x1 = y & x2 = y & y1 = x
& y2 = x by A3,A2;
assume not x in variables_in (x1 'in' x2);
let v;
A9: v/(y,v.x).x1 = v.y1 by A8,FUNCT_7:32,128;
A10: v/(y,v.x).x2 = v.y2 by A8,FUNCT_7:32,128;
A11: (x1 'in' x2)/(y,x) = y1 'in' y2 by A8,ZF_LANG1:154;
thus M,v |= (x1 'in' x2)/(y,x) implies M,v/(y,v.x) |= x1 'in' x2
proof
assume M,v |= (x1 'in' x2)/(y,x);
then v.y1 in v.y2 by A11,ZF_MODEL:13;
hence thesis by A9,A10,ZF_MODEL:13;
end;
assume M,v/(y,v.x) |= x1 'in' x2;
then v/(y,v.x).x1 in v/(y,v.x).x2 by ZF_MODEL:13;
hence thesis by A11,A9,A10,ZF_MODEL:13;
end;
A12: for H1,H2 st V[H1] & V[H2] holds V[H1 '&' H2]
proof
let H1,H2 such that
A13: not x in variables_in H1 implies for v holds M,v |= H1/(y,x) iff
M,v/(y,v.x) |= H1 and
A14: not x in variables_in H2 implies for v holds M,v |= H2/(y,x) iff
M,v/(y,v.x) |= H2;
assume not x in variables_in (H1 '&' H2);
then
A15: not x in variables_in H1 \/ variables_in H2 by ZF_LANG1:141;
let v;
thus M,v |= (H1 '&' H2)/(y,x) implies M,v/(y,v.x) |= H1 '&' H2
proof
assume M,v |= (H1 '&' H2)/(y,x);
then
A16: M,v |= (H1/(y,x)) '&' (H2/(y,x)) by ZF_LANG1:158;
then M,v |= H2/(y,x) by ZF_MODEL:15;
then
A17: M,v/(y,v.x) |= H2 by A14,A15,XBOOLE_0:def 3;
M,v |= H1/(y,x) by A16,ZF_MODEL:15;
then M,v/(y,v.x) |= H1 by A13,A15,XBOOLE_0:def 3;
hence thesis by A17,ZF_MODEL:15;
end;
assume
A18: M,v/(y,v.x) |= H1 '&' H2;
then M,v/(y,v.x) |= H2 by ZF_MODEL:15;
then
A19: M,v |= H2/(y,x) by A14,A15,XBOOLE_0:def 3;
M,v/(y,v.x) |= H1 by A18,ZF_MODEL:15;
then M,v |= H1/(y,x) by A13,A15,XBOOLE_0:def 3;
then M,v |= (H1/(y,x)) '&' (H2/(y,x)) by A19,ZF_MODEL:15;
hence thesis by ZF_LANG1:158;
end;
A20: for H,z st V[H] holds V[All(z,H)]
proof
let H,z such that
A21: not x in variables_in H implies for v holds M,v |= H/(y,x) iff M,
v/(y,v.x) |= H;
z = y or z <> y;
then consider s being Variable such that
A22: z = y & s = x or z <> y & s = z;
assume
A23: not x in variables_in All(z,H);
then
A24: not x in variables_in H \/ {z} by ZF_LANG1:142;
then not x in {z} by XBOOLE_0:def 3;
then
A25: x <> z by TARSKI:def 1;
let v;
Free H c= variables_in H by ZF_LANG1:151;
then
A26: not x in Free H by A24,XBOOLE_0:def 3;
thus M,v |= All(z,H)/(y,x) implies M,v/(y,v.x) |= All(z,H)
proof
assume M,v |= All(z,H)/(y,x);
then
A27: M,v |= All(s,H/(y,x)) by A22,ZF_LANG1:159,160;
A28: now
assume that
A29: z = y and
A30: s = x;
now
let m;
A31: v/(x,m).x = m by FUNCT_7:128;
M,v/(x,m) |= H/(y,x) by A27,A30,ZF_LANG1:71;
then
A32: M,(v/(x,m))/(y,v/(x,m).x) |= H by A21,A24,XBOOLE_0:def 3;
(v/(x,m))/(y,m) = (v/(y,m))/(x,m) by A25,A29,FUNCT_7:33;
then M,(v/(y,m))/(x,m) |= All(x,H) by A26,A32,A31,ZFMODEL1:10;
then
A33: M,((v/(y,m))/(x,m))/(x,v/(y,m).x) |= H by ZF_LANG1:71;
((v/(y,m))/(x,m))/(x,v/(y,m).x) = (v/(y,m))/(x,v/(y,m).x) by
FUNCT_7:34;
hence M,v/(y,m) |= H by A33,FUNCT_7:35;
end;
then M,v |= All(y,H) by ZF_LANG1:71;
hence thesis by A29,ZF_LANG1:72;
end;
now
assume that
A34: z <> y and
A35: s = z;
now
let m;
M,v/(z,m) |= H/(y,x) by A27,A35,ZF_LANG1:71;
then
A36: M,(v/(z,m))/(y,v/(z,m).x) |= H by A21,A24,XBOOLE_0:def 3;
v/(z,m).x = v.x by A25,FUNCT_7:32;
hence M,(v/(y,v.x))/(z,m) |= H by A34,A36,FUNCT_7:33;
end;
hence thesis by ZF_LANG1:71;
end;
hence thesis by A22,A28;
end;
assume
A37: M,v/(y,v.x) |= All(z,H);
Free All(z,H) c= variables_in All(z,H) by ZF_LANG1:151;
then
A38: not x in Free All(z,H) by A23;
A39: now
assume that
A40: z = y and
s = x;
M,v |= All(y,H) by A37,A40,ZF_LANG1:72;
then
A41: M,v |= All(x,All(y,H)) by A38,A40,ZFMODEL1:10;
now
let m;
M,v/(x,m) |= All(y,H) by A41,ZF_LANG1:71;
then
A42: M,(v/(x,m))/(y,m) |= H by ZF_LANG1:71;
v/(x,m).x = m by FUNCT_7:128;
hence M,v/(x,m) |= H/(y,x) by A21,A24,A42,XBOOLE_0:def 3;
end;
then M,v |= All(x,H/(y,x)) by ZF_LANG1:71;
hence thesis by A40,ZF_LANG1:160;
end;
now
assume that
A43: z <> y and
s = z;
now
let m;
M,(v/(y,v.x))/(z,m) |= H by A37,ZF_LANG1:71;
then M,(v/(z,m))/(y,v.x) |= H by A43,FUNCT_7:33;
then M,(v/(z,m))/(y,v/(z,m).x) |= H by A25,FUNCT_7:32;
hence M,v/(z,m) |= H/(y,x) by A21,A24,XBOOLE_0:def 3;
end;
then M,v |= All(z,H/(y,x)) by ZF_LANG1:71;
hence thesis by A43,ZF_LANG1:159;
end;
hence thesis by A22,A39;
end;
A44: for H st V[H] holds V['not' H]
proof
let H such that
A45: not x in variables_in H implies for v holds M,v |= H/(y,x) iff M,
v/(y,v.x) |= H;
assume
A46: not x in variables_in 'not' H;
let v;
thus M,v |= ('not' H)/(y,x) implies M,v/(y,v.x) |= 'not' H
proof
assume M,v |= ('not' H)/(y,x);
then M,v |= 'not'(H/(y,x)) by ZF_LANG1:156;
then not M,v |= H/(y,x) by ZF_MODEL:14;
then not M,v/(y,v.x) |= H by A45,A46,ZF_LANG1:140;
hence thesis by ZF_MODEL:14;
end;
assume M,v/(y,v.x) |= 'not' H;
then not M,v/(y,v.x) |= H by ZF_MODEL:14;
then not M,v |= H/(y,x) by A45,A46,ZF_LANG1:140;
then M,v |= 'not'(H/(y,x)) by ZF_MODEL:14;
hence thesis by ZF_LANG1:156;
end;
for H holds V[H] from ZF_LANG1:sch 1(A1,A44,A12,A20);
hence thesis;
end;
theorem Th13:
not x in variables_in H & M,v |= H implies M,v/(x,v.y) |= H/(y,x )
proof
assume that
A1: not x in variables_in H and
A2: M,v |= H;
A3: v/(x,v.y).x = v.y by FUNCT_7:128;
x = y or x <> y;
then
A4: v/(x,v.y)/(y,v.y) = v/(y,v.y)/(x,v.y) by FUNCT_7:33;
A5: v/(y,v.y) = v by FUNCT_7:35;
M,v/(x,v.y) |= H by A1,A2,Th5;
hence thesis by A1,A4,A3,A5,Th12;
end;
theorem Th14:
not x.0 in Free H & M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '='
x.0))) & not x in variables_in H & not y in Free H & x <> x.0 & x <> x.3 & x <>
x.4 implies not x.0 in Free (H/(y,x)) & M,v/(x,v.y) |= All(x.3,Ex(x.0,All(x.4,H
/(y,x) <=> x.4 '=' x.0))) & def_func'(H,v) = def_func'(H/(y,x),v/(x,v.y))
proof
A1: x.0 <> x.4 by ZF_LANG1:76;
A2: x.3 <> x.4 by ZF_LANG1:76;
set F = H/(y,x), f = v/(x,v.y);
assume that
A3: not x.0 in Free H and
A4: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) and
A5: not x in variables_in H and
A6: not y in Free H and
A7: x <> x.0 and
A8: x <> x.3 and
A9: x <> x.4;
Free F c= variables_in F & not x.0 in variables_in F or not x.0 in {x} &
not x.0 in Free H \ {y} by A3,A7,TARSKI:def 1,XBOOLE_0:def 5;
then
not x.0 in Free F or Free F c= (Free H \ {y}) \/ {x} & not x.0 in (Free
H \ {y}) \/ {x} by Th1,XBOOLE_0:def 3;
hence
A10: not x.0 in Free F;
A11: x.0 <> x.3 by ZF_LANG1:76;
now
let m3;
M,v/(x.3,m3) |= Ex(x.0,All(x.4,H <=> x.4 '=' x.0)) by A4,ZF_LANG1:71;
then consider m such that
A12: M,v/(x.3,m3)/(x.0,m) |= All(x.4,H <=> x.4 '=' x.0) by ZF_LANG1:73;
set f1 = f/(x.3,m3)/(x.0,m);
now
let m4;
A13: v/(x.3,m3)/(x.0,m)/(x.4,m4).(x.4) = m4 by FUNCT_7:128;
A14: v/(x.3,m3)/(x.0,m)/(x.4,m4).(x.0) = v/(x.3,m3)/(x.0,m).(x.0) by
FUNCT_7:32,ZF_LANG1:76;
A15: f1/(x.4,m4).(x.0) = f1.(x.0) by FUNCT_7:32,ZF_LANG1:76;
A16: f1/(x.4,m4).(x.4) = m4 by FUNCT_7:128;
A17: f1.(x.0) = m by FUNCT_7:128;
A18: v/(x.3,m3)/(x.0,m).(x.0) = m by FUNCT_7:128;
A19: M,v/(x.3,m3)/(x.0,m)/(x.4,m4) |= H <=> x.4 '=' x.0 by A12,ZF_LANG1:71;
A20: now
assume M,f1/(x.4,m4) |= x.4 '=' x.0;
then m = m4 by A16,A15,A17,ZF_MODEL:12;
then M,v/(x.3,m3)/(x.0,m)/(x.4,m4) |= x.4 '=' x.0 by A13,A14,A18,
ZF_MODEL:12;
then M,v/(x.3,m3)/(x.0,m)/(x.4,m4) |= H by A19,ZF_MODEL:19;
then M,v/(x.3,m3)/(x.0,m)/(x.4,m4)/(x,v.y) |= H by A5,Th5;
then M,f1/(x.4,m4) |= H by A7,A8,A9,A11,A1,A2,Th7;
then M,f1/(x.4,m4)/(y,f1/(x.4,m4).x) |= H by A6,Th9;
hence M,f1/(x.4,m4) |= F by A5,Th12;
end;
now
assume M,f1/(x.4,m4) |= F;
then M,f1/(x.4,m4)/(y,f1/(x.4,m4).x) |= H by A5,Th12;
then M,f1/(x.4,m4) |= H by A6,Th9;
then M,v/(x.3,m3)/(x.0,m)/(x.4,m4)/(x,v.y) |= H by A7,A8,A9,A11,A1,A2
,Th7;
then M,v/(x.3,m3)/(x.0,m)/(x.4,m4) |= H by A5,Th5;
then M,v/(x.3,m3)/(x.0,m)/(x.4,m4) |= x.4 '=' x.0 by A19,ZF_MODEL:19;
then m = m4 by A13,A14,A18,ZF_MODEL:12;
hence M,f1/(x.4,m4) |= x.4 '=' x.0 by A16,A15,A17,ZF_MODEL:12;
end;
hence M,f1/(x.4,m4) |= F <=> x.4 '=' x.0 by A20,ZF_MODEL:19;
end;
then M,f1 |= All(x.4,F <=> x.4 '=' x.0) by ZF_LANG1:71;
hence M,f/(x.3,m3) |= Ex(x.0,All(x.4,F <=> x.4 '=' x.0)) by ZF_LANG1:73;
end;
hence
A21: M,f |= All(x.3,Ex(x.0,All(x.4,F <=> x.4 '=' x.0))) by ZF_LANG1:71;
A22: Free H c= variables_in H by ZF_LANG1:151;
Free F = Free H by A5,A6,Th2;
then
A23: not x in Free F by A5,A22;
let a be Element of M;
set a9 = def_func'(H,v).a;
M,v/(x.3,a)/(x.4,a9) |= H by A3,A4,Th10;
then M,v/(x.3,a)/(x.4,a9)/(x,v.y) |= H by A5,Th5;
then M,f/(x.3,a)/(x.4,a9) |= H by A8,A9,A2,Th6;
then M,f/(x.3,a)/(x.4,a9)/(x,f/(x.3,a)/(x.4,a9).y) |= F by A5,Th13;
then M,f/(x.3,a)/(x.4,a9) |= F by A23,Th9;
hence def_func'(H,v).a = def_func'(F,f).a by A10,A21,Th10;
end;
theorem
not x in variables_in H implies (M |= H/(y,x) iff M |= H)
proof
assume
A1: not x in variables_in H;
thus M |= H/(y,x) implies M |= H
proof
assume
A2: M,v |= H/(y,x);
let v;
A3: v/(x,v.y).x = v.y by FUNCT_7:128;
M,v/(x,v.y) |= H/(y,x) by A2;
then M,(v/(x,v.y))/(y,v.y) |= H by A1,A3,Th12;
then
A4: M,((v/(x,v.y))/(y,v.y))/(x,v.x) |= H by A1,Th5;
x = y or x <> y;
then
M,(v/(x,v.y))/(x,v.x) |= H or M,((v/(y,v.y))/(x,v.y))/(x,v.x) |= H by A4,
FUNCT_7:33;
then M,v/(x,v.x) |= H or M,(v/(y,v.y))/(x,v.x) |= H by FUNCT_7:34;
then M,v/(x,v.x) |= H by FUNCT_7:35;
hence thesis by FUNCT_7:35;
end;
assume
A5: M,v |= H;
let v;
M,v/(y,v.x) |= H by A5;
hence thesis by A1,Th12;
end;
theorem Th16:
not x.0 in Free H1 & M,v1 |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4
'=' x.0))) implies ex H2,v2 st (for j st j < i & x.j in variables_in H2 holds j
= 3 or j = 4) & not x.0 in Free H2 & M,v2 |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4
'=' x.0))) & def_func'(H1,v1) = def_func'(H2,v2)
proof
defpred ZF[ZF-formula,Nat] means for v1 st not x.0 in Free $1 & M
,v1 |= All(x.3,Ex(x.0,All(x.4,$1 <=> x.4 '=' x.0))) ex H2,v2 st (for j st j <
$2 & x.j in variables_in H2 holds j = 3 or j = 4) & not x.0 in Free H2 & M,v2
|= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) & def_func'($1,v1) = def_func'(
H2,v2);
defpred P[Nat] means for H holds ZF[H,$1];
A1: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A2: ZF[H,i];
let H,v1 such that
A3: not x.0 in Free H and
A4: M,v1 |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
A5: i = 0 implies thesis
proof
assume
A6: i = 0;
consider k such that
A7: for j st x.j in variables_in H holds j < k by Th3;
k > 4 or not k > 4;
then consider k1 being Element of NAT such that
A8: k > 4 & k1 = k or not k > 4 & k1 = 5;
take F = H/(x.0,x.k1), v1/(x.k1,v1.(x.0));
thus for j st j < i+1 & x.j in variables_in F holds j = 3 or j = 4
proof
let j;
assume j < i+1;
then j <= 0 by A6,NAT_1:13;
then j = 0;
hence thesis by A8,ZF_LANG1:76,184;
end;
A9: x.k1 <> x.0 by A8,ZF_LANG1:76;
k1 <> 3 by A8;
then
A10: x.k1 <> x.3 by ZF_LANG1:76;
A11: x.k1 <> x.4 by A8,ZF_LANG1:76;
not x.k1 in variables_in H by A7,A8,XXREAL_0:2;
hence thesis by A3,A4,A9,A10,A11,Th14;
end;
A12: i <> 0 & i <> 3 & i <> 4 implies thesis
proof
A13: x.3 <> x.4 by ZF_LANG1:76;
assume that
A14: i <> 0 and
A15: i <> 3 and
A16: i <> 4;
reconsider ii=i as Element of NAT by ORDINAL1:def 12;
A17: x.0 <> x.ii by A14,ZF_LANG1:76;
consider H1,v9 such that
A18: for j st j < i & x.j in variables_in H1 holds j = 3 or j = 4 and
A19: not x.0 in Free H1 and
A20: M,v9 |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) and
A21: def_func'(H,v1) = def_func'(H1,v9) by A2,A3,A4;
consider k being Element of NAT such that
A22: for j st x.j in variables_in All(x.4,x.ii,H1) holds j < k by Th3;
take H2 = H1/(x.ii,x.k),v2 = v9/(x.k,v9.(x.ii));
A23: variables_in All(x.4,x.ii,H1) = variables_in H1 \/ {x.4,x.ii} by
ZF_LANG1:147;
x.ii in {x.4,x.ii} by TARSKI:def 2;
then
A24: x.ii in variables_in All(x.4,x.ii, H1 ) by A23,XBOOLE_0:def 3;
then
A25: x.ii <> x.k by A22;
then
A26: v2/(x.ii,v2.(x.k)) = v9/(x.ii,v2.(x.k))/(x.k,v9.(x.ii)) by FUNCT_7:33;
thus for j st j < i+1 & x.j in variables_in H2 holds j = 3 or j = 4
proof
x.ii in {x.ii} by TARSKI:def 1;
then
A27: not x.ii in variables_in H1 \ {x.ii} by XBOOLE_0:def 5;
A28: not x.ii in {x.k} by A25,TARSKI:def 1;
let j;
A29: variables_in H2 c= (variables_in H1 \ {x.ii}) \/ {x.k} by ZF_LANG1:187;
assume j < i+1;
then
A30: j <= i by NAT_1:13;
then j < k by A22,A24,XXREAL_0:2;
then
A31: x.j <> x.k by ZF_LANG1:76;
assume
A32: x.j in variables_in H2;
then x.j in variables_in H1 \ {x.ii} or x.j in {x.k} by A29,
XBOOLE_0:def 3;
then
A33: x.j in variables_in H1 by A31,TARSKI:def 1,XBOOLE_0:def 5;
j = i or j < i by A30,XXREAL_0:1;
hence thesis by A18,A27,A28,A29,A32,A33,XBOOLE_0:def 3;
end;
A34: v2.(x.k) = v9.(x.ii) by FUNCT_7:128;
A35: Free H2 c= (Free H1 \ {x.ii}) \/ {x.k} by Th1;
A36: x.4 <> x.ii by A16,ZF_LANG1:76;
A37: x.3 <> x.ii by A15,ZF_LANG1:76;
then
A38: All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0)))/(x.ii,x.k) = All(x.3,Ex
(x.0,All(x.4,H1 <=> x.4 '=' x.0))/(x.ii,x.k)) by ZF_LANG1:159
.= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0)/(x.ii,x.k))) by A17,
ZF_LANG1:164
.= All(x.3,Ex(x.0,All(x.4,(H1 <=> x.4 '=' x.0)/(x.ii,x.k)))) by A36,
ZF_LANG1:159
.= All(x.3,Ex(x.0,All(x.4,H2 <=> ((x.4 '=' x.0)/(x.ii,x.k))))) by
ZF_LANG1:163
.= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) by A17,A36,ZF_LANG1:152
;
A39: v9/(x.ii,v9.(x.ii)) = v9 by FUNCT_7:35;
A40: not x.0 in Free H1 \ {x.ii} by A19,XBOOLE_0:def 5;
not x.k in variables_in All(x.4,x.ii,H1) by A22;
then
A41: not x.k in variables_in H1 by A23,XBOOLE_0:def 3;
x.4 in {x.4,x.ii} by TARSKI:def 2;
then
A42: x.4 in variables_in All(x.4,x.ii,H1) by A23,XBOOLE_0:def 3;
then
A43: x.4 <> x.k by A22;
then
A44: not x.k in {x.4} by TARSKI:def 1;
A45: 0 <> k by A22,A42;
then
A46: x.0 <> x.k by ZF_LANG1:76;
then
A47: not x.k in { x.0} by TARSKI:def 1;
not x.k in {x.4,x.0} by A46,A43,TARSKI:def 2;
then not x.k in variables_in H1 \/ {x.4,x.0} by A41,XBOOLE_0:def 3;
then not x.k in variables_in H1 \/ {x.4,x.0} \/ {x.4} by A44,
XBOOLE_0:def 3;
then
A48: not x.k in variables_in H1 \/ {x.4,x.0} \/ {x.4} \/ {x.0} by A47,
XBOOLE_0:def 3;
A49: x.0 <> x.3 by ZF_LANG1:76;
A50: not x.0 in {x.k} by A46,TARSKI:def 1;
then
A51: not x.0 in Free H2 by A40,A35,XBOOLE_0:def 3;
thus not x.0 in Free H2 by A40,A50,A35,XBOOLE_0:def 3;
A52: variables_in All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) =
variables_in Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0)) \/ {x.3} by ZF_LANG1:142
.= variables_in All(x.4,H1 <=> x.4 '=' x.0) \/ {x.0} \/ {x.3} by
ZF_LANG1:146
.= variables_in (H1 <=> x.4 '=' x.0) \/ {x.4} \/ {x.0} \/ {x.3} by
ZF_LANG1:142
.= variables_in H1 \/ variables_in (x.4 '=' x.0) \/ {x.4} \/ {x.0}
\/ {x.3} by ZF_LANG1:145
.= variables_in H1 \/ {x.4,x.0} \/ {x.4} \/ {x.0} \/ {x.3} by
ZF_LANG1:138;
A53: x.0 <> x.4 by ZF_LANG1:76;
A54: 3 <> k by A22,A42;
then
A55: x.3 <> x.k by ZF_LANG1:76;
then not x.k in {x.3} by TARSKI:def 1;
then
A56: not x.k in variables_in All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))
) by A52,A48,XBOOLE_0:def 3;
then M,v2 |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) by A20,Th5;
hence
A57: M,v2 |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) by A38,A56,A34,A39
,A26,Th12;
now
let e be Element of M;
A58: v2.(x.k) = v9.(x.ii) by FUNCT_7:128;
A59: v2/(x.3,e).(x.k) = v2.(x.k) by A54,FUNCT_7:32,ZF_LANG1:76;
M,v9/(x.3,e) |= Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0)) by A20,ZF_LANG1:71;
then consider e9 being Element of M such that
A60: M,v9/(x.3,e)/(x.0,e9) |= All(x.4,H1 <=> x.4 '=' x.0) by ZF_LANG1:73;
A61: v9/(x.3,e)/(x.0,e9)/(x.4,e9).(x.0) = v9/(x.3,e)/(x.0,e9).(x.0) by
FUNCT_7:32,ZF_LANG1:76;
A62: v9/(x.3,e)/(x.0,e9).(x.0) = e9 by FUNCT_7:128;
v9/(x.3,e)/(x.0,e9)/(x.4,e9).(x.4) = e9 by FUNCT_7:128;
then
A63: M,v9/(x.3,e)/(x.0,e9)/(x.4,e9) |= x.4 '=' x.0 by A61,A62,ZF_MODEL:12;
A64: M,v9/(x.3,e)/(x.0,e9)/(x.4,e9) |= H1 <=> x.4 '=' x.0 by A60,ZF_LANG1:71
;
then
A65: M,v9/(x.3,e)/(x.0,e9)/(x.4,e9) |= H1 by A63,ZF_MODEL:19;
A66: v2/(x.3,e).(x.k) = v2/(x.3,e)/(x.4,e9).(x.k) by A43,FUNCT_7:32;
A67: v2/(x.3,e)/(x.4,e9)/(x.0,e9).(x.k) = v2/(x.3,e)/(x.4,e9).(x.k) by A45,
FUNCT_7:32,ZF_LANG1:76;
A68: v9/(x.3,e)/(x.0,e9)/(x.4,e9) = v9/(x.3,e)/(x.4,e9)/(x.0,e9) by
FUNCT_7:33,ZF_LANG1:76;
A69: v2/(x.ii,v2.(x.k)) = v9/(x.ii,v2.(x.k))/(x.k,v9.(x.ii))
by A25,FUNCT_7:33;
A70: v9/(x.ii,v9.(x.ii)) = v9 by FUNCT_7:35;
v2/(x.3,e)/(x.4,e9)/(x.0,e9) = v9/(x.3,e)/(x.4,e9)/(x.0,e9)/(x.k,
v9.(x. ii)) by A46,A55,A43,A49,A53,A13,Th7;
then
A71: M,v2/(x.3,e)/(x.4,e9)/(x.0,e9) |= H1 by A41,A65,A68,Th5;
v2/(x.3,e)/(x.4,e9)/(x.0,e9)/(x.ii,v2.(x.k)) = v2/(x.ii,v2.(x.k))/(
x.3,e) /(x.4,e9)/(x.0,e9) by A17,A37,A36,A49,A53,A13,Th7;
then M,v2/(x.3,e)/(x.4,e9)/(x.0,e9) |= H2 by A41,A71,A67,A66,A59,A69
,A58,A70,Th12;
then M,v2/(x.3,e)/(x.4,e9) |= H2 by A51,Th9;
then
A72: def_func'(H2,v2).e = e9 by A51,A57,Th10;
M,v9/(x.3,e)/(x.4,e9)/(x.0,e9) |= H1 by A64,A63,A68,ZF_MODEL:19;
then M,v9/(x.3,e)/(x.4,e9) |= H1 by A19,Th9;
hence def_func'(H2,v2).e = def_func'(H1,v9).e by A19,A20,A72,Th10;
end;
hence def_func'(H2,v2) = def_func'(H,v1) by A21;
end;
now
assume
A73: i = 3 or i = 4;
thus thesis
proof
consider H2,v2 such that
A74: for j st j < i & x.j in variables_in H2 holds j = 3 or j = 4 and
A75: not x.0 in Free H2 and
A76: M,v2 |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) and
A77: def_func'(H,v1) = def_func'(H2,v2) by A2,A3,A4;
take H2,v2;
thus for j st j < i+1 & x.j in variables_in H2 holds j = 3 or j = 4
proof
let j;
assume that
A78: j < i+1 and
A79: x.j in variables_in H2;
j <= i by A78,NAT_1:13;
then j < i or j = i by XXREAL_0:1;
hence thesis by A73,A74,A79;
end;
thus thesis by A75,A76,A77;
end;
end;
hence thesis by A12,A5;
end;
A80: P[0]
proof
let H;
let v1 such that
A81: not x.0 in Free H and
A82: M,v1 |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
take H,v1;
thus thesis by A81,A82;
end;
for i being Nat holds P[i] from NAT_1:sch 2(A80,A1);
hence thesis;
end;
theorem
not x.0 in Free H1 & M,v1 |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0
))) implies ex H2,v2 st Free H1 /\ Free H2 c= {x.3,x.4} & not x.0 in Free H2 &
M,v2 |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) & def_func'(H1,v1) =
def_func'(H2,v2)
proof
assume that
A1: not x.0 in Free H1 and
A2: M,v1 |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0)));
consider i such that
A3: for j st x.j in variables_in H1 holds j < i by Th3;
consider H2,v2 such that
A4: for j st j < i & x.j in variables_in H2 holds j=3 or j=4 and
A5: not x.0 in Free H2 and
A6: M,v2 |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) and
A7: def_func'(H1,v1) = def_func'(H2,v2) by A1,A2,Th16;
take H2,v2;
thus Free H1 /\ Free H2 c= {x.3,x.4}
proof
A8: Free H2 c= variables_in H2 by ZF_LANG1:151;
let a be object;
A9: Free H1 c= variables_in H1 by ZF_LANG1:151;
assume
A10: a in Free H1 /\ Free H2;
then
A11: a in Free H2 by XBOOLE_0:def 4;
reconsider x = a as Variable by A10;
consider j such that
A12: x = x.j by ZF_LANG1:77;
a in Free H1 by A10,XBOOLE_0:def 4;
then j = 3 or j = 4 by A3,A4,A11,A12,A9,A8;
hence thesis by A12,TARSKI:def 2;
end;
thus thesis by A5,A6,A7;
end;
::
:: Definable functions
::
reserve F,G for Function;
theorem
F is_definable_in M & G is_definable_in M implies F*G is_definable_in M
proof
set x0 = x.0, x3 = x.3, x4 = x.4;
given H1 such that
A1: Free H1 c= { x.3,x.4 } and
A2: M |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) and
A3: F = def_func(H1,M);
given H2 such that
A4: Free H2 c= { x.3,x.4 } and
A5: M |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) and
A6: G = def_func(H2,M);
reconsider F,G as Function of M,M by A3,A6;
consider x such that
A7: not x in variables_in All(x.0,x.3,x.4,H1 '&' H2) by Th3;
A8: variables_in All(x.0,x.3,x.4,H1 '&' H2) = variables_in (H1 '&' H2) \/ {
x.0,x.3,x.4} by ZF_LANG1:149;
then
A9: not x in {x.0,x.3,x.4} by A7,XBOOLE_0:def 3;
then
A10: x <> x.3 by ENUMSET1:def 1;
take H = Ex(x,(H1/(x.3,x)) '&' (H2/(x.4,x)));
thus
A11: Free H c= {x.3,x.4}
proof
let a be object;
assume a in Free H;
then
A12: a in Free ((H1/(x.3,x)) '&' (H2/(x.4,x))) \ {x} by ZF_LANG1:66;
then a in Free ((H1/(x.3,x)) '&' (H2/(x.4,x))) by XBOOLE_0:def 5;
then a in Free (H1/(x.3,x)) \/ Free (H2/(x.4,x)) by ZF_LANG1:61;
then
Free (H1/(x.3,x)) c= (Free H1 \ {x.3}) \/ {x} & a in Free (H1/(x.3,x)
) or Free (H2/(x.4,x)) c= (Free H2 \ {x.4}) \/ {x} & a in Free (H2/(x.4,x)) by
Th1,XBOOLE_0:def 3;
then
A13: Free H1 \ {x.3} c= Free H1 & a in (Free H1 \ {x.3}) \/ {x} or Free H2
\ {x.4} c= Free H2 & a in (Free H2 \ {x.4}) \/ {x} by XBOOLE_1:36;
not a in {x} by A12,XBOOLE_0:def 5;
then
Free H1 \ {x.3} c= {x.3,x.4} & a in Free H1 \ {x.3} or Free H2 \ {x.4
} c= {x.3,x.4} & a in Free H2 \ {x.4} by A1,A4,A13,XBOOLE_0:def 3;
hence thesis;
end;
A14: x0 <> x4 by ZF_LANG1:76;
A15: x3 <> x4 by ZF_LANG1:76;
A16: x <> x.4 by A9,ENUMSET1:def 1;
variables_in (H1 '&' H2) = variables_in H1 \/ variables_in H2 by ZF_LANG1:141
;
then
A17: not x in variables_in H1 \/ variables_in H2 by A7,A8,XBOOLE_0:def 3;
then
A18: not x in variables_in H1 by XBOOLE_0:def 3;
A19: not x in variables_in H2 by A17,XBOOLE_0:def 3;
A20: x0 <> x3 by ZF_LANG1:76;
then
A21: not x0 in Free H2 by A4,A14,TARSKI:def 2;
thus
A22: M |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)))
proof
let v;
now
let m3 be Element of M;
M,v |= All(x3,Ex(x0,All(x4,H2 <=> x4 '=' x0))) by A5;
then M,v/(x3,m3) |= Ex(x0,All(x4,H2 <=> x4 '=' x0)) by ZF_LANG1:71;
then consider m0 being Element of M such that
A23: M,v/(x3,m3)/(x0,m0) |= All(x4,H2 <=> x4 '=' x0) by ZF_LANG1:73;
M,v |= All(x3,Ex(x0,All(x4,H1 <=> x4 '=' x0))) by A2;
then M,v/(x3,m0) |= Ex(x0,All(x4,H1 <=> x4 '=' x0)) by ZF_LANG1:71;
then consider m being Element of M such that
A24: M,v/(x3,m0)/(x0,m) |= All(x4,H1 <=> x4 '=' x0) by ZF_LANG1:73;
now
let m4 be Element of M;
A25: now
assume M,v/(x3,m3)/(x0,m)/(x4,m4) |= H;
then consider m9 being Element of M such that
A26: M,v/(x3,m3)/(x0,m)/(x4,m4)/(x,m9) |= (H1/(x3,x)) '&' (H2/(
x4,x)) by ZF_LANG1:73;
set v9 = v/(x3,m3)/(x0,m)/(x4,m4)/(x,m9);
A27: v9.x = m9 by FUNCT_7:128;
A28: v9/(x4,m9) = v/(x3,m3)/(x0,m)/(x,m9)/(x4,m9) by Th8
.= v/(x3,m3)/(x0,m)/(x4,m9)/(x,m9) by A16,FUNCT_7:33;
M,v9 |= H2/(x4,x) by A26,ZF_MODEL:15;
then M,v9/(x4,m9) |= H2 by A19,A27,Th12;
then
A29: M,v/(x3,m3)/(x0,m)/(x4,m9) |= H2 by A19,A28,Th5;
A30: v/(x3,m3)/(x4,m9)/(x0,m0) = v/(x3,m3)/(x4,m9)/(x0,m)/(x0,m0) by
FUNCT_7:34;
A31: v/(x3,m3)/(x0,m)/(x4,m4).x0 = v/(x3,m3)/(x0,m).x0 by FUNCT_7:32
,ZF_LANG1:76;
A32: v/(x3,m0)/(x0,m)/(x4,m4).x0 = v/(x3,m0)/(x0,m).x0 by FUNCT_7:32
,ZF_LANG1:76;
M,v9 |= H1/(x3,x) by A26,ZF_MODEL:15;
then
A33: M,v9/(x3,m9) |= H1 by A18,A27,Th12;
A34: v/(x3,m3)/(x0,m0)/(x4,m9) = v/(x3,m3)/(x4,m9)/(x0,m0) by FUNCT_7:33
,ZF_LANG1:76;
A35: M,v/(x3,m3)/(x0,m0)/(x4,m9) |= H2 <=> x4 '=' x0 by A23,ZF_LANG1:71;
A36: v/(x3,m3)/(x0,m0)/(x4,m9).x0 = v/(x3,m3)/(x0,m0).x0 by FUNCT_7:32
,ZF_LANG1:76;
v/(x3,m3)/(x0,m)/(x4,m9) = v/(x3,m3)/(x4,m9)/(x0,m) by FUNCT_7:33
,ZF_LANG1:76;
then M,v/(x3,m3)/(x0,m0)/(x4,m9) |= H2 by A21,A30,A34,A29,Th9;
then M,v/(x3,m3)/(x0,m0)/(x4,m9) |= x4 '=' x0 by A35,ZF_MODEL:19;
then
A37: v/(x3,m3)/(x0,m0)/(x4,m9).x4 = v/(x3,m3)/(x0,m0)/(x4,m9).x0 by
ZF_MODEL:12;
A38: v/(x3,m3)/(x0,m0).x0 = m0 by FUNCT_7:128;
v/(x3,m3)/(x0,m0)/(x4,m9).x4 = m9 by FUNCT_7:128;
then
v9/(x3,m9) = v/(x3,m3)/(x0,m)/(x4,m4)/(x3,m0)/(x,m9) by A10,A37,A38
,A36,FUNCT_7:33
.= v/(x0,m)/(x4,m4)/(x3,m0)/(x,m9) by Th8
.= v/(x3,m0)/(x0,m)/(x4,m4)/(x,m9) by A20,A14,A15,Th6;
then
A39: M,v/(x3,m0)/(x0,m)/(x4,m4) |= H1 by A18,A33,Th5;
M,v/(x3,m0)/(x0,m)/(x4,m4) |= H1 <=> x4 '=' x0 by A24,ZF_LANG1:71;
then M,v/(x3,m0)/(x0,m)/(x4,m4) |= x4 '=' x0 by A39,ZF_MODEL:19;
then
A40: v/(x3,m0)/(x0,m)/(x4,m4).x4 = v/(x3,m0)/(x0,m)/(x4,m4).x0 by
ZF_MODEL:12;
A41: v/(x3,m0)/(x0,m).x0 = m by FUNCT_7:128;
A42: v/(x3,m3)/(x0,m).x0 = m by FUNCT_7:128;
A43: v/(x3,m3)/(x0,m)/(x4,m4).x4 = m4 by FUNCT_7:128;
v/(x3,m0)/(x0,m)/(x4,m4).x4 = m4 by FUNCT_7:128;
hence M,v/(x3,m3)/(x0,m)/(x4,m4) |= x4 '=' x0 by A40,A41,A43,A42,A32
,A31,ZF_MODEL:12;
end;
now
set v9 = v/(x3,m3)/(x0,m)/(x4,m4)/(x,m0);
A44: v/(x3,m0)/(x0,m).x0 = m by FUNCT_7:128;
A45: v/(x3,m3)/(x0,m)/(x4,m4).x4 = m4 by FUNCT_7:128;
A46: M,v/(x3,m3)/(x0,m0)/(x4,m0) |= H2 <=> x4 '=' x0 by A23,ZF_LANG1:71;
A47: v/(x3,m3)/(x0,m)/(x4,m4).x0 = v/(x3,m3)/(x0,m).x0 by FUNCT_7:32
,ZF_LANG1:76;
assume M,v/(x3,m3)/(x0,m)/(x4,m4) |= x4 '=' x0;
then
A48: v/(x3,m3)/(x0,m)/(x4,m4).x4 = v/(x3,m3)/(x0,m)/(x4,m4).x0 by
ZF_MODEL:12;
A49: v/(x3,m3)/(x0,m).x0 = m by FUNCT_7:128;
A50: v/(x3,m3)/(x0,m0)/(x4,m0).x0 = v/(x3,m3)/(x0,m0).x0 by FUNCT_7:32
,ZF_LANG1:76;
A51: M,v/(x3,m0)/(x0,m)/(x4,m4) |= H1 <=> x4 '=' x0 by A24,ZF_LANG1:71;
A52: v/(x3,m0)/(x0,m)/(x4,m4).x0 = v/(x3,m0)/(x0,m).x0 by FUNCT_7:32
,ZF_LANG1:76;
v/(x3,m0)/(x0,m)/(x4,m4).x4 = m4 by FUNCT_7:128;
then M,v/(x3,m0)/(x0,m)/(x4,m4) |= x4 '=' x0 by A48,A44,A45,A49,A52
,A47,ZF_MODEL:12;
then M,v/(x3,m0)/(x0,m)/(x4,m4) |= H1 by A51,ZF_MODEL:19;
then
A53: M,v/(x3,m0)/(x0,m)/(x4,m4)/(x,m0) |= H1 by A18,Th5;
A54: v/(x3,m3)/(x0,m0).x0 = m0 by FUNCT_7:128;
v/(x3,m3)/(x0,m0)/(x4,m0).x4 = m0 by FUNCT_7:128;
then M,v/(x3,m3)/(x0,m0)/(x4,m0) |= x4 '=' x0 by A54,A50,ZF_MODEL:12;
then M,v/(x3,m3)/(x0,m0)/(x4,m0) |= H2 by A46,ZF_MODEL:19;
then
A55: M,v/(x3,m3)/(x0,m0)/(x4,m0)/(x0,m) |= H2 by A21,Th9;
A56: v/(x3,m3)/(x0,m)/(x4,m0) = v/(x3,m3)/(x4,m0)/(x0,m) by FUNCT_7:33
,ZF_LANG1:76;
v/(x3,m3)/(x0,m0)/(x4,m0)/(x0,m) = v/(x3,m3)/(x4,m0)/(x0,m) by Th8;
then
A57: M,v/(x3,m3)/(x0,m)/(x4,m0)/(x,m0) |= H2 by A19,A55,A56,Th5;
A58: v9.x = m0 by FUNCT_7:128;
v9/(x3,m0) = v/(x3,m3)/(x0,m)/(x4,m4)/(x3,m0)/(x,m0) by A10,
FUNCT_7:33
.= v/(x0,m)/(x4,m4)/(x3,m0)/(x,m0) by Th8
.= v/(x3,m0)/(x0,m)/(x4,m4)/(x,m0) by A20,A14,A15,Th6;
then
A59: M,v9 |= H1/(x3,x) by A18,A53,A58,Th12;
v9/(x4,m0) = v/(x3,m3)/(x0,m)/(x,m0)/(x4,m0) by Th8
.= v/(x3,m3)/(x0,m)/(x4,m0)/(x,m0) by A16,FUNCT_7:33;
then M,v9 |= H2/(x4,x) by A19,A57,A58,Th12;
then M,v9 |= (H1/(x3,x)) '&' (H2/(x4,x)) by A59,ZF_MODEL:15;
hence M,v/(x3,m3)/(x0,m)/(x4,m4) |= H by ZF_LANG1:73;
end;
hence M,v/(x3,m3)/(x0,m)/(x4,m4) |= H <=> x4 '=' x0 by A25,ZF_MODEL:19;
end;
then M,v/(x3,m3)/(x0,m) |= All(x4,H <=> x4 '=' x0) by ZF_LANG1:71;
hence M,v/(x3,m3) |= Ex(x0,All(x4,H <=> x4 '=' x0)) by ZF_LANG1:73;
end;
hence thesis by ZF_LANG1:71;
end;
now
let v;
thus M,v |= H implies (F*G).(v.x3) = v.x4
proof
assume M,v |= H;
then consider m such that
A60: M,v/(x,m) |= (H1/(x3,x)) '&' (H2/(x4,x)) by ZF_LANG1:73;
A61: v/(x,m).x = m by FUNCT_7:128;
M,v/(x,m) |= (H1/(x3,x)) by A60,ZF_MODEL:15;
then M,v/(x,m)/(x3,m) |= H1 by A18,A61,Th12;
then
A62: F.(v/(x,m)/(x3,m).x3) = v/(x,m)/(x3,m).x4 by A1,A2,A3,ZFMODEL1:def 2;
A63: v/(x,m)/(x3,m).x3 = m by FUNCT_7:128;
A64: v/(x,m)/(x4,m).x3 = v/(x,m).x3 by FUNCT_7:32,ZF_LANG1:76;
A65: v.x3 = v/(x,m).x3 by A10,FUNCT_7:32;
A66: v/(x,m)/(x3,m).x4 = v/(x,m).x4 by FUNCT_7:32,ZF_LANG1:76;
M,v/(x,m) |= (H2/(x4,x)) by A60,ZF_MODEL:15;
then M,v/(x,m)/(x4,m) |= H2 by A19,A61,Th12;
then
A67: G.(v/(x,m)/(x4,m).x3) = v/(x,m)/(x4,m).x4 by A4,A5,A6,ZFMODEL1:def 2;
A68: v/(x,m)/(x4,m).x4 = m by FUNCT_7:128;
v.x4 = v/(x,m).x4 by A16,FUNCT_7:32;
hence thesis by A62,A63,A67,A68,A66,A64,A65,FUNCT_2:15;
end;
set m = G.(v.x3);
A69: v/(x4,m).x4 = m by FUNCT_7:128;
A70: v/(x,m).x = m by FUNCT_7:128;
A71: v/(x,m)/(x4,m) = v/(x4,m)/(x,m) by A16,FUNCT_7:33;
v/(x4,m).x3 = v.x3 by FUNCT_7:32,ZF_LANG1:76;
then M,v/(x4,m) |= H2 by A4,A5,A6,A69,ZFMODEL1:def 2;
then M,v/(x,m)/(x4,m) |= H2 by A19,A71,Th5;
then
A72: M,v/(x,m) |= (H2/(x4,x)) by A19,A70,Th12;
A73: v/(x3,m).x3 = m by FUNCT_7:128;
assume (F*G).(v.x3) = v.x4;
then
A74: F.m = v.x4 by FUNCT_2:15;
A75: v/(x,m)/(x3,m) = v/(x3,m)/(x,m) by A10,FUNCT_7:33;
v/(x3,m).x4 = v.x4 by FUNCT_7:32,ZF_LANG1:76;
then M,v/(x3,m) |= H1 by A1,A2,A3,A74,A73,ZFMODEL1:def 2;
then M,v/(x,m)/(x3,m) |= H1 by A18,A75,Th5;
then M,v/(x,m) |= (H1/(x3,x)) by A18,A70,Th12;
then M,v/(x,m) |= (H1/(x3,x)) '&' (H2/(x4,x)) by A72,ZF_MODEL:15;
hence M,v |= H by ZF_LANG1:73;
end;
hence thesis by A11,A22,ZFMODEL1:def 2;
end;
theorem Th19:
not x.0 in Free H implies (M,v |= All(x.3,Ex(x.0,All(x.4,H <=>
x.4 '=' x.0))) iff for m1 ex m2 st for m3 holds M,v/(x.3,m1)/(x.4,m3) |= H iff
m3 = m2)
proof
assume
A1: not x.0 in Free H;
thus M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) implies for m1 ex m2
st for m3 holds M,v/(x.3,m1)/(x.4,m3) |= H iff m3 = m2
proof
assume
A2: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
let m1;
M,v/(x.3,m1) |= Ex(x.0,All(x.4,H <=> x.4 '=' x.0)) by A2,ZF_LANG1:71;
then consider m2 such that
A3: M,v/(x.3,m1)/(x.0,m2) |= All(x.4,H <=> x.4 '=' x.0) by ZF_LANG1:73;
take m2;
let m3;
thus M,v/(x.3,m1)/(x.4,m3) |= H implies m3 = m2
proof
assume M,v/(x.3,m1)/(x.4,m3) |= H;
then M,v/(x.3,m1)/(x.4,m3)/(x.0,m2) |= H by A1,Th9;
then
A4: M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= H by FUNCT_7:33,ZF_LANG1:76;
M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= H <=> x.4 '=' x.0 by A3,ZF_LANG1:71;
then
A5: M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= x.4 '=' x.0 by A4,ZF_MODEL:19;
A6: m2 = v/(x.3,m1)/(x.0,m2).(x.0) by FUNCT_7:128;
A7: v/(x.3,m1)/(x.0,m2)/(x.4,m3).(x.0) = v/(x.3,m1)/(x.0,m2).(x.0) by
FUNCT_7:32,ZF_LANG1:76;
v/(x.3,m1)/(x.0,m2)/(x.4,m3).(x.4) = m3 by FUNCT_7:128;
hence thesis by A6,A7,A5,ZF_MODEL:12;
end;
assume m3 = m2;
then
A8: M,v/(x.3,m1)/(x.0,m3)/(x.4,m3) |= H <=> x.4 '=' x.0 by A3,ZF_LANG1:71;
A9: v/(x.3,m1)/(x.0,m3)/(x.4,m3).(x.0) = v/(x.3,m1)/(x.0,m3).(x.0) by
FUNCT_7:32,ZF_LANG1:76;
A10: v/(x.3,m1)/(x.0,m3).(x.0) = m3 by FUNCT_7:128;
v/(x.3,m1)/(x.0,m3)/(x.4,m3).(x.4) = m3 by FUNCT_7:128;
then M,v/(x.3,m1)/(x.0,m3)/(x.4,m3) |= x.4 '=' x.0 by A9,A10,ZF_MODEL:12;
then M,v/(x.3,m1)/(x.0,m3)/(x.4,m3) |= H by A8,ZF_MODEL:19;
then M,v/(x.3,m1)/(x.4,m3)/(x.0,m3) |= H by FUNCT_7:33,ZF_LANG1:76;
hence thesis by A1,Th9;
end;
assume
A11: for m1 ex m2 st for m3 holds M,v/(x.3,m1)/(x.4,m3) |= H iff m3 = m2;
now
let m1;
consider m2 such that
A12: M,v/(x.3,m1)/(x.4,m3) |= H iff m3 = m2 by A11;
now
let m3;
A13: v/(x.3,m1)/(x.0,m2)/(x.4,m3).(x.0) = v/(x.3,m1)/(x.0,m2).(x.0) by
FUNCT_7:32,ZF_LANG1:76;
A14: v/(x.3,m1)/(x.0,m2).(x.0) = m2 by FUNCT_7:128;
A15: v/(x.3,m1)/(x.0,m2)/(x.4,m3).(x.4) = m3 by FUNCT_7:128;
A16: now
assume M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= x.4 '=' x.0;
then m3 = m2 by A15,A13,A14,ZF_MODEL:12;
then M,v/(x.3,m1)/(x.4,m3) |= H by A12;
then M,v/(x.3,m1)/(x.4,m3)/(x.0,m2) |= H by A1,Th9;
hence M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= H by FUNCT_7:33,ZF_LANG1:76;
end;
now
assume M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= H;
then M,v/(x.3,m1)/(x.4,m3)/(x.0,m2) |= H by FUNCT_7:33,ZF_LANG1:76;
then M,v/(x.3,m1)/(x.4,m3) |= H by A1,Th9;
then m3 = m2 by A12;
hence M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= x.4 '=' x.0 by A15,A13,A14,
ZF_MODEL:12;
end;
hence M,v/(x.3,m1)/(x.0,m2)/(x.4,m3) |= H <=> x.4 '=' x.0 by A16,
ZF_MODEL:19;
end;
then M,v/(x.3,m1)/(x.0,m2) |= All(x.4,H <=> x.4 '=' x.0) by ZF_LANG1:71;
hence M,v/(x.3,m1) |= Ex(x.0,All(x.4,H <=> x.4 '=' x.0)) by ZF_LANG1:73;
end;
hence thesis by ZF_LANG1:71;
end;
theorem
F is_definable_in M & G is_definable_in M & Free H c= {x.3} implies
for FG be Function st dom FG = M & for v holds (M,v |= H implies FG.(v.x.3) = F
.(v.x.3)) & (M,v |= 'not' H implies FG.(v.x.3) = G.(v.x.3)) holds FG
is_definable_in M
proof
A1: {x.3,x.3,x.4} = {x.3,x.4} by ENUMSET1:30;
A2: {x.3} \/ {x.3,x.4} = {x.3,x.3,x.4} by ENUMSET1:2;
given H1 such that
A3: Free H1 c= {x.3,x.4} and
A4: M |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) and
A5: F = def_func(H1,M);
given H2 such that
A6: Free H2 c= {x.3,x.4} and
A7: M |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) and
A8: G = def_func(H2,M);
assume
A9: Free H c= {x.3};
then
A10: not x.4 in Free H by Lm3,TARSKI:def 1;
let FG be Function such that
A11: dom FG = M and
A12: for v holds (M,v |= H implies FG.(v.x.3) = F.(v.x.3)) & (M,v |=
'not' H implies FG.(v.x.3) = G.(v.x.3));
rng FG c= M
proof
set v = the Function of VAR,M;
let a be object;
assume a in rng FG;
then consider b being object such that
A13: b in M and
A14: a = FG.b by A11,FUNCT_1:def 3;
reconsider b as Element of M by A13;
A15: M,v/(x.3,b) |= H or M,v/(x.3,b) |= 'not' H by ZF_MODEL:14;
v/(x.3,b).(x.3) = b by FUNCT_7:128;
then FG.b = def_func(H1,M).b or FG.b = def_func(H2,M).b by A5,A8,A12,A15;
hence thesis by A14;
end;
then reconsider f = FG as Function of M,M by A11,FUNCT_2:def 1,RELSET_1:4;
take I = H '&' H1 'or' 'not' H '&' H2;
A16: Free ('not' H) = Free H by ZF_LANG1:60;
Free (H '&' H1) = Free H \/ Free H1 by ZF_LANG1:61;
then
A17: Free (H '&' H1) c= {x.3,x.4} by A3,A9,A2,A1,XBOOLE_1:13;
A18: not x.0 in Free H2 by A6,Lm1,Lm2,TARSKI:def 2;
A19: not x.0 in Free H1 by A3,Lm1,Lm2,TARSKI:def 2;
Free ('not' H '&' H2) = Free ('not' H) \/ Free H2 by ZF_LANG1:61;
then
A20: Free ('not' H '&' H2) c= {x.3,x.4} by A6,A9,A16,A2,A1,XBOOLE_1:13;
A21: Free I = Free (H '&' H1) \/ Free ('not' H '&' H2) by ZF_LANG1:63;
hence Free I c= {x.3,x.4} by A17,A20,XBOOLE_1:8;
then
A22: not x.0 in Free I by Lm1,Lm2,TARSKI:def 2;
A23: now
let v;
now
let m3;
M,v |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) by A4;
then consider m1 such that
A24: M,v/(x.3,m3)/(x.4,m4) |= H1 iff m4 = m1 by A19,Th19;
M,v |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) by A7;
then consider m2 such that
A25: M,v/(x.3,m3)/(x.4,m4) |= H2 iff m4 = m2 by A18,Th19;
not M,v/(x.3,m3) |= 'not' H & M,v/(x.3,m3) |= H or M,v/(x.3,m3) |=
'not' H & not M,v/(x.3,m3) |= H by ZF_MODEL:14;
then consider m such that
A26: not M,v/(x.3,m3) |= 'not' H & M,v/(x.3,m3) |= H & m = m1 or M,v
/(x.3,m3) |= 'not' H & m = m2 & not M,v/(x.3,m3) |= H;
take m;
let m4;
thus M,v/(x.3,m3)/(x.4,m4) |= I implies m4 = m
proof
assume M,v/(x.3,m3)/(x.4,m4) |= I;
then M,v/(x.3,m3)/(x.4,m4) |= H '&' H1 or M,v/(x.3,m3)/(x.4,m4) |=
'not' H '&' H2 by ZF_MODEL:17;
then
M,v/(x.3,m3)/(x.4,m4) |= H & M,v/(x.3,m3)/(x.4,m4) |= H1 or M,v/(
x.3,m3)/(x.4,m4) |= 'not' H & M,v/(x.3,m3)/(x.4,m4) |= H2 by ZF_MODEL:15;
hence thesis by A10,A16,A24,A25,A26,Th9;
end;
assume m4 = m;
then
M,v/(x.3,m3)/(x.4,m4) |= H & M,v/(x.3,m3)/(x.4,m4) |= H1 or M,v/(x.
3,m3)/(x.4,m4) |= 'not' H & M,v/(x.3,m3)/(x.4,m4) |= H2 by A10,A16,A24,A25,A26
,Th9;
then
M,v/(x.3,m3)/(x.4,m4) |= H '&' H1 or M,v/(x.3,m3)/(x.4,m4) |= 'not'
H '&' H2 by ZF_MODEL:15;
hence M,v/(x.3,m3)/(x.4,m4) |= I by ZF_MODEL:17;
end;
hence M,v |= All(x.3,Ex(x.0,All(x.4,I <=> x.4 '=' x.0))) by A22,Th19;
end;
hence
A27: M |= All(x.3,Ex(x.0,All(x.4,I <=> x.4 '=' x.0)));
now
set v = the Function of VAR,M;
let a be Element of M;
set m4 = def_func(I,M).a;
A28: M,v |= All(x.3,Ex(x.0,All(x.4,I <=> x.4 '=' x.0))) by A23;
def_func(I,M) = def_func'(I,v) by A21,A17,A20,A27,Th11,XBOOLE_1:8;
then M,v/(x.3,a)/(x.4,m4) |= I by A22,A28,Th10;
then M,v/(x.3,a)/(x.4,m4) |= H '&' H1 or M,v/(x.3,a)/(x.4,m4) |= 'not' H
'&' H2 by ZF_MODEL:17;
then M,v/(x.3,a)/(x.4,m4) |= H & M,v/(x.3,a)/(x.4,m4) |= H1 & M,v |= All(
x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) & def_func(H1,M) = def_func'(H1,v) or
M,v/(x.3,a)/(x.4,m4) |= 'not' H & M,v/(x.3,a)/(x.4,m4) |= H2 & M,v |= All(x.3,
Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) & def_func(H2,M) = def_func'(H2,v) by A3
,A4,A6,A7,Th11,ZF_MODEL:15;
then
A29: M,v/(x.3,a) |= H & m4 = F.a or M,v/(x.3,a) |= 'not' H & m4 = G.a by A5,A8
,A10,A16,A19,A18,Th9,Th10;
v/(x.3,a).(x.3) = a by FUNCT_7:128;
hence f.a = def_func(I,M).a by A12,A29;
end;
hence thesis by FUNCT_2:63;
end;
theorem
F is_parametrically_definable_in M & G is_parametrically_definable_in
M implies G*F is_parametrically_definable_in M
proof
given H1 being ZF-formula, v1 being Function of VAR,M such that
A1: {x.0,x.1,x.2} misses Free H1 and
A2: M,v1 |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) and
A3: F = def_func'(H1,v1);
given H2 being ZF-formula, v2 being Function of VAR,M such that
A4: {x.0,x.1,x.2} misses Free H2 and
A5: M,v2 |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) and
A6: G = def_func'(H2,v2);
reconsider F9 = F, G9 = G as Function of M,M by A3,A6;
deffunc G(object) = v2.$1;
consider i such that
A7: for j st x.j in variables_in H2 holds j < i by Th3;
i > 4 or not i > 4;
then consider i3 being Element of NAT such that
A8: i > 4 & i3 = i or not i > 4 & i3 = 5;
A9: x.0 in {x.0,x.1,x.2} by ENUMSET1:def 1;
then not x.0 in Free H1 by A1,XBOOLE_0:3;
then consider H3 being ZF-formula, v3 being Function of VAR,M such that
A10: for j st j < i3 & x.j in variables_in H3 holds j = 3 or j = 4 and
A11: not x.0 in Free H3 and
A12: M,v3 |= All(x.3,Ex(x.0,All(x.4,H3 <=> x.4 '=' x.0))) and
A13: def_func'(H1,v1) = def_func'(H3,v3) by A2,Th16;
consider k1 being Element of NAT such that
A14: for j st x.j in variables_in H3 holds j < k1 by Th3;
k1 > i3 or k1 <= i3;
then consider k being Element of NAT such that
A15: k1 > i3 & k = k1 or k1 <= i3 & k = i3+1;
deffunc F(object) = v3.$1;
defpred C[object] means $1 in Free H3;
take H = Ex(x.k,(H3/(x.4,x.k)) '&' (H2/(x.3,x.k)));
consider v being Function such that
A16: dom v = VAR &
for a being object st a in VAR holds (C[a] implies v.a = F(a)) & (
not C[a] implies v.a = G(a)) from PARTFUN1:sch 1;
rng v c= M
proof
let b be object;
assume b in rng v;
then consider a being object such that
A17: a in dom v and
A18: b = v.a by FUNCT_1:def 3;
reconsider a as Variable by A16,A17;
b = v3.a or b = v2.a by A16,A18;
hence thesis;
end;
then reconsider v as Function of VAR,M by A16,FUNCT_2:def 1,RELSET_1:4;
take v;
A19: {x.0,x.1,x.2} misses Free H3
proof
A20: i3 > 2 by A8,XXREAL_0:2;
A21: i3 > 1 by A8,XXREAL_0:2;
assume {x.0,x.1,x.2} meets Free H3;
then consider a being object such that
A22: a in {x.0,x.1,x.2} and
A23: a in Free H3 by XBOOLE_0:3;
A24: Free H3 c= variables_in H3 by ZF_LANG1:151;
a = x.0 or a = x.1 or a = x.2 by A22,ENUMSET1:def 1;
hence contradiction by A10,A21,A20,A23,A24;
end;
A25: now
let a be object;
assume
A26: a in {x.0,x.1,x.2};
assume a in Free H;
then
A27: a in Free ((H3/(x.4,x.k)) '&' (H2/(x.3,x.k))) \ {x.k} by ZF_LANG1:66;
then
A28: not a in {x.k} by XBOOLE_0:def 5;
A29: Free ((H3/(x.4,x.k)) '&' (H2/(x.3,x.k))) = Free (H3/(x.4,x.k)) \/
Free (H2/(x.3,x.k)) by ZF_LANG1:61;
a in Free ((H3/(x.4,x.k)) '&' (H2/(x.3,x.k))) by A27,XBOOLE_0:def 5;
then
Free (H3/(x.4,x.k)) c= (Free H3 \ {x.4}) \/ {x.k} & a in Free (H3/(x.
4,x.k)) or a in Free (H2/(x.3,x.k)) & Free (H2/(x.3,x.k)) c= (Free H2 \ {x.3})
\/ {x.k} by A29,Th1,XBOOLE_0:def 3;
then a in Free H3 \ {x.4} or a in Free H2 \ {x.3} by A28,XBOOLE_0:def 3;
then a in Free H3 or a in Free H2 by XBOOLE_0:def 5;
hence contradiction by A4,A19,A26,XBOOLE_0:3;
end;
hence {x.0,x.1,x.2} misses Free H by XBOOLE_0:3;
x.0 in {x.0,x.1,x.2} by ENUMSET1:def 1;
then
A30: not x.0 in Free H by A25;
A31: k <> 4 by A8,A15,NAT_1:13;
then
A32: x.k <> x.4 by ZF_LANG1:76;
A33: i <= i3 by A8,XXREAL_0:2;
A34: not x.k in variables_in H2
proof
assume not thesis;
then k < i by A7;
hence contradiction by A33,A15,NAT_1:13,XXREAL_0:2;
end;
A35: x in Free H2 implies not x in Free H3 or x = x.3 or x = x.4
proof
A36: Free H3 c= variables_in H3 by ZF_LANG1:151;
assume that
A37: x in Free H2 and
A38: x in Free H3;
consider j such that
A39: x = x.j by ZF_LANG1:77;
Free H2 c= variables_in H2 by ZF_LANG1:151;
then j < i3 by A7,A33,A39,A37,XXREAL_0:2;
hence thesis by A10,A36,A39,A38;
end;
A40: k <> 3 by A8,A15,NAT_1:13,XXREAL_0:2;
then
A41: x.k <> x.3 by ZF_LANG1:76;
A42: not x.k in variables_in H3
proof
assume not thesis;
then k < k1 by A14;
hence contradiction by A15,NAT_1:13;
end;
A43: not x.0 in Free H2 by A4,A9,XBOOLE_0:3;
now
let m1;
A44: not x.3 in variables_in (H2/(x.3,x.k)) by A40,ZF_LANG1:76,184;
consider m such that
A45: M,v3/(x.3,m1)/(x.4,m4) |= H3 iff m4 = m by A11,A12,Th19;
A46: now
let x;
assume
A47: x in Free (H3/(x.4,x.k));
Free (H3/(x.4,x.k)) c= (Free H3 \ {x.4}) \/ {x.k} by Th1;
then x in Free H3 \ {x.4} or x in {x.k} by A47,XBOOLE_0:def 3;
then x in Free H3 & not x in {x.4} or x = x.k by TARSKI:def 1
,XBOOLE_0:def 5;
then (x in Free H3 & x.3 <> x & x <> x.k or x = x.4 or x = x.3) & x <>
x.4 or v/(x.3,m1)/(x.k,m).x = m & v3/(x.3,m1)/(x.k,m).x = m by FUNCT_7:128
,TARSKI:def 1;
then v/(x.3,m1)/(x.k,m).x = v/(x.3,m1).x & v/(x.3,m1).x = v.x & v.x =
v3.x & v3.x = v3/(x.3,m1).x & v3/(x.3,m1).x = v3/(x.3,m1)/(x.k,m).x or v/(x.3,
m1)/(x.k,m).x = v/(x.3,m1).x & v/(x.3,m1).x = m1 & m1 = v3/(x.3,m1).x & v3/(x.3
,m1).x = v3/(x.3,m1)/(x.k,m).x or v/(x.3,m1)/(x.k,m).x = v3/(x.3,m1)/(x.k,m).x
by A41,A16,FUNCT_7:32,128;
hence v/(x.3,m1)/(x.k,m).x = v3/(x.3,m1)/(x.k,m).x;
end;
consider r being Element of M such that
A48: M,v2/(x.3,m)/(x.4,m4) |= H2 iff m4 = r by A5,A43,Th19;
take r;
let m3;
A49: v3/(x.3,m1)/(x.4,m).(x.4) = m by FUNCT_7:128;
thus M,v/(x.3,m1)/(x.4,m3) |= H implies m3 = r
proof
A50: now
let x;
assume x in Free H2;
then not x in Free H3 & x <> x.3 & x <> x.4 or x = x.3 or x = x.4 by
A35;
then
v/(x.3,m)/(x.4,m3).x = v/(x.3,m).x & v/(x.3,m).x = v.x & v.x = v2
.x & v2.x = v2/(x.3,m).x & v2/(x.3,m).x = v2/(x.3,m)/(x.4,m3).x or v/(x.3,m)/(
x.4,m3).x = v/(x.3,m).x & v/(x.3,m).x = m & v2/(x.3,m)/(x.4,m3).x = v2/(x.3,m).
x & v2/(x.3,m).x = m or v/(x.3,m)/(x.4,m3).x = m3 & v2/(x.3,m)/(x.4,m3).x = m3
by A16,Lm3,FUNCT_7:32,128;
hence v/(x.3,m)/(x.4,m3).x = v2/(x.3,m)/(x.4,m3).x;
end;
assume M,v/(x.3,m1)/(x.4,m3) |= H;
then consider n being Element of M such that
A51: M,v/(x.3,m1)/(x.4,m3)/(x.k,n) |= (H3/(x.4,x.k)) '&' (H2/(x.3,x.
k)) by ZF_LANG1:73;
A52: now
let x;
assume
A53: x in Free H3;
A54: v/(x.3,m1)/(x.4,n).(x.4) = n by FUNCT_7:128;
A55: v3/(x.3,m1)/(x.4,n).(x.3) = v3/(x.3,m1).(x.3) by FUNCT_7:32,ZF_LANG1:76
;
A56: v/(x.3,m1)/(x.4,n).(x.3) = v/(x.3,m1).(x.3) by FUNCT_7:32,ZF_LANG1:76;
A57: v/(x.3,m1).(x.3) = m1 by FUNCT_7:128;
x = x.3 or x = x.4 or x <> x.3 & x <> x.4;
then
v/(x.3,m1)/(x.4,n).x = v3/(x.3,m1)/(x.4,n).x or v/(x.3,m1).x = v.
x & v3/(x.3,m1).x = v3.x & v/(x.3,m1)/(x.4,n).x = v/(x.3,m1).x & v3/(x.3,m1)/(
x.4,n).x = v3/(x.3,m1).x by A54,A57,A56,A55,FUNCT_7:32,128;
hence v/(x.3,m1)/(x.4,n).x = v3/(x.3,m1)/(x.4,n).x by A16,A53;
end;
A58: M,v/(x.3,m1)/(x.4,m3)/(x.k,n) |= H2/(x.3,x.k) by A51,ZF_MODEL:15;
A59: v/(x.3,m1)/(x.4,m3)/(x.k,n).(x.k) = n by FUNCT_7:128;
M,v/(x.3,m1)/(x.4,m3)/(x.k,n) |= H3/(x.4,x.k) by A51,ZF_MODEL:15;
then M,v/(x.3,m1)/(x.4,m3)/(x.k,n)/(x.4,n) |= H3 by A42,A59,Th12;
then M,v/(x.3,m1)/(x.k,n)/(x.4,n) |= H3 by Th8;
then M,v/(x.3,m1)/(x.4,n)/(x.k,n) |= H3 by A31,FUNCT_7:33,ZF_LANG1:76;
then M,v/(x.3,m1)/(x.4,n) |= H3 by A42,Th5;
then M,v3/(x.3,m1)/(x.4,n) |= H3 by A52,ZF_LANG1:75;
then n = m by A45;
then M,v/(x.3,m1)/(x.4,m3)/(x.k,m)/(x.3,m) |= H2 by A34,A59,A58,Th12;
then M,v/(x.4,m3)/(x.k,m)/(x.3,m) |= H2 by Th8;
then M,v/(x.3,m)/(x.4,m3)/(x.k,m) |= H2 by A41,A32,Lm3,Th6;
then M,v/(x.3,m)/(x.4,m3) |= H2 by A34,Th5;
then M,v2/(x.3,m)/(x.4,m3) |= H2 by A50,ZF_LANG1:75;
hence thesis by A48;
end;
assume m3 = r;
then
A60: M,v2/(x.3,m)/(x.4,m3) |= H2 by A48;
A61: v2/(x.3,m).(x.3) = m by FUNCT_7:128;
A62: now
let x;
assume
A63: x in Free (H2/(x.3,x.k));
Free (H2/(x.3,x.k)) c= (Free H2 \ {x.3}) \/ {x.k} by Th1;
then x in Free H2 \ {x.3} or x in {x.k} by A63,XBOOLE_0:def 3;
then x in Free H2 & not x in {x.3} or x = x.k by TARSKI:def 1
,XBOOLE_0:def 5;
then (not x in Free H3 & x.4 <> x & x <> x.k or x = x.3 or x = x.4) & x
<> x.3 or v/(x.4,m3)/(x.k,m).x = m & v2/(x.4,m3)/(x.k,m).x = m by A35,
FUNCT_7:128,TARSKI:def 1;
then v/(x.4,m3)/(x.k,m).x = v/(x.4,m3).x & v/(x.4,m3).x = v.x & v.x =
v2.x & v2.x = v2/(x.4,m3).x & v2/(x.4,m3).x = v2/(x.4,m3)/(x.k,m).x or v/(x.4,
m3)/(x.k,m).x = v/(x.4,m3).x & v/(x.4,m3).x = m3 & m3 = v2/(x.4,m3).x & v2/(x.4
,m3).x = v2/(x.4,m3)/(x.k,m).x or v/(x.4,m3)/(x.k,m).x = v2/(x.4,m3)/(x.k,m).x
by A32,A16,FUNCT_7:32,128;
hence v/(x.4,m3)/(x.k,m).x = v2/(x.4,m3)/(x.k,m).x;
end;
A64: not x.4 in variables_in (H3/(x.4,x.k)) by A31,ZF_LANG1:76,184;
M,v3/(x.3,m1)/(x.4,m) |= H3 by A45;
then M,v3/(x.3,m1)/(x.4,m)/(x.k,m) |= H3/(x.4,x.k) by A42,A49,Th13;
then M,v3/(x.3,m1)/(x.k,m)/(x.4,m) |= H3/(x.4,x.k) by A31,FUNCT_7:33
,ZF_LANG1:76;
then M,v3/(x.3,m1)/(x.k,m) |= H3/(x.4,x.k) by A64,Th5;
then M,v/(x.3,m1)/(x.k,m) |= H3/(x.4,x.k) by A46,ZF_LANG1:75;
then M,v/(x.3,m1)/(x.k,m)/(x.4,m3) |= H3/(x.4,x.k) by A64,Th5;
then
A65: M,v/(x.3,m1)/(x.4,m3)/(x.k,m) |= H3/(x.4,x.k) by A31,FUNCT_7:33
,ZF_LANG1:76;
v2/(x.3,m)/(x.4,m3).(x.3) = v2/(x.3,m).(x.3) by FUNCT_7:32,ZF_LANG1:76;
then M,v2/(x.3,m)/(x.4,m3)/(x.k,m) |= H2/(x.3,x.k) by A34,A61,A60,Th13;
then M,v2/(x.4,m3)/(x.k,m)/(x.3,m) |= H2/(x.3,x.k) by A41,A32,Lm3,Th6;
then M,v2/(x.4,m3)/(x.k,m) |= H2/(x.3,x.k) by A44,Th5;
then M,v/(x.4,m3)/(x.k,m) |= H2/(x.3,x.k) by A62,ZF_LANG1:75;
then M,v/(x.4,m3)/(x.k,m)/(x.3,m1) |= H2/(x.3,x.k) by A44,Th5;
then M,v/(x.3,m1)/(x.4,m3)/(x.k,m) |= H2/(x.3,x.k) by A41,A32,Lm3,Th6;
then M,v/(x.3,m1)/(x.4,m3)/(x.k,m) |= (H3/(x.4,x.k)) '&' (H2/(x.3,x.k))
by A65,ZF_MODEL:15;
hence M,v/(x.3,m1)/(x.4,m3) |= H by ZF_LANG1:73;
end;
hence
A66: M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) by A30,Th19;
now
let a be object;
assume a in M;
then reconsider m1 = a as Element of M;
set m3 = def_func'(H,v).m1;
A67: (G9*F9).m1 = G9.(F9.m1) by FUNCT_2:15;
M,v/(x.3,m1)/(x.4,m3) |= H by A30,A66,Th10;
then consider n being Element of M such that
A68: M,v/(x.3,m1)/(x.4,m3)/(x.k,n) |= (H3/(x.4,x.k)) '&' (H2/(x.3,x.k
)) by ZF_LANG1:73;
A69: now
let x;
assume
A70: x in Free H3;
A71: v/(x.3,m1)/(x.4,n).(x.4) = n by FUNCT_7:128;
A72: v3/(x.3,m1)/(x.4,n).(x.3) = v3/(x.3,m1).(x.3) by FUNCT_7:32,ZF_LANG1:76;
A73: v/(x.3,m1)/(x.4,n).(x.3) = v/(x.3,m1).(x.3) by FUNCT_7:32,ZF_LANG1:76;
A74: v/(x.3,m1).(x.3) = m1 by FUNCT_7:128;
x = x.3 or x = x.4 or x <> x.3 & x <> x.4;
then v/(x.3,m1)/(x.4,n).x = v3/(x.3,m1)/(x.4,n).x or v/(x.3,m1).x = v.x
& v3/(x.3,m1).x = v3.x & v/(x.3,m1)/(x.4,n).x = v/(x.3,m1).x & v3/(x.3,m1)/(x.4
,n).x = v3/(x.3,m1).x by A71,A74,A73,A72,FUNCT_7:32,128;
hence v/(x.3,m1)/(x.4,n).x = v3/(x.3,m1)/(x.4,n).x by A16,A70;
end;
A75: now
let x;
assume x in Free H2;
then not x in Free H3 & x <> x.3 & x <> x.4 or x = x.3 or x = x.4 by A35;
then v/(x.3,n)/(x.4,m3).x = v/(x.3,n).x & v/(x.3,n).x = v.x & v.x = v2.
x & v2.x = v2/(x.3,n).x & v2/(x.3,n).x = v2/(x.3,n)/(x.4,m3).x or v/(x.3,n)/(x.
4,m3).x = v/(x.3,n).x & v/(x.3,n).x = n & v2/(x.3,n)/(x.4,m3).x = v2/(x.3,n).x
& v2/(x.3,n).x = n or v/(x.3,n)/(x.4,m3).x = m3 & v2/(x.3,n)/(x.4,m3).x = m3
by A16,Lm3,FUNCT_7:32,128;
hence v/(x.3,n)/(x.4,m3).x = v2/(x.3,n)/(x.4,m3).x;
end;
A76: v/(x.3,m1)/(x.4,m3)/(x.k,n).(x.k) = n by FUNCT_7:128;
M,v/(x.3,m1)/(x.4,m3)/(x.k,n) |= H2/(x.3,x.k) by A68,ZF_MODEL:15;
then M,v/(x.3,m1)/(x.4,m3)/(x.k,n)/(x.3,n) |= H2 by A34,A76,Th12;
then M,v/(x.4,m3)/(x.k,n)/(x.3,n) |= H2 by Th8;
then M,v/(x.3,n)/(x.4,m3)/(x.k,n) |= H2 by A41,A32,Lm3,Th6;
then M,v/(x.3,n)/(x.4,m3) |= H2 by A34,Th5;
then M,v2/(x.3,n)/(x.4,m3) |= H2 by A75,ZF_LANG1:75;
then
A77: G9.n = m3 by A5,A6,A43,Th10;
M,v/(x.3,m1)/(x.4,m3)/(x.k,n) |= H3/(x.4,x.k) by A68,ZF_MODEL:15;
then M,v/(x.3,m1)/(x.4,m3)/(x.k,n)/(x.4,n) |= H3 by A42,A76,Th12;
then M,v/(x.3,m1)/(x.k,n)/(x.4,n) |= H3 by Th8;
then M,v/(x.3,m1)/(x.4,n)/(x.k,n) |= H3 by A31,FUNCT_7:33,ZF_LANG1:76;
then M,v/(x.3,m1)/(x.4,n) |= H3 by A42,Th5;
then M,v3/(x.3,m1)/(x.4,n) |= H3 by A69,ZF_LANG1:75;
hence (G9*F9).a = def_func'(H,v).a by A3,A11,A12,A13,A77,A67,Th10;
end;
hence thesis by FUNCT_2:12;
end;
theorem
{x.0,x.1,x.2} misses Free H1 & M,v |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.
4 '=' x.0))) & {x.0,x.1,x.2} misses Free H2 & M,v |= All(x.3,Ex(x.0,All(x.4,H2
<=> x.4 '=' x.0))) & {x.0,x.1,x.2} misses Free H & not x.4 in Free H implies
for FG be Function st dom FG = M & for m holds (M,v/(x.3,m) |= H implies FG.m =
def_func'(H1,v).m) & (M,v/(x.3,m) |= 'not' H implies FG.m = def_func'(H2,v).m)
holds FG is_parametrically_definable_in M
proof
assume that
A1: {x.0,x.1,x.2} misses Free H1 and
A2: M,v |= All(x.3,Ex(x.0,All(x.4,H1 <=> x.4 '=' x.0))) and
A3: {x.0,x.1,x.2} misses Free H2 and
A4: M,v |= All(x.3,Ex(x.0,All(x.4,H2 <=> x.4 '=' x.0))) and
A5: {x.0,x.1,x.2} misses Free H and
A6: not x.4 in Free H;
let FG be Function such that
A7: dom FG = M and
A8: (M,v/(x.3,m) |= H implies FG.m = def_func'(H1,v).m) & (M,v/(x.3,m)
|= 'not' H implies FG.m = def_func'(H2,v).m);
rng FG c= M
proof
let a be object;
assume a in rng FG;
then consider b being object such that
A9: b in M and
A10: a = FG.b by A7,FUNCT_1:def 3;
reconsider b as Element of M by A9;
M,v/(x.3,b) |= H or M,v/(x.3,b) |= 'not' H by ZF_MODEL:14;
then a = def_func'(H1,v).b or a = def_func'(H2,v).b by A8,A10;
hence thesis;
end;
then reconsider f = FG as Function of M,M by A7,FUNCT_2:def 1,RELSET_1:4;
A11: x.0 in {x.0,x.1,x.2} by ENUMSET1:def 1;
then
A12: not x.0 in Free H1 by A1,XBOOLE_0:3;
take p = H '&' H1 'or' 'not' H '&' H2, v;
A13: Free 'not' H = Free H by ZF_LANG1:60;
A14: now
let x be set;
A15: Free ('not' H '&' H2) = Free 'not' H \/ Free H2 by ZF_LANG1:61;
assume x in Free p;
then x in Free (H '&' H1) \/ Free ('not' H '&' H2) by ZF_LANG1:63;
then
A16: x in Free (H '&' H1) or x in Free ('not' H '&' H2) by XBOOLE_0:def 3;
Free (H '&' H1) = Free H \/ Free H1 by ZF_LANG1:61;
hence x in Free H or x in Free H1 or x in Free H2 by A13,A16,A15,
XBOOLE_0:def 3;
end;
now
let a be object;
assume that
A17: a in {x.0,x.1,x.2} and
A18: a in Free p;
a in Free H or a in Free H1 or a in Free H2 by A14,A18;
hence contradiction by A1,A3,A5,A17,XBOOLE_0:3;
end;
hence {x.0,x.1,x.2} misses Free p by XBOOLE_0:3;
A19: not x.0 in Free H2 by A3,A11,XBOOLE_0:3;
not x.0 in Free H by A5,A11,XBOOLE_0:3;
then
A20: not x.0 in Free p by A14,A12,A19;
now
let m3;
consider r1 being Element of M such that
A21: M,v/(x.3,m3)/(x.4,m4) |= H1 iff m4 = r1 by A2,A12,Th19;
consider r2 being Element of M such that
A22: M,v/(x.3,m3)/(x.4,m4) |= H2 iff m4 = r2 by A4,A19,Th19;
M,v/(x.3,m3) |= H & not M,v/(x.3,m3) |= 'not' H or not M,v/(x.3,m3)
|= H & M,v/(x.3,m3) |= 'not' H by ZF_MODEL:14;
then consider r being Element of M such that
A23: M,v/(x.3,m3) |= H & not M,v/(x.3,m3) |= 'not' H & r = r1 or not M
,v/(x.3,m3) |= H & M,v/(x.3,m3) |= 'not' H & r = r2;
take r;
let m4;
thus M,v/(x.3,m3)/(x.4,m4) |= p implies m4 = r
proof
assume M,v/(x.3,m3)/(x.4,m4) |= p;
then
M,v/(x.3,m3)/(x.4,m4) |= H '&' H1 or M,v/(x.3,m3)/(x.4,m4) |= 'not'
H '&' H2 by ZF_MODEL:17;
then
M,v/(x.3,m3)/(x.4,m4) |= H & M,v/(x.3,m3)/(x.4,m4) |= H1 or M,v/(x.
3,m3)/(x.4,m4) |= 'not' H & M,v/(x.3,m3)/(x.4,m4) |= H2 by ZF_MODEL:15;
hence thesis by A6,A13,A21,A22,A23,Th9;
end;
assume m4 = r;
then
M,v/(x.3,m3)/(x.4,m4) |= H & M,v/(x.3,m3)/(x.4,m4) |= H1 or M,v/(x.3,
m3)/(x.4,m4) |= 'not' H & M,v/(x.3,m3)/(x.4,m4) |= H2 by A6,A13,A21,A22,A23,Th9
;
then
M,v/(x.3,m3)/(x.4,m4) |= H '&' H1 or M,v/(x.3,m3)/(x.4,m4) |= 'not' H
'&' H2 by ZF_MODEL:15;
hence M,v/(x.3,m3)/(x.4,m4) |= p by ZF_MODEL:17;
end;
hence
A24: M,v |= All(x.3,Ex(x.0,All(x.4,p <=> x.4 '=' x.0))) by A20,Th19;
now
let a be Element of M;
set r = def_func'(p,v).a;
M,v/(x.3,a)/(x.4,r) |= p by A20,A24,Th10;
then
M,v/(x.3,a)/(x.4,r) |= H '&' H1 or M,v/(x.3,a)/(x.4,r) |= 'not' H '&'
H2 by ZF_MODEL:17;
then
M,v/(x.3,a)/(x.4,r) |= H & M,v/(x.3,a)/(x.4,r) |= H1 or M,v/(x.3,a)/(
x.4,r) |= 'not' H & M,v/(x.3,a)/(x.4,r) |= H2 by ZF_MODEL:15;
then M,v/(x.3,a) |= H & r = def_func'(H1,v).a or M,v/(x.3,a) |= 'not' H &
r = def_func'(H2,v).a by A2,A4,A6,A13,A12,A19,Th9,Th10;
hence f.a = def_func'(p,v).a by A8;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th23:
id M is_definable_in M
proof
take H = x.3 '=' x.4;
thus
A1: Free H c= {x.3,x.4} by ZF_LANG1:58;
reconsider i = id M as Function of M,M;
now
let v;
now
let m3;
now
let m4;
A2: m3 = v/(x.3,m3).(x.3) by FUNCT_7:128;
A3: v/(x.3,m3)/(x.0,m3)/(x.4,m4).(x.0) = v/(x.3,m3)/(x.0,m3).(x.0) by
FUNCT_7:32,ZF_LANG1:76;
A4: v/(x.3,m3)/(x.0,m3).(x.0) = m3 by FUNCT_7:128;
A5: v/(x.3,m3)/(x.0,m3).(x.3) = v/(x.3,m3).(x.3) by FUNCT_7:32,ZF_LANG1:76;
A6: v/(x.3,m3)/(x.0,m3)/(x.4,m4).(x.3) = v/(x.3,m3)/(x.0,m3).(x.3) by
FUNCT_7:32,ZF_LANG1:76;
A7: now
assume M,v/(x.3,m3)/(x.0,m3)/(x.4,m4) |= H;
then v/(x.3,m3)/(x.0,m3)/(x.4,m4).(x.3) = v/(x.3,m3)/(x.0,m3)/(x.4,
m4).(x.4) by ZF_MODEL:12;
hence
M,v/(x.3,m3)/(x.0,m3)/(x.4,m4) |= x.4 '=' x.0 by A6,A2,A5,A3,A4,
ZF_MODEL:12;
end;
A8: v/(x.3,m3)/(x.0,m3)/(x.4,m4).(x.4) = m4 by FUNCT_7:128;
now
assume M,v/(x.3,m3)/(x.0,m3)/(x.4,m4) |= x.4 '=' x.0;
then m4 = m3 by A3,A4,A8,ZF_MODEL:12;
hence M,v/(x.3,m3)/(x.0,m3)/(x.4,m4) |= H by A6,A2,A5,A8,ZF_MODEL:12;
end;
hence M,v/(x.3,m3)/(x.0,m3)/(x.4,m4) |= H <=> x.4 '=' x.0 by A7,
ZF_MODEL:19;
end;
then M,v/(x.3,m3)/(x.0,m3) |= All(x.4,H <=> x.4 '=' x.0) by ZF_LANG1:71;
hence M,v/(x.3,m3) |= Ex(x.0,All(x.4,H <=> x.4 '=' x.0)) by ZF_LANG1:73;
end;
hence M,v |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0))) by ZF_LANG1:71;
end;
hence
A9: M |= All(x.3,Ex(x.0,All(x.4,H <=> x.4 '=' x.0)));
now
set v = the Function of VAR,M;
let a be Element of M;
A10: a = v/(x.3,a).(x.3) by FUNCT_7:128;
A11: v/(x.3,a)/(x.4,a).(x.4) = a by FUNCT_7:128;
A12: v/(x.3,a)/(x.4,a).(x.3) = v/(x.3,a).(x.3) by FUNCT_7:32,ZF_LANG1:76;
then M,v/(x.3,a)/(x.4,a) |= H by A10,A11,ZF_MODEL:12;
then def_func(H,M).a = a by A1,A9,A12,A10,A11,ZFMODEL1:def 2;
hence i.a = def_func(H,M).a;
end;
hence id M = def_func(H,M);
end;
theorem
id M is_parametrically_definable_in M by Th23,ZFMODEL1:14;