let M be non empty set ; :: thesis: 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
let H1, H2, H be ZF-formula; :: thesis: 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
let v be Function of VAR ,M; :: thesis: ( {(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 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 )
assume that
A1: ( {(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 ))))) ) and
A2: ( {(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 ))))) ) and
A3: ( {(x. 0 ),(x. 1),(x. 2)} misses Free H & not x. 4 in Free H ) ; :: thesis: 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
let FG be Function; :: thesis: ( 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 ) ) ) implies FG is_parametrically_definable_in M )
assume that
A4: dom FG = M and
A5: 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 ) ) ; :: thesis: FG is_parametrically_definable_in M
take p = (H '&' H1) 'or' (('not' H) '&' H2); :: according to ZFMODEL1:def 4 :: thesis: ex b1 being Element of K29(K30(VAR ,M)) st
( {(x. 0 ),(x. 1),(x. 2)} misses Free p & M,b1 |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(p <=> ((x. 4) '=' (x. 0 ))))) & FG = def_func' p,b1 )
take v ; :: thesis: ( {(x. 0 ),(x. 1),(x. 2)} misses Free p & M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(p <=> ((x. 4) '=' (x. 0 ))))) & FG = def_func' p,v )
A6: Free ('not' H) = Free H by ZF_LANG1:65;
A7: now
let x be set ; :: thesis: ( not x in Free p or x in Free H or x in Free H1 or x in Free H2 )
assume x in Free p ; :: thesis: ( x in Free H or x in Free H1 or x in Free H2 )
then x in (Free (H '&' H1)) \/ (Free (('not' H) '&' H2)) by ZF_LANG1:68;
then ( ( x in Free (H '&' H1) or x in Free (('not' H) '&' H2) ) & Free (H '&' H1) = (Free H) \/ (Free H1) & Free (('not' H) '&' H2) = (Free ('not' H)) \/ (Free H2) ) by XBOOLE_0:def 3, ZF_LANG1:66;
hence ( x in Free H or x in Free H1 or x in Free H2 ) by A6, XBOOLE_0:def 3; :: thesis: verum
end;
x. 0 in {(x. 0 ),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A8: ( not x. 0 in Free H & not x. 0 in Free H1 & not x. 0 in Free H2 ) by A1, A2, A3, XBOOLE_0:3;
then A9: not x. 0 in Free p by A7;
now
let a be set ; :: thesis: ( a in {(x. 0 ),(x. 1),(x. 2)} implies not a in Free p )
assume A10: ( a in {(x. 0 ),(x. 1),(x. 2)} & a in Free p ) ; :: thesis: contradiction
then ( a in Free H or a in Free H1 or a in Free H2 ) by A7;
hence contradiction by A1, A2, A3, A10, XBOOLE_0:3; :: thesis: verum
end;
hence {(x. 0 ),(x. 1),(x. 2)} misses Free p by XBOOLE_0:3; :: thesis: ( M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(p <=> ((x. 4) '=' (x. 0 ))))) & FG = def_func' p,v )
now
let m3 be Element of M; :: thesis: ex r being Element of M st
for m4 being Element of M holds
( ( M,(v / (x. 3),m3) / (x. 4),m4 |= p implies m4 = r ) & ( m4 = r implies M,(v / (x. 3),m3) / (x. 4),m4 |= p ) )
consider r1 being Element of M such that
A11: for m4 being Element of M holds
( M,(v / (x. 3),m3) / (x. 4),m4 |= H1 iff m4 = r1 ) by A1, A8, Th20;
consider r2 being Element of M such that
A12: for m4 being Element of M holds
( M,(v / (x. 3),m3) / (x. 4),m4 |= H2 iff m4 = r2 ) by A2, A8, Th20;
( ( M,v / (x. 3),m3 |= H & not M,v / (x. 3),m3 |= 'not' H ) or ( not M,v / (x. 3),m3 |= H & M,v / (x. 3),m3 |= 'not' H ) ) by ZF_MODEL:14;
then consider r being Element of M such that
A13: ( ( M,v / (x. 3),m3 |= H & not M,v / (x. 3),m3 |= 'not' H & r = r1 ) or ( not M,v / (x. 3),m3 |= H & M,v / (x. 3),m3 |= 'not' H & r = r2 ) ) ;
take r = r; :: thesis: for m4 being Element of M holds
( ( M,(v / (x. 3),m3) / (x. 4),m4 |= p implies m4 = r ) & ( m4 = r implies M,(v / (x. 3),m3) / (x. 4),m4 |= p ) )
let m4 be Element of M; :: thesis: ( ( M,(v / (x. 3),m3) / (x. 4),m4 |= p implies m4 = r ) & ( m4 = r implies M,(v / (x. 3),m3) / (x. 4),m4 |= p ) )
thus ( M,(v / (x. 3),m3) / (x. 4),m4 |= p implies m4 = r ) :: thesis: ( m4 = r implies M,(v / (x. 3),m3) / (x. 4),m4 |= p )
proof
assume M,(v / (x. 3),m3) / (x. 4),m4 |= p ; :: thesis: m4 = r
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 = r by A3, A6, A11, A12, A13, Th10; :: thesis: verum
end;
assume m4 = r ; :: thesis: M,(v / (x. 3),m3) / (x. 4),m4 |= p
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 A3, A6, A11, A12, A13, 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 |= p by ZF_MODEL:17; :: thesis: verum
end;
hence A14: M,v |= All (x. 3),(Ex (x. 0 ),(All (x. 4),(p <=> ((x. 4) '=' (x. 0 ))))) by A9, Th20; :: thesis: FG = def_func' p,v
rng FG c= M
proof
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
A15: ( b in M & a = FG . b ) by A4, FUNCT_1:def 5;
reconsider b = b as Element of M by A15;
( M,v / (x. 3),b |= H or M,v / (x. 3),b |= 'not' H ) by ZF_MODEL:14;
then ( a = (def_func' H1,v) . b or a = (def_func' H2,v) . b ) by A5, A15;
hence a in M ; :: thesis: verum
end;
then reconsider f = FG as Function of M,M by A4, FUNCT_2:def 1, RELSET_1:11;
now
let a be Element of M; :: thesis: f . a = (def_func' p,v) . a
set r = (def_func' p,v) . a;
M,(v / (x. 3),a) / (x. 4),((def_func' p,v) . a) |= p by A9, A14, Th11;
then ( M,(v / (x. 3),a) / (x. 4),((def_func' p,v) . a) |= H '&' H1 or M,(v / (x. 3),a) / (x. 4),((def_func' p,v) . a) |= ('not' H) '&' H2 ) by ZF_MODEL:17;
then ( ( M,(v / (x. 3),a) / (x. 4),((def_func' p,v) . a) |= H & M,(v / (x. 3),a) / (x. 4),((def_func' p,v) . a) |= H1 ) or ( M,(v / (x. 3),a) / (x. 4),((def_func' p,v) . a) |= 'not' H & M,(v / (x. 3),a) / (x. 4),((def_func' p,v) . a) |= H2 ) ) by ZF_MODEL:15;
then ( ( M,v / (x. 3),a |= H & (def_func' p,v) . a = (def_func' H1,v) . a ) or ( M,v / (x. 3),a |= 'not' H & (def_func' p,v) . a = (def_func' H2,v) . a ) ) by A1, A2, A3, A6, A8, Th10, Th11;
hence f . a = (def_func' p,v) . a by A5; :: thesis: verum
end;
hence FG = def_func' p,v by FUNCT_2:113; :: thesis: verum