:: Definable Functions :: by Grzegorz Bancerek :: :: Received September 26, 1990 :: Copyright (c) 1990-2018 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, XXREAL_0, 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;