:: Definable Functions
:: by Grzegorz Bancerek
::
:: Received September 26, 1990
:: Copyright (c) 1990 Association of Mizar Users

theorem Th1: :: ZFMODEL2:1

for x, y being Variable
for H being ZF-formula holds Free (H / x,y) c= ((Free H) \ {x}) \/ {y}

proof end;

theorem Th2: :: ZFMODEL2:2

for y, x being Variable
for H being ZF-formula st not y in variables_in H holds
( ( 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 end;

theorem :: ZFMODEL2:3

for H being ZF-formula holds variables_in H is finite

proof end;

theorem Th4: :: ZFMODEL2:4

for H being ZF-formula holds
( ex i being Element of NAT st
for j being Element of NAT st x. j in variables_in H holds
j < i & not for x being Variable holds x in variables_in H )

proof end;

theorem Th5: :: ZFMODEL2:5

for x being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H holds
( M,v |= H iff M,v |= All x,H )

proof end;

theorem Th6: :: ZFMODEL2:6

for x being Variable
for M being non empty set
for m being Element of M
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H holds
( M,v |= H iff M,v / x,m |= H )

proof end;

theorem Th7: :: ZFMODEL2:7

for x, y, z being Variable
for M being non empty set
for m1, m2, m3 being Element of M
for v being Function of VAR ,M st x <> y & y <> z & z <> x holds
( ((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 end;

theorem Th8: :: ZFMODEL2:8

for x1, x2, x3, x4 being Variable
for M being non empty set
for m1, m2, m3, m4 being Element of M
for v being Function of VAR ,M st x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 holds
( (((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 end;

theorem Th9: :: ZFMODEL2:9

for x1, x2, x3, x4 being Variable
for M being non empty set
for m1, m2, m, m3, m4 being Element of M
for v being Function of VAR ,M holds
( ((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 end;

theorem Th10: :: ZFMODEL2:10

for x being Variable
for M being non empty set
for m being Element of M
for H being ZF-formula
for v being Function of VAR ,M st not x in Free H holds
( M,v |= H iff M,v / x,m |= H )

proof end;

theorem Th11: :: ZFMODEL2:11

for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x. 0 in Free H & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
for m1, m2 being Element of M holds
( (def_func' H,v) . m1 = m2 iff M,(v / (x. 3),m1) / (x. 4),m2 |= H )

proof end;

Lm1: ( x. 0 <> x. 3 & x. 0 <> x. 4 & x. 3 <> x. 4 )
by ZF_LANG1:86;

theorem Th12: :: ZFMODEL2:12

for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st Free H c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) holds
def_func' H,v = def_func H,M

proof end;

theorem Th13: :: ZFMODEL2:13

for x, y being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H holds
( M,v |= H / y,x iff M,v / y,(v . x) |= H )

proof end;

theorem Th14: :: ZFMODEL2:14

for x, y being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x in variables_in H & M,v |= H holds
M,v / x,(v . y) |= H / y,x

proof end;

theorem Th15: :: ZFMODEL2:15

for x, y being Variable
for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st 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 holds
( 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 end;

theorem :: ZFMODEL2:16

for x, y being Variable
for M being non empty set
for H being ZF-formula st not x in variables_in H holds
( M |= H / y,x iff M |= H )

proof end;

theorem Th17: :: ZFMODEL2:17

for M being non empty set
for i being Element of NAT
for H1 being ZF-formula
for v1 being Function of VAR ,M st not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR ,M st
( ( for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
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 end;

theorem :: ZFMODEL2:18

for M being non empty set
for H1 being ZF-formula
for v1 being Function of VAR ,M st not x. 0 in Free H1 & M,v1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) holds
ex H2 being ZF-formula ex v2 being Function of VAR ,M 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 end;

theorem :: ZFMODEL2:19

for M being non empty set
for F, G being Function st F is_definable_in M & G is_definable_in M holds
F * G is_definable_in M

proof end;

theorem Th20: :: ZFMODEL2:20

for M being non empty set
for H being ZF-formula
for v being Function of VAR ,M st not x. 0 in Free H holds
( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H <=> ((x. 4) '=' (x. 0 ))))) iff for m1 being Element of M ex m2 being Element of M st
for m3 being Element of M holds
( M,(v / (x. 3),m1) / (x. 4),m3 |= H iff m3 = m2 ) )

proof end;

theorem :: ZFMODEL2:21

for M being non empty set
for H being ZF-formula
for F, G being Function st F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} holds
for FG being Function st dom FG = M & ( for v being Function of VAR ,M 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 end;

theorem :: ZFMODEL2:22

for M being non empty set
for F, G being Function st F is_parametrically_definable_in M & G is_parametrically_definable_in M holds
G * F is_parametrically_definable_in M

proof end;

theorem :: ZFMODEL2:23

for M being non empty set
for H1, H2, H being ZF-formula
for v being Function of VAR ,M st {(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 holds
for FG being Function st dom FG = M & ( for m being Element of 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 end;

theorem Th24: :: ZFMODEL2:24

for M being non empty set holds id M is_definable_in M

proof end;

theorem :: ZFMODEL2:25

for M being non empty set holds id M is_parametrically_definable_in M by Th24, ZFMODEL1:18;