:: 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;