:: Definable Functions :: by Grzegorz Bancerek :: :: Received September 26, 1990 :: Copyright (c) 1990-2012 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} proofend; 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 ) ) proofend; registration let H be ZF-formula; cluster variables_in H -> finite ; coherence variables_in H is finite proofend; end; theorem Th3: :: ZFMODEL2:3 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 ) proofend; theorem Th4: :: ZFMODEL2:4 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) ) proofend; theorem Th5: :: ZFMODEL2:5 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 ) proofend; theorem Th6: :: ZFMODEL2:6 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) ) proofend; theorem Th7: :: ZFMODEL2:7 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) ) proofend; theorem Th8: :: ZFMODEL2:8 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) ) proofend; theorem Th9: :: ZFMODEL2:9 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 ) proofend; theorem Th10: :: ZFMODEL2:10 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 ) proofend; Lm1: x. 0 <> x. 3 by ZF_LANG1:76; Lm2: x. 0 <> x. 4 by ZF_LANG1:76; Lm3: x. 3 <> x. 4 by ZF_LANG1:76; theorem Th11: :: ZFMODEL2:11 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) proofend; theorem Th12: :: ZFMODEL2:12 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 ) proofend; 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 & M,v |= H holds M,v / (x,(v . y)) |= H / (y,x) proofend; 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. 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)))) ) proofend; theorem :: ZFMODEL2:15 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 ) proofend; theorem Th16: :: ZFMODEL2:16 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) ) proofend; theorem :: ZFMODEL2:17 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) ) proofend; theorem :: ZFMODEL2:18 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 proofend; theorem Th19: :: ZFMODEL2:19 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 ) ) proofend; theorem :: ZFMODEL2:20 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 proofend; theorem :: ZFMODEL2:21 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 proofend; theorem :: ZFMODEL2:22 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 proofend; theorem Th23: :: ZFMODEL2:23 for M being non empty set holds id M is_definable_in M proofend; theorem :: ZFMODEL2:24 for M being non empty set holds id M is_parametrically_definable_in M by Th23, ZFMODEL1:14;