:: Definable Functions :: by Grzegorz Bancerek :: :: Received September 26, 1990 :: Copyright (c) 1990-2021 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; 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 :: ZFMODEL2:1 Free (H/(x,y)) c= (Free H \ {x}) \/ {y}; theorem :: ZFMODEL2:2 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) ; registration let H; cluster variables_in H -> finite; end; theorem :: ZFMODEL2:3 (ex i st for j st x.j in variables_in H holds j < i) & ex x st not x in variables_in H; theorem :: ZFMODEL2:4 not x in variables_in H implies (M,v |= H iff M,v |= All(x,H)); theorem :: ZFMODEL2:5 not x in variables_in H implies (M,v |= H iff M,v/(x,m) |= H); theorem :: ZFMODEL2:6 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); theorem :: ZFMODEL2:7 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); theorem :: ZFMODEL2:8 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); theorem :: ZFMODEL2:9 not x in Free H implies (M,v |= H iff M,v/(x,m) |= H); theorem :: ZFMODEL2:10 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; theorem :: ZFMODEL2:11 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); theorem :: ZFMODEL2:12 not x in variables_in H implies (M,v |= H/(y,x) iff M,v/(y,v.x) |= H); theorem :: ZFMODEL2:13 not x in variables_in H & M,v |= H implies M,v/(x,v.y) |= H/(y,x ); theorem :: ZFMODEL2:14 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)); theorem :: ZFMODEL2:15 not x in variables_in H implies (M |= H/(y,x) iff M |= H); theorem :: ZFMODEL2:16 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); theorem :: ZFMODEL2:17 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); :: :: Definable functions :: reserve F,G for Function; theorem :: ZFMODEL2:18 F is_definable_in M & G is_definable_in M implies F*G is_definable_in M; theorem :: ZFMODEL2:19 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); theorem :: ZFMODEL2:20 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; theorem :: ZFMODEL2:21 F is_parametrically_definable_in M & G is_parametrically_definable_in M implies G*F is_parametrically_definable_in M; theorem :: ZFMODEL2:22 {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; theorem :: ZFMODEL2:23 id M is_definable_in M; theorem :: ZFMODEL2:24 id M is_parametrically_definable_in M;