let M be non empty set ; :: thesis: 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
let H be ZF-formula; :: thesis: 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
let F, G be Function; :: thesis: ( F is_definable_in M & G is_definable_in M & Free H c= {(x. 3)} implies 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 )
A1: {(x. 3),(x. 3),(x. 4)} = {(x. 3),(x. 4)} by ENUMSET1:70;
A2: {(x. 3)} \/ {(x. 3),(x. 4)} = {(x. 3),(x. 3),(x. 4)} by ENUMSET1:42;
given H1 being ZF-formula such that A3: Free H1 c= {(x. 3),(x. 4)} and
A4: M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) and
A5: F = def_func H1,M ; :: according to ZFMODEL1:def 3 :: thesis: ( not G is_definable_in M or not Free H c= {(x. 3)} or 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 )
given H2 being ZF-formula such that A6: Free H2 c= {(x. 3),(x. 4)} and
A7: M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) and
A8: G = def_func H2,M ; :: according to ZFMODEL1:def 3 :: thesis: ( not Free H c= {(x. 3)} or 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 )
assume A9: Free H c= {(x. 3)} ; :: thesis: 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
then A10: not x. 4 in Free H by Lm3, TARSKI:def 1;
let FG be Function; :: thesis: ( 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)) ) ) ) implies FG is_definable_in M )
assume that
A11: dom FG = M and
A12: 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)) ) ) ; :: thesis: FG is_definable_in M
rng FG c= M

proof

consider v being Function of VAR ,M;
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in rng FG or a in M )
assume a in rng FG ; :: thesis: a in M
then consider b being set such that
A13: b in M and
A14: a = FG . b by A11, FUNCT_1:def 5;
reconsider b = b as Element of M by A13;
A15: ( M,v / (x. 3),b |= H or M,v / (x. 3),b |= 'not' H ) by ZF_MODEL:14;
(v / (x. 3),b) . (x. 3) = b by FUNCT_7:130;
then ( FG . b = (def_func H1,M) . b or FG . b = (def_func H2,M) . b ) by A5, A8, A12, A15;
hence a in M by A14; :: thesis: verum

end;

then reconsider f = FG as Function of M,M by A11, FUNCT_2:def 1, RELSET_1:11;
take I = (H '&' H1) 'or' (('not' H) '&' H2); :: according to ZFMODEL1:def 3 :: thesis: ( Free I c= {(x. 3),(x. 4)} & M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(I <=> ((x. 4) '=' (x. 0 ))))) & FG = def_func I,M )
A16: Free ('not' H) = Free H by ZF_LANG1:65;
Free (H '&' H1) = (Free H) \/ (Free H1) by ZF_LANG1:66;
then A17: Free (H '&' H1) c= {(x. 3),(x. 4)} by A3, A9, A2, A1, XBOOLE_1:13;
A18: not x. 0 in Free H2 by A6, Lm1, Lm2, TARSKI:def 2;
A19: not x. 0 in Free H1 by A3, Lm1, Lm2, TARSKI:def 2;
Free (('not' H) '&' H2) = (Free ('not' H)) \/ (Free H2) by ZF_LANG1:66;
then A20: Free (('not' H) '&' H2) c= {(x. 3),(x. 4)} by A6, A9, A16, A2, A1, XBOOLE_1:13;
A21: Free I = (Free (H '&' H1)) \/ (Free (('not' H) '&' H2)) by ZF_LANG1:68;
hence Free I c= {(x. 3),(x. 4)} by A17, A20, XBOOLE_1:8; :: thesis: ( M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(I <=> ((x. 4) '=' (x. 0 ))))) & FG = def_func I,M )
then A22: not x. 0 in Free I by Lm1, Lm2, TARSKI:def 2;

A23: now

let v be Function of VAR ,M; :: thesis: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(I <=> ((x. 4) '=' (x. 0 )))))

now

let m3 be Element of M; :: thesis: ex m being Element of M st
for m4 being Element of M holds
( ( M,(v / (x. 3),m3) / (x. 4),m4 |= I implies m4 = m ) & ( m4 = m implies M,(v / (x. 3),m3) / (x. 4),m4 |= I ) )
M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) by A4, ZF_MODEL:def 5;
then consider m1 being Element of M such that
A24: for m4 being Element of M holds
( M,(v / (x. 3),m3) / (x. 4),m4 |= H1 iff m4 = m1 ) by A19, Th20;
M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) by A7, ZF_MODEL:def 5;
then consider m2 being Element of M such that
A25: for m4 being Element of M holds
( M,(v / (x. 3),m3) / (x. 4),m4 |= H2 iff m4 = m2 ) by A18, Th20;
( ( not M,v / (x. 3),m3 |= 'not' H & M,v / (x. 3),m3 |= H ) or ( M,v / (x. 3),m3 |= 'not' H & not M,v / (x. 3),m3 |= H ) ) by ZF_MODEL:14;
then consider m being Element of M such that
A26: ( ( not M,v / (x. 3),m3 |= 'not' H & M,v / (x. 3),m3 |= H & m = m1 ) or ( M,v / (x. 3),m3 |= 'not' H & m = m2 & not M,v / (x. 3),m3 |= H ) ) ;
take m = m; :: thesis: for m4 being Element of M holds
( ( M,(v / (x. 3),m3) / (x. 4),m4 |= I implies m4 = m ) & ( m4 = m implies M,(v / (x. 3),m3) / (x. 4),m4 |= I ) )
let m4 be Element of M; :: thesis: ( ( M,(v / (x. 3),m3) / (x. 4),m4 |= I implies m4 = m ) & ( m4 = m implies M,(v / (x. 3),m3) / (x. 4),m4 |= I ) )
thus ( M,(v / (x. 3),m3) / (x. 4),m4 |= I implies m4 = m ) :: thesis: ( m4 = m implies M,(v / (x. 3),m3) / (x. 4),m4 |= I )

proof

assume M,(v / (x. 3),m3) / (x. 4),m4 |= I ; :: thesis: m4 = m
then ( M,(v / (x. 3),m3) / (x. 4),m4 |= H '&' H1 or M,(v / (x. 3),m3) / (x. 4),m4 |= ('not' H) '&' H2 ) by ZF_MODEL:17;
then ( ( M,(v / (x. 3),m3) / (x. 4),m4 |= H & M,(v / (x. 3),m3) / (x. 4),m4 |= H1 ) or ( M,(v / (x. 3),m3) / (x. 4),m4 |= 'not' H & M,(v / (x. 3),m3) / (x. 4),m4 |= H2 ) ) by ZF_MODEL:15;
hence m4 = m by A10, A16, A24, A25, A26, Th10; :: thesis: verum

end;

assume m4 = m ; :: thesis: M,(v / (x. 3),m3) / (x. 4),m4 |= I
then ( ( M,(v / (x. 3),m3) / (x. 4),m4 |= H & M,(v / (x. 3),m3) / (x. 4),m4 |= H1 ) or ( M,(v / (x. 3),m3) / (x. 4),m4 |= 'not' H & M,(v / (x. 3),m3) / (x. 4),m4 |= H2 ) ) by A10, A16, A24, A25, A26, Th10;
then ( M,(v / (x. 3),m3) / (x. 4),m4 |= H '&' H1 or M,(v / (x. 3),m3) / (x. 4),m4 |= ('not' H) '&' H2 ) by ZF_MODEL:15;
hence M,(v / (x. 3),m3) / (x. 4),m4 |= I by ZF_MODEL:17; :: thesis: verum

end;

hence M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(I <=> ((x. 4) '=' (x. 0 ))))) by A22, Th20; :: thesis: verum

end;

hence A27: M |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(I <=> ((x. 4) '=' (x. 0 ))))) by ZF_MODEL:def 5; :: thesis: FG = def_func I,M

now

consider v being Function of VAR ,M;
let a be Element of M; :: thesis: f . a = (def_func I,M) . a
set m4 = (def_func I,M) . a;
A28: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(I <=> ((x. 4) '=' (x. 0 ))))) by A23;
def_func I,M = def_func' I,v by A21, A17, A20, A27, Th12, XBOOLE_1:8;
then M,(v / (x. 3),a) / (x. 4),((def_func I,M) . a) |= I by A22, A28, Th11;
then ( M,(v / (x. 3),a) / (x. 4),((def_func I,M) . a) |= H '&' H1 or M,(v / (x. 3),a) / (x. 4),((def_func I,M) . a) |= ('not' H) '&' H2 ) by ZF_MODEL:17;
then ( ( M,(v / (x. 3),a) / (x. 4),((def_func I,M) . a) |= H & M,(v / (x. 3),a) / (x. 4),((def_func I,M) . a) |= H1 & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H1 <=> ((x. 4) '=' (x. 0 ))))) & def_func H1,M = def_func' H1,v ) or ( M,(v / (x. 3),a) / (x. 4),((def_func I,M) . a) |= 'not' H & M,(v / (x. 3),a) / (x. 4),((def_func I,M) . a) |= H2 & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(H2 <=> ((x. 4) '=' (x. 0 ))))) & def_func H2,M = def_func' H2,v ) ) by A3, A4, A6, A7, Th12, ZF_MODEL:15, ZF_MODEL:def 5;
then A29: ( ( M,v / (x. 3),a |= H & (def_func I,M) . a = F . a ) or ( M,v / (x. 3),a |= 'not' H & (def_func I,M) . a = G . a ) ) by A5, A8, A10, A16, A19, A18, Th10, Th11;
(v / (x. 3),a) . (x. 3) = a by FUNCT_7:130;
hence f . a = (def_func I,M) . a by A12, A29; :: thesis: verum

end;

hence FG = def_func I,M by FUNCT_2:113; :: thesis: verum