Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

Definable Functions

by
Grzegorz Bancerek

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;
```