let M be non empty set ; :: thesis: for H, H1, H2 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 H, H1, H2 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 and
A2: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) and
A3: {(x. 0),(x. 1),(x. 2)} misses Free H2 and
A4: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and
A5: {(x. 0),(x. 1),(x. 2)} misses Free H and
A6: 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
A7: dom FG = M and
A8: 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
rng FG c= M
proof
let a be object ; :: 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 object such that
A9: b in M and
A10: a = FG . b by A7, FUNCT_1:def 3;
reconsider b = b as Element of M by A9;
( 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 A8, A10;
hence a in M ; :: thesis: verum
end;
then reconsider f = FG as Function of M,M by A7, FUNCT_2:def 1, RELSET_1:4;
A11: x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def 1;
then A12: not x. 0 in Free H1 by A1, XBOOLE_0:3;
take p = (H '&' H1) 'or' (('not' H) '&' H2); :: according to ZFMODEL1:def 4 :: thesis: ex b1 being Element of K27(K28(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) )
A13: Free ('not' H) = Free H by ZF_LANG1:60;
A14: now :: thesis: for x being set holds
( not x in Free p or x in Free H or x in Free H1 or x in Free H2 )
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 )
A15: Free (('not' H) '&' H2) = (Free ('not' H)) \/ (Free H2) by ZF_LANG1:61;
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:63;
then A16: ( x in Free (H '&' H1) or x in Free (('not' H) '&' H2) ) by XBOOLE_0:def 3;
Free (H '&' H1) = (Free H) \/ (Free H1) by ZF_LANG1:61;
hence ( x in Free H or x in Free H1 or x in Free H2 ) by A13, A16, A15, XBOOLE_0:def 3; :: thesis: verum
end;
now :: thesis: for a being object st a in {(x. 0),(x. 1),(x. 2)} holds
not a in Free p
let a be object ; :: thesis: ( a in {(x. 0),(x. 1),(x. 2)} implies not a in Free p )
assume that
A17: a in {(x. 0),(x. 1),(x. 2)} and
A18: a in Free p ; :: thesis: contradiction
( a in Free H or a in Free H1 or a in Free H2 ) by A14, A18;
hence contradiction by A1, A3, A5, A17, 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) )
A19: not x. 0 in Free H2 by A3, A11, XBOOLE_0:3;
not x. 0 in Free H by A5, A11, XBOOLE_0:3;
then A20: not x. 0 in Free p by A14, A12, A19;
now :: thesis: for m3 being Element of M 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 ) )
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
A21: for m4 being Element of M holds
( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H1 iff m4 = r1 ) by A2, A12, Th19;
consider r2 being Element of M such that
A22: for m4 being Element of M holds
( M,(v / ((x. 3),m3)) / ((x. 4),m4) |= H2 iff m4 = r2 ) by A4, A19, Th19;
( ( 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
A23: ( ( 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 A6, A13, A21, A22, A23, Th9; :: 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 A6, A13, A21, A22, A23, Th9;
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 A24: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(p <=> ((x. 4) '=' (x. 0)))))))) by A20, Th19; :: thesis: FG = def_func' (p,v)
now :: thesis: for a being Element of M holds f . a = (def_func' (p,v)) . a
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 A20, A24, Th10;
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 A2, A4, A6, A13, A12, A19, Th9, Th10;
hence f . a = (def_func' (p,v)) . a by A8; :: thesis: verum
end;
hence FG = def_func' (p,v) by FUNCT_2:63; :: thesis: verum