The abstract of the Mizar article:

Definable Functions

by

Grzegorz Bancerek

Received September 26, 1990

MML identifier: ZFMODEL2

[ Mizar article, MML identifier index ]

environ

 vocabulary ZF_LANG, FUNCT_1, ZF_MODEL, ARYTM_3, BOOLE, QC_LANG3, FINSET_1,
      RELAT_1, ZFMODEL1;
 notation TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, XREAL_0, NAT_1, RELAT_1,
      FUNCT_1, FINSET_1, PARTFUN1, FUNCT_2, ZF_LANG, ZF_MODEL, ZFMODEL1,
      ZF_LANG1;
 constructors NAT_1, ENUMSET1, ZF_MODEL, ZFMODEL1, ZF_LANG1, XREAL_0, MEMBERED,
      PARTFUN1, XBOOLE_0;
 clusters FUNCT_1, FINSET_1, ZF_LANG, RELSET_1, FINSEQ_1, XREAL_0, ARYTM_3,
      ZFMISC_1, FUNCT_2, PARTFUN1, XBOOLE_0;
 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 Nat,
         m,m1,m2,m3,m4 for Element of M,
         H,H1,H2 for ZF-formula,
         v,v',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);

theorem :: ZFMODEL2:3
   variables_in H is finite;

theorem :: ZFMODEL2:4
  (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:5
  not x in variables_in H implies (M,v |= H iff M,v |= All(x,H));

theorem :: ZFMODEL2:6
  not x in variables_in H implies (M,v |= H iff M,v/(x,m) |= H);

theorem :: ZFMODEL2:7
  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:8
  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:9
  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:10
  not x in Free H implies (M,v |= H iff M,v/(x,m) |= H);

theorem :: ZFMODEL2:11
 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:12
  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:13
  not x in variables_in H implies (M,v |= H/(y,x) iff M,v/(y,v.x) |= H);

theorem :: ZFMODEL2:14
  not x in variables_in H & M,v |= H implies M,v/(x,v.y) |= H/(y,x);

theorem :: ZFMODEL2:15
 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 & y <> x.3 & y <> x.4 & 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:16
    not x in variables_in H implies (M |= H/(y,x) iff M |= H);

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 (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:18
   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:19
   F is_definable_in M & G is_definable_in M implies F*G is_definable_in M;

theorem :: ZFMODEL2:20
 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:21
   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:22
   F is_parametrically_definable_in M & G is_parametrically_definable_in M
   implies G*F is_parametrically_definable_in M;

theorem :: ZFMODEL2:23
   {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:24
  id M is_definable_in M;

theorem :: ZFMODEL2:25
   id M is_parametrically_definable_in M;