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

begin

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;

registration

let H be ZF-formula;
cluster variables_in H -> finite ;
coherence
variables_in H is finite

proof end;

end;

theorem :: ZFMODEL2:3

canceled;

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
by ZF_LANG1:86;

Lm2: x. 0 <> x. 4
by ZF_LANG1:86;

Lm3: 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 & 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;