:: ZFMODEL2 semantic presentation
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
let x, y be Variable; ::_thesis: for H being ZF-formula holds Free (H / (x,y)) c= ((Free H) \ {x}) \/ {y}
let H be ZF-formula; ::_thesis: Free (H / (x,y)) c= ((Free H) \ {x}) \/ {y}
defpred S1[ ZF-formula] means Free ($1 / (x,y)) c= ((Free $1) \ {x}) \/ {y};
A1: for x1, x2 being Variable holds
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1, x2 be Variable; ::_thesis: ( S1[x1 '=' x2] & S1[x1 'in' x2] )
A2: ( x2 = x or x2 <> x ) ;
( x1 = x or x1 <> x ) ;
then consider y1, y2 being Variable such that
A3: ( ( x1 <> x & x2 <> x & y1 = x1 & y2 = x2 ) or ( x1 = x & x2 <> x & y1 = y & y2 = x2 ) or ( x1 <> x & x2 = x & y1 = x1 & y2 = y ) or ( x1 = x & x2 = x & y1 = y & y2 = y ) ) by A2;
A4: {y1,y2} c= ({x1,x2} \ {x}) \/ {y}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in {y1,y2} or a in ({x1,x2} \ {x}) \/ {y} )
assume a in {y1,y2} ; ::_thesis: a in ({x1,x2} \ {x}) \/ {y}
then ( ( ( a = x1 or a = x2 ) & a <> x ) or a = y ) by A3, TARSKI:def_2;
then ( ( a in {x1,x2} & not a in {x} ) or a in {y} ) by TARSKI:def_1, TARSKI:def_2;
then ( a in {x1,x2} \ {x} or a in {y} ) by XBOOLE_0:def_5;
hence a in ({x1,x2} \ {x}) \/ {y} by XBOOLE_0:def_3; ::_thesis: verum
end;
(x1 'in' x2) / (x,y) = y1 'in' y2 by A3, ZF_LANG1:154;
then A5: Free ((x1 'in' x2) / (x,y)) = {y1,y2} by ZF_LANG1:59;
(x1 '=' x2) / (x,y) = y1 '=' y2 by A3, ZF_LANG1:152;
then Free ((x1 '=' x2) / (x,y)) = {y1,y2} by ZF_LANG1:58;
hence ( S1[x1 '=' x2] & S1[x1 'in' x2] ) by A5, A4, ZF_LANG1:58, ZF_LANG1:59; ::_thesis: verum
end;
A6: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
assume that
A7: S1[H1] and
A8: S1[H2] ; ::_thesis: S1[H1 '&' H2]
A9: Free ((H1 / (x,y)) '&' (H2 / (x,y))) = (Free (H1 / (x,y))) \/ (Free (H2 / (x,y))) by ZF_LANG1:61;
A10: (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) c= (((Free H1) \/ (Free H2)) \ {x}) \/ {y}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) or a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y} )
assume a in (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) ; ::_thesis: a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y}
then ( a in ((Free H1) \ {x}) \/ {y} or a in ((Free H2) \ {x}) \/ {y} ) by XBOOLE_0:def_3;
then ( a in (Free H1) \ {x} or a in (Free H2) \ {x} or a in {y} ) by XBOOLE_0:def_3;
then ( ( ( a in Free H1 or a in Free H2 ) & not a in {x} ) or a in {y} ) by XBOOLE_0:def_5;
then ( ( a in (Free H1) \/ (Free H2) & not a in {x} ) or a in {y} ) by XBOOLE_0:def_3;
then ( a in ((Free H1) \/ (Free H2)) \ {x} or a in {y} ) by XBOOLE_0:def_5;
hence a in (((Free H1) \/ (Free H2)) \ {x}) \/ {y} by XBOOLE_0:def_3; ::_thesis: verum
end;
A11: (H1 '&' H2) / (x,y) = (H1 / (x,y)) '&' (H2 / (x,y)) by ZF_LANG1:158;
A12: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by ZF_LANG1:61;
(Free (H1 / (x,y))) \/ (Free (H2 / (x,y))) c= (((Free H1) \ {x}) \/ {y}) \/ (((Free H2) \ {x}) \/ {y}) by A7, A8, XBOOLE_1:13;
hence S1[H1 '&' H2] by A9, A12, A11, A10, XBOOLE_1:1; ::_thesis: verum
end;
A13: for H being ZF-formula
for z being Variable st S1[H] holds
S1[ All (z,H)]
proof
let H be ZF-formula; ::_thesis: for z being Variable st S1[H] holds
S1[ All (z,H)]
let z be Variable; ::_thesis: ( S1[H] implies S1[ All (z,H)] )
A14: Free (All (z,H)) = (Free H) \ {z} by ZF_LANG1:62;
( z = x or z <> x ) ;
then consider s being Variable such that
A15: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
A16: (((Free H) \ {x}) \/ {y}) \ {s} c= (((Free H) \ {z}) \ {x}) \/ {y}
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (((Free H) \ {x}) \/ {y}) \ {s} or a in (((Free H) \ {z}) \ {x}) \/ {y} )
assume A17: a in (((Free H) \ {x}) \/ {y}) \ {s} ; ::_thesis: a in (((Free H) \ {z}) \ {x}) \/ {y}
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def_3;
then ( ( a in Free H & not a in {z} & not a in {x} ) or a in {y} ) by A15, A17, XBOOLE_0:def_5;
then ( ( a in (Free H) \ {z} & not a in {x} ) or a in {y} ) by XBOOLE_0:def_5;
then ( a in ((Free H) \ {z}) \ {x} or a in {y} ) by XBOOLE_0:def_5;
hence a in (((Free H) \ {z}) \ {x}) \/ {y} by XBOOLE_0:def_3; ::_thesis: verum
end;
assume S1[H] ; ::_thesis: S1[ All (z,H)]
then A18: (Free (H / (x,y))) \ {s} c= (((Free H) \ {x}) \/ {y}) \ {s} by XBOOLE_1:33;
A19: Free (All (s,(H / (x,y)))) = (Free (H / (x,y))) \ {s} by ZF_LANG1:62;
(All (z,H)) / (x,y) = All (s,(H / (x,y))) by A15, ZF_LANG1:159, ZF_LANG1:160;
hence S1[ All (z,H)] by A19, A14, A18, A16, XBOOLE_1:1; ::_thesis: verum
end;
A20: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; ::_thesis: ( S1[H] implies S1[ 'not' H] )
A21: Free ('not' H) = Free H by ZF_LANG1:60;
Free ('not' (H / (x,y))) = Free (H / (x,y)) by ZF_LANG1:60;
hence ( S1[H] implies S1[ 'not' H] ) by A21, ZF_LANG1:156; ::_thesis: verum
end;
for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A1, A20, A6, A13);
hence Free (H / (x,y)) c= ((Free H) \ {x}) \/ {y} ; ::_thesis: verum
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
let y, x be Variable; ::_thesis: 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 ) )
let H be ZF-formula; ::_thesis: ( not y in variables_in H implies ( ( 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 ) ) )
defpred S1[ ZF-formula] means ( not y in variables_in $1 implies ( ( x in Free $1 implies Free ($1 / (x,y)) = ((Free $1) \ {x}) \/ {y} ) & ( not x in Free $1 implies Free ($1 / (x,y)) = Free $1 ) ) );
A1: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
assume that
A2: S1[H1] and
A3: S1[H2] and
A4: not y in variables_in (H1 '&' H2) ; ::_thesis: ( ( x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} ) & ( not x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) ) )
A5: Free ((H1 / (x,y)) '&' (H2 / (x,y))) = (Free (H1 / (x,y))) \/ (Free (H2 / (x,y))) by ZF_LANG1:61;
set H = H1 '&' H2;
A6: Free (H1 '&' H2) = (Free H1) \/ (Free H2) by ZF_LANG1:61;
A7: variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;
A8: (H1 '&' H2) / (x,y) = (H1 / (x,y)) '&' (H2 / (x,y)) by ZF_LANG1:158;
thus ( x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} ) ::_thesis: ( not x in Free (H1 '&' H2) implies Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) )
proof
assume A9: x in Free (H1 '&' H2) ; ::_thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}
A10: now__::_thesis:_(_not_x_in_Free_H1_implies_Free_((H1_'&'_H2)_/_(x,y))_=_((Free_(H1_'&'_H2))_\_{x})_\/_{y}_)
assume A11: not x in Free H1 ; ::_thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}
then Free H1 = (Free H1) \ {x} by ZFMISC_1:57;
hence Free ((H1 '&' H2) / (x,y)) = (((Free H1) \ {x}) \/ ((Free H2) \ {x})) \/ {y} by A2, A3, A4, A6, A5, A7, A8, A9, A11, XBOOLE_0:def_3, XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by A6, XBOOLE_1:42 ;
::_thesis: verum
end;
A12: now__::_thesis:_(_not_x_in_Free_H2_implies_Free_((H1_'&'_H2)_/_(x,y))_=_((Free_(H1_'&'_H2))_\_{x})_\/_{y}_)
assume A13: not x in Free H2 ; ::_thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}
then Free H2 = (Free H2) \ {x} by ZFMISC_1:57;
hence Free ((H1 '&' H2) / (x,y)) = (((Free H1) \ {x}) \/ ((Free H2) \ {x})) \/ {y} by A2, A3, A4, A6, A5, A7, A8, A9, A13, XBOOLE_0:def_3, XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} by A6, XBOOLE_1:42 ;
::_thesis: verum
end;
now__::_thesis:_(_x_in_Free_H1_&_x_in_Free_H2_implies_Free_((H1_'&'_H2)_/_(x,y))_=_((Free_(H1_'&'_H2))_\_{x})_\/_{y}_)
assume that
A14: x in Free H1 and
A15: x in Free H2 ; ::_thesis: Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y}
thus Free ((H1 '&' H2) / (x,y)) = (({y} \/ ((Free H1) \ {x})) \/ ((Free H2) \ {x})) \/ {y} by A2, A3, A4, A5, A7, A8, A14, A15, XBOOLE_0:def_3, XBOOLE_1:4
.= ({y} \/ (((Free H1) \ {x}) \/ ((Free H2) \ {x}))) \/ {y} by XBOOLE_1:4
.= (((Free (H1 '&' H2)) \ {x}) \/ {y}) \/ {y} by A6, XBOOLE_1:42
.= ((Free (H1 '&' H2)) \ {x}) \/ ({y} \/ {y}) by XBOOLE_1:4
.= ((Free (H1 '&' H2)) \ {x}) \/ {y} ; ::_thesis: verum
end;
hence Free ((H1 '&' H2) / (x,y)) = ((Free (H1 '&' H2)) \ {x}) \/ {y} by A10, A12; ::_thesis: verum
end;
assume not x in Free (H1 '&' H2) ; ::_thesis: Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2)
hence Free ((H1 '&' H2) / (x,y)) = Free (H1 '&' H2) by A2, A3, A4, A6, A5, A7, XBOOLE_0:def_3, ZF_LANG1:158; ::_thesis: verum
end;
A16: for H being ZF-formula
for z being Variable st S1[H] holds
S1[ All (z,H)]
proof
let H be ZF-formula; ::_thesis: for z being Variable st S1[H] holds
S1[ All (z,H)]
let z be Variable; ::_thesis: ( S1[H] implies S1[ All (z,H)] )
assume that
A17: S1[H] and
A18: not y in variables_in (All (z,H)) ; ::_thesis: ( ( x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y} ) & ( not x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) ) )
set G = (All (z,H)) / (x,y);
A19: Free (All (z,H)) = (Free H) \ {z} by ZF_LANG1:62;
( z = x or z <> x ) ;
then consider s being Variable such that
A20: ( ( z = x & s = y ) or ( z <> x & s = z ) ) ;
A21: (All (z,H)) / (x,y) = All (s,(H / (x,y))) by A20, ZF_LANG1:159, ZF_LANG1:160;
A22: Free (All (s,(H / (x,y)))) = (Free (H / (x,y))) \ {s} by ZF_LANG1:62;
A23: variables_in (All (z,H)) = (variables_in H) \/ {z} by ZF_LANG1:142;
thus ( x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y} ) ::_thesis: ( not x in Free (All (z,H)) implies Free ((All (z,H)) / (x,y)) = Free (All (z,H)) )
proof
assume A24: x in Free (All (z,H)) ; ::_thesis: Free ((All (z,H)) / (x,y)) = ((Free (All (z,H))) \ {x}) \/ {y}
then A25: not x in {z} by A19, XBOOLE_0:def_5;
thus Free ((All (z,H)) / (x,y)) c= ((Free (All (z,H))) \ {x}) \/ {y} :: according to XBOOLE_0:def_10 ::_thesis: ((Free (All (z,H))) \ {x}) \/ {y} c= Free ((All (z,H)) / (x,y))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Free ((All (z,H)) / (x,y)) or a in ((Free (All (z,H))) \ {x}) \/ {y} )
assume A26: a in Free ((All (z,H)) / (x,y)) ; ::_thesis: a in ((Free (All (z,H))) \ {x}) \/ {y}
then a in ((Free H) \ {x}) \/ {y} by A17, A18, A19, A22, A23, A21, A24, XBOOLE_0:def_3, XBOOLE_0:def_5;
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def_3;
then A27: ( ( a in Free H & not a in {x} ) or a in {y} ) by XBOOLE_0:def_5;
not a in {z} by A20, A22, A21, A25, A26, TARSKI:def_1, XBOOLE_0:def_5;
then ( ( a in Free (All (z,H)) & not a in {x} ) or a in {y} ) by A19, A27, XBOOLE_0:def_5;
then ( a in (Free (All (z,H))) \ {x} or a in {y} ) by XBOOLE_0:def_5;
hence a in ((Free (All (z,H))) \ {x}) \/ {y} by XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ((Free (All (z,H))) \ {x}) \/ {y} or a in Free ((All (z,H)) / (x,y)) )
assume a in ((Free (All (z,H))) \ {x}) \/ {y} ; ::_thesis: a in Free ((All (z,H)) / (x,y))
then ( a in (Free (All (z,H))) \ {x} or a in {y} ) by XBOOLE_0:def_3;
then A28: ( ( a in Free (All (z,H)) & not a in {x} ) or ( a in {y} & a = y ) ) by TARSKI:def_1, XBOOLE_0:def_5;
then ( ( a in Free H & not a in {x} ) or a in {y} ) by A19, XBOOLE_0:def_5;
then ( a in (Free H) \ {x} or a in {y} ) by XBOOLE_0:def_5;
then A29: a in ((Free H) \ {x}) \/ {y} by XBOOLE_0:def_3;
not a in {z} by A18, A19, A23, A28, XBOOLE_0:def_3, XBOOLE_0:def_5;
hence a in Free ((All (z,H)) / (x,y)) by A20, A17, A18, A19, A22, A23, A21, A24, A25, A29, TARSKI:def_1, XBOOLE_0:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;
assume not x in Free (All (z,H)) ; ::_thesis: Free ((All (z,H)) / (x,y)) = Free (All (z,H))
then A30: ( not x in Free H or x in {z} ) by A19, XBOOLE_0:def_5;
A31: Free (All (z,H)) c= variables_in (All (z,H)) by ZF_LANG1:151;
A32: now__::_thesis:_(_x_in_Free_H_implies_Free_((All_(z,H))_/_(x,y))_=_Free_(All_(z,H))_)
assume A33: x in Free H ; ::_thesis: Free ((All (z,H)) / (x,y)) = Free (All (z,H))
thus Free ((All (z,H)) / (x,y)) = Free (All (z,H)) ::_thesis: verum
proof
thus Free ((All (z,H)) / (x,y)) c= Free (All (z,H)) :: according to XBOOLE_0:def_10 ::_thesis: Free (All (z,H)) c= Free ((All (z,H)) / (x,y))
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Free ((All (z,H)) / (x,y)) or a in Free (All (z,H)) )
assume A34: a in Free ((All (z,H)) / (x,y)) ; ::_thesis: a in Free (All (z,H))
then A35: not a in {y} by A20, A22, A21, A30, A33, TARSKI:def_1, XBOOLE_0:def_5;
a in ((Free H) \ {z}) \/ {y} by A20, A17, A18, A22, A23, A21, A30, A33, A34, TARSKI:def_1, XBOOLE_0:def_3, XBOOLE_0:def_5;
hence a in Free (All (z,H)) by A19, A35, XBOOLE_0:def_3; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Free (All (z,H)) or a in Free ((All (z,H)) / (x,y)) )
assume A36: a in Free (All (z,H)) ; ::_thesis: a in Free ((All (z,H)) / (x,y))
then a <> y by A18, A31;
then A37: not a in {y} by TARSKI:def_1;
a in ((Free H) \ {x}) \/ {y} by A20, A19, A30, A33, A36, TARSKI:def_1, XBOOLE_0:def_3;
hence a in Free ((All (z,H)) / (x,y)) by A20, A17, A18, A22, A23, A21, A30, A33, A37, TARSKI:def_1, XBOOLE_0:def_3, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
now__::_thesis:_(_not_x_in_Free_H_implies_Free_((All_(z,H))_/_(x,y))_=_Free_(All_(z,H))_)
assume not x in Free H ; ::_thesis: Free ((All (z,H)) / (x,y)) = Free (All (z,H))
then ( ( Free ((All (z,H)) / (x,y)) = ((Free H) \ {z}) \ {y} & not y in Free (All (z,H)) ) or Free ((All (z,H)) / (x,y)) = (Free H) \ {z} ) by A20, A17, A18, A22, A23, A21, A31, XBOOLE_0:def_3, ZFMISC_1:57;
hence Free ((All (z,H)) / (x,y)) = Free (All (z,H)) by A19, ZFMISC_1:57; ::_thesis: verum
end;
hence Free ((All (z,H)) / (x,y)) = Free (All (z,H)) by A32; ::_thesis: verum
end;
A38: for x1, x2 being Variable holds
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1, x2 be Variable; ::_thesis: ( S1[x1 '=' x2] & S1[x1 'in' x2] )
A39: ( x2 = x or x2 <> x ) ;
( x1 = x or x1 <> x ) ;
then consider y1, y2 being Variable such that
A40: ( ( x1 <> x & x2 <> x & y1 = x1 & y2 = x2 ) or ( x1 = x & x2 <> x & y1 = y & y2 = x2 ) or ( x1 <> x & x2 = x & y1 = x1 & y2 = y ) or ( x1 = x & x2 = x & y1 = y & y2 = y ) ) by A39;
(x1 '=' x2) / (x,y) = y1 '=' y2 by A40, ZF_LANG1:152;
then A41: Free ((x1 '=' x2) / (x,y)) = {y1,y2} by ZF_LANG1:58;
A42: Free (x1 '=' x2) = {x1,x2} by ZF_LANG1:58;
A43: variables_in (x1 '=' x2) = {x1,x2} by ZF_LANG1:138;
thus S1[x1 '=' x2] ::_thesis: S1[x1 'in' x2]
proof
assume not y in variables_in (x1 '=' x2) ; ::_thesis: ( ( x in Free (x1 '=' x2) implies Free ((x1 '=' x2) / (x,y)) = ((Free (x1 '=' x2)) \ {x}) \/ {y} ) & ( not x in Free (x1 '=' x2) implies Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2) ) )
thus ( x in Free (x1 '=' x2) implies Free ((x1 '=' x2) / (x,y)) = ((Free (x1 '=' x2)) \ {x}) \/ {y} ) ::_thesis: ( not x in Free (x1 '=' x2) implies Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2) )
proof
assume A44: x in Free (x1 '=' x2) ; ::_thesis: Free ((x1 '=' x2) / (x,y)) = ((Free (x1 '=' x2)) \ {x}) \/ {y}
thus Free ((x1 '=' x2) / (x,y)) c= ((Free (x1 '=' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def_10 ::_thesis: ((Free (x1 '=' x2)) \ {x}) \/ {y} c= Free ((x1 '=' x2) / (x,y))
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ((Free (x1 '=' x2)) \ {x}) \/ {y} or a in Free ((x1 '=' x2) / (x,y)) )
assume a in ((Free (x1 '=' x2)) \ {x}) \/ {y} ; ::_thesis: a in Free ((x1 '=' x2) / (x,y))
then ( a in (Free (x1 '=' x2)) \ {x} or a in {y} ) by XBOOLE_0:def_3;
then ( ( a in Free (x1 '=' x2) & not a in {x} ) or a in {y} ) by XBOOLE_0:def_5;
then ( ( ( a = x1 or a = x2 ) & a <> x ) or a = y ) by A42, TARSKI:def_1, TARSKI:def_2;
hence a in Free ((x1 '=' x2) / (x,y)) by A40, A41, A42, A44, TARSKI:def_2; ::_thesis: verum
end;
assume not x in Free (x1 '=' x2) ; ::_thesis: Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2)
hence Free ((x1 '=' x2) / (x,y)) = Free (x1 '=' x2) by A42, A43, ZF_LANG1:182; ::_thesis: verum
end;
A45: Free (x1 'in' x2) = {x1,x2} by ZF_LANG1:59;
assume not y in variables_in (x1 'in' x2) ; ::_thesis: ( ( x in Free (x1 'in' x2) implies Free ((x1 'in' x2) / (x,y)) = ((Free (x1 'in' x2)) \ {x}) \/ {y} ) & ( not x in Free (x1 'in' x2) implies Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2) ) )
(x1 'in' x2) / (x,y) = y1 'in' y2 by A40, ZF_LANG1:154;
then A46: Free ((x1 'in' x2) / (x,y)) = {y1,y2} by ZF_LANG1:59;
thus ( x in Free (x1 'in' x2) implies Free ((x1 'in' x2) / (x,y)) = ((Free (x1 'in' x2)) \ {x}) \/ {y} ) ::_thesis: ( not x in Free (x1 'in' x2) implies Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2) )
proof
assume A47: x in Free (x1 'in' x2) ; ::_thesis: Free ((x1 'in' x2) / (x,y)) = ((Free (x1 'in' x2)) \ {x}) \/ {y}
thus Free ((x1 'in' x2) / (x,y)) c= ((Free (x1 'in' x2)) \ {x}) \/ {y} by Th1; :: according to XBOOLE_0:def_10 ::_thesis: ((Free (x1 'in' x2)) \ {x}) \/ {y} c= Free ((x1 'in' x2) / (x,y))
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in ((Free (x1 'in' x2)) \ {x}) \/ {y} or a in Free ((x1 'in' x2) / (x,y)) )
assume a in ((Free (x1 'in' x2)) \ {x}) \/ {y} ; ::_thesis: a in Free ((x1 'in' x2) / (x,y))
then ( a in (Free (x1 'in' x2)) \ {x} or a in {y} ) by XBOOLE_0:def_3;
then ( ( a in Free (x1 'in' x2) & not a in {x} ) or a in {y} ) by XBOOLE_0:def_5;
then ( ( ( a = x1 or a = x2 ) & a <> x ) or a = y ) by A45, TARSKI:def_1, TARSKI:def_2;
hence a in Free ((x1 'in' x2) / (x,y)) by A40, A46, A45, A47, TARSKI:def_2; ::_thesis: verum
end;
assume not x in Free (x1 'in' x2) ; ::_thesis: Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2)
hence Free ((x1 'in' x2) / (x,y)) = Free (x1 'in' x2) by A41, A42, A46, A45, A43, ZF_LANG1:182; ::_thesis: verum
end;
A48: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; ::_thesis: ( S1[H] implies S1[ 'not' H] )
A49: Free ('not' H) = Free H by ZF_LANG1:60;
Free ('not' (H / (x,y))) = Free (H / (x,y)) by ZF_LANG1:60;
hence ( S1[H] implies S1[ 'not' H] ) by A49, ZF_LANG1:140, ZF_LANG1:156; ::_thesis: verum
end;
for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A38, A48, A1, A16);
hence ( not y in variables_in H implies ( ( 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 ) ) ) ; ::_thesis: verum
end;
registration
let H be ZF-formula;
cluster variables_in H -> finite ;
coherence
variables_in H is finite
proof
variables_in H = (rng H) \ {0,1,2,3,4} by ZF_LANG1:def_2;
hence variables_in H is finite ; ::_thesis: verum
end;
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 )
proof
let H be ZF-formula; ::_thesis: ( 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 )
defpred S1[ ZF-formula] means ex i being Element of NAT st
for j being Element of NAT st x. j in variables_in $1 holds
j < i;
A1: for x, y being Variable holds
( S1[x '=' y] & S1[x 'in' y] )
proof
let x, y be Variable; ::_thesis: ( S1[x '=' y] & S1[x 'in' y] )
consider i being Element of NAT such that
A2: x = x. i by ZF_LANG1:77;
consider j being Element of NAT such that
A3: y = x. j by ZF_LANG1:77;
j <= j + i by NAT_1:11;
then A4: j < (i + j) + 1 by NAT_1:13;
i <= i + j by NAT_1:11;
then A5: i < (i + j) + 1 by NAT_1:13;
A6: variables_in (x '=' y) = {x,y} by ZF_LANG1:138;
thus S1[x '=' y] ::_thesis: S1[x 'in' y]
proof
take (i + j) + 1 ; ::_thesis: for j being Element of NAT st x. j in variables_in (x '=' y) holds
j < (i + j) + 1
let k be Element of NAT ; ::_thesis: ( x. k in variables_in (x '=' y) implies k < (i + j) + 1 )
assume x. k in variables_in (x '=' y) ; ::_thesis: k < (i + j) + 1
then ( x. k = x. i or x. k = x. j ) by A2, A3, A6, TARSKI:def_2;
hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; ::_thesis: verum
end;
take (i + j) + 1 ; ::_thesis: for j being Element of NAT st x. j in variables_in (x 'in' y) holds
j < (i + j) + 1
let k be Element of NAT ; ::_thesis: ( x. k in variables_in (x 'in' y) implies k < (i + j) + 1 )
A7: variables_in (x 'in' y) = {x,y} by ZF_LANG1:139;
assume x. k in variables_in (x 'in' y) ; ::_thesis: k < (i + j) + 1
then ( x. k = x. i or x. k = x. j ) by A2, A3, A7, TARSKI:def_2;
hence k < (i + j) + 1 by A5, A4, ZF_LANG1:76; ::_thesis: verum
end;
A8: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
given i1 being Element of NAT such that A9: for j being Element of NAT st x. j in variables_in H1 holds
j < i1 ; ::_thesis: ( not S1[H2] or S1[H1 '&' H2] )
given i2 being Element of NAT such that A10: for j being Element of NAT st x. j in variables_in H2 holds
j < i2 ; ::_thesis: S1[H1 '&' H2]
( i1 <= i2 or i1 > i2 ) ;
then consider i being Element of NAT such that
A11: ( ( i1 <= i2 & i = i2 ) or ( i1 > i2 & i = i1 ) ) ;
take i ; ::_thesis: for j being Element of NAT st x. j in variables_in (H1 '&' H2) holds
j < i
let j be Element of NAT ; ::_thesis: ( x. j in variables_in (H1 '&' H2) implies j < i )
assume x. j in variables_in (H1 '&' H2) ; ::_thesis: j < i
then x. j in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;
then ( x. j in variables_in H1 or x. j in variables_in H2 ) by XBOOLE_0:def_3;
then ( j < i1 or j < i2 ) by A9, A10;
hence j < i by A11, XXREAL_0:2; ::_thesis: verum
end;
A12: for H being ZF-formula
for x being Variable st S1[H] holds
S1[ All (x,H)]
proof
let H be ZF-formula; ::_thesis: for x being Variable st S1[H] holds
S1[ All (x,H)]
let x be Variable; ::_thesis: ( S1[H] implies S1[ All (x,H)] )
given i1 being Element of NAT such that A13: for j being Element of NAT st x. j in variables_in H holds
j < i1 ; ::_thesis: S1[ All (x,H)]
consider i2 being Element of NAT such that
A14: x = x. i2 by ZF_LANG1:77;
( i1 <= i2 + 1 or i1 > i2 + 1 ) ;
then consider i being Element of NAT such that
A15: ( ( i1 <= i2 + 1 & i = i2 + 1 ) or ( i1 > i2 + 1 & i = i1 ) ) ;
take i ; ::_thesis: for j being Element of NAT st x. j in variables_in (All (x,H)) holds
j < i
let j be Element of NAT ; ::_thesis: ( x. j in variables_in (All (x,H)) implies j < i )
assume x. j in variables_in (All (x,H)) ; ::_thesis: j < i
then x. j in (variables_in H) \/ {x} by ZF_LANG1:142;
then ( x. j in variables_in H or ( x. j in {x} & i2 + 0 = i2 & 0 < 1 ) ) by XBOOLE_0:def_3;
then ( j < i1 or ( x. j = x. i2 & i2 < i2 + 1 ) ) by A13, A14, TARSKI:def_1, XREAL_1:6;
then ( j < i1 or j < i2 + 1 ) by ZF_LANG1:76;
hence j < i by A15, XXREAL_0:2; ::_thesis: verum
end;
A16: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; ::_thesis: ( S1[H] implies S1[ 'not' H] )
variables_in ('not' H) = variables_in H by ZF_LANG1:140;
hence ( S1[H] implies S1[ 'not' H] ) ; ::_thesis: verum
end;
for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A1, A16, A8, A12);
then consider i being Element of NAT such that
A17: for j being Element of NAT st x. j in variables_in H holds
j < i ;
thus ex i being Element of NAT st
for j being Element of NAT st x. j in variables_in H holds
j < i by A17; ::_thesis: not for x being Variable holds x in variables_in H
take x. i ; ::_thesis: not x. i in variables_in H
thus not x. i in variables_in H by A17; ::_thesis: verum
end;
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) )
proof
let x be Variable; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let H be ZF-formula; ::_thesis: for v being Function of VAR,M st not x in variables_in H holds
( M,v |= H iff M,v |= All (x,H) )
let v be Function of VAR,M; ::_thesis: ( not x in variables_in H implies ( M,v |= H iff M,v |= All (x,H) ) )
Free H c= variables_in H by ZF_LANG1:151;
then A1: ( x in Free H implies x in variables_in H ) ;
v / (x,(v . x)) = v by FUNCT_7:35;
hence ( not x in variables_in H implies ( M,v |= H iff M,v |= All (x,H) ) ) by A1, ZFMODEL1:10, ZF_LANG1:71; ::_thesis: verum
end;
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 )
proof
let x be Variable; ::_thesis: 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 )
let M be non empty set ; ::_thesis: 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 )
let m be Element of M; ::_thesis: 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 )
let H be ZF-formula; ::_thesis: for v being Function of VAR,M st not x in variables_in H holds
( M,v |= H iff M,v / (x,m) |= H )
let v be Function of VAR,M; ::_thesis: ( not x in variables_in H implies ( M,v |= H iff M,v / (x,m) |= H ) )
A1: ( M,v / (x,m) |= All (x,H) implies M,(v / (x,m)) / (x,(v . x)) |= H ) by ZF_LANG1:71;
A2: (v / (x,m)) / (x,(v . x)) = v / (x,(v . x)) by FUNCT_7:34;
( M,v |= All (x,H) implies M,v / (x,m) |= H ) by ZF_LANG1:71;
hence ( not x in variables_in H implies ( M,v |= H iff M,v / (x,m) |= H ) ) by A1, A2, Th4, FUNCT_7:35; ::_thesis: verum
end;
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) )
proof
let x, y, z be Variable; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let m1, m2, m3 be Element of M; ::_thesis: 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) )
let v be Function of VAR,M; ::_thesis: ( x <> y & y <> z & z <> x implies ( ((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) ) )
assume that
A1: x <> y and
A2: y <> z and
A3: z <> x ; ::_thesis: ( ((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) )
A4: (v / (z,m3)) / (y,m2) = (v / (y,m2)) / (z,m3) by A2, FUNCT_7:33;
(v / (x,m1)) / (y,m2) = (v / (y,m2)) / (x,m1) by A1, FUNCT_7:33;
hence ( ((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) ) by A3, A4, FUNCT_7:33; ::_thesis: verum
end;
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) )
proof
let x1, x2, x3, x4 be Variable; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let m1, m2, m3, m4 be Element of M; ::_thesis: 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) )
let v be Function of VAR,M; ::_thesis: ( x1 <> x2 & x1 <> x3 & x1 <> x4 & x2 <> x3 & x2 <> x4 & x3 <> x4 implies ( (((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) ) )
assume that
A1: x1 <> x2 and
A2: x1 <> x3 and
A3: x1 <> x4 and
A4: x2 <> x3 and
A5: x2 <> x4 and
A6: x3 <> x4 ; ::_thesis: ( (((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) )
A7: (((v / (x1,m1)) / (x3,m3)) / (x4,m4)) / (x2,m2) = (((v / (x3,m3)) / (x4,m4)) / (x1,m1)) / (x2,m2) by A2, A3, A6, Th6;
A8: (((v / (x2,m2)) / (x3,m3)) / (x1,m1)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m1) by A3, FUNCT_7:33;
((v / (x1,m1)) / (x2,m2)) / (x3,m3) = ((v / (x2,m2)) / (x3,m3)) / (x1,m1) by A1, A2, A4, Th6;
hence ( (((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) ) by A4, A5, A6, A8, A7, Th6; ::_thesis: verum
end;
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) )
proof
let x1, x2, x3, x4 be Variable; ::_thesis: 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) )
let M be non empty set ; ::_thesis: 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) )
let m1, m2, m, m3, m4 be Element of M; ::_thesis: 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) )
let v be Function of VAR,M; ::_thesis: ( ((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) )
A1: ( ((v / (x1,m1)) / (x2,m2)) / (x1,m) = ((v / (x2,m2)) / (x1,m1)) / (x1,m) or x1 = x2 ) by FUNCT_7:33;
hence ((v / (x1,m1)) / (x2,m2)) / (x1,m) = (v / (x2,m2)) / (x1,m) by FUNCT_7:34; ::_thesis: ( (((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) )
( x1 = x3 or x1 <> x3 ) ;
then A2: ( ( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m) = (((v / (x1,m1)) / (x2,m2)) / (x1,m)) / (x3,m3) & ((v / (x2,m2)) / (x3,m3)) / (x1,m) = ((v / (x2,m2)) / (x1,m)) / (x3,m3) ) or ( (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m) = ((v / (x1,m1)) / (x2,m2)) / (x1,m) & ((v / (x2,m2)) / (x3,m3)) / (x1,m) = (v / (x2,m2)) / (x1,m) ) ) by FUNCT_7:33, FUNCT_7:34;
hence (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m) = ((v / (x2,m2)) / (x3,m3)) / (x1,m) by A1, FUNCT_7:34; ::_thesis: ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m)
( x1 = x4 or x1 <> x4 ) ;
then ( ( ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m) = ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m)) / (x4,m4) & (((v / (x2,m2)) / (x3,m3)) / (x1,m)) / (x4,m4) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m) ) or ( ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m) = (((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x1,m) & (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m) = ((v / (x2,m2)) / (x3,m3)) / (x1,m) ) ) by FUNCT_7:33, FUNCT_7:34;
hence ((((v / (x1,m1)) / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m) = (((v / (x2,m2)) / (x3,m3)) / (x4,m4)) / (x1,m) by A1, A2, FUNCT_7:34; ::_thesis: verum
end;
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 )
proof
let x be Variable; ::_thesis: 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 )
let M be non empty set ; ::_thesis: 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 )
let m be Element of M; ::_thesis: 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 )
let H be ZF-formula; ::_thesis: for v being Function of VAR,M st not x in Free H holds
( M,v |= H iff M,v / (x,m) |= H )
let v be Function of VAR,M; ::_thesis: ( not x in Free H implies ( M,v |= H iff M,v / (x,m) |= H ) )
A1: v / (x,(v . x)) = v by FUNCT_7:35;
assume A2: not x in Free H ; ::_thesis: ( M,v |= H iff M,v / (x,m) |= H )
then ( M,v |= H implies M,v |= All (x,H) ) by ZFMODEL1:10;
hence ( M,v |= H implies M,v / (x,m) |= H ) by ZF_LANG1:71; ::_thesis: ( M,v / (x,m) |= H implies M,v |= H )
assume M,v / (x,m) |= H ; ::_thesis: M,v |= H
then A3: M,v / (x,m) |= All (x,H) by A2, ZFMODEL1:10;
(v / (x,m)) / (x,(v . x)) = v / (x,(v . x)) by FUNCT_7:34;
hence M,v |= H by A3, A1, ZF_LANG1:71; ::_thesis: verum
end;
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 )
proof
let M be non empty set ; ::_thesis: 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 )
let H be ZF-formula; ::_thesis: 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 )
let v be Function of VAR,M; ::_thesis: ( not x. 0 in Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies for m1, m2 being Element of M holds
( (def_func' (H,v)) . m1 = m2 iff M,(v / ((x. 3),m1)) / ((x. 4),m2) |= H ) )
assume that
A1: not x. 0 in Free H and
A2: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: for m1, m2 being Element of M holds
( (def_func' (H,v)) . m1 = m2 iff M,(v / ((x. 3),m1)) / ((x. 4),m2) |= H )
let m1, m2 be Element of M; ::_thesis: ( (def_func' (H,v)) . m1 = m2 iff M,(v / ((x. 3),m1)) / ((x. 4),m2) |= H )
A3: (v / ((x. 3),m1)) . (x. 3) = m1 by FUNCT_7:128;
A4: now__::_thesis:_for_y_being_Variable_st_((v_/_((x._3),m1))_/_((x._4),m2))_._y_<>_v_._y_&_x._0_<>_y_&_x._3_<>_y_holds_
not_x._4_<>_y
let y be Variable; ::_thesis: ( ((v / ((x. 3),m1)) / ((x. 4),m2)) . y <> v . y & x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume A5: ((v / ((x. 3),m1)) / ((x. 4),m2)) . y <> v . y ; ::_thesis: ( x. 0 <> y & x. 3 <> y implies not x. 4 <> y )
assume that
x. 0 <> y and
A6: x. 3 <> y and
A7: x. 4 <> y ; ::_thesis: contradiction
((v / ((x. 3),m1)) / ((x. 4),m2)) . y = (v / ((x. 3),m1)) . y by A7, FUNCT_7:32;
hence contradiction by A5, A6, FUNCT_7:32; ::_thesis: verum
end;
A8: ((v / ((x. 3),m1)) / ((x. 4),m2)) . (x. 3) = (v / ((x. 3),m1)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
((v / ((x. 3),m1)) / ((x. 4),m2)) . (x. 4) = m2 by FUNCT_7:128;
hence ( (def_func' (H,v)) . m1 = m2 iff M,(v / ((x. 3),m1)) / ((x. 4),m2) |= H ) by A1, A2, A3, A8, A4, ZFMODEL1:def_1; ::_thesis: verum
end;
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)
proof
let M be non empty set ; ::_thesis: 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)
let H be ZF-formula; ::_thesis: 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)
let v be Function of VAR,M; ::_thesis: ( Free H c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies def_func' (H,v) = def_func (H,M) )
assume that
A1: Free H c= {(x. 3),(x. 4)} and
A2: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: def_func' (H,v) = def_func (H,M)
A3: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by A2, ZF_MODEL:def_5;
let a be Element of M; :: according to FUNCT_2:def_8 ::_thesis: (def_func' (H,v)) . a = (def_func (H,M)) . a
set r = (def_func' (H,v)) . a;
A4: ((v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) . (x. 3) = (v / ((x. 3),a)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
not x. 0 in Free H by A1, Lm1, Lm2, TARSKI:def_2;
then A5: M,(v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H by A3, Th10;
A6: (v / ((x. 3),a)) . (x. 3) = a by FUNCT_7:128;
((v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) . (x. 4) = (def_func' (H,v)) . a by FUNCT_7:128;
hence (def_func' (H,v)) . a = (def_func (H,M)) . a by A1, A2, A5, A4, A6, ZFMODEL1:def_2; ::_thesis: verum
end;
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 )
proof
let x, y be Variable; ::_thesis: 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 )
let M be non empty set ; ::_thesis: 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 )
let H be ZF-formula; ::_thesis: 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 )
let v be Function of VAR,M; ::_thesis: ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) )
defpred S1[ ZF-formula] means ( not x in variables_in $1 implies for v being Function of VAR,M holds
( M,v |= $1 / (y,x) iff M,v / (y,(v . x)) |= $1 ) );
A1: for x1, x2 being Variable holds
( S1[x1 '=' x2] & S1[x1 'in' x2] )
proof
let x1, x2 be Variable; ::_thesis: ( S1[x1 '=' x2] & S1[x1 'in' x2] )
A2: ( x2 = y or x2 <> y ) ;
A3: ( x1 = y or x1 <> y ) ;
thus S1[x1 '=' x2] ::_thesis: S1[x1 'in' x2]
proof
assume not x in variables_in (x1 '=' x2) ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )
let v be Function of VAR,M; ::_thesis: ( M,v |= (x1 '=' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 '=' x2 )
consider y1, y2 being Variable such that
A4: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;
A5: (v / (y,(v . x))) . x2 = v . y2 by A4, FUNCT_7:32, FUNCT_7:128;
A6: (v / (y,(v . x))) . x1 = v . y1 by A4, FUNCT_7:32, FUNCT_7:128;
A7: (x1 '=' x2) / (y,x) = y1 '=' y2 by A4, ZF_LANG1:152;
thus ( M,v |= (x1 '=' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 '=' x2 ) ::_thesis: ( M,v / (y,(v . x)) |= x1 '=' x2 implies M,v |= (x1 '=' x2) / (y,x) )
proof
assume M,v |= (x1 '=' x2) / (y,x) ; ::_thesis: M,v / (y,(v . x)) |= x1 '=' x2
then v . y1 = v . y2 by A7, ZF_MODEL:12;
hence M,v / (y,(v . x)) |= x1 '=' x2 by A6, A5, ZF_MODEL:12; ::_thesis: verum
end;
assume M,v / (y,(v . x)) |= x1 '=' x2 ; ::_thesis: M,v |= (x1 '=' x2) / (y,x)
then (v / (y,(v . x))) . x1 = (v / (y,(v . x))) . x2 by ZF_MODEL:12;
hence M,v |= (x1 '=' x2) / (y,x) by A7, A6, A5, ZF_MODEL:12; ::_thesis: verum
end;
consider y1, y2 being Variable such that
A8: ( ( x1 <> y & x2 <> y & y1 = x1 & y2 = x2 ) or ( x1 = y & x2 <> y & y1 = x & y2 = x2 ) or ( x1 <> y & x2 = y & y1 = x1 & y2 = x ) or ( x1 = y & x2 = y & y1 = x & y2 = x ) ) by A3, A2;
assume not x in variables_in (x1 'in' x2) ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )
let v be Function of VAR,M; ::_thesis: ( M,v |= (x1 'in' x2) / (y,x) iff M,v / (y,(v . x)) |= x1 'in' x2 )
A9: (v / (y,(v . x))) . x1 = v . y1 by A8, FUNCT_7:32, FUNCT_7:128;
A10: (v / (y,(v . x))) . x2 = v . y2 by A8, FUNCT_7:32, FUNCT_7:128;
A11: (x1 'in' x2) / (y,x) = y1 'in' y2 by A8, ZF_LANG1:154;
thus ( M,v |= (x1 'in' x2) / (y,x) implies M,v / (y,(v . x)) |= x1 'in' x2 ) ::_thesis: ( M,v / (y,(v . x)) |= x1 'in' x2 implies M,v |= (x1 'in' x2) / (y,x) )
proof
assume M,v |= (x1 'in' x2) / (y,x) ; ::_thesis: M,v / (y,(v . x)) |= x1 'in' x2
then v . y1 in v . y2 by A11, ZF_MODEL:13;
hence M,v / (y,(v . x)) |= x1 'in' x2 by A9, A10, ZF_MODEL:13; ::_thesis: verum
end;
assume M,v / (y,(v . x)) |= x1 'in' x2 ; ::_thesis: M,v |= (x1 'in' x2) / (y,x)
then (v / (y,(v . x))) . x1 in (v / (y,(v . x))) . x2 by ZF_MODEL:13;
hence M,v |= (x1 'in' x2) / (y,x) by A11, A9, A10, ZF_MODEL:13; ::_thesis: verum
end;
A12: for H1, H2 being ZF-formula st S1[H1] & S1[H2] holds
S1[H1 '&' H2]
proof
let H1, H2 be ZF-formula; ::_thesis: ( S1[H1] & S1[H2] implies S1[H1 '&' H2] )
assume that
A13: ( not x in variables_in H1 implies for v being Function of VAR,M holds
( M,v |= H1 / (y,x) iff M,v / (y,(v . x)) |= H1 ) ) and
A14: ( not x in variables_in H2 implies for v being Function of VAR,M holds
( M,v |= H2 / (y,x) iff M,v / (y,(v . x)) |= H2 ) ) ; ::_thesis: S1[H1 '&' H2]
assume not x in variables_in (H1 '&' H2) ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )
then A15: not x in (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;
let v be Function of VAR,M; ::_thesis: ( M,v |= (H1 '&' H2) / (y,x) iff M,v / (y,(v . x)) |= H1 '&' H2 )
thus ( M,v |= (H1 '&' H2) / (y,x) implies M,v / (y,(v . x)) |= H1 '&' H2 ) ::_thesis: ( M,v / (y,(v . x)) |= H1 '&' H2 implies M,v |= (H1 '&' H2) / (y,x) )
proof
assume M,v |= (H1 '&' H2) / (y,x) ; ::_thesis: M,v / (y,(v . x)) |= H1 '&' H2
then A16: M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by ZF_LANG1:158;
then M,v |= H2 / (y,x) by ZF_MODEL:15;
then A17: M,v / (y,(v . x)) |= H2 by A14, A15, XBOOLE_0:def_3;
M,v |= H1 / (y,x) by A16, ZF_MODEL:15;
then M,v / (y,(v . x)) |= H1 by A13, A15, XBOOLE_0:def_3;
hence M,v / (y,(v . x)) |= H1 '&' H2 by A17, ZF_MODEL:15; ::_thesis: verum
end;
assume A18: M,v / (y,(v . x)) |= H1 '&' H2 ; ::_thesis: M,v |= (H1 '&' H2) / (y,x)
then M,v / (y,(v . x)) |= H2 by ZF_MODEL:15;
then A19: M,v |= H2 / (y,x) by A14, A15, XBOOLE_0:def_3;
M,v / (y,(v . x)) |= H1 by A18, ZF_MODEL:15;
then M,v |= H1 / (y,x) by A13, A15, XBOOLE_0:def_3;
then M,v |= (H1 / (y,x)) '&' (H2 / (y,x)) by A19, ZF_MODEL:15;
hence M,v |= (H1 '&' H2) / (y,x) by ZF_LANG1:158; ::_thesis: verum
end;
A20: for H being ZF-formula
for z being Variable st S1[H] holds
S1[ All (z,H)]
proof
let H be ZF-formula; ::_thesis: for z being Variable st S1[H] holds
S1[ All (z,H)]
let z be Variable; ::_thesis: ( S1[H] implies S1[ All (z,H)] )
assume A21: ( not x in variables_in H implies for v being Function of VAR,M holds
( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; ::_thesis: S1[ All (z,H)]
( z = y or z <> y ) ;
then consider s being Variable such that
A22: ( ( z = y & s = x ) or ( z <> y & s = z ) ) ;
assume A23: not x in variables_in (All (z,H)) ; ::_thesis: for v being Function of VAR,M holds
( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )
then A24: not x in (variables_in H) \/ {z} by ZF_LANG1:142;
then not x in {z} by XBOOLE_0:def_3;
then A25: x <> z by TARSKI:def_1;
let v be Function of VAR,M; ::_thesis: ( M,v |= (All (z,H)) / (y,x) iff M,v / (y,(v . x)) |= All (z,H) )
Free H c= variables_in H by ZF_LANG1:151;
then A26: not x in Free H by A24, XBOOLE_0:def_3;
thus ( M,v |= (All (z,H)) / (y,x) implies M,v / (y,(v . x)) |= All (z,H) ) ::_thesis: ( M,v / (y,(v . x)) |= All (z,H) implies M,v |= (All (z,H)) / (y,x) )
proof
assume M,v |= (All (z,H)) / (y,x) ; ::_thesis: M,v / (y,(v . x)) |= All (z,H)
then A27: M,v |= All (s,(H / (y,x))) by A22, ZF_LANG1:159, ZF_LANG1:160;
A28: now__::_thesis:_(_z_=_y_&_s_=_x_implies_M,v_/_(y,(v_._x))_|=_All_(z,H)_)
assume that
A29: z = y and
A30: s = x ; ::_thesis: M,v / (y,(v . x)) |= All (z,H)
now__::_thesis:_for_m_being_Element_of_M_holds_M,v_/_(y,m)_|=_H
let m be Element of M; ::_thesis: M,v / (y,m) |= H
A31: (v / (x,m)) . x = m by FUNCT_7:128;
M,v / (x,m) |= H / (y,x) by A27, A30, ZF_LANG1:71;
then A32: M,(v / (x,m)) / (y,((v / (x,m)) . x)) |= H by A21, A24, XBOOLE_0:def_3;
(v / (x,m)) / (y,m) = (v / (y,m)) / (x,m) by A25, A29, FUNCT_7:33;
then M,(v / (y,m)) / (x,m) |= All (x,H) by A26, A32, A31, ZFMODEL1:10;
then A33: M,((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) |= H by ZF_LANG1:71;
((v / (y,m)) / (x,m)) / (x,((v / (y,m)) . x)) = (v / (y,m)) / (x,((v / (y,m)) . x)) by FUNCT_7:34;
hence M,v / (y,m) |= H by A33, FUNCT_7:35; ::_thesis: verum
end;
then M,v |= All (y,H) by ZF_LANG1:71;
hence M,v / (y,(v . x)) |= All (z,H) by A29, ZF_LANG1:72; ::_thesis: verum
end;
now__::_thesis:_(_z_<>_y_&_s_=_z_implies_M,v_/_(y,(v_._x))_|=_All_(z,H)_)
assume that
A34: z <> y and
A35: s = z ; ::_thesis: M,v / (y,(v . x)) |= All (z,H)
now__::_thesis:_for_m_being_Element_of_M_holds_M,(v_/_(y,(v_._x)))_/_(z,m)_|=_H
let m be Element of M; ::_thesis: M,(v / (y,(v . x))) / (z,m) |= H
M,v / (z,m) |= H / (y,x) by A27, A35, ZF_LANG1:71;
then A36: M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A21, A24, XBOOLE_0:def_3;
(v / (z,m)) . x = v . x by A25, FUNCT_7:32;
hence M,(v / (y,(v . x))) / (z,m) |= H by A34, A36, FUNCT_7:33; ::_thesis: verum
end;
hence M,v / (y,(v . x)) |= All (z,H) by ZF_LANG1:71; ::_thesis: verum
end;
hence M,v / (y,(v . x)) |= All (z,H) by A22, A28; ::_thesis: verum
end;
assume A37: M,v / (y,(v . x)) |= All (z,H) ; ::_thesis: M,v |= (All (z,H)) / (y,x)
Free (All (z,H)) c= variables_in (All (z,H)) by ZF_LANG1:151;
then A38: not x in Free (All (z,H)) by A23;
A39: now__::_thesis:_(_z_=_y_&_s_=_x_implies_M,v_|=_(All_(z,H))_/_(y,x)_)
assume that
A40: z = y and
s = x ; ::_thesis: M,v |= (All (z,H)) / (y,x)
M,v |= All (y,H) by A37, A40, ZF_LANG1:72;
then A41: M,v |= All (x,(All (y,H))) by A38, A40, ZFMODEL1:10;
now__::_thesis:_for_m_being_Element_of_M_holds_M,v_/_(x,m)_|=_H_/_(y,x)
let m be Element of M; ::_thesis: M,v / (x,m) |= H / (y,x)
M,v / (x,m) |= All (y,H) by A41, ZF_LANG1:71;
then A42: M,(v / (x,m)) / (y,m) |= H by ZF_LANG1:71;
(v / (x,m)) . x = m by FUNCT_7:128;
hence M,v / (x,m) |= H / (y,x) by A21, A24, A42, XBOOLE_0:def_3; ::_thesis: verum
end;
then M,v |= All (x,(H / (y,x))) by ZF_LANG1:71;
hence M,v |= (All (z,H)) / (y,x) by A40, ZF_LANG1:160; ::_thesis: verum
end;
now__::_thesis:_(_z_<>_y_&_s_=_z_implies_M,v_|=_(All_(z,H))_/_(y,x)_)
assume that
A43: z <> y and
s = z ; ::_thesis: M,v |= (All (z,H)) / (y,x)
now__::_thesis:_for_m_being_Element_of_M_holds_M,v_/_(z,m)_|=_H_/_(y,x)
let m be Element of M; ::_thesis: M,v / (z,m) |= H / (y,x)
M,(v / (y,(v . x))) / (z,m) |= H by A37, ZF_LANG1:71;
then M,(v / (z,m)) / (y,(v . x)) |= H by A43, FUNCT_7:33;
then M,(v / (z,m)) / (y,((v / (z,m)) . x)) |= H by A25, FUNCT_7:32;
hence M,v / (z,m) |= H / (y,x) by A21, A24, XBOOLE_0:def_3; ::_thesis: verum
end;
then M,v |= All (z,(H / (y,x))) by ZF_LANG1:71;
hence M,v |= (All (z,H)) / (y,x) by A43, ZF_LANG1:159; ::_thesis: verum
end;
hence M,v |= (All (z,H)) / (y,x) by A22, A39; ::_thesis: verum
end;
A44: for H being ZF-formula st S1[H] holds
S1[ 'not' H]
proof
let H be ZF-formula; ::_thesis: ( S1[H] implies S1[ 'not' H] )
assume A45: ( not x in variables_in H implies for v being Function of VAR,M holds
( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; ::_thesis: S1[ 'not' H]
assume A46: not x in variables_in ('not' H) ; ::_thesis: for v being Function of VAR,M holds
( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )
let v be Function of VAR,M; ::_thesis: ( M,v |= ('not' H) / (y,x) iff M,v / (y,(v . x)) |= 'not' H )
thus ( M,v |= ('not' H) / (y,x) implies M,v / (y,(v . x)) |= 'not' H ) ::_thesis: ( M,v / (y,(v . x)) |= 'not' H implies M,v |= ('not' H) / (y,x) )
proof
assume M,v |= ('not' H) / (y,x) ; ::_thesis: M,v / (y,(v . x)) |= 'not' H
then M,v |= 'not' (H / (y,x)) by ZF_LANG1:156;
then not M,v |= H / (y,x) by ZF_MODEL:14;
then not M,v / (y,(v . x)) |= H by A45, A46, ZF_LANG1:140;
hence M,v / (y,(v . x)) |= 'not' H by ZF_MODEL:14; ::_thesis: verum
end;
assume M,v / (y,(v . x)) |= 'not' H ; ::_thesis: M,v |= ('not' H) / (y,x)
then not M,v / (y,(v . x)) |= H by ZF_MODEL:14;
then not M,v |= H / (y,x) by A45, A46, ZF_LANG1:140;
then M,v |= 'not' (H / (y,x)) by ZF_MODEL:14;
hence M,v |= ('not' H) / (y,x) by ZF_LANG1:156; ::_thesis: verum
end;
for H being ZF-formula holds S1[H] from ZF_LANG1:sch_1(A1, A44, A12, A20);
hence ( not x in variables_in H implies ( M,v |= H / (y,x) iff M,v / (y,(v . x)) |= H ) ) ; ::_thesis: verum
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 & M,v |= H holds
M,v / (x,(v . y)) |= H / (y,x)
proof
let x, y be Variable; ::_thesis: 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)
let M be non empty set ; ::_thesis: 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)
let H be ZF-formula; ::_thesis: 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)
let v be Function of VAR,M; ::_thesis: ( not x in variables_in H & M,v |= H implies M,v / (x,(v . y)) |= H / (y,x) )
assume that
A1: not x in variables_in H and
A2: M,v |= H ; ::_thesis: M,v / (x,(v . y)) |= H / (y,x)
A3: (v / (x,(v . y))) . x = v . y by FUNCT_7:128;
( x = y or x <> y ) ;
then A4: (v / (x,(v . y))) / (y,(v . y)) = (v / (y,(v . y))) / (x,(v . y)) by FUNCT_7:33;
A5: v / (y,(v . y)) = v by FUNCT_7:35;
M,v / (x,(v . y)) |= H by A1, A2, Th5;
hence M,v / (x,(v . y)) |= H / (y,x) by A1, A4, A3, A5, Th12; ::_thesis: verum
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. 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
let x, y be Variable; ::_thesis: 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)))) )
let M be non empty set ; ::_thesis: 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)))) )
let H be ZF-formula; ::_thesis: 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)))) )
let v be Function of VAR,M; ::_thesis: ( 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 implies ( 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)))) ) )
A1: x. 0 <> x. 4 by ZF_LANG1:76;
A2: x. 3 <> x. 4 by ZF_LANG1:76;
set F = H / (y,x);
set f = v / (x,(v . y));
assume that
A3: not x. 0 in Free H and
A4: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) and
A5: not x in variables_in H and
A6: not y in Free H and
A7: x <> x. 0 and
A8: x <> x. 3 and
A9: x <> x. 4 ; ::_thesis: ( 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)))) )
( ( Free (H / (y,x)) c= variables_in (H / (y,x)) & not x. 0 in variables_in (H / (y,x)) ) or ( not x. 0 in {x} & not x. 0 in (Free H) \ {y} ) ) by A3, A7, TARSKI:def_1, XBOOLE_0:def_5;
then ( not x. 0 in Free (H / (y,x)) or ( Free (H / (y,x)) c= ((Free H) \ {y}) \/ {x} & not x. 0 in ((Free H) \ {y}) \/ {x} ) ) by Th1, XBOOLE_0:def_3;
hence A10: not x. 0 in Free (H / (y,x)) ; ::_thesis: ( 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)))) )
A11: x. 0 <> x. 3 by ZF_LANG1:76;
now__::_thesis:_for_m3_being_Element_of_M_holds_M,(v_/_(x,(v_._y)))_/_((x._3),m3)_|=_Ex_((x._0),(All_((x._4),((H_/_(y,x))_<=>_((x._4)_'='_(x._0))))))
let m3 be Element of M; ::_thesis: M,(v / (x,(v . y))) / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0))))))
M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A4, ZF_LANG1:71;
then consider m being Element of M such that
A12: M,(v / ((x. 3),m3)) / ((x. 0),m) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
set f1 = ((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m);
now__::_thesis:_for_m4_being_Element_of_M_holds_M,(((v_/_(x,(v_._y)))_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_(H_/_(y,x))_<=>_((x._4)_'='_(x._0))
let m4 be Element of M; ::_thesis: M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (H / (y,x)) <=> ((x. 4) '=' (x. 0))
A13: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
A14: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A15: ((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = (((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A16: ((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
A17: (((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A18: ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A19: M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A12, ZF_LANG1:71;
A20: now__::_thesis:_(_M,(((v_/_(x,(v_._y)))_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_(x._4)_'='_(x._0)_implies_M,(((v_/_(x,(v_._y)))_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_H_/_(y,x)_)
assume M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ; ::_thesis: M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x)
then m = m4 by A16, A15, A17, ZF_MODEL:12;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A13, A14, A18, ZF_MODEL:12;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A19, ZF_MODEL:19;
then M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,(v . y)) |= H by A5, Th5;
then M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A7, A8, A9, A11, A1, A2, Th7;
then M,((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (y,(((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . x)) |= H by A6, Th9;
hence M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) by A5, Th12; ::_thesis: verum
end;
now__::_thesis:_(_M,(((v_/_(x,(v_._y)))_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_H_/_(y,x)_implies_M,(((v_/_(x,(v_._y)))_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_(x._4)_'='_(x._0)_)
assume M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H / (y,x) ; ::_thesis: M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0)
then M,((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (y,(((((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . x)) |= H by A5, Th12;
then M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A6, Th9;
then M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,(v . y)) |= H by A7, A8, A9, A11, A1, A2, Th7;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by A5, Th5;
then M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A19, ZF_MODEL:19;
then m = m4 by A13, A14, A18, ZF_MODEL:12;
hence M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A16, A15, A17, ZF_MODEL:12; ::_thesis: verum
end;
hence M,(((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (H / (y,x)) <=> ((x. 4) '=' (x. 0)) by A20, ZF_MODEL:19; ::_thesis: verum
end;
then M,((v / (x,(v . y))) / ((x. 3),m3)) / ((x. 0),m) |= All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:71;
hence M,(v / (x,(v . y))) / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:73; ::_thesis: verum
end;
hence A21: M,v / (x,(v . y)) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H / (y,x)) <=> ((x. 4) '=' (x. 0)))))))) by ZF_LANG1:71; ::_thesis: def_func' (H,v) = def_func' ((H / (y,x)),(v / (x,(v . y))))
A22: Free H c= variables_in H by ZF_LANG1:151;
Free (H / (y,x)) = Free H by A5, A6, Th2;
then A23: not x in Free (H / (y,x)) by A5, A22;
let a be Element of M; :: according to FUNCT_2:def_8 ::_thesis: (def_func' (H,v)) . a = (def_func' ((H / (y,x)),(v / (x,(v . y))))) . a
set a9 = (def_func' (H,v)) . a;
M,(v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H by A3, A4, Th10;
then M,((v / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) / (x,(v . y)) |= H by A5, Th5;
then M,((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H by A8, A9, A2, Th6;
then M,(((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) / (x,((((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a))) . y)) |= H / (y,x) by A5, Th13;
then M,((v / (x,(v . y))) / ((x. 3),a)) / ((x. 4),((def_func' (H,v)) . a)) |= H / (y,x) by A23, Th9;
hence (def_func' (H,v)) . a = (def_func' ((H / (y,x)),(v / (x,(v . y))))) . a by A10, A21, Th10; ::_thesis: verum
end;
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 )
proof
let x, y be Variable; ::_thesis: 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 )
let M be non empty set ; ::_thesis: for H being ZF-formula st not x in variables_in H holds
( M |= H / (y,x) iff M |= H )
let H be ZF-formula; ::_thesis: ( not x in variables_in H implies ( M |= H / (y,x) iff M |= H ) )
assume A1: not x in variables_in H ; ::_thesis: ( M |= H / (y,x) iff M |= H )
thus ( M |= H / (y,x) implies M |= H ) ::_thesis: ( M |= H implies M |= H / (y,x) )
proof
assume A2: for v being Function of VAR,M holds M,v |= H / (y,x) ; :: according to ZF_MODEL:def_5 ::_thesis: M |= H
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= H
A3: (v / (x,(v . y))) . x = v . y by FUNCT_7:128;
M,v / (x,(v . y)) |= H / (y,x) by A2;
then M,(v / (x,(v . y))) / (y,(v . y)) |= H by A1, A3, Th12;
then A4: M,((v / (x,(v . y))) / (y,(v . y))) / (x,(v . x)) |= H by A1, Th5;
( x = y or x <> y ) ;
then ( M,(v / (x,(v . y))) / (x,(v . x)) |= H or M,((v / (y,(v . y))) / (x,(v . y))) / (x,(v . x)) |= H ) by A4, FUNCT_7:33;
then ( M,v / (x,(v . x)) |= H or M,(v / (y,(v . y))) / (x,(v . x)) |= H ) by FUNCT_7:34;
then M,v / (x,(v . x)) |= H by FUNCT_7:35;
hence M,v |= H by FUNCT_7:35; ::_thesis: verum
end;
assume A5: for v being Function of VAR,M holds M,v |= H ; :: according to ZF_MODEL:def_5 ::_thesis: M |= H / (y,x)
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= H / (y,x)
M,v / (y,(v . x)) |= H by A5;
hence M,v |= H / (y,x) by A1, Th12; ::_thesis: verum
end;
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) )
proof
let M be non empty set ; ::_thesis: 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) )
let i be Element of NAT ; ::_thesis: 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) )
let H1 be ZF-formula; ::_thesis: 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) )
let v1 be Function of VAR,M; ::_thesis: ( not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) implies 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) ) )
defpred S1[ ZF-formula, Element of NAT ] means for v1 being Function of VAR,M st not x. 0 in Free $1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),($1 <=> ((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 < $2 & 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' ($1,v1) = def_func' (H2,v2) );
defpred S2[ Element of NAT ] means for H being ZF-formula holds S1[H,$1];
A1: for i being Element of NAT st S2[i] holds
S2[i + 1]
proof
let i be Element of NAT ; ::_thesis: ( S2[i] implies S2[i + 1] )
assume A2: for H being ZF-formula holds S1[H,i] ; ::_thesis: S2[i + 1]
let H be ZF-formula; ::_thesis: S1[H,i + 1]
let v1 be Function of VAR,M; ::_thesis: ( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )
assume that
A3: not x. 0 in Free H and
A4: M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
A5: ( i = 0 implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )
proof
assume A6: i = 0 ; ::_thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
consider k being Element of NAT such that
A7: for j being Element of NAT st x. j in variables_in H holds
j < k by Th3;
( k > 4 or not k > 4 ) ;
then consider k1 being Element of NAT such that
A8: ( ( k > 4 & k1 = k ) or ( not k > 4 & k1 = 5 ) ) ;
take F = H / ((x. 0),(x. k1)); ::_thesis: ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 ) & not x. 0 in Free F & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,v2) )
take v1 / ((x. k1),(v1 . (x. 0))) ; ::_thesis: ( ( for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 ) & not x. 0 in Free F & M,v1 / ((x. k1),(v1 . (x. 0))) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,(v1 / ((x. k1),(v1 . (x. 0))))) )
thus for j being Element of NAT st j < i + 1 & x. j in variables_in F & not j = 3 holds
j = 4 ::_thesis: ( not x. 0 in Free F & M,v1 / ((x. k1),(v1 . (x. 0))) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,(v1 / ((x. k1),(v1 . (x. 0))))) )
proof
let j be Element of NAT ; ::_thesis: ( j < i + 1 & x. j in variables_in F & not j = 3 implies j = 4 )
assume j < i + 1 ; ::_thesis: ( not x. j in variables_in F or j = 3 or j = 4 )
then j <= 0 by A6, NAT_1:13;
then j = 0 by NAT_1:2;
hence ( not x. j in variables_in F or j = 3 or j = 4 ) by A8, ZF_LANG1:76, ZF_LANG1:184; ::_thesis: verum
end;
A9: x. k1 <> x. 0 by A8, ZF_LANG1:76;
k1 <> 3 by A8;
then A10: x. k1 <> x. 3 by ZF_LANG1:76;
A11: x. k1 <> x. 4 by A8, ZF_LANG1:76;
not x. k1 in variables_in H by A7, A8, XXREAL_0:2;
hence ( not x. 0 in Free F & M,v1 / ((x. k1),(v1 . (x. 0))) |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(F <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (F,(v1 / ((x. k1),(v1 . (x. 0))))) ) by A3, A4, A9, A10, A11, Th14; ::_thesis: verum
end;
A12: ( i <> 0 & i <> 3 & i <> 4 implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) )
proof
A13: x. 3 <> x. 4 by ZF_LANG1:76;
assume that
A14: i <> 0 and
A15: i <> 3 and
A16: i <> 4 ; ::_thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
A17: x. 0 <> x. i by A14, ZF_LANG1:76;
consider H1 being ZF-formula, v9 being Function of VAR,M such that
A18: for j being Element of NAT st j < i & x. j in variables_in H1 & not j = 3 holds
j = 4 and
A19: not x. 0 in Free H1 and
A20: M,v9 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) and
A21: def_func' (H,v1) = def_func' (H1,v9) by A2, A3, A4;
consider k being Element of NAT such that
A22: for j being Element of NAT st x. j in variables_in (All ((x. 4),(x. i),H1)) holds
j < k by Th3;
take H2 = H1 / ((x. i),(x. k)); ::_thesis: ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
take v2 = v9 / ((x. k),(v9 . (x. i))); ::_thesis: ( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
A23: variables_in (All ((x. 4),(x. i),H1)) = (variables_in H1) \/ {(x. 4),(x. i)} by ZF_LANG1:147;
x. i in {(x. 4),(x. i)} by TARSKI:def_2;
then A24: x. i in variables_in (All ((x. 4),(x. i),H1)) by A23, XBOOLE_0:def_3;
then A25: x. i <> x. k by A22;
then A26: v2 / ((x. i),(v2 . (x. k))) = (v9 / ((x. i),(v2 . (x. k)))) / ((x. k),(v9 . (x. i))) by FUNCT_7:33;
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ::_thesis: ( not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
proof
x. i in {(x. i)} by TARSKI:def_1;
then A27: not x. i in (variables_in H1) \ {(x. i)} by XBOOLE_0:def_5;
A28: not x. i in {(x. k)} by A25, TARSKI:def_1;
let j be Element of NAT ; ::_thesis: ( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )
A29: variables_in H2 c= ((variables_in H1) \ {(x. i)}) \/ {(x. k)} by ZF_LANG1:187;
assume j < i + 1 ; ::_thesis: ( not x. j in variables_in H2 or j = 3 or j = 4 )
then A30: j <= i by NAT_1:13;
then j < k by A22, A24, XXREAL_0:2;
then A31: x. j <> x. k by ZF_LANG1:76;
assume A32: x. j in variables_in H2 ; ::_thesis: ( j = 3 or j = 4 )
then ( x. j in (variables_in H1) \ {(x. i)} or x. j in {(x. k)} ) by A29, XBOOLE_0:def_3;
then A33: x. j in variables_in H1 by A31, TARSKI:def_1, XBOOLE_0:def_5;
( j = i or j < i ) by A30, XXREAL_0:1;
hence ( j = 3 or j = 4 ) by A18, A27, A28, A29, A32, A33, XBOOLE_0:def_3; ::_thesis: verum
end;
A34: v2 . (x. k) = v9 . (x. i) by FUNCT_7:128;
A35: Free H2 c= ((Free H1) \ {(x. i)}) \/ {(x. k)} by Th1;
A36: x. 4 <> x. i by A16, ZF_LANG1:76;
A37: x. 3 <> x. i by A15, ZF_LANG1:76;
then A38: (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) / ((x. i),(x. k)) = All ((x. 3),((Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))) / ((x. i),(x. k)))) by ZF_LANG1:159
.= All ((x. 3),(Ex ((x. 0),((All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))) / ((x. i),(x. k)))))) by A17, ZF_LANG1:164
.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),((H1 <=> ((x. 4) '=' (x. 0))) / ((x. i),(x. k)))))))) by A36, ZF_LANG1:159
.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> (((x. 4) '=' (x. 0)) / ((x. i),(x. k))))))))) by ZF_LANG1:163
.= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A17, A36, ZF_LANG1:152 ;
A39: v9 / ((x. i),(v9 . (x. i))) = v9 by FUNCT_7:35;
A40: not x. 0 in (Free H1) \ {(x. i)} by A19, XBOOLE_0:def_5;
not x. k in variables_in (All ((x. 4),(x. i),H1)) by A22;
then A41: not x. k in variables_in H1 by A23, XBOOLE_0:def_3;
x. 4 in {(x. 4),(x. i)} by TARSKI:def_2;
then A42: x. 4 in variables_in (All ((x. 4),(x. i),H1)) by A23, XBOOLE_0:def_3;
then A43: x. 4 <> x. k by A22;
then A44: not x. k in {(x. 4)} by TARSKI:def_1;
A45: 0 <> k by A22, A42;
then A46: x. 0 <> x. k by ZF_LANG1:76;
then A47: not x. k in {(x. 0)} by TARSKI:def_1;
not x. k in {(x. 4),(x. 0)} by A46, A43, TARSKI:def_2;
then not x. k in (variables_in H1) \/ {(x. 4),(x. 0)} by A41, XBOOLE_0:def_3;
then not x. k in ((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)} by A44, XBOOLE_0:def_3;
then A48: not x. k in (((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)} by A47, XBOOLE_0:def_3;
A49: x. 0 <> x. 3 by ZF_LANG1:76;
A50: not x. 0 in {(x. k)} by A46, TARSKI:def_1;
then A51: not x. 0 in Free H2 by A40, A35, XBOOLE_0:def_3;
thus not x. 0 in Free H2 by A40, A50, A35, XBOOLE_0:def_3; ::_thesis: ( M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
A52: variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) = (variables_in (Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) \/ {(x. 3)} by ZF_LANG1:142
.= ((variables_in (All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:146
.= (((variables_in (H1 <=> ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:142
.= ((((variables_in H1) \/ (variables_in ((x. 4) '=' (x. 0)))) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:145
.= ((((variables_in H1) \/ {(x. 4),(x. 0)}) \/ {(x. 4)}) \/ {(x. 0)}) \/ {(x. 3)} by ZF_LANG1:138 ;
A53: x. 0 <> x. 4 by ZF_LANG1:76;
A54: 3 <> k by A22, A42;
then A55: x. 3 <> x. k by ZF_LANG1:76;
then not x. k in {(x. 3)} by TARSKI:def_1;
then A56: not x. k in variables_in (All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0))))))))) by A52, A48, XBOOLE_0:def_3;
then M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) by A20, Th5;
hence A57: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A38, A56, A34, A39, A26, Th12; ::_thesis: def_func' (H,v1) = def_func' (H2,v2)
now__::_thesis:_for_e_being_Element_of_M_holds_(def_func'_(H2,v2))_._e_=_(def_func'_(H1,v9))_._e
let e be Element of M; ::_thesis: (def_func' (H2,v2)) . e = (def_func' (H1,v9)) . e
A58: v2 . (x. k) = v9 . (x. i) by FUNCT_7:128;
A59: (v2 / ((x. 3),e)) . (x. k) = v2 . (x. k) by A54, FUNCT_7:32, ZF_LANG1:76;
M,v9 / ((x. 3),e) |= Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))) by A20, ZF_LANG1:71;
then consider e9 being Element of M such that
A60: M,(v9 / ((x. 3),e)) / ((x. 0),e9) |= All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
A61: (((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9)) . (x. 0) = ((v9 / ((x. 3),e)) / ((x. 0),e9)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A62: ((v9 / ((x. 3),e)) / ((x. 0),e9)) . (x. 0) = e9 by FUNCT_7:128;
(((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9)) . (x. 4) = e9 by FUNCT_7:128;
then A63: M,((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) |= (x. 4) '=' (x. 0) by A61, A62, ZF_MODEL:12;
A64: M,((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) |= H1 <=> ((x. 4) '=' (x. 0)) by A60, ZF_LANG1:71;
then A65: M,((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) |= H1 by A63, ZF_MODEL:19;
A66: (v2 / ((x. 3),e)) . (x. k) = ((v2 / ((x. 3),e)) / ((x. 4),e9)) . (x. k) by A43, FUNCT_7:32;
A67: (((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) . (x. k) = ((v2 / ((x. 3),e)) / ((x. 4),e9)) . (x. k) by A45, FUNCT_7:32, ZF_LANG1:76;
A68: ((v9 / ((x. 3),e)) / ((x. 0),e9)) / ((x. 4),e9) = ((v9 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) by FUNCT_7:33, ZF_LANG1:76;
A69: v2 / ((x. i),(v2 . (x. k))) = (v9 / ((x. i),(v2 . (x. k)))) / ((x. k),(v9 . (x. i))) by A25, FUNCT_7:33;
A70: v9 / ((x. i),(v9 . (x. i))) = v9 by FUNCT_7:35;
((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) = (((v9 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) / ((x. k),(v9 . (x. i))) by A46, A55, A43, A49, A53, A13, Th7;
then A71: M,((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) |= H1 by A41, A65, A68, Th5;
(((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9)) / ((x. i),(v2 . (x. k))) = (((v2 / ((x. i),(v2 . (x. k)))) / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) by A17, A37, A36, A49, A53, A13, Th7;
then M,((v2 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) |= H2 by A41, A71, A67, A66, A59, A69, A58, A70, Th12;
then M,(v2 / ((x. 3),e)) / ((x. 4),e9) |= H2 by A51, Th9;
then A72: (def_func' (H2,v2)) . e = e9 by A51, A57, Th10;
M,((v9 / ((x. 3),e)) / ((x. 4),e9)) / ((x. 0),e9) |= H1 by A64, A63, A68, ZF_MODEL:19;
then M,(v9 / ((x. 3),e)) / ((x. 4),e9) |= H1 by A19, Th9;
hence (def_func' (H2,v2)) . e = (def_func' (H1,v9)) . e by A19, A20, A72, Th10; ::_thesis: verum
end;
hence def_func' (H2,v2) = def_func' (H,v1) by A21, FUNCT_2:63; ::_thesis: verum
end;
now__::_thesis:_(_(_i_=_3_or_i_=_4_)_implies_ex_H2_being_ZF-formula_ex_v2_being_Function_of_VAR,M_st_
(_(_for_j_being_Element_of_NAT_st_j_<_i_+_1_&_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'_(H,v1)_=_def_func'_(H2,v2)_)_)
assume A73: ( i = 3 or i = 4 ) ; ::_thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
thus ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) ::_thesis: verum
proof
consider H2 being ZF-formula, v2 being Function of VAR,M such that
A74: for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 and
A75: not x. 0 in Free H2 and
A76: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and
A77: def_func' (H,v1) = def_func' (H2,v2) by A2, A3, A4;
take H2 ; ::_thesis: ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
take v2 ; ::_thesis: ( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) )
thus for j being Element of NAT st j < i + 1 & x. j in variables_in H2 & not j = 3 holds
j = 4 ::_thesis: ( not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) )
proof
let j be Element of NAT ; ::_thesis: ( j < i + 1 & x. j in variables_in H2 & not j = 3 implies j = 4 )
assume that
A78: j < i + 1 and
A79: x. j in variables_in H2 ; ::_thesis: ( j = 3 or j = 4 )
j <= i by A78, NAT_1:13;
then ( j < i or j = i ) by XXREAL_0:1;
hence ( j = 3 or j = 4 ) by A73, A74, A79; ::_thesis: verum
end;
thus ( not x. 0 in Free H2 & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H2,v2) ) by A75, A76, A77; ::_thesis: verum
end;
end;
hence ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < i + 1 & 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' (H,v1) = def_func' (H2,v2) ) by A12, A5; ::_thesis: verum
end;
A80: S2[ 0 ]
proof
let H be ZF-formula; ::_thesis: S1[H, 0 ]
let v1 be Function of VAR,M; ::_thesis: ( not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < 0 & 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' (H,v1) = def_func' (H2,v2) ) )
assume that
A81: not x. 0 in Free H and
A82: M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: ex H2 being ZF-formula ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < 0 & 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' (H,v1) = def_func' (H2,v2) )
take H ; ::_thesis: ex v2 being Function of VAR,M st
( ( for j being Element of NAT st j < 0 & x. j in variables_in H & not j = 3 holds
j = 4 ) & not x. 0 in Free H & M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v2) )
take v1 ; ::_thesis: ( ( for j being Element of NAT st j < 0 & x. j in variables_in H & not j = 3 holds
j = 4 ) & not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v1) )
thus ( ( for j being Element of NAT st j < 0 & x. j in variables_in H & not j = 3 holds
j = 4 ) & not x. 0 in Free H & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & def_func' (H,v1) = def_func' (H,v1) ) by A81, A82, NAT_1:2; ::_thesis: verum
end;
for i being Element of NAT holds S2[i] from NAT_1:sch_1(A80, A1);
hence ( not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) implies 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) ) ) ; ::_thesis: verum
end;
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) )
proof
let M be non empty set ; ::_thesis: 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) )
let H1 be ZF-formula; ::_thesis: 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) )
let v1 be Function of VAR,M; ::_thesis: ( not x. 0 in Free H1 & M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) implies 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) ) )
assume that
A1: not x. 0 in Free H1 and
A2: M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: 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) )
consider i being Element of NAT such that
A3: for j being Element of NAT st x. j in variables_in H1 holds
j < i by Th3;
consider H2 being ZF-formula, v2 being Function of VAR,M such that
A4: for j being Element of NAT st j < i & x. j in variables_in H2 & not j = 3 holds
j = 4 and
A5: not x. 0 in Free H2 and
A6: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and
A7: def_func' (H1,v1) = def_func' (H2,v2) by A1, A2, Th16;
take H2 ; ::_thesis: 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) )
take v2 ; ::_thesis: ( (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) )
thus (Free H1) /\ (Free H2) c= {(x. 3),(x. 4)} ::_thesis: ( 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
A8: Free H2 c= variables_in H2 by ZF_LANG1:151;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (Free H1) /\ (Free H2) or a in {(x. 3),(x. 4)} )
A9: Free H1 c= variables_in H1 by ZF_LANG1:151;
assume A10: a in (Free H1) /\ (Free H2) ; ::_thesis: a in {(x. 3),(x. 4)}
then A11: a in Free H2 by XBOOLE_0:def_4;
reconsider x = a as Variable by A10;
consider j being Element of NAT such that
A12: x = x. j by ZF_LANG1:77;
a in Free H1 by A10, XBOOLE_0:def_4;
then ( j = 3 or j = 4 ) by A3, A4, A11, A12, A9, A8;
hence a in {(x. 3),(x. 4)} by A12, TARSKI:def_2; ::_thesis: verum
end;
thus ( 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) ) by A5, A6, A7; ::_thesis: verum
end;
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
proof
let M be non empty set ; ::_thesis: for F, G being Function st F is_definable_in M & G is_definable_in M holds
F * G is_definable_in M
let F, G be Function; ::_thesis: ( F is_definable_in M & G is_definable_in M implies F * G is_definable_in M )
set x0 = x. 0;
set x3 = x. 3;
set x4 = x. 4;
given H1 being ZF-formula such that A1: Free H1 c= {(x. 3),(x. 4)} and
A2: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) and
A3: F = def_func (H1,M) ; :: according to ZFMODEL1:def_3 ::_thesis: ( not G is_definable_in M or F * G is_definable_in M )
given H2 being ZF-formula such that A4: Free H2 c= {(x. 3),(x. 4)} and
A5: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and
A6: G = def_func (H2,M) ; :: according to ZFMODEL1:def_3 ::_thesis: F * G is_definable_in M
reconsider F = F, G = G as Function of M,M by A3, A6;
consider x being Variable such that
A7: not x in variables_in (All ((x. 0),(x. 3),(x. 4),(H1 '&' H2))) by Th3;
A8: variables_in (All ((x. 0),(x. 3),(x. 4),(H1 '&' H2))) = (variables_in (H1 '&' H2)) \/ {(x. 0),(x. 3),(x. 4)} by ZF_LANG1:149;
then A9: not x in {(x. 0),(x. 3),(x. 4)} by A7, XBOOLE_0:def_3;
then A10: x <> x. 3 by ENUMSET1:def_1;
take H = Ex (x,((H1 / ((x. 3),x)) '&' (H2 / ((x. 4),x)))); :: according to ZFMODEL1:def_3 ::_thesis: ( Free H c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F * G = def_func (H,M) )
thus A11: Free H c= {(x. 3),(x. 4)} ::_thesis: ( M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & F * G = def_func (H,M) )
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Free H or a in {(x. 3),(x. 4)} )
assume a in Free H ; ::_thesis: a in {(x. 3),(x. 4)}
then A12: a in (Free ((H1 / ((x. 3),x)) '&' (H2 / ((x. 4),x)))) \ {x} by ZF_LANG1:66;
then a in Free ((H1 / ((x. 3),x)) '&' (H2 / ((x. 4),x))) by XBOOLE_0:def_5;
then a in (Free (H1 / ((x. 3),x))) \/ (Free (H2 / ((x. 4),x))) by ZF_LANG1:61;
then ( ( Free (H1 / ((x. 3),x)) c= ((Free H1) \ {(x. 3)}) \/ {x} & a in Free (H1 / ((x. 3),x)) ) or ( Free (H2 / ((x. 4),x)) c= ((Free H2) \ {(x. 4)}) \/ {x} & a in Free (H2 / ((x. 4),x)) ) ) by Th1, XBOOLE_0:def_3;
then A13: ( ( (Free H1) \ {(x. 3)} c= Free H1 & a in ((Free H1) \ {(x. 3)}) \/ {x} ) or ( (Free H2) \ {(x. 4)} c= Free H2 & a in ((Free H2) \ {(x. 4)}) \/ {x} ) ) by XBOOLE_1:36;
not a in {x} by A12, XBOOLE_0:def_5;
then ( ( (Free H1) \ {(x. 3)} c= {(x. 3),(x. 4)} & a in (Free H1) \ {(x. 3)} ) or ( (Free H2) \ {(x. 4)} c= {(x. 3),(x. 4)} & a in (Free H2) \ {(x. 4)} ) ) by A1, A4, A13, XBOOLE_0:def_3, XBOOLE_1:1;
hence a in {(x. 3),(x. 4)} ; ::_thesis: verum
end;
A14: x. 0 <> x. 4 by ZF_LANG1:76;
A15: x. 3 <> x. 4 by ZF_LANG1:76;
A16: x <> x. 4 by A9, ENUMSET1:def_1;
variables_in (H1 '&' H2) = (variables_in H1) \/ (variables_in H2) by ZF_LANG1:141;
then A17: not x in (variables_in H1) \/ (variables_in H2) by A7, A8, XBOOLE_0:def_3;
then A18: not x in variables_in H1 by XBOOLE_0:def_3;
A19: not x in variables_in H2 by A17, XBOOLE_0:def_3;
A20: x. 0 <> x. 3 by ZF_LANG1:76;
then A21: not x. 0 in Free H2 by A4, A14, TARSKI:def_2;
thus A22: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ::_thesis: F * G = def_func (H,M)
proof
let v be Function of VAR,M; :: according to ZF_MODEL:def_5 ::_thesis: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
now__::_thesis:_for_m3_being_Element_of_M_holds_M,v_/_((x._3),m3)_|=_Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))
let m3 be Element of M; ::_thesis: M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) by A5, ZF_MODEL:def_5;
then M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:71;
then consider m0 being Element of M such that
A23: M,(v / ((x. 3),m3)) / ((x. 0),m0) |= All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) by A2, ZF_MODEL:def_5;
then M,v / ((x. 3),m0) |= Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:71;
then consider m being Element of M such that
A24: M,(v / ((x. 3),m0)) / ((x. 0),m) |= All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
now__::_thesis:_for_m4_being_Element_of_M_holds_M,((v_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_H_<=>_((x._4)_'='_(x._0))
let m4 be Element of M; ::_thesis: M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0))
A25: now__::_thesis:_(_M,((v_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_H_implies_M,((v_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_(x._4)_'='_(x._0)_)
assume M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H ; ::_thesis: M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0)
then consider m9 being Element of M such that
A26: M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9) |= (H1 / ((x. 3),x)) '&' (H2 / ((x. 4),x)) by ZF_LANG1:73;
set v9 = (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9);
A27: ((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9)) . x = m9 by FUNCT_7:128;
A28: ((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9)) / ((x. 4),m9) = (((v / ((x. 3),m3)) / ((x. 0),m)) / (x,m9)) / ((x. 4),m9) by Th8
.= (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m9)) / (x,m9) by A16, FUNCT_7:33 ;
M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9) |= H2 / ((x. 4),x) by A26, ZF_MODEL:15;
then M,((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9)) / ((x. 4),m9) |= H2 by A19, A27, Th12;
then A29: M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m9) |= H2 by A19, A28, Th5;
A30: ((v / ((x. 3),m3)) / ((x. 4),m9)) / ((x. 0),m0) = (((v / ((x. 3),m3)) / ((x. 4),m9)) / ((x. 0),m)) / ((x. 0),m0) by FUNCT_7:34;
A31: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A32: (((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m0)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9) |= H1 / ((x. 3),x) by A26, ZF_MODEL:15;
then A33: M,((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9)) / ((x. 3),m9) |= H1 by A18, A27, Th12;
A34: ((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9) = ((v / ((x. 3),m3)) / ((x. 4),m9)) / ((x. 0),m0) by FUNCT_7:33, ZF_LANG1:76;
A35: M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9) |= H2 <=> ((x. 4) '=' (x. 0)) by A23, ZF_LANG1:71;
A36: (((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m0)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m9) = ((v / ((x. 3),m3)) / ((x. 4),m9)) / ((x. 0),m) by FUNCT_7:33, ZF_LANG1:76;
then M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9) |= H2 by A21, A30, A34, A29, Th9;
then M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9) |= (x. 4) '=' (x. 0) by A35, ZF_MODEL:19;
then A37: (((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9)) . (x. 4) = (((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9)) . (x. 0) by ZF_MODEL:12;
A38: ((v / ((x. 3),m3)) / ((x. 0),m0)) . (x. 0) = m0 by FUNCT_7:128;
(((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m9)) . (x. 4) = m9 by FUNCT_7:128;
then ((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9)) / ((x. 3),m9) = ((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / ((x. 3),m0)) / (x,m9) by A10, A37, A38, A36, FUNCT_7:33
.= (((v / ((x. 0),m)) / ((x. 4),m4)) / ((x. 3),m0)) / (x,m9) by Th8
.= (((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m9) by A20, A14, A15, Th6 ;
then A39: M,((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4) |= H1 by A18, A33, Th5;
M,((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4) |= H1 <=> ((x. 4) '=' (x. 0)) by A24, ZF_LANG1:71;
then M,((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A39, ZF_MODEL:19;
then A40: (((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = (((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) by ZF_MODEL:12;
A41: ((v / ((x. 3),m0)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A42: ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A43: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
(((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
hence M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A40, A41, A43, A42, A32, A31, ZF_MODEL:12; ::_thesis: verum
end;
now__::_thesis:_(_M,((v_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_(x._4)_'='_(x._0)_implies_M,((v_/_((x._3),m3))_/_((x._0),m))_/_((x._4),m4)_|=_H_)
set v9 = (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0);
A44: ((v / ((x. 3),m0)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A45: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
A46: M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0) |= H2 <=> ((x. 4) '=' (x. 0)) by A23, ZF_LANG1:71;
A47: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
assume M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ; ::_thesis: M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H
then A48: (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) by ZF_MODEL:12;
A49: ((v / ((x. 3),m3)) / ((x. 0),m)) . (x. 0) = m by FUNCT_7:128;
A50: (((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m0)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A51: M,((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4) |= H1 <=> ((x. 4) '=' (x. 0)) by A24, ZF_LANG1:71;
A52: (((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m0)) / ((x. 0),m)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
(((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
then M,((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A48, A44, A45, A49, A52, A47, ZF_MODEL:12;
then M,((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4) |= H1 by A51, ZF_MODEL:19;
then A53: M,(((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0) |= H1 by A18, Th5;
A54: ((v / ((x. 3),m3)) / ((x. 0),m0)) . (x. 0) = m0 by FUNCT_7:128;
(((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0)) . (x. 4) = m0 by FUNCT_7:128;
then M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0) |= (x. 4) '=' (x. 0) by A54, A50, ZF_MODEL:12;
then M,((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0) |= H2 by A46, ZF_MODEL:19;
then A55: M,(((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0)) / ((x. 0),m) |= H2 by A21, Th9;
A56: ((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m0) = ((v / ((x. 3),m3)) / ((x. 4),m0)) / ((x. 0),m) by FUNCT_7:33, ZF_LANG1:76;
(((v / ((x. 3),m3)) / ((x. 0),m0)) / ((x. 4),m0)) / ((x. 0),m) = ((v / ((x. 3),m3)) / ((x. 4),m0)) / ((x. 0),m) by Th8;
then A57: M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m0)) / (x,m0) |= H2 by A19, A55, A56, Th5;
A58: ((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0)) . x = m0 by FUNCT_7:128;
((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0)) / ((x. 3),m0) = ((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / ((x. 3),m0)) / (x,m0) by A10, FUNCT_7:33
.= (((v / ((x. 0),m)) / ((x. 4),m4)) / ((x. 3),m0)) / (x,m0) by Th8
.= (((v / ((x. 3),m0)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0) by A20, A14, A15, Th6 ;
then A59: M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0) |= H1 / ((x. 3),x) by A18, A53, A58, Th12;
((((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0)) / ((x. 4),m0) = (((v / ((x. 3),m3)) / ((x. 0),m)) / (x,m0)) / ((x. 4),m0) by Th8
.= (((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m0)) / (x,m0) by A16, FUNCT_7:33 ;
then M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0) |= H2 / ((x. 4),x) by A19, A57, A58, Th12;
then M,(((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4)) / (x,m0) |= (H1 / ((x. 3),x)) '&' (H2 / ((x. 4),x)) by A59, ZF_MODEL:15;
hence M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H by ZF_LANG1:73; ::_thesis: verum
end;
hence M,((v / ((x. 3),m3)) / ((x. 0),m)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A25, ZF_MODEL:19; ::_thesis: verum
end;
then M,(v / ((x. 3),m3)) / ((x. 0),m) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:71;
hence M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:73; ::_thesis: verum
end;
hence M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by ZF_LANG1:71; ::_thesis: verum
end;
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_
(_(_M,v_|=_H_implies_(F_*_G)_._(v_._(x._3))_=_v_._(x._4)_)_&_(_(F_*_G)_._(v_._(x._3))_=_v_._(x._4)_implies_M,v_|=_H_)_)
let v be Function of VAR,M; ::_thesis: ( ( M,v |= H implies (F * G) . (v . (x. 3)) = v . (x. 4) ) & ( (F * G) . (v . (x. 3)) = v . (x. 4) implies M,v |= H ) )
thus ( M,v |= H implies (F * G) . (v . (x. 3)) = v . (x. 4) ) ::_thesis: ( (F * G) . (v . (x. 3)) = v . (x. 4) implies M,v |= H )
proof
assume M,v |= H ; ::_thesis: (F * G) . (v . (x. 3)) = v . (x. 4)
then consider m being Element of M such that
A60: M,v / (x,m) |= (H1 / ((x. 3),x)) '&' (H2 / ((x. 4),x)) by ZF_LANG1:73;
A61: (v / (x,m)) . x = m by FUNCT_7:128;
M,v / (x,m) |= H1 / ((x. 3),x) by A60, ZF_MODEL:15;
then M,(v / (x,m)) / ((x. 3),m) |= H1 by A18, A61, Th12;
then A62: F . (((v / (x,m)) / ((x. 3),m)) . (x. 3)) = ((v / (x,m)) / ((x. 3),m)) . (x. 4) by A1, A2, A3, ZFMODEL1:def_2;
A63: ((v / (x,m)) / ((x. 3),m)) . (x. 3) = m by FUNCT_7:128;
A64: ((v / (x,m)) / ((x. 4),m)) . (x. 3) = (v / (x,m)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A65: v . (x. 3) = (v / (x,m)) . (x. 3) by A10, FUNCT_7:32;
A66: ((v / (x,m)) / ((x. 3),m)) . (x. 4) = (v / (x,m)) . (x. 4) by FUNCT_7:32, ZF_LANG1:76;
M,v / (x,m) |= H2 / ((x. 4),x) by A60, ZF_MODEL:15;
then M,(v / (x,m)) / ((x. 4),m) |= H2 by A19, A61, Th12;
then A67: G . (((v / (x,m)) / ((x. 4),m)) . (x. 3)) = ((v / (x,m)) / ((x. 4),m)) . (x. 4) by A4, A5, A6, ZFMODEL1:def_2;
A68: ((v / (x,m)) / ((x. 4),m)) . (x. 4) = m by FUNCT_7:128;
v . (x. 4) = (v / (x,m)) . (x. 4) by A16, FUNCT_7:32;
hence (F * G) . (v . (x. 3)) = v . (x. 4) by A62, A63, A67, A68, A66, A64, A65, FUNCT_2:15; ::_thesis: verum
end;
set m = G . (v . (x. 3));
A69: (v / ((x. 4),(G . (v . (x. 3))))) . (x. 4) = G . (v . (x. 3)) by FUNCT_7:128;
A70: (v / (x,(G . (v . (x. 3))))) . x = G . (v . (x. 3)) by FUNCT_7:128;
A71: (v / (x,(G . (v . (x. 3))))) / ((x. 4),(G . (v . (x. 3)))) = (v / ((x. 4),(G . (v . (x. 3))))) / (x,(G . (v . (x. 3)))) by A16, FUNCT_7:33;
(v / ((x. 4),(G . (v . (x. 3))))) . (x. 3) = v . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
then M,v / ((x. 4),(G . (v . (x. 3)))) |= H2 by A4, A5, A6, A69, ZFMODEL1:def_2;
then M,(v / (x,(G . (v . (x. 3))))) / ((x. 4),(G . (v . (x. 3)))) |= H2 by A19, A71, Th5;
then A72: M,v / (x,(G . (v . (x. 3)))) |= H2 / ((x. 4),x) by A19, A70, Th12;
A73: (v / ((x. 3),(G . (v . (x. 3))))) . (x. 3) = G . (v . (x. 3)) by FUNCT_7:128;
assume (F * G) . (v . (x. 3)) = v . (x. 4) ; ::_thesis: M,v |= H
then A74: F . (G . (v . (x. 3))) = v . (x. 4) by FUNCT_2:15;
A75: (v / (x,(G . (v . (x. 3))))) / ((x. 3),(G . (v . (x. 3)))) = (v / ((x. 3),(G . (v . (x. 3))))) / (x,(G . (v . (x. 3)))) by A10, FUNCT_7:33;
(v / ((x. 3),(G . (v . (x. 3))))) . (x. 4) = v . (x. 4) by FUNCT_7:32, ZF_LANG1:76;
then M,v / ((x. 3),(G . (v . (x. 3)))) |= H1 by A1, A2, A3, A74, A73, ZFMODEL1:def_2;
then M,(v / (x,(G . (v . (x. 3))))) / ((x. 3),(G . (v . (x. 3)))) |= H1 by A18, A75, Th5;
then M,v / (x,(G . (v . (x. 3)))) |= H1 / ((x. 3),x) by A18, A70, Th12;
then M,v / (x,(G . (v . (x. 3)))) |= (H1 / ((x. 3),x)) '&' (H2 / ((x. 4),x)) by A72, ZF_MODEL:15;
hence M,v |= H by ZF_LANG1:73; ::_thesis: verum
end;
hence F * G = def_func (H,M) by A11, A22, ZFMODEL1:def_2; ::_thesis: verum
end;
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 ) )
proof
let M be non empty set ; ::_thesis: 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 ) )
let H be ZF-formula; ::_thesis: 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 ) )
let v be Function of VAR,M; ::_thesis: ( not x. 0 in Free H implies ( 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 ) ) )
assume A1: not x. 0 in Free H ; ::_thesis: ( 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 ) )
thus ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) implies 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 ) ) ::_thesis: ( ( 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 ) ) implies M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) )
proof
assume A2: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) ; ::_thesis: 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 )
let m1 be Element of M; ::_thesis: 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 )
M,v / ((x. 3),m1) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by A2, ZF_LANG1:71;
then consider m2 being Element of M such that
A3: M,(v / ((x. 3),m1)) / ((x. 0),m2) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:73;
take m2 ; ::_thesis: for m3 being Element of M holds
( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H iff m3 = m2 )
let m3 be Element of M; ::_thesis: ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H iff m3 = m2 )
thus ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = m2 ) ::_thesis: ( m3 = m2 implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H )
proof
assume M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ; ::_thesis: m3 = m2
then M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. 0),m2) |= H by A1, Th9;
then A4: M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H by FUNCT_7:33, ZF_LANG1:76;
M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H <=> ((x. 4) '=' (x. 0)) by A3, ZF_LANG1:71;
then A5: M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= (x. 4) '=' (x. 0) by A4, ZF_MODEL:19;
A6: m2 = ((v / ((x. 3),m1)) / ((x. 0),m2)) . (x. 0) by FUNCT_7:128;
A7: (((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3)) . (x. 0) = ((v / ((x. 3),m1)) / ((x. 0),m2)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
(((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3)) . (x. 4) = m3 by FUNCT_7:128;
hence m3 = m2 by A6, A7, A5, ZF_MODEL:12; ::_thesis: verum
end;
assume m3 = m2 ; ::_thesis: M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H
then A8: M,((v / ((x. 3),m1)) / ((x. 0),m3)) / ((x. 4),m3) |= H <=> ((x. 4) '=' (x. 0)) by A3, ZF_LANG1:71;
A9: (((v / ((x. 3),m1)) / ((x. 0),m3)) / ((x. 4),m3)) . (x. 0) = ((v / ((x. 3),m1)) / ((x. 0),m3)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A10: ((v / ((x. 3),m1)) / ((x. 0),m3)) . (x. 0) = m3 by FUNCT_7:128;
(((v / ((x. 3),m1)) / ((x. 0),m3)) / ((x. 4),m3)) . (x. 4) = m3 by FUNCT_7:128;
then M,((v / ((x. 3),m1)) / ((x. 0),m3)) / ((x. 4),m3) |= (x. 4) '=' (x. 0) by A9, A10, ZF_MODEL:12;
then M,((v / ((x. 3),m1)) / ((x. 0),m3)) / ((x. 4),m3) |= H by A8, ZF_MODEL:19;
then M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. 0),m3) |= H by FUNCT_7:33, ZF_LANG1:76;
hence M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H by A1, Th9; ::_thesis: verum
end;
assume A11: 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 ) ; ::_thesis: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
now__::_thesis:_for_m1_being_Element_of_M_holds_M,v_/_((x._3),m1)_|=_Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))
let m1 be Element of M; ::_thesis: M,v / ((x. 3),m1) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))
consider m2 being Element of M such that
A12: for m3 being Element of M holds
( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H iff m3 = m2 ) by A11;
now__::_thesis:_for_m3_being_Element_of_M_holds_M,((v_/_((x._3),m1))_/_((x._0),m2))_/_((x._4),m3)_|=_H_<=>_((x._4)_'='_(x._0))
let m3 be Element of M; ::_thesis: M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H <=> ((x. 4) '=' (x. 0))
A13: (((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3)) . (x. 0) = ((v / ((x. 3),m1)) / ((x. 0),m2)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A14: ((v / ((x. 3),m1)) / ((x. 0),m2)) . (x. 0) = m2 by FUNCT_7:128;
A15: (((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3)) . (x. 4) = m3 by FUNCT_7:128;
A16: now__::_thesis:_(_M,((v_/_((x._3),m1))_/_((x._0),m2))_/_((x._4),m3)_|=_(x._4)_'='_(x._0)_implies_M,((v_/_((x._3),m1))_/_((x._0),m2))_/_((x._4),m3)_|=_H_)
assume M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= (x. 4) '=' (x. 0) ; ::_thesis: M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H
then m3 = m2 by A15, A13, A14, ZF_MODEL:12;
then M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H by A12;
then M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. 0),m2) |= H by A1, Th9;
hence M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H by FUNCT_7:33, ZF_LANG1:76; ::_thesis: verum
end;
now__::_thesis:_(_M,((v_/_((x._3),m1))_/_((x._0),m2))_/_((x._4),m3)_|=_H_implies_M,((v_/_((x._3),m1))_/_((x._0),m2))_/_((x._4),m3)_|=_(x._4)_'='_(x._0)_)
assume M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H ; ::_thesis: M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= (x. 4) '=' (x. 0)
then M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. 0),m2) |= H by FUNCT_7:33, ZF_LANG1:76;
then M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H by A1, Th9;
then m3 = m2 by A12;
hence M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= (x. 4) '=' (x. 0) by A15, A13, A14, ZF_MODEL:12; ::_thesis: verum
end;
hence M,((v / ((x. 3),m1)) / ((x. 0),m2)) / ((x. 4),m3) |= H <=> ((x. 4) '=' (x. 0)) by A16, ZF_MODEL:19; ::_thesis: verum
end;
then M,(v / ((x. 3),m1)) / ((x. 0),m2) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:71;
hence M,v / ((x. 3),m1) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:73; ::_thesis: verum
end;
hence M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by ZF_LANG1:71; ::_thesis: verum
end;
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
proof
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:30;
A2: {(x. 3)} \/ {(x. 3),(x. 4)} = {(x. 3),(x. 3),(x. 4)} by ENUMSET1:2;
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
set v = the 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_3;
reconsider b = b as Element of M by A13;
A15: ( M, the Function of VAR,M / ((x. 3),b) |= H or M, the Function of VAR,M / ((x. 3),b) |= 'not' H ) by ZF_MODEL:14;
( the Function of VAR,M / ((x. 3),b)) . (x. 3) = b by FUNCT_7:128;
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:4;
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:60;
Free (H '&' H1) = (Free H) \/ (Free H1) by ZF_LANG1:61;
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:61;
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:63;
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__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_All_((x._3),(Ex_((x._0),(All_((x._4),(I_<=>_((x._4)_'='_(x._0))))))))
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__::_thesis:_for_m3_being_Element_of_M_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_)_)
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, Th19;
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, Th19;
( ( 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, Th9; ::_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, 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) |= 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, Th19; ::_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__::_thesis:_for_a_being_Element_of_M_holds_f_._a_=_(def_func_(I,M))_._a
set v = the 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, the Function of VAR,M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(I <=> ((x. 4) '=' (x. 0)))))))) by A23;
def_func (I,M) = def_func' (I, the Function of VAR,M) by A21, A17, A20, A27, Th11, XBOOLE_1:8;
then M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= I by A22, A28, Th10;
then ( M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H '&' H1 or M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= ('not' H) '&' H2 ) by ZF_MODEL:17;
then ( ( M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H & M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H1 & M, the Function of VAR,M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) & def_func (H1,M) = def_func' (H1, the Function of VAR,M) ) or ( M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= 'not' H & M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),((def_func (I,M)) . a)) |= H2 & M, the Function of VAR,M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) & def_func (H2,M) = def_func' (H2, the Function of VAR,M) ) ) by A3, A4, A6, A7, Th11, ZF_MODEL:15, ZF_MODEL:def_5;
then A29: ( ( M, the Function of VAR,M / ((x. 3),a) |= H & (def_func (I,M)) . a = F . a ) or ( M, the Function of VAR,M / ((x. 3),a) |= 'not' H & (def_func (I,M)) . a = G . a ) ) by A5, A8, A10, A16, A19, A18, Th9, Th10;
( the Function of VAR,M / ((x. 3),a)) . (x. 3) = a by FUNCT_7:128;
hence f . a = (def_func (I,M)) . a by A12, A29; ::_thesis: verum
end;
hence FG = def_func (I,M) by FUNCT_2:63; ::_thesis: verum
end;
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
proof
let M be non empty set ; ::_thesis: 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
let F, G be Function; ::_thesis: ( F is_parametrically_definable_in M & G is_parametrically_definable_in M implies G * F is_parametrically_definable_in M )
given H1 being ZF-formula, v1 being Function of VAR,M such that A1: {(x. 0),(x. 1),(x. 2)} misses Free H1 and
A2: M,v1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H1 <=> ((x. 4) '=' (x. 0)))))))) and
A3: F = def_func' (H1,v1) ; :: according to ZFMODEL1:def_4 ::_thesis: ( not G is_parametrically_definable_in M or G * F is_parametrically_definable_in M )
given H2 being ZF-formula, v2 being Function of VAR,M such that A4: {(x. 0),(x. 1),(x. 2)} misses Free H2 and
A5: M,v2 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H2 <=> ((x. 4) '=' (x. 0)))))))) and
A6: G = def_func' (H2,v2) ; :: according to ZFMODEL1:def_4 ::_thesis: G * F is_parametrically_definable_in M
reconsider F9 = F, G9 = G as Function of M,M by A3, A6;
deffunc H1( set ) -> set = v2 . $1;
consider i being Element of NAT such that
A7: for j being Element of NAT st x. j in variables_in H2 holds
j < i by Th3;
( i > 4 or not i > 4 ) ;
then consider i3 being Element of NAT such that
A8: ( ( i > 4 & i3 = i ) or ( not i > 4 & i3 = 5 ) ) ;
A9: x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
then not x. 0 in Free H1 by A1, XBOOLE_0:3;
then consider H3 being ZF-formula, v3 being Function of VAR,M such that
A10: for j being Element of NAT st j < i3 & x. j in variables_in H3 & not j = 3 holds
j = 4 and
A11: not x. 0 in Free H3 and
A12: M,v3 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H3 <=> ((x. 4) '=' (x. 0)))))))) and
A13: def_func' (H1,v1) = def_func' (H3,v3) by A2, Th16;
consider k1 being Element of NAT such that
A14: for j being Element of NAT st x. j in variables_in H3 holds
j < k1 by Th3;
( k1 > i3 or k1 <= i3 ) ;
then consider k being Element of NAT such that
A15: ( ( k1 > i3 & k = k1 ) or ( k1 <= i3 & k = i3 + 1 ) ) ;
deffunc H2( set ) -> set = v3 . $1;
defpred S1[ set ] means $1 in Free H3;
take H = Ex ((x. k),((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))))); :: according to ZFMODEL1:def_4 ::_thesis: ex b1 being Element of K27(K28(VAR,M)) st
( {(x. 0),(x. 1),(x. 2)} misses Free H & M,b1 |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & G * F = def_func' (H,b1) )
consider v being Function such that
A16: ( dom v = VAR & ( for a being set st a in VAR holds
( ( S1[a] implies v . a = H2(a) ) & ( not S1[a] implies v . a = H1(a) ) ) ) ) from PARTFUN1:sch_1();
rng v c= M
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in rng v or b in M )
assume b in rng v ; ::_thesis: b in M
then consider a being set such that
A17: a in dom v and
A18: b = v . a by FUNCT_1:def_3;
reconsider a = a as Variable by A16, A17;
( b = v3 . a or b = v2 . a ) by A16, A18;
hence b in M ; ::_thesis: verum
end;
then reconsider v = v as Function of VAR,M by A16, FUNCT_2:def_1, RELSET_1:4;
take v ; ::_thesis: ( {(x. 0),(x. 1),(x. 2)} misses Free H & M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & G * F = def_func' (H,v) )
A19: {(x. 0),(x. 1),(x. 2)} misses Free H3
proof
A20: i3 > 2 by A8, XXREAL_0:2;
A21: i3 > 1 by A8, XXREAL_0:2;
assume {(x. 0),(x. 1),(x. 2)} meets Free H3 ; ::_thesis: contradiction
then consider a being set such that
A22: a in {(x. 0),(x. 1),(x. 2)} and
A23: a in Free H3 by XBOOLE_0:3;
A24: Free H3 c= variables_in H3 by ZF_LANG1:151;
( a = x. 0 or a = x. 1 or a = x. 2 ) by A22, ENUMSET1:def_1;
hence contradiction by A10, A21, A20, A23, A24; ::_thesis: verum
end;
A25: now__::_thesis:_for_a_being_set_st_a_in_{(x._0),(x._1),(x._2)}_holds_
not_a_in_Free_H
let a be set ; ::_thesis: ( a in {(x. 0),(x. 1),(x. 2)} implies not a in Free H )
assume A26: a in {(x. 0),(x. 1),(x. 2)} ; ::_thesis: not a in Free H
assume a in Free H ; ::_thesis: contradiction
then A27: a in (Free ((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))))) \ {(x. k)} by ZF_LANG1:66;
then A28: not a in {(x. k)} by XBOOLE_0:def_5;
A29: Free ((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k)))) = (Free (H3 / ((x. 4),(x. k)))) \/ (Free (H2 / ((x. 3),(x. k)))) by ZF_LANG1:61;
a in Free ((H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k)))) by A27, XBOOLE_0:def_5;
then ( ( Free (H3 / ((x. 4),(x. k))) c= ((Free H3) \ {(x. 4)}) \/ {(x. k)} & a in Free (H3 / ((x. 4),(x. k))) ) or ( a in Free (H2 / ((x. 3),(x. k))) & Free (H2 / ((x. 3),(x. k))) c= ((Free H2) \ {(x. 3)}) \/ {(x. k)} ) ) by A29, Th1, XBOOLE_0:def_3;
then ( a in (Free H3) \ {(x. 4)} or a in (Free H2) \ {(x. 3)} ) by A28, XBOOLE_0:def_3;
then ( a in Free H3 or a in Free H2 ) by XBOOLE_0:def_5;
hence contradiction by A4, A19, A26, XBOOLE_0:3; ::_thesis: verum
end;
hence {(x. 0),(x. 1),(x. 2)} misses Free H by XBOOLE_0:3; ::_thesis: ( M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & G * F = def_func' (H,v) )
x. 0 in {(x. 0),(x. 1),(x. 2)} by ENUMSET1:def_1;
then A30: not x. 0 in Free H by A25;
A31: k <> 4 by A8, A15, NAT_1:13;
then A32: x. k <> x. 4 by ZF_LANG1:76;
A33: i <= i3 by A8, XXREAL_0:2;
A34: not x. k in variables_in H2
proof
assume x. k in variables_in H2 ; ::_thesis: contradiction
then k < i by A7;
hence contradiction by A33, A15, NAT_1:13, XXREAL_0:2; ::_thesis: verum
end;
A35: for x being Variable holds
( not x in Free H2 or not x in Free H3 or x = x. 3 or x = x. 4 )
proof
let x be Variable; ::_thesis: ( not x in Free H2 or not x in Free H3 or x = x. 3 or x = x. 4 )
A36: Free H3 c= variables_in H3 by ZF_LANG1:151;
assume that
A37: x in Free H2 and
A38: x in Free H3 ; ::_thesis: ( x = x. 3 or x = x. 4 )
consider j being Element of NAT such that
A39: x = x. j by ZF_LANG1:77;
Free H2 c= variables_in H2 by ZF_LANG1:151;
then j < i3 by A7, A33, A39, A37, XXREAL_0:2;
hence ( x = x. 3 or x = x. 4 ) by A10, A36, A39, A38; ::_thesis: verum
end;
A40: k <> 3 by A8, A15, NAT_1:13, XXREAL_0:2;
then A41: x. k <> x. 3 by ZF_LANG1:76;
A42: not x. k in variables_in H3
proof
assume x. k in variables_in H3 ; ::_thesis: contradiction
then k < k1 by A14;
hence contradiction by A15, NAT_1:13; ::_thesis: verum
end;
A43: not x. 0 in Free H2 by A4, A9, XBOOLE_0:3;
now__::_thesis:_for_m1_being_Element_of_M_ex_r_being_Element_of_M_st_
for_m3_being_Element_of_M_holds_
(_(_M,(v_/_((x._3),m1))_/_((x._4),m3)_|=_H_implies_m3_=_r_)_&_(_m3_=_r_implies_M,(v_/_((x._3),m1))_/_((x._4),m3)_|=_H_)_)
let m1 be Element of M; ::_thesis: ex r being Element of M st
for m3 being Element of M holds
( ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) & ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ) )
A44: not x. 3 in variables_in (H2 / ((x. 3),(x. k))) by A40, ZF_LANG1:76, ZF_LANG1:184;
consider m being Element of M such that
A45: for m4 being Element of M holds
( M,(v3 / ((x. 3),m1)) / ((x. 4),m4) |= H3 iff m4 = m ) by A11, A12, Th19;
A46: now__::_thesis:_for_x_being_Variable_st_x_in_Free_(H3_/_((x._4),(x._k)))_holds_
((v_/_((x._3),m1))_/_((x._k),m))_._x_=_((v3_/_((x._3),m1))_/_((x._k),m))_._x
let x be Variable; ::_thesis: ( x in Free (H3 / ((x. 4),(x. k))) implies ((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x )
assume A47: x in Free (H3 / ((x. 4),(x. k))) ; ::_thesis: ((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x
Free (H3 / ((x. 4),(x. k))) c= ((Free H3) \ {(x. 4)}) \/ {(x. k)} by Th1;
then ( x in (Free H3) \ {(x. 4)} or x in {(x. k)} ) by A47, XBOOLE_0:def_3;
then ( ( x in Free H3 & not x in {(x. 4)} ) or x = x. k ) by TARSKI:def_1, XBOOLE_0:def_5;
then ( ( ( ( x in Free H3 & x. 3 <> x & x <> x. k ) or x = x. 4 or x = x. 3 ) & x <> x. 4 ) or ( ((v / ((x. 3),m1)) / ((x. k),m)) . x = m & ((v3 / ((x. 3),m1)) / ((x. k),m)) . x = m ) ) by FUNCT_7:128, TARSKI:def_1;
then ( ( ((v / ((x. 3),m1)) / ((x. k),m)) . x = (v / ((x. 3),m1)) . x & (v / ((x. 3),m1)) . x = v . x & v . x = v3 . x & v3 . x = (v3 / ((x. 3),m1)) . x & (v3 / ((x. 3),m1)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x ) or ( ((v / ((x. 3),m1)) / ((x. k),m)) . x = (v / ((x. 3),m1)) . x & (v / ((x. 3),m1)) . x = m1 & m1 = (v3 / ((x. 3),m1)) . x & (v3 / ((x. 3),m1)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x ) or ((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x ) by A41, A16, FUNCT_7:32, FUNCT_7:128;
hence ((v / ((x. 3),m1)) / ((x. k),m)) . x = ((v3 / ((x. 3),m1)) / ((x. k),m)) . x ; ::_thesis: verum
end;
consider r being Element of M such that
A48: for m4 being Element of M holds
( M,(v2 / ((x. 3),m)) / ((x. 4),m4) |= H2 iff m4 = r ) by A5, A43, Th19;
take r = r; ::_thesis: for m3 being Element of M holds
( ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) & ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ) )
let m3 be Element of M; ::_thesis: ( ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) & ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ) )
A49: ((v3 / ((x. 3),m1)) / ((x. 4),m)) . (x. 4) = m by FUNCT_7:128;
thus ( M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H implies m3 = r ) ::_thesis: ( m3 = r implies M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H )
proof
A50: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H2_holds_
((v_/_((x._3),m))_/_((x._4),m3))_._x_=_((v2_/_((x._3),m))_/_((x._4),m3))_._x
let x be Variable; ::_thesis: ( x in Free H2 implies ((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x )
assume x in Free H2 ; ::_thesis: ((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x
then ( ( not x in Free H3 & x <> x. 3 & x <> x. 4 ) or x = x. 3 or x = x. 4 ) by A35;
then ( ( ((v / ((x. 3),m)) / ((x. 4),m3)) . x = (v / ((x. 3),m)) . x & (v / ((x. 3),m)) . x = v . x & v . x = v2 . x & v2 . x = (v2 / ((x. 3),m)) . x & (v2 / ((x. 3),m)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x ) or ( ((v / ((x. 3),m)) / ((x. 4),m3)) . x = (v / ((x. 3),m)) . x & (v / ((x. 3),m)) . x = m & ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x = (v2 / ((x. 3),m)) . x & (v2 / ((x. 3),m)) . x = m ) or ( ((v / ((x. 3),m)) / ((x. 4),m3)) . x = m3 & ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x = m3 ) ) by A16, Lm3, FUNCT_7:32, FUNCT_7:128;
hence ((v / ((x. 3),m)) / ((x. 4),m3)) . x = ((v2 / ((x. 3),m)) / ((x. 4),m3)) . x ; ::_thesis: verum
end;
assume M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H ; ::_thesis: m3 = r
then consider n being Element of M such that
A51: M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),n) |= (H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))) by ZF_LANG1:73;
A52: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H3_holds_
((v_/_((x._3),m1))_/_((x._4),n))_._x_=_((v3_/_((x._3),m1))_/_((x._4),n))_._x
let x be Variable; ::_thesis: ( x in Free H3 implies ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x )
assume A53: x in Free H3 ; ::_thesis: ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x
A54: ((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 4) = n by FUNCT_7:128;
A55: ((v3 / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v3 / ((x. 3),m1)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A56: ((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v / ((x. 3),m1)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A57: (v / ((x. 3),m1)) . (x. 3) = m1 by FUNCT_7:128;
( x = x. 3 or x = x. 4 or ( x <> x. 3 & x <> x. 4 ) ) ;
then ( ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x or ( (v / ((x. 3),m1)) . x = v . x & (v3 / ((x. 3),m1)) . x = v3 . x & ((v / ((x. 3),m1)) / ((x. 4),n)) . x = (v / ((x. 3),m1)) . x & ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x = (v3 / ((x. 3),m1)) . x ) ) by A54, A57, A56, A55, FUNCT_7:32, FUNCT_7:128;
hence ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x by A16, A53; ::_thesis: verum
end;
A58: M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),n) |= H2 / ((x. 3),(x. k)) by A51, ZF_MODEL:15;
A59: (((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),n)) . (x. k) = n by FUNCT_7:128;
M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),n) |= H3 / ((x. 4),(x. k)) by A51, ZF_MODEL:15;
then M,(((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),n)) / ((x. 4),n) |= H3 by A42, A59, Th12;
then M,((v / ((x. 3),m1)) / ((x. k),n)) / ((x. 4),n) |= H3 by Th8;
then M,((v / ((x. 3),m1)) / ((x. 4),n)) / ((x. k),n) |= H3 by A31, FUNCT_7:33, ZF_LANG1:76;
then M,(v / ((x. 3),m1)) / ((x. 4),n) |= H3 by A42, Th5;
then M,(v3 / ((x. 3),m1)) / ((x. 4),n) |= H3 by A52, ZF_LANG1:75;
then n = m by A45;
then M,(((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),m)) / ((x. 3),m) |= H2 by A34, A59, A58, Th12;
then M,((v / ((x. 4),m3)) / ((x. k),m)) / ((x. 3),m) |= H2 by Th8;
then M,((v / ((x. 3),m)) / ((x. 4),m3)) / ((x. k),m) |= H2 by A41, A32, Lm3, Th6;
then M,(v / ((x. 3),m)) / ((x. 4),m3) |= H2 by A34, Th5;
then M,(v2 / ((x. 3),m)) / ((x. 4),m3) |= H2 by A50, ZF_LANG1:75;
hence m3 = r by A48; ::_thesis: verum
end;
assume m3 = r ; ::_thesis: M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H
then A60: M,(v2 / ((x. 3),m)) / ((x. 4),m3) |= H2 by A48;
A61: (v2 / ((x. 3),m)) . (x. 3) = m by FUNCT_7:128;
A62: now__::_thesis:_for_x_being_Variable_st_x_in_Free_(H2_/_((x._3),(x._k)))_holds_
((v_/_((x._4),m3))_/_((x._k),m))_._x_=_((v2_/_((x._4),m3))_/_((x._k),m))_._x
let x be Variable; ::_thesis: ( x in Free (H2 / ((x. 3),(x. k))) implies ((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x )
assume A63: x in Free (H2 / ((x. 3),(x. k))) ; ::_thesis: ((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x
Free (H2 / ((x. 3),(x. k))) c= ((Free H2) \ {(x. 3)}) \/ {(x. k)} by Th1;
then ( x in (Free H2) \ {(x. 3)} or x in {(x. k)} ) by A63, XBOOLE_0:def_3;
then ( ( x in Free H2 & not x in {(x. 3)} ) or x = x. k ) by TARSKI:def_1, XBOOLE_0:def_5;
then ( ( ( ( not x in Free H3 & x. 4 <> x & x <> x. k ) or x = x. 3 or x = x. 4 ) & x <> x. 3 ) or ( ((v / ((x. 4),m3)) / ((x. k),m)) . x = m & ((v2 / ((x. 4),m3)) / ((x. k),m)) . x = m ) ) by A35, FUNCT_7:128, TARSKI:def_1;
then ( ( ((v / ((x. 4),m3)) / ((x. k),m)) . x = (v / ((x. 4),m3)) . x & (v / ((x. 4),m3)) . x = v . x & v . x = v2 . x & v2 . x = (v2 / ((x. 4),m3)) . x & (v2 / ((x. 4),m3)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x ) or ( ((v / ((x. 4),m3)) / ((x. k),m)) . x = (v / ((x. 4),m3)) . x & (v / ((x. 4),m3)) . x = m3 & m3 = (v2 / ((x. 4),m3)) . x & (v2 / ((x. 4),m3)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x ) or ((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x ) by A32, A16, FUNCT_7:32, FUNCT_7:128;
hence ((v / ((x. 4),m3)) / ((x. k),m)) . x = ((v2 / ((x. 4),m3)) / ((x. k),m)) . x ; ::_thesis: verum
end;
A64: not x. 4 in variables_in (H3 / ((x. 4),(x. k))) by A31, ZF_LANG1:76, ZF_LANG1:184;
M,(v3 / ((x. 3),m1)) / ((x. 4),m) |= H3 by A45;
then M,((v3 / ((x. 3),m1)) / ((x. 4),m)) / ((x. k),m) |= H3 / ((x. 4),(x. k)) by A42, A49, Th13;
then M,((v3 / ((x. 3),m1)) / ((x. k),m)) / ((x. 4),m) |= H3 / ((x. 4),(x. k)) by A31, FUNCT_7:33, ZF_LANG1:76;
then M,(v3 / ((x. 3),m1)) / ((x. k),m) |= H3 / ((x. 4),(x. k)) by A64, Th5;
then M,(v / ((x. 3),m1)) / ((x. k),m) |= H3 / ((x. 4),(x. k)) by A46, ZF_LANG1:75;
then M,((v / ((x. 3),m1)) / ((x. k),m)) / ((x. 4),m3) |= H3 / ((x. 4),(x. k)) by A64, Th5;
then A65: M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),m) |= H3 / ((x. 4),(x. k)) by A31, FUNCT_7:33, ZF_LANG1:76;
((v2 / ((x. 3),m)) / ((x. 4),m3)) . (x. 3) = (v2 / ((x. 3),m)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
then M,((v2 / ((x. 3),m)) / ((x. 4),m3)) / ((x. k),m) |= H2 / ((x. 3),(x. k)) by A34, A61, A60, Th13;
then M,((v2 / ((x. 4),m3)) / ((x. k),m)) / ((x. 3),m) |= H2 / ((x. 3),(x. k)) by A41, A32, Lm3, Th6;
then M,(v2 / ((x. 4),m3)) / ((x. k),m) |= H2 / ((x. 3),(x. k)) by A44, Th5;
then M,(v / ((x. 4),m3)) / ((x. k),m) |= H2 / ((x. 3),(x. k)) by A62, ZF_LANG1:75;
then M,((v / ((x. 4),m3)) / ((x. k),m)) / ((x. 3),m1) |= H2 / ((x. 3),(x. k)) by A44, Th5;
then M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),m) |= H2 / ((x. 3),(x. k)) by A41, A32, Lm3, Th6;
then M,((v / ((x. 3),m1)) / ((x. 4),m3)) / ((x. k),m) |= (H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))) by A65, ZF_MODEL:15;
hence M,(v / ((x. 3),m1)) / ((x. 4),m3) |= H by ZF_LANG1:73; ::_thesis: verum
end;
hence A66: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by A30, Th19; ::_thesis: G * F = def_func' (H,v)
now__::_thesis:_for_a_being_set_st_a_in_M_holds_
(G9_*_F9)_._a_=_(def_func'_(H,v))_._a
let a be set ; ::_thesis: ( a in M implies (G9 * F9) . a = (def_func' (H,v)) . a )
assume a in M ; ::_thesis: (G9 * F9) . a = (def_func' (H,v)) . a
then reconsider m1 = a as Element of M ;
set m3 = (def_func' (H,v)) . m1;
A67: (G9 * F9) . m1 = G9 . (F9 . m1) by FUNCT_2:15;
M,(v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1)) |= H by A30, A66, Th10;
then consider n being Element of M such that
A68: M,((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n) |= (H3 / ((x. 4),(x. k))) '&' (H2 / ((x. 3),(x. k))) by ZF_LANG1:73;
A69: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H3_holds_
((v_/_((x._3),m1))_/_((x._4),n))_._x_=_((v3_/_((x._3),m1))_/_((x._4),n))_._x
let x be Variable; ::_thesis: ( x in Free H3 implies ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x )
assume A70: x in Free H3 ; ::_thesis: ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x
A71: ((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 4) = n by FUNCT_7:128;
A72: ((v3 / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v3 / ((x. 3),m1)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A73: ((v / ((x. 3),m1)) / ((x. 4),n)) . (x. 3) = (v / ((x. 3),m1)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A74: (v / ((x. 3),m1)) . (x. 3) = m1 by FUNCT_7:128;
( x = x. 3 or x = x. 4 or ( x <> x. 3 & x <> x. 4 ) ) ;
then ( ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x or ( (v / ((x. 3),m1)) . x = v . x & (v3 / ((x. 3),m1)) . x = v3 . x & ((v / ((x. 3),m1)) / ((x. 4),n)) . x = (v / ((x. 3),m1)) . x & ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x = (v3 / ((x. 3),m1)) . x ) ) by A71, A74, A73, A72, FUNCT_7:32, FUNCT_7:128;
hence ((v / ((x. 3),m1)) / ((x. 4),n)) . x = ((v3 / ((x. 3),m1)) / ((x. 4),n)) . x by A16, A70; ::_thesis: verum
end;
A75: now__::_thesis:_for_x_being_Variable_st_x_in_Free_H2_holds_
((v_/_((x._3),n))_/_((x._4),((def_func'_(H,v))_._m1)))_._x_=_((v2_/_((x._3),n))_/_((x._4),((def_func'_(H,v))_._m1)))_._x
let x be Variable; ::_thesis: ( x in Free H2 implies ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x )
assume x in Free H2 ; ::_thesis: ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x
then ( ( not x in Free H3 & x <> x. 3 & x <> x. 4 ) or x = x. 3 or x = x. 4 ) by A35;
then ( ( ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (v / ((x. 3),n)) . x & (v / ((x. 3),n)) . x = v . x & v . x = v2 . x & v2 . x = (v2 / ((x. 3),n)) . x & (v2 / ((x. 3),n)) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x ) or ( ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (v / ((x. 3),n)) . x & (v / ((x. 3),n)) . x = n & ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (v2 / ((x. 3),n)) . x & (v2 / ((x. 3),n)) . x = n ) or ( ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (def_func' (H,v)) . m1 & ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = (def_func' (H,v)) . m1 ) ) by A16, Lm3, FUNCT_7:32, FUNCT_7:128;
hence ((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x = ((v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) . x ; ::_thesis: verum
end;
A76: (((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) . (x. k) = n by FUNCT_7:128;
M,((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n) |= H2 / ((x. 3),(x. k)) by A68, ZF_MODEL:15;
then M,(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / ((x. 3),n) |= H2 by A34, A76, Th12;
then M,((v / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / ((x. 3),n) |= H2 by Th8;
then M,((v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n) |= H2 by A41, A32, Lm3, Th6;
then M,(v / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1)) |= H2 by A34, Th5;
then M,(v2 / ((x. 3),n)) / ((x. 4),((def_func' (H,v)) . m1)) |= H2 by A75, ZF_LANG1:75;
then A77: G9 . n = (def_func' (H,v)) . m1 by A5, A6, A43, Th10;
M,((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n) |= H3 / ((x. 4),(x. k)) by A68, ZF_MODEL:15;
then M,(((v / ((x. 3),m1)) / ((x. 4),((def_func' (H,v)) . m1))) / ((x. k),n)) / ((x. 4),n) |= H3 by A42, A76, Th12;
then M,((v / ((x. 3),m1)) / ((x. k),n)) / ((x. 4),n) |= H3 by Th8;
then M,((v / ((x. 3),m1)) / ((x. 4),n)) / ((x. k),n) |= H3 by A31, FUNCT_7:33, ZF_LANG1:76;
then M,(v / ((x. 3),m1)) / ((x. 4),n) |= H3 by A42, Th5;
then M,(v3 / ((x. 3),m1)) / ((x. 4),n) |= H3 by A69, ZF_LANG1:75;
hence (G9 * F9) . a = (def_func' (H,v)) . a by A3, A11, A12, A13, A77, A67, Th10; ::_thesis: verum
end;
hence G * F = def_func' (H,v) by FUNCT_2:12; ::_thesis: verum
end;
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
proof
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 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 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
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_set_st_a_in_{(x._0),(x._1),(x._2)}_holds_
not_a_in_Free_p
let a be set ; ::_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
end;
theorem Th23: :: ZFMODEL2:23
for M being non empty set holds id M is_definable_in M
proof
let M be non empty set ; ::_thesis: id M is_definable_in M
take H = (x. 3) '=' (x. 4); :: according to ZFMODEL1:def_3 ::_thesis: ( Free H c= {(x. 3),(x. 4)} & M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & id M = def_func (H,M) )
thus A1: Free H c= {(x. 3),(x. 4)} by ZF_LANG1:58; ::_thesis: ( M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) & id M = def_func (H,M) )
reconsider i = id M as Function of M,M ;
now__::_thesis:_for_v_being_Function_of_VAR,M_holds_M,v_|=_All_((x._3),(Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))))
let v be Function of VAR,M; ::_thesis: M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))))
now__::_thesis:_for_m3_being_Element_of_M_holds_M,v_/_((x._3),m3)_|=_Ex_((x._0),(All_((x._4),(H_<=>_((x._4)_'='_(x._0))))))
let m3 be Element of M; ::_thesis: M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0))))))
now__::_thesis:_for_m4_being_Element_of_M_holds_M,((v_/_((x._3),m3))_/_((x._0),m3))_/_((x._4),m4)_|=_H_<=>_((x._4)_'='_(x._0))
let m4 be Element of M; ::_thesis: M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0))
A2: m3 = (v / ((x. 3),m3)) . (x. 3) by FUNCT_7:128;
A3: (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 0) = ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 0) by FUNCT_7:32, ZF_LANG1:76;
A4: ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 0) = m3 by FUNCT_7:128;
A5: ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 3) = (v / ((x. 3),m3)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A6: (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 3) = ((v / ((x. 3),m3)) / ((x. 0),m3)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
A7: now__::_thesis:_(_M,((v_/_((x._3),m3))_/_((x._0),m3))_/_((x._4),m4)_|=_H_implies_M,((v_/_((x._3),m3))_/_((x._0),m3))_/_((x._4),m4)_|=_(x._4)_'='_(x._0)_)
assume M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H ; ::_thesis: M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0)
then (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 3) = (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 4) by ZF_MODEL:12;
hence M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) by A6, A2, A5, A3, A4, ZF_MODEL:12; ::_thesis: verum
end;
A8: (((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4)) . (x. 4) = m4 by FUNCT_7:128;
now__::_thesis:_(_M,((v_/_((x._3),m3))_/_((x._0),m3))_/_((x._4),m4)_|=_(x._4)_'='_(x._0)_implies_M,((v_/_((x._3),m3))_/_((x._0),m3))_/_((x._4),m4)_|=_H_)
assume M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= (x. 4) '=' (x. 0) ; ::_thesis: M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H
then m4 = m3 by A3, A4, A8, ZF_MODEL:12;
hence M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H by A6, A2, A5, A8, ZF_MODEL:12; ::_thesis: verum
end;
hence M,((v / ((x. 3),m3)) / ((x. 0),m3)) / ((x. 4),m4) |= H <=> ((x. 4) '=' (x. 0)) by A7, ZF_MODEL:19; ::_thesis: verum
end;
then M,(v / ((x. 3),m3)) / ((x. 0),m3) |= All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))) by ZF_LANG1:71;
hence M,v / ((x. 3),m3) |= Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))) by ZF_LANG1:73; ::_thesis: verum
end;
hence M,v |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by ZF_LANG1:71; ::_thesis: verum
end;
hence A9: M |= All ((x. 3),(Ex ((x. 0),(All ((x. 4),(H <=> ((x. 4) '=' (x. 0)))))))) by ZF_MODEL:def_5; ::_thesis: id M = def_func (H,M)
now__::_thesis:_for_a_being_Element_of_M_holds_i_._a_=_(def_func_(H,M))_._a
set v = the Function of VAR,M;
let a be Element of M; ::_thesis: i . a = (def_func (H,M)) . a
A10: a = ( the Function of VAR,M / ((x. 3),a)) . (x. 3) by FUNCT_7:128;
A11: (( the Function of VAR,M / ((x. 3),a)) / ((x. 4),a)) . (x. 4) = a by FUNCT_7:128;
A12: (( the Function of VAR,M / ((x. 3),a)) / ((x. 4),a)) . (x. 3) = ( the Function of VAR,M / ((x. 3),a)) . (x. 3) by FUNCT_7:32, ZF_LANG1:76;
then M,( the Function of VAR,M / ((x. 3),a)) / ((x. 4),a) |= H by A10, A11, ZF_MODEL:12;
then (def_func (H,M)) . a = a by A1, A9, A12, A10, A11, ZFMODEL1:def_2;
hence i . a = (def_func (H,M)) . a by FUNCT_1:18; ::_thesis: verum
end;
hence id M = def_func (H,M) by FUNCT_2:63; ::_thesis: verum
end;
theorem :: ZFMODEL2:24
for M being non empty set holds id M is_parametrically_definable_in M by Th23, ZFMODEL1:14;