:: ZF_LANG semantic presentation begin definition func VAR -> Subset of NAT equals :: ZF_LANG:def 1 { k where k is Element of NAT : 5 <= k } ; coherence { k where k is Element of NAT : 5 <= k } is Subset of NAT proof set X = { k where k is Element of NAT : 5 <= k } ; { k where k is Element of NAT : 5 <= k } c= NAT proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { k where k is Element of NAT : 5 <= k } or a in NAT ) assume a in { k where k is Element of NAT : 5 <= k } ; ::_thesis: a in NAT then ex k being Element of NAT st ( a = k & 5 <= k ) ; hence a in NAT ; ::_thesis: verum end; hence { k where k is Element of NAT : 5 <= k } is Subset of NAT ; ::_thesis: verum end; end; :: deftheorem defines VAR ZF_LANG:def_1_:_ VAR = { k where k is Element of NAT : 5 <= k } ; registration cluster VAR -> non empty ; coherence not VAR is empty proof 5 in { k where k is Element of NAT : 5 <= k } ; hence not VAR is empty ; ::_thesis: verum end; end; definition mode Variable is Element of VAR ; end; definition let n be Element of NAT ; func x. n -> Variable equals :: ZF_LANG:def 2 5 + n; coherence 5 + n is Variable proof set x = 5 + n; 5 <= 5 + n by NAT_1:11; then 5 + n in { k where k is Element of NAT : 5 <= k } ; hence 5 + n is Variable ; ::_thesis: verum end; end; :: deftheorem defines x. ZF_LANG:def_2_:_ for n being Element of NAT holds x. n = 5 + n; definition let x be Variable; :: original: <* redefine func<*x*> -> FinSequence of NAT ; coherence <*x*> is FinSequence of NAT proof reconsider VAR9 = VAR as non empty Subset of NAT ; reconsider x9 = x as Element of VAR9 ; reconsider x9 = x9 as Element of NAT ; <*x9*> is FinSequence of NAT ; hence <*x*> is FinSequence of NAT ; ::_thesis: verum end; end; definition let x, y be Variable; funcx '=' y -> FinSequence of NAT equals :: ZF_LANG:def 3 (<*0*> ^ <*x*>) ^ <*y*>; coherence (<*0*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ; funcx 'in' y -> FinSequence of NAT equals :: ZF_LANG:def 4 (<*1*> ^ <*x*>) ^ <*y*>; coherence (<*1*> ^ <*x*>) ^ <*y*> is FinSequence of NAT ; end; :: deftheorem defines '=' ZF_LANG:def_3_:_ for x, y being Variable holds x '=' y = (<*0*> ^ <*x*>) ^ <*y*>; :: deftheorem defines 'in' ZF_LANG:def_4_:_ for x, y being Variable holds x 'in' y = (<*1*> ^ <*x*>) ^ <*y*>; theorem :: ZF_LANG:1 for x, y, z, t being Variable st x '=' y = z '=' t holds ( x = z & y = t ) proof let x, y, z, t be Variable; ::_thesis: ( x '=' y = z '=' t implies ( x = z & y = t ) ) A1: ( (<*0*> ^ <*x*>) ^ <*y*> = <*0*> ^ (<*x*> ^ <*y*>) & (<*0*> ^ <*z*>) ^ <*t*> = <*0*> ^ (<*z*> ^ <*t*>) ) by FINSEQ_1:32; A2: ( <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:44; A3: ( <*x*> ^ <*y*> = <*x,y*> & <*z*> ^ <*t*> = <*z,t*> ) by FINSEQ_1:def_9; A4: ( <*z,t*> . 1 = z & <*z,t*> . 2 = t ) by FINSEQ_1:44; assume x '=' y = z '=' t ; ::_thesis: ( x = z & y = t ) hence ( x = z & y = t ) by A1, A2, A4, A3, FINSEQ_1:33; ::_thesis: verum end; theorem :: ZF_LANG:2 for x, y, z, t being Variable st x 'in' y = z 'in' t holds ( x = z & y = t ) proof let x, y, z, t be Variable; ::_thesis: ( x 'in' y = z 'in' t implies ( x = z & y = t ) ) A1: ( (<*1*> ^ <*x*>) ^ <*y*> = <*1*> ^ (<*x*> ^ <*y*>) & (<*1*> ^ <*z*>) ^ <*t*> = <*1*> ^ (<*z*> ^ <*t*>) ) by FINSEQ_1:32; A2: ( <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:44; A3: ( <*x*> ^ <*y*> = <*x,y*> & <*z*> ^ <*t*> = <*z,t*> ) by FINSEQ_1:def_9; A4: ( <*z,t*> . 1 = z & <*z,t*> . 2 = t ) by FINSEQ_1:44; assume x 'in' y = z 'in' t ; ::_thesis: ( x = z & y = t ) hence ( x = z & y = t ) by A1, A2, A4, A3, FINSEQ_1:33; ::_thesis: verum end; definition let p be FinSequence of NAT ; func 'not' p -> FinSequence of NAT equals :: ZF_LANG:def 5 <*2*> ^ p; coherence <*2*> ^ p is FinSequence of NAT ; let q be FinSequence of NAT ; funcp '&' q -> FinSequence of NAT equals :: ZF_LANG:def 6 (<*3*> ^ p) ^ q; coherence (<*3*> ^ p) ^ q is FinSequence of NAT ; end; :: deftheorem defines 'not' ZF_LANG:def_5_:_ for p being FinSequence of NAT holds 'not' p = <*2*> ^ p; :: deftheorem defines '&' ZF_LANG:def_6_:_ for p, q being FinSequence of NAT holds p '&' q = (<*3*> ^ p) ^ q; definition let x be Variable; let p be FinSequence of NAT ; func All (x,p) -> FinSequence of NAT equals :: ZF_LANG:def 7 (<*4*> ^ <*x*>) ^ p; coherence (<*4*> ^ <*x*>) ^ p is FinSequence of NAT ; end; :: deftheorem defines All ZF_LANG:def_7_:_ for x being Variable for p being FinSequence of NAT holds All (x,p) = (<*4*> ^ <*x*>) ^ p; theorem Th3: :: ZF_LANG:3 for p, q being FinSequence of NAT for x, y being Variable st All (x,p) = All (y,q) holds ( x = y & p = q ) proof let p, q be FinSequence of NAT ; ::_thesis: for x, y being Variable st All (x,p) = All (y,q) holds ( x = y & p = q ) let x, y be Variable; ::_thesis: ( All (x,p) = All (y,q) implies ( x = y & p = q ) ) A1: ( (<*4*> ^ <*x*>) ^ p = <*4*> ^ (<*x*> ^ p) & (<*4*> ^ <*y*>) ^ q = <*4*> ^ (<*y*> ^ q) ) by FINSEQ_1:32; A2: ( (<*x*> ^ p) . 1 = x & (<*y*> ^ q) . 1 = y ) by FINSEQ_1:41; assume A3: All (x,p) = All (y,q) ; ::_thesis: ( x = y & p = q ) hence x = y by A1, A2, FINSEQ_1:33; ::_thesis: p = q <*x*> ^ p = <*y*> ^ q by A3, A1, FINSEQ_1:33; hence p = q by A2, FINSEQ_1:33; ::_thesis: verum end; definition func WFF -> non empty set means :Def8: :: ZF_LANG:def 8 ( ( for a being set st a in it holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in it & x 'in' y in it ) ) & ( for p being FinSequence of NAT st p in it holds 'not' p in it ) & ( for p, q being FinSequence of NAT st p in it & q in it holds p '&' q in it ) & ( for x being Variable for p being FinSequence of NAT st p in it holds All (x,p) in it ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds it c= D ) ); existence ex b1 being non empty set st ( ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds 'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p '&' q in b1 ) & ( for x being Variable for p being FinSequence of NAT st p in b1 holds All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b1 c= D ) ) proof defpred S1[ set ] means ( ( for a being set st a in $1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in $1 & x 'in' y in $1 ) ) & ( for p being FinSequence of NAT st p in $1 holds 'not' p in $1 ) & ( for p, q being FinSequence of NAT st p in $1 & q in $1 holds p '&' q in $1 ) & ( for x being Variable for p being FinSequence of NAT st p in $1 holds All (x,p) in $1 ) ); defpred S2[ set ] means for D being non empty set st S1[D] holds $1 in D; consider Y being set such that A1: for a being set holds ( a in Y iff ( a in NAT * & S2[a] ) ) from XBOOLE_0:sch_1(); now__::_thesis:_ex_b_being_FinSequence_of_NAT_st_b_in_Y set a = (x. 0) '=' (x. 0); take b = (x. 0) '=' (x. 0); ::_thesis: b in Y ( (x. 0) '=' (x. 0) in NAT * & ( for D being non empty set st S1[D] holds (x. 0) '=' (x. 0) in D ) ) by FINSEQ_1:def_11; hence b in Y by A1; ::_thesis: verum end; then reconsider Y = Y as non empty set ; take Y ; ::_thesis: ( ( for a being set st a in Y holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in Y & x 'in' y in Y ) ) & ( for p being FinSequence of NAT st p in Y holds 'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds p '&' q in Y ) & ( for x being Variable for p being FinSequence of NAT st p in Y holds All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds Y c= D ) ) thus for a being set st a in Y holds a is FinSequence of NAT ::_thesis: ( ( for x, y being Variable holds ( x '=' y in Y & x 'in' y in Y ) ) & ( for p being FinSequence of NAT st p in Y holds 'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds p '&' q in Y ) & ( for x being Variable for p being FinSequence of NAT st p in Y holds All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds Y c= D ) ) proof let a be set ; ::_thesis: ( a in Y implies a is FinSequence of NAT ) assume a in Y ; ::_thesis: a is FinSequence of NAT then a in NAT * by A1; hence a is FinSequence of NAT by FINSEQ_1:def_11; ::_thesis: verum end; thus for x, y being Variable holds ( x '=' y in Y & x 'in' y in Y ) ::_thesis: ( ( for p being FinSequence of NAT st p in Y holds 'not' p in Y ) & ( for p, q being FinSequence of NAT st p in Y & q in Y holds p '&' q in Y ) & ( for x being Variable for p being FinSequence of NAT st p in Y holds All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds Y c= D ) ) proof let x, y be Variable; ::_thesis: ( x '=' y in Y & x 'in' y in Y ) ( x '=' y in NAT * & ( for D being non empty set st S1[D] holds x '=' y in D ) ) by FINSEQ_1:def_11; hence x '=' y in Y by A1; ::_thesis: x 'in' y in Y ( x 'in' y in NAT * & ( for D being non empty set st S1[D] holds x 'in' y in D ) ) by FINSEQ_1:def_11; hence x 'in' y in Y by A1; ::_thesis: verum end; thus for p being FinSequence of NAT st p in Y holds 'not' p in Y ::_thesis: ( ( for p, q being FinSequence of NAT st p in Y & q in Y holds p '&' q in Y ) & ( for x being Variable for p being FinSequence of NAT st p in Y holds All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds Y c= D ) ) proof let p be FinSequence of NAT ; ::_thesis: ( p in Y implies 'not' p in Y ) assume A2: p in Y ; ::_thesis: 'not' p in Y A3: for D being non empty set st S1[D] holds 'not' p in D proof let D be non empty set ; ::_thesis: ( S1[D] implies 'not' p in D ) assume A4: S1[D] ; ::_thesis: 'not' p in D then p in D by A1, A2; hence 'not' p in D by A4; ::_thesis: verum end; 'not' p in NAT * by FINSEQ_1:def_11; hence 'not' p in Y by A1, A3; ::_thesis: verum end; thus for q, p being FinSequence of NAT st q in Y & p in Y holds q '&' p in Y ::_thesis: ( ( for x being Variable for p being FinSequence of NAT st p in Y holds All (x,p) in Y ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds Y c= D ) ) proof let q, p be FinSequence of NAT ; ::_thesis: ( q in Y & p in Y implies q '&' p in Y ) assume A5: ( q in Y & p in Y ) ; ::_thesis: q '&' p in Y A6: for D being non empty set st S1[D] holds q '&' p in D proof let D be non empty set ; ::_thesis: ( S1[D] implies q '&' p in D ) assume A7: S1[D] ; ::_thesis: q '&' p in D then ( p in D & q in D ) by A1, A5; hence q '&' p in D by A7; ::_thesis: verum end; q '&' p in NAT * by FINSEQ_1:def_11; hence q '&' p in Y by A1, A6; ::_thesis: verum end; thus for x being Variable for p being FinSequence of NAT st p in Y holds All (x,p) in Y ::_thesis: for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds Y c= D proof let x be Variable; ::_thesis: for p being FinSequence of NAT st p in Y holds All (x,p) in Y let p be FinSequence of NAT ; ::_thesis: ( p in Y implies All (x,p) in Y ) assume A8: p in Y ; ::_thesis: All (x,p) in Y A9: for D being non empty set st S1[D] holds All (x,p) in D proof let D be non empty set ; ::_thesis: ( S1[D] implies All (x,p) in D ) assume A10: S1[D] ; ::_thesis: All (x,p) in D then p in D by A1, A8; hence All (x,p) in D by A10; ::_thesis: verum end; All (x,p) in NAT * by FINSEQ_1:def_11; hence All (x,p) in Y by A1, A9; ::_thesis: verum end; let D be non empty set ; ::_thesis: ( ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) implies Y c= D ) assume A11: S1[D] ; ::_thesis: Y c= D let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Y or a in D ) assume a in Y ; ::_thesis: a in D hence a in D by A1, A11; ::_thesis: verum end; uniqueness for b1, b2 being non empty set st ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds 'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p '&' q in b1 ) & ( for x being Variable for p being FinSequence of NAT st p in b1 holds All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b1 c= D ) & ( for a being set st a in b2 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b2 & x 'in' y in b2 ) ) & ( for p being FinSequence of NAT st p in b2 holds 'not' p in b2 ) & ( for p, q being FinSequence of NAT st p in b2 & q in b2 holds p '&' q in b2 ) & ( for x being Variable for p being FinSequence of NAT st p in b2 holds All (x,p) in b2 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b2 c= D ) holds b1 = b2 proof let D1, D2 be non empty set ; ::_thesis: ( ( for a being set st a in D1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D1 & x 'in' y in D1 ) ) & ( for p being FinSequence of NAT st p in D1 holds 'not' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds p '&' q in D1 ) & ( for x being Variable for p being FinSequence of NAT st p in D1 holds All (x,p) in D1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds D1 c= D ) & ( for a being set st a in D2 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D2 & x 'in' y in D2 ) ) & ( for p being FinSequence of NAT st p in D2 holds 'not' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds p '&' q in D2 ) & ( for x being Variable for p being FinSequence of NAT st p in D2 holds All (x,p) in D2 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds D2 c= D ) implies D1 = D2 ) assume ( ( for a being set st a in D1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D1 & x 'in' y in D1 ) ) & ( for p being FinSequence of NAT st p in D1 holds 'not' p in D1 ) & ( for p, q being FinSequence of NAT st p in D1 & q in D1 holds p '&' q in D1 ) & ( for x being Variable for p being FinSequence of NAT st p in D1 holds All (x,p) in D1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds D1 c= D ) & ( for a being set st a in D2 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D2 & x 'in' y in D2 ) ) & ( for p being FinSequence of NAT st p in D2 holds 'not' p in D2 ) & ( for p, q being FinSequence of NAT st p in D2 & q in D2 holds p '&' q in D2 ) & ( for x being Variable for p being FinSequence of NAT st p in D2 holds All (x,p) in D2 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds D2 c= D ) ) ; ::_thesis: D1 = D2 then ( D1 c= D2 & D2 c= D1 ) ; hence D1 = D2 by XBOOLE_0:def_10; ::_thesis: verum end; end; :: deftheorem Def8 defines WFF ZF_LANG:def_8_:_ for b1 being non empty set holds ( b1 = WFF iff ( ( for a being set st a in b1 holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in b1 & x 'in' y in b1 ) ) & ( for p being FinSequence of NAT st p in b1 holds 'not' p in b1 ) & ( for p, q being FinSequence of NAT st p in b1 & q in b1 holds p '&' q in b1 ) & ( for x being Variable for p being FinSequence of NAT st p in b1 holds All (x,p) in b1 ) & ( for D being non empty set st ( for a being set st a in D holds a is FinSequence of NAT ) & ( for x, y being Variable holds ( x '=' y in D & x 'in' y in D ) ) & ( for p being FinSequence of NAT st p in D holds 'not' p in D ) & ( for p, q being FinSequence of NAT st p in D & q in D holds p '&' q in D ) & ( for x being Variable for p being FinSequence of NAT st p in D holds All (x,p) in D ) holds b1 c= D ) ) ); definition let IT be FinSequence of NAT ; attrIT is ZF-formula-like means :Def9: :: ZF_LANG:def 9 IT is Element of WFF ; end; :: deftheorem Def9 defines ZF-formula-like ZF_LANG:def_9_:_ for IT being FinSequence of NAT holds ( IT is ZF-formula-like iff IT is Element of WFF ); registration cluster Relation-like NAT -defined NAT -valued Function-like V33() FinSequence-like FinSubsequence-like ZF-formula-like for FinSequence of NAT ; existence ex b1 being FinSequence of NAT st b1 is ZF-formula-like proof set x = the Element of WFF ; reconsider x = the Element of WFF as FinSequence of NAT by Def8; take x ; ::_thesis: x is ZF-formula-like thus x is Element of WFF ; :: according to ZF_LANG:def_9 ::_thesis: verum end; end; definition mode ZF-formula is ZF-formula-like FinSequence of NAT ; end; theorem :: ZF_LANG:4 for a being set holds ( a is ZF-formula iff a in WFF ) proof let a be set ; ::_thesis: ( a is ZF-formula iff a in WFF ) thus ( a is ZF-formula implies a in WFF ) ::_thesis: ( a in WFF implies a is ZF-formula ) proof assume a is ZF-formula ; ::_thesis: a in WFF then a is Element of WFF by Def9; hence a in WFF ; ::_thesis: verum end; assume a in WFF ; ::_thesis: a is ZF-formula hence a is ZF-formula by Def8, Def9; ::_thesis: verum end; registration let x, y be Variable; clusterx '=' y -> ZF-formula-like ; coherence x '=' y is ZF-formula-like proof x '=' y is Element of WFF by Def8; hence x '=' y is ZF-formula-like by Def9; ::_thesis: verum end; clusterx 'in' y -> ZF-formula-like ; coherence x 'in' y is ZF-formula-like proof x 'in' y is Element of WFF by Def8; hence x 'in' y is ZF-formula-like by Def9; ::_thesis: verum end; end; registration let H be ZF-formula; cluster 'not' H -> ZF-formula-like ; coherence 'not' H is ZF-formula-like proof H is Element of WFF by Def9; then 'not' H is Element of WFF by Def8; hence 'not' H is ZF-formula-like by Def9; ::_thesis: verum end; let G be ZF-formula; clusterH '&' G -> ZF-formula-like ; coherence H '&' G is ZF-formula-like proof ( H is Element of WFF & G is Element of WFF ) by Def9; then H '&' G is Element of WFF by Def8; hence H '&' G is ZF-formula-like by Def9; ::_thesis: verum end; end; registration let x be Variable; let H be ZF-formula; cluster All (x,H) -> ZF-formula-like ; coherence All (x,H) is ZF-formula-like proof H is Element of WFF by Def9; then All (x,H) is Element of WFF by Def8; hence All (x,H) is ZF-formula-like by Def9; ::_thesis: verum end; end; definition let H be ZF-formula; attrH is being_equality means :Def10: :: ZF_LANG:def 10 ex x, y being Variable st H = x '=' y; attrH is being_membership means :Def11: :: ZF_LANG:def 11 ex x, y being Variable st H = x 'in' y; attrH is negative means :Def12: :: ZF_LANG:def 12 ex H1 being ZF-formula st H = 'not' H1; attrH is conjunctive means :Def13: :: ZF_LANG:def 13 ex F, G being ZF-formula st H = F '&' G; attrH is universal means :Def14: :: ZF_LANG:def 14 ex x being Variable ex H1 being ZF-formula st H = All (x,H1); end; :: deftheorem Def10 defines being_equality ZF_LANG:def_10_:_ for H being ZF-formula holds ( H is being_equality iff ex x, y being Variable st H = x '=' y ); :: deftheorem Def11 defines being_membership ZF_LANG:def_11_:_ for H being ZF-formula holds ( H is being_membership iff ex x, y being Variable st H = x 'in' y ); :: deftheorem Def12 defines negative ZF_LANG:def_12_:_ for H being ZF-formula holds ( H is negative iff ex H1 being ZF-formula st H = 'not' H1 ); :: deftheorem Def13 defines conjunctive ZF_LANG:def_13_:_ for H being ZF-formula holds ( H is conjunctive iff ex F, G being ZF-formula st H = F '&' G ); :: deftheorem Def14 defines universal ZF_LANG:def_14_:_ for H being ZF-formula holds ( H is universal iff ex x being Variable ex H1 being ZF-formula st H = All (x,H1) ); theorem :: ZF_LANG:5 for H being ZF-formula holds ( ( H is being_equality implies ex x, y being Variable st H = x '=' y ) & ( ex x, y being Variable st H = x '=' y implies H is being_equality ) & ( H is being_membership implies ex x, y being Variable st H = x 'in' y ) & ( ex x, y being Variable st H = x 'in' y implies H is being_membership ) & ( H is negative implies ex H1 being ZF-formula st H = 'not' H1 ) & ( ex H1 being ZF-formula st H = 'not' H1 implies H is negative ) & ( H is conjunctive implies ex F, G being ZF-formula st H = F '&' G ) & ( ex F, G being ZF-formula st H = F '&' G implies H is conjunctive ) & ( H is universal implies ex x being Variable ex H1 being ZF-formula st H = All (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = All (x,H1) implies H is universal ) ) by Def10, Def11, Def12, Def13, Def14; definition let H be ZF-formula; attrH is atomic means :Def15: :: ZF_LANG:def 15 ( H is being_equality or H is being_membership ); end; :: deftheorem Def15 defines atomic ZF_LANG:def_15_:_ for H being ZF-formula holds ( H is atomic iff ( H is being_equality or H is being_membership ) ); definition let F, G be ZF-formula; funcF 'or' G -> ZF-formula equals :: ZF_LANG:def 16 'not' (('not' F) '&' ('not' G)); coherence 'not' (('not' F) '&' ('not' G)) is ZF-formula ; funcF => G -> ZF-formula equals :: ZF_LANG:def 17 'not' (F '&' ('not' G)); coherence 'not' (F '&' ('not' G)) is ZF-formula ; end; :: deftheorem defines 'or' ZF_LANG:def_16_:_ for F, G being ZF-formula holds F 'or' G = 'not' (('not' F) '&' ('not' G)); :: deftheorem defines => ZF_LANG:def_17_:_ for F, G being ZF-formula holds F => G = 'not' (F '&' ('not' G)); definition let F, G be ZF-formula; funcF <=> G -> ZF-formula equals :: ZF_LANG:def 18 (F => G) '&' (G => F); coherence (F => G) '&' (G => F) is ZF-formula ; end; :: deftheorem defines <=> ZF_LANG:def_18_:_ for F, G being ZF-formula holds F <=> G = (F => G) '&' (G => F); definition let x be Variable; let H be ZF-formula; func Ex (x,H) -> ZF-formula equals :: ZF_LANG:def 19 'not' (All (x,('not' H))); coherence 'not' (All (x,('not' H))) is ZF-formula ; end; :: deftheorem defines Ex ZF_LANG:def_19_:_ for x being Variable for H being ZF-formula holds Ex (x,H) = 'not' (All (x,('not' H))); definition let H be ZF-formula; attrH is disjunctive means :Def20: :: ZF_LANG:def 20 ex F, G being ZF-formula st H = F 'or' G; attrH is conditional means :Def21: :: ZF_LANG:def 21 ex F, G being ZF-formula st H = F => G; attrH is biconditional means :Def22: :: ZF_LANG:def 22 ex F, G being ZF-formula st H = F <=> G; attrH is existential means :Def23: :: ZF_LANG:def 23 ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1); end; :: deftheorem Def20 defines disjunctive ZF_LANG:def_20_:_ for H being ZF-formula holds ( H is disjunctive iff ex F, G being ZF-formula st H = F 'or' G ); :: deftheorem Def21 defines conditional ZF_LANG:def_21_:_ for H being ZF-formula holds ( H is conditional iff ex F, G being ZF-formula st H = F => G ); :: deftheorem Def22 defines biconditional ZF_LANG:def_22_:_ for H being ZF-formula holds ( H is biconditional iff ex F, G being ZF-formula st H = F <=> G ); :: deftheorem Def23 defines existential ZF_LANG:def_23_:_ for H being ZF-formula holds ( H is existential iff ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) ); theorem :: ZF_LANG:6 for H being ZF-formula holds ( ( H is disjunctive implies ex F, G being ZF-formula st H = F 'or' G ) & ( ex F, G being ZF-formula st H = F 'or' G implies H is disjunctive ) & ( H is conditional implies ex F, G being ZF-formula st H = F => G ) & ( ex F, G being ZF-formula st H = F => G implies H is conditional ) & ( H is biconditional implies ex F, G being ZF-formula st H = F <=> G ) & ( ex F, G being ZF-formula st H = F <=> G implies H is biconditional ) & ( H is existential implies ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) ) & ( ex x being Variable ex H1 being ZF-formula st H = Ex (x,H1) implies H is existential ) ) by Def20, Def21, Def22, Def23; definition let x, y be Variable; let H be ZF-formula; func All (x,y,H) -> ZF-formula equals :: ZF_LANG:def 24 All (x,(All (y,H))); coherence All (x,(All (y,H))) is ZF-formula ; func Ex (x,y,H) -> ZF-formula equals :: ZF_LANG:def 25 Ex (x,(Ex (y,H))); coherence Ex (x,(Ex (y,H))) is ZF-formula ; end; :: deftheorem defines All ZF_LANG:def_24_:_ for x, y being Variable for H being ZF-formula holds All (x,y,H) = All (x,(All (y,H))); :: deftheorem defines Ex ZF_LANG:def_25_:_ for x, y being Variable for H being ZF-formula holds Ex (x,y,H) = Ex (x,(Ex (y,H))); theorem :: ZF_LANG:7 for x, y being Variable for H being ZF-formula holds ( All (x,y,H) = All (x,(All (y,H))) & Ex (x,y,H) = Ex (x,(Ex (y,H))) ) ; definition let x, y, z be Variable; let H be ZF-formula; func All (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 26 All (x,(All (y,z,H))); coherence All (x,(All (y,z,H))) is ZF-formula ; func Ex (x,y,z,H) -> ZF-formula equals :: ZF_LANG:def 27 Ex (x,(Ex (y,z,H))); coherence Ex (x,(Ex (y,z,H))) is ZF-formula ; end; :: deftheorem defines All ZF_LANG:def_26_:_ for x, y, z being Variable for H being ZF-formula holds All (x,y,z,H) = All (x,(All (y,z,H))); :: deftheorem defines Ex ZF_LANG:def_27_:_ for x, y, z being Variable for H being ZF-formula holds Ex (x,y,z,H) = Ex (x,(Ex (y,z,H))); theorem :: ZF_LANG:8 for x, y, z being Variable for H being ZF-formula holds ( All (x,y,z,H) = All (x,(All (y,z,H))) & Ex (x,y,z,H) = Ex (x,(Ex (y,z,H))) ) ; theorem Th9: :: ZF_LANG:9 for H being ZF-formula holds ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal ) proof let H be ZF-formula; ::_thesis: ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal ) A1: H is Element of WFF by Def9; assume A2: ( not H is being_equality & not H is being_membership & not H is negative & not H is conjunctive & not H is universal ) ; ::_thesis: contradiction then (x. 0) '=' (x. 1) <> H by Def10; then A3: not (x. 0) '=' (x. 1) in {H} by TARSKI:def_1; A4: now__::_thesis:_for_x,_y_being_Variable_holds_ (_x_'='_y_in_WFF_\_{H}_&_x_'in'_y_in_WFF_\_{H}_) let x, y be Variable; ::_thesis: ( x '=' y in WFF \ {H} & x 'in' y in WFF \ {H} ) x '=' y <> H by A2, Def10; then A5: not x '=' y in {H} by TARSKI:def_1; x '=' y in WFF by Def8; hence x '=' y in WFF \ {H} by A5, XBOOLE_0:def_5; ::_thesis: x 'in' y in WFF \ {H} x 'in' y <> H by A2, Def11; then A6: not x 'in' y in {H} by TARSKI:def_1; x 'in' y in WFF by Def8; hence x 'in' y in WFF \ {H} by A6, XBOOLE_0:def_5; ::_thesis: verum end; A7: now__::_thesis:_for_x_being_Variable for_p_being_FinSequence_of_NAT_st_p_in_WFF_\_{H}_holds_ All_(x,p)_in_WFF_\_{H} let x be Variable; ::_thesis: for p being FinSequence of NAT st p in WFF \ {H} holds All (x,p) in WFF \ {H} let p be FinSequence of NAT ; ::_thesis: ( p in WFF \ {H} implies All (x,p) in WFF \ {H} ) assume A8: p in WFF \ {H} ; ::_thesis: All (x,p) in WFF \ {H} then reconsider H1 = p as ZF-formula by Def9; All (x,H1) <> H by A2, Def14; then A9: not All (x,p) in {H} by TARSKI:def_1; All (x,p) in WFF by A8, Def8; hence All (x,p) in WFF \ {H} by A9, XBOOLE_0:def_5; ::_thesis: verum end; A10: now__::_thesis:_for_p,_q_being_FinSequence_of_NAT_st_p_in_WFF_\_{H}_&_q_in_WFF_\_{H}_holds_ p_'&'_q_in_WFF_\_{H} let p, q be FinSequence of NAT ; ::_thesis: ( p in WFF \ {H} & q in WFF \ {H} implies p '&' q in WFF \ {H} ) assume A11: ( p in WFF \ {H} & q in WFF \ {H} ) ; ::_thesis: p '&' q in WFF \ {H} then reconsider F = p, G = q as ZF-formula by Def9; F '&' G <> H by A2, Def13; then A12: not p '&' q in {H} by TARSKI:def_1; p '&' q in WFF by A11, Def8; hence p '&' q in WFF \ {H} by A12, XBOOLE_0:def_5; ::_thesis: verum end; A13: now__::_thesis:_for_p_being_FinSequence_of_NAT_st_p_in_WFF_\_{H}_holds_ 'not'_p_in_WFF_\_{H} let p be FinSequence of NAT ; ::_thesis: ( p in WFF \ {H} implies 'not' p in WFF \ {H} ) assume A14: p in WFF \ {H} ; ::_thesis: 'not' p in WFF \ {H} then reconsider H1 = p as ZF-formula by Def9; 'not' H1 <> H by A2, Def12; then A15: not 'not' p in {H} by TARSKI:def_1; 'not' p in WFF by A14, Def8; hence 'not' p in WFF \ {H} by A15, XBOOLE_0:def_5; ::_thesis: verum end; (x. 0) '=' (x. 1) in WFF by Def8; then A16: WFF \ {H} is non empty set by A3, XBOOLE_0:def_5; for a being set st a in WFF \ {H} holds a is FinSequence of NAT by Def8; then WFF c= WFF \ {H} by A16, A4, A13, A10, A7, Def8; then H in WFF \ {H} by A1, TARSKI:def_3; then not H in {H} by XBOOLE_0:def_5; hence contradiction by TARSKI:def_1; ::_thesis: verum end; theorem Th10: :: ZF_LANG:10 for H being ZF-formula holds ( H is atomic or H is negative or H is conjunctive or H is universal ) proof let H be ZF-formula; ::_thesis: ( H is atomic or H is negative or H is conjunctive or H is universal ) assume ( not H is being_equality & not H is being_membership ) ; :: according to ZF_LANG:def_15 ::_thesis: ( H is negative or H is conjunctive or H is universal ) hence ( H is negative or H is conjunctive or H is universal ) by Th9; ::_thesis: verum end; theorem Th11: :: ZF_LANG:11 for H being ZF-formula st H is atomic holds len H = 3 proof let H be ZF-formula; ::_thesis: ( H is atomic implies len H = 3 ) A1: now__::_thesis:_(_H_is_being_equality_&_H_is_atomic_implies_len_H_=_3_) assume H is being_equality ; ::_thesis: ( H is atomic implies len H = 3 ) then consider x, y being Variable such that A2: H = x '=' y by Def10; H = <*0,x,y*> by A2, FINSEQ_1:def_10; hence ( H is atomic implies len H = 3 ) by FINSEQ_1:45; ::_thesis: verum end; A3: now__::_thesis:_(_H_is_being_membership_&_H_is_atomic_implies_len_H_=_3_) assume H is being_membership ; ::_thesis: ( H is atomic implies len H = 3 ) then consider x, y being Variable such that A4: H = x 'in' y by Def11; H = <*1,x,y*> by A4, FINSEQ_1:def_10; hence ( H is atomic implies len H = 3 ) by FINSEQ_1:45; ::_thesis: verum end; assume H is atomic ; ::_thesis: len H = 3 hence len H = 3 by A1, A3, Def15; ::_thesis: verum end; theorem Th12: :: ZF_LANG:12 for H being ZF-formula holds ( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H ) proof let H be ZF-formula; ::_thesis: ( H is atomic or ex H1 being ZF-formula st (len H1) + 1 <= len H ) A1: now__::_thesis:_for_H_being_ZF-formula_st_H_is_universal_holds_ ex_H1_being_ZF-formula_st_(len_H1)_+_1_<=_len_H let H be ZF-formula; ::_thesis: ( H is universal implies ex H1 being ZF-formula st (len H1) + 1 <= len H ) assume H is universal ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H then consider x being Variable, H1 being ZF-formula such that A2: H = All (x,H1) by Def14; take H1 = H1; ::_thesis: (len H1) + 1 <= len H A3: ( len <*4,x*> = 2 & <*4*> ^ <*x*> = <*4,x*> ) by FINSEQ_1:44, FINSEQ_1:def_9; A4: (1 + 1) + (len H1) = 1 + (1 + (len H1)) ; len H = (len (<*4*> ^ <*x*>)) + (len H1) by A2, FINSEQ_1:22; hence (len H1) + 1 <= len H by A3, A4, NAT_1:11; ::_thesis: verum end; A5: now__::_thesis:_for_H_being_ZF-formula_st_H_is_negative_holds_ ex_H1_being_ZF-formula_st_(len_H1)_+_1_<=_len_H let H be ZF-formula; ::_thesis: ( H is negative implies ex H1 being ZF-formula st (len H1) + 1 <= len H ) assume H is negative ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H then consider H1 being ZF-formula such that A6: H = 'not' H1 by Def12; take H1 = H1; ::_thesis: (len H1) + 1 <= len H len H = (len <*2*>) + (len H1) by A6, FINSEQ_1:22; hence (len H1) + 1 <= len H by FINSEQ_1:40; ::_thesis: verum end; A7: now__::_thesis:_for_H_being_ZF-formula_st_H_is_conjunctive_holds_ ex_H1_being_ZF-formula_st_(len_H1)_+_1_<=_len_H let H be ZF-formula; ::_thesis: ( H is conjunctive implies ex H1 being ZF-formula st (len H1) + 1 <= len H ) assume H is conjunctive ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H then consider H1, F1 being ZF-formula such that A8: H = H1 '&' F1 by Def13; take H1 = H1; ::_thesis: (len H1) + 1 <= len H A9: ( len (<*3*> ^ H1) = (len <*3*>) + (len H1) & len <*3*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; len H = (len (<*3*> ^ H1)) + (len F1) by A8, FINSEQ_1:22; hence (len H1) + 1 <= len H by A9, NAT_1:11; ::_thesis: verum end; assume not H is atomic ; ::_thesis: ex H1 being ZF-formula st (len H1) + 1 <= len H then ( H is negative or H is conjunctive or H is universal ) by Th10; hence ex H1 being ZF-formula st (len H1) + 1 <= len H by A5, A7, A1; ::_thesis: verum end; theorem Th13: :: ZF_LANG:13 for H being ZF-formula holds 3 <= len H proof let H be ZF-formula; ::_thesis: 3 <= len H now__::_thesis:_(_not_H_is_atomic_implies_3_<=_len_H_) assume not H is atomic ; ::_thesis: 3 <= len H then consider H1 being ZF-formula such that A1: (len H1) + 1 <= len H by Th12; A2: now__::_thesis:_(_not_H1_is_atomic_implies_3_<=_len_H_) assume not H1 is atomic ; ::_thesis: 3 <= len H then consider F being ZF-formula such that A3: (len F) + 1 <= len H1 by Th12; A4: now__::_thesis:_(_not_F_is_atomic_implies_3_<=_len_H_) assume not F is atomic ; ::_thesis: 3 <= len H then consider F1 being ZF-formula such that A5: (len F1) + 1 <= len F by Th12; 0 <= len F1 by NAT_1:2; then 0 + 1 <= (len F1) + 1 by XREAL_1:7; then 1 <= len F by A5, XXREAL_0:2; then 1 + 1 <= (len F) + 1 by XREAL_1:7; then 2 <= len H1 by A3, XXREAL_0:2; then 2 + 1 <= (len H1) + 1 by XREAL_1:7; hence 3 <= len H by A1, XXREAL_0:2; ::_thesis: verum end; A6: ((len F) + 1) + 1 <= (len H1) + 1 by A3, XREAL_1:7; now__::_thesis:_(_F_is_atomic_implies_3_<=_len_H_) assume F is atomic ; ::_thesis: 3 <= len H then len F = 3 by Th11; then (3 + 1) + 1 <= len H by A1, A6, XXREAL_0:2; hence 3 <= len H by XXREAL_0:2; ::_thesis: verum end; hence 3 <= len H by A4; ::_thesis: verum end; now__::_thesis:_(_H1_is_atomic_implies_3_<=_len_H_) assume H1 is atomic ; ::_thesis: 3 <= len H then 3 + 1 <= len H by A1, Th11; hence 3 <= len H by XXREAL_0:2; ::_thesis: verum end; hence 3 <= len H by A2; ::_thesis: verum end; hence 3 <= len H by Th11; ::_thesis: verum end; theorem :: ZF_LANG:14 for H being ZF-formula st len H = 3 holds H is atomic proof let H be ZF-formula; ::_thesis: ( len H = 3 implies H is atomic ) assume A1: len H = 3 ; ::_thesis: H is atomic assume not H is atomic ; ::_thesis: contradiction then consider H1 being ZF-formula such that A2: (len H1) + 1 <= len H by Th12; 3 <= len H1 by Th13; then 3 + 1 <= (len H1) + 1 by XREAL_1:7; hence contradiction by A1, A2, XXREAL_0:2; ::_thesis: verum end; theorem Th15: :: ZF_LANG:15 for x, y being Variable holds ( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 ) proof let x, y be Variable; ::_thesis: ( (x '=' y) . 1 = 0 & (x 'in' y) . 1 = 1 ) thus (x '=' y) . 1 = (<*0*> ^ (<*x*> ^ <*y*>)) . 1 by FINSEQ_1:32 .= 0 by FINSEQ_1:41 ; ::_thesis: (x 'in' y) . 1 = 1 thus (x 'in' y) . 1 = (<*1*> ^ (<*x*> ^ <*y*>)) . 1 by FINSEQ_1:32 .= 1 by FINSEQ_1:41 ; ::_thesis: verum end; theorem Th16: :: ZF_LANG:16 for F, G being ZF-formula holds (F '&' G) . 1 = 3 proof let F, G be ZF-formula; ::_thesis: (F '&' G) . 1 = 3 thus (F '&' G) . 1 = (<*3*> ^ (F ^ G)) . 1 by FINSEQ_1:32 .= 3 by FINSEQ_1:41 ; ::_thesis: verum end; theorem Th17: :: ZF_LANG:17 for x being Variable for H being ZF-formula holds (All (x,H)) . 1 = 4 proof let x be Variable; ::_thesis: for H being ZF-formula holds (All (x,H)) . 1 = 4 let H be ZF-formula; ::_thesis: (All (x,H)) . 1 = 4 thus (All (x,H)) . 1 = (<*4*> ^ (<*x*> ^ H)) . 1 by FINSEQ_1:32 .= 4 by FINSEQ_1:41 ; ::_thesis: verum end; theorem Th18: :: ZF_LANG:18 for H being ZF-formula st H is being_equality holds H . 1 = 0 proof let H be ZF-formula; ::_thesis: ( H is being_equality implies H . 1 = 0 ) assume H is being_equality ; ::_thesis: H . 1 = 0 then consider x, y being Variable such that A1: H = x '=' y by Def10; H = <*0,x,y*> by A1, FINSEQ_1:def_10; hence H . 1 = 0 by FINSEQ_1:45; ::_thesis: verum end; theorem Th19: :: ZF_LANG:19 for H being ZF-formula st H is being_membership holds H . 1 = 1 proof let H be ZF-formula; ::_thesis: ( H is being_membership implies H . 1 = 1 ) assume H is being_membership ; ::_thesis: H . 1 = 1 then consider x, y being Variable such that A1: H = x 'in' y by Def11; H = <*1,x,y*> by A1, FINSEQ_1:def_10; hence H . 1 = 1 by FINSEQ_1:45; ::_thesis: verum end; theorem Th20: :: ZF_LANG:20 for H being ZF-formula st H is negative holds H . 1 = 2 proof let H be ZF-formula; ::_thesis: ( H is negative implies H . 1 = 2 ) assume H is negative ; ::_thesis: H . 1 = 2 then ex H1 being ZF-formula st H = 'not' H1 by Def12; hence H . 1 = 2 by FINSEQ_1:41; ::_thesis: verum end; theorem Th21: :: ZF_LANG:21 for H being ZF-formula st H is conjunctive holds H . 1 = 3 proof let H be ZF-formula; ::_thesis: ( H is conjunctive implies H . 1 = 3 ) assume H is conjunctive ; ::_thesis: H . 1 = 3 then consider F, G being ZF-formula such that A1: H = F '&' G by Def13; (<*3*> ^ F) ^ G = <*3*> ^ (F ^ G) by FINSEQ_1:32; hence H . 1 = 3 by A1, FINSEQ_1:41; ::_thesis: verum end; theorem Th22: :: ZF_LANG:22 for H being ZF-formula st H is universal holds H . 1 = 4 proof let H be ZF-formula; ::_thesis: ( H is universal implies H . 1 = 4 ) assume H is universal ; ::_thesis: H . 1 = 4 then consider x being Variable, H1 being ZF-formula such that A1: H = All (x,H1) by Def14; (<*4*> ^ <*x*>) ^ H1 = <*4*> ^ (<*x*> ^ H1) by FINSEQ_1:32; hence H . 1 = 4 by A1, FINSEQ_1:41; ::_thesis: verum end; theorem Th23: :: ZF_LANG:23 for H being ZF-formula holds ( ( H is being_equality & H . 1 = 0 ) or ( H is being_membership & H . 1 = 1 ) or ( H is negative & H . 1 = 2 ) or ( H is conjunctive & H . 1 = 3 ) or ( H is universal & H . 1 = 4 ) ) proof let H be ZF-formula; ::_thesis: ( ( H is being_equality & H . 1 = 0 ) or ( H is being_membership & H . 1 = 1 ) or ( H is negative & H . 1 = 2 ) or ( H is conjunctive & H . 1 = 3 ) or ( H is universal & H . 1 = 4 ) ) percases ( H is being_equality or H is being_membership or H is negative or H is conjunctive or H is universal ) by Th9; case H is being_equality ; ::_thesis: H . 1 = 0 hence H . 1 = 0 by Th18; ::_thesis: verum end; case H is being_membership ; ::_thesis: H . 1 = 1 hence H . 1 = 1 by Th19; ::_thesis: verum end; case H is negative ; ::_thesis: H . 1 = 2 hence H . 1 = 2 by Th20; ::_thesis: verum end; case H is conjunctive ; ::_thesis: H . 1 = 3 hence H . 1 = 3 by Th21; ::_thesis: verum end; case H is universal ; ::_thesis: H . 1 = 4 hence H . 1 = 4 by Th22; ::_thesis: verum end; end; end; theorem :: ZF_LANG:24 for H being ZF-formula st H . 1 = 0 holds H is being_equality by Th23; theorem :: ZF_LANG:25 for H being ZF-formula st H . 1 = 1 holds H is being_membership by Th23; theorem :: ZF_LANG:26 for H being ZF-formula st H . 1 = 2 holds H is negative by Th23; theorem :: ZF_LANG:27 for H being ZF-formula st H . 1 = 3 holds H is conjunctive by Th23; theorem :: ZF_LANG:28 for H being ZF-formula st H . 1 = 4 holds H is universal by Th23; theorem Th29: :: ZF_LANG:29 for H, F being ZF-formula for sq being FinSequence st H = F ^ sq holds H = F proof let H, F be ZF-formula; ::_thesis: for sq being FinSequence st H = F ^ sq holds H = F let sq be FinSequence; ::_thesis: ( H = F ^ sq implies H = F ) defpred S1[ Nat] means for H, F being ZF-formula for sq being FinSequence st len H = $1 & H = F ^ sq holds H = F; for n being Nat st ( for k being Nat st k < n holds for H, F being ZF-formula for sq being FinSequence st len H = k & H = F ^ sq holds H = F ) holds for H, F being ZF-formula for sq being FinSequence st len H = n & H = F ^ sq holds H = F proof let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds for H, F being ZF-formula for sq being FinSequence st len H = k & H = F ^ sq holds H = F ) implies for H, F being ZF-formula for sq being FinSequence st len H = n & H = F ^ sq holds H = F ) assume A1: for k being Nat st k < n holds for H, F being ZF-formula for sq being FinSequence st len H = k & H = F ^ sq holds H = F ; ::_thesis: for H, F being ZF-formula for sq being FinSequence st len H = n & H = F ^ sq holds H = F let H, F be ZF-formula; ::_thesis: for sq being FinSequence st len H = n & H = F ^ sq holds H = F let sq be FinSequence; ::_thesis: ( len H = n & H = F ^ sq implies H = F ) assume that A2: len H = n and A3: H = F ^ sq ; ::_thesis: H = F 3 <= len F by Th13; then ( dom F = Seg (len F) & 1 <= len F ) by FINSEQ_1:def_3, XXREAL_0:2; then A4: 1 in dom F by FINSEQ_1:1; A5: now__::_thesis:_(_H_is_negative_implies_H_=_F_) A6: len <*2*> = 1 by FINSEQ_1:40; assume A7: H is negative ; ::_thesis: H = F then consider H1 being ZF-formula such that A8: H = 'not' H1 by Def12; (F ^ sq) . 1 = 2 by A3, A7, Th20; then F . 1 = 2 by A4, FINSEQ_1:def_7; then F is negative by Th23; then consider F1 being ZF-formula such that A9: F = 'not' F1 by Def12; (len <*2*>) + (len H1) = len H by A8, FINSEQ_1:22; then A10: len H1 < len H by A6, NAT_1:13; (<*2*> ^ F1) ^ sq = <*2*> ^ (F1 ^ sq) by FINSEQ_1:32; then H1 = F1 ^ sq by A3, A8, A9, FINSEQ_1:33; hence H = F by A1, A2, A8, A9, A10; ::_thesis: verum end; A11: now__::_thesis:_(_H_is_conjunctive_implies_H_=_F_) assume A12: H is conjunctive ; ::_thesis: H = F then consider G1, G being ZF-formula such that A13: H = G1 '&' G by Def13; A14: (len G) + (1 + (len G1)) = ((len G) + 1) + (len G1) ; A15: ( len (<*3*> ^ G1) = (len <*3*>) + (len G1) & len <*3*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; (len (<*3*> ^ G1)) + (len G) = len H by A13, FINSEQ_1:22; then (len G) + 1 <= len H by A15, A14, NAT_1:11; then A16: len G < len H by NAT_1:13; (F ^ sq) . 1 = 3 by A3, A12, Th21; then F . 1 = 3 by A4, FINSEQ_1:def_7; then F is conjunctive by Th23; then consider F1, H1 being ZF-formula such that A17: F = F1 '&' H1 by Def13; A18: now__::_thesis:_(_ex_sq9_being_FinSequence_st_F1_=_G1_^_sq9_implies_F1_=_G1_) A19: (((len F1) + 1) + (len H1)) + (len sq) = ((len F1) + 1) + ((len H1) + (len sq)) ; given sq9 being FinSequence such that A20: F1 = G1 ^ sq9 ; ::_thesis: F1 = G1 A21: ( len (F ^ sq) = (len F) + (len sq) & len <*3*> = 1 ) by FINSEQ_1:22, FINSEQ_1:40; ( len (<*3*> ^ F1) = (len <*3*>) + (len F1) & len F = (len (<*3*> ^ F1)) + (len H1) ) by A17, FINSEQ_1:22; then (len F1) + 1 <= len H by A3, A21, A19, NAT_1:11; then len F1 < len H by NAT_1:13; hence F1 = G1 by A1, A2, A20; ::_thesis: verum end; A22: ( (<*3*> ^ F1) ^ H1 = <*3*> ^ (F1 ^ H1) & (<*3*> ^ (F1 ^ H1)) ^ sq = <*3*> ^ ((F1 ^ H1) ^ sq) ) by FINSEQ_1:32; A23: now__::_thesis:_(_ex_sq9_being_FinSequence_st_G1_=_F1_^_sq9_implies_G1_=_F1_) given sq9 being FinSequence such that A24: G1 = F1 ^ sq9 ; ::_thesis: G1 = F1 A25: len <*3*> = 1 by FINSEQ_1:40; ( (len (<*3*> ^ G1)) + (len G) = len H & len (<*3*> ^ G1) = (len <*3*>) + (len G1) ) by A13, FINSEQ_1:22; then (len G1) + 1 <= len H by A25, NAT_1:11; then len G1 < len H by NAT_1:13; hence G1 = F1 by A1, A2, A24; ::_thesis: verum end; A26: (F1 ^ H1) ^ sq = F1 ^ (H1 ^ sq) by FINSEQ_1:32; (<*3*> ^ G1) ^ G = <*3*> ^ (G1 ^ G) by FINSEQ_1:32; then A27: G1 ^ G = F1 ^ (H1 ^ sq) by A3, A13, A17, A22, A26, FINSEQ_1:33; then ( len F1 <= len G1 implies ex sq9 being FinSequence st G1 = F1 ^ sq9 ) by FINSEQ_1:47; then G = H1 ^ sq by A27, A23, A18, FINSEQ_1:33, FINSEQ_1:47; hence H = F by A1, A2, A3, A17, A22, A26, A16; ::_thesis: verum end; A28: now__::_thesis:_(_H_is_universal_implies_H_=_F_) assume A29: H is universal ; ::_thesis: H = F then consider x being Variable, H1 being ZF-formula such that A30: H = All (x,H1) by Def14; A31: <*4*> ^ <*x*> = <*4,x*> by FINSEQ_1:def_9; A32: ( len <*4,x*> = 2 & 1 + (1 + (len H1)) = (1 + (len H1)) + 1 ) by FINSEQ_1:44; (len (<*4*> ^ <*x*>)) + (len H1) = len H by A30, FINSEQ_1:22; then (len H1) + 1 <= len H by A32, A31, NAT_1:11; then A33: len H1 < len H by NAT_1:13; (F ^ sq) . 1 = 4 by A3, A29, Th22; then F . 1 = 4 by A4, FINSEQ_1:def_7; then F is universal by Th23; then consider y being Variable, F1 being ZF-formula such that A34: F = All (y,F1) by Def14; A35: ( (<*x*> ^ H1) . 1 = x & (<*y*> ^ (F1 ^ sq)) . 1 = y ) by FINSEQ_1:41; A36: ((<*4*> ^ <*y*>) ^ F1) ^ sq = (<*4*> ^ <*y*>) ^ (F1 ^ sq) by FINSEQ_1:32; ( (<*4*> ^ <*x*>) ^ H1 = <*4*> ^ (<*x*> ^ H1) & (<*4*> ^ <*y*>) ^ (F1 ^ sq) = <*4*> ^ (<*y*> ^ (F1 ^ sq)) ) by FINSEQ_1:32; then <*x*> ^ H1 = <*y*> ^ (F1 ^ sq) by A3, A30, A34, A36, FINSEQ_1:33; then H1 = F1 ^ sq by A35, FINSEQ_1:33; hence H = F by A1, A2, A3, A34, A36, A33; ::_thesis: verum end; A37: (len F) + (len sq) = len (F ^ sq) by FINSEQ_1:22; now__::_thesis:_(_H_is_atomic_implies_H_=_F_) A38: 3 <= len F by Th13; assume H is atomic ; ::_thesis: H = F then A39: len H = 3 by Th11; then len F <= 3 by A3, A37, NAT_1:11; then 3 + (len sq) = 3 + 0 by A3, A37, A39, A38, XXREAL_0:1; then sq = {} ; hence H = F by A3, FINSEQ_1:34; ::_thesis: verum end; hence H = F by A5, A28, A11, Th10; ::_thesis: verum end; then A40: for k being Nat st ( for n being Nat st n < k holds S1[n] ) holds S1[k] ; A41: for n being Nat holds S1[n] from NAT_1:sch_4(A40); len H = len H ; hence ( H = F ^ sq implies H = F ) by A41; ::_thesis: verum end; theorem Th30: :: ZF_LANG:30 for H, G, H1, G1 being ZF-formula st H '&' G = H1 '&' G1 holds ( H = H1 & G = G1 ) proof let H, G, H1, G1 be ZF-formula; ::_thesis: ( H '&' G = H1 '&' G1 implies ( H = H1 & G = G1 ) ) assume A1: H '&' G = H1 '&' G1 ; ::_thesis: ( H = H1 & G = G1 ) ( (<*3*> ^ H) ^ G = <*3*> ^ (H ^ G) & (<*3*> ^ H1) ^ G1 = <*3*> ^ (H1 ^ G1) ) by FINSEQ_1:32; then A2: H ^ G = H1 ^ G1 by A1, FINSEQ_1:33; then A3: ( len H1 <= len H implies ex sq being FinSequence st H = H1 ^ sq ) by FINSEQ_1:47; A4: ( len H <= len H1 implies ex sq being FinSequence st H1 = H ^ sq ) by A2, FINSEQ_1:47; hence H = H1 by A3, Th29; ::_thesis: G = G1 ( ex sq being FinSequence st H1 = H ^ sq implies H1 = H ) by Th29; hence G = G1 by A1, A3, A4, Th29, FINSEQ_1:33; ::_thesis: verum end; theorem Th31: :: ZF_LANG:31 for F, G, F1, G1 being ZF-formula st F 'or' G = F1 'or' G1 holds ( F = F1 & G = G1 ) proof let F, G, F1, G1 be ZF-formula; ::_thesis: ( F 'or' G = F1 'or' G1 implies ( F = F1 & G = G1 ) ) assume F 'or' G = F1 'or' G1 ; ::_thesis: ( F = F1 & G = G1 ) then ('not' F) '&' ('not' G) = ('not' F1) '&' ('not' G1) by FINSEQ_1:33; then ( 'not' F = 'not' F1 & 'not' G = 'not' G1 ) by Th30; hence ( F = F1 & G = G1 ) by FINSEQ_1:33; ::_thesis: verum end; theorem Th32: :: ZF_LANG:32 for F, G, F1, G1 being ZF-formula st F => G = F1 => G1 holds ( F = F1 & G = G1 ) proof let F, G, F1, G1 be ZF-formula; ::_thesis: ( F => G = F1 => G1 implies ( F = F1 & G = G1 ) ) assume F => G = F1 => G1 ; ::_thesis: ( F = F1 & G = G1 ) then A1: F '&' ('not' G) = F1 '&' ('not' G1) by FINSEQ_1:33; hence F = F1 by Th30; ::_thesis: G = G1 'not' G = 'not' G1 by A1, Th30; hence G = G1 by FINSEQ_1:33; ::_thesis: verum end; theorem Th33: :: ZF_LANG:33 for F, G, F1, G1 being ZF-formula st F <=> G = F1 <=> G1 holds ( F = F1 & G = G1 ) proof let F, G, F1, G1 be ZF-formula; ::_thesis: ( F <=> G = F1 <=> G1 implies ( F = F1 & G = G1 ) ) assume F <=> G = F1 <=> G1 ; ::_thesis: ( F = F1 & G = G1 ) then F => G = F1 => G1 by Th30; hence ( F = F1 & G = G1 ) by Th32; ::_thesis: verum end; theorem Th34: :: ZF_LANG:34 for x, y being Variable for H, G being ZF-formula st Ex (x,H) = Ex (y,G) holds ( x = y & H = G ) proof let x, y be Variable; ::_thesis: for H, G being ZF-formula st Ex (x,H) = Ex (y,G) holds ( x = y & H = G ) let H, G be ZF-formula; ::_thesis: ( Ex (x,H) = Ex (y,G) implies ( x = y & H = G ) ) assume Ex (x,H) = Ex (y,G) ; ::_thesis: ( x = y & H = G ) then A1: All (x,('not' H)) = All (y,('not' G)) by FINSEQ_1:33; then 'not' H = 'not' G by Th3; hence ( x = y & H = G ) by A1, Th3, FINSEQ_1:33; ::_thesis: verum end; definition let H be ZF-formula; assume A1: H is atomic ; func Var1 H -> Variable equals :Def28: :: ZF_LANG:def 28 H . 2; coherence H . 2 is Variable proof A2: ( ex x, y being Variable st H = x 'in' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ; A3: ( ex x, y being Variable st H = x '=' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ; ( H is being_equality or H is being_membership ) by A1, Def15; then consider k being Element of NAT , x, y being Variable such that A4: H = (<*k*> ^ <*x*>) ^ <*y*> by A3, A2, Def10, Def11; H = <*k,x,y*> by A4, FINSEQ_1:def_10; hence H . 2 is Variable by FINSEQ_1:45; ::_thesis: verum end; func Var2 H -> Variable equals :Def29: :: ZF_LANG:def 29 H . 3; coherence H . 3 is Variable proof A5: ( ex x, y being Variable st H = x 'in' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ; A6: ( ex x, y being Variable st H = x '=' y implies ex k being Element of NAT ex x, y being Variable st H = (<*k*> ^ <*x*>) ^ <*y*> ) ; ( H is being_equality or H is being_membership ) by A1, Def15; then consider k being Element of NAT , x, y being Variable such that A7: H = (<*k*> ^ <*x*>) ^ <*y*> by A6, A5, Def10, Def11; H = <*k,x,y*> by A7, FINSEQ_1:def_10; hence H . 3 is Variable by FINSEQ_1:45; ::_thesis: verum end; end; :: deftheorem Def28 defines Var1 ZF_LANG:def_28_:_ for H being ZF-formula st H is atomic holds Var1 H = H . 2; :: deftheorem Def29 defines Var2 ZF_LANG:def_29_:_ for H being ZF-formula st H is atomic holds Var2 H = H . 3; theorem :: ZF_LANG:35 for H being ZF-formula st H is atomic holds ( Var1 H = H . 2 & Var2 H = H . 3 ) by Def28, Def29; theorem Th36: :: ZF_LANG:36 for H being ZF-formula st H is being_equality holds H = (Var1 H) '=' (Var2 H) proof let H be ZF-formula; ::_thesis: ( H is being_equality implies H = (Var1 H) '=' (Var2 H) ) assume A1: H is being_equality ; ::_thesis: H = (Var1 H) '=' (Var2 H) then consider x, y being Variable such that A2: H = x '=' y by Def10; (<*0*> ^ <*x*>) ^ <*y*> = <*0,x,y*> by FINSEQ_1:def_10; then A3: ( H . 2 = x & H . 3 = y ) by A2, FINSEQ_1:45; A4: H is atomic by A1, Def15; then H . 2 = Var1 H by Def28; hence H = (Var1 H) '=' (Var2 H) by A2, A4, A3, Def29; ::_thesis: verum end; theorem Th37: :: ZF_LANG:37 for H being ZF-formula st H is being_membership holds H = (Var1 H) 'in' (Var2 H) proof let H be ZF-formula; ::_thesis: ( H is being_membership implies H = (Var1 H) 'in' (Var2 H) ) assume A1: H is being_membership ; ::_thesis: H = (Var1 H) 'in' (Var2 H) then consider x, y being Variable such that A2: H = x 'in' y by Def11; (<*1*> ^ <*x*>) ^ <*y*> = <*1,x,y*> by FINSEQ_1:def_10; then A3: ( H . 2 = x & H . 3 = y ) by A2, FINSEQ_1:45; A4: H is atomic by A1, Def15; then H . 2 = Var1 H by Def28; hence H = (Var1 H) 'in' (Var2 H) by A2, A4, A3, Def29; ::_thesis: verum end; definition let H be ZF-formula; assume A1: H is negative ; func the_argument_of H -> ZF-formula means :Def30: :: ZF_LANG:def 30 'not' it = H; existence ex b1 being ZF-formula st 'not' b1 = H by A1, Def12; uniqueness for b1, b2 being ZF-formula st 'not' b1 = H & 'not' b2 = H holds b1 = b2 by FINSEQ_1:33; end; :: deftheorem Def30 defines the_argument_of ZF_LANG:def_30_:_ for H being ZF-formula st H is negative holds for b2 being ZF-formula holds ( b2 = the_argument_of H iff 'not' b2 = H ); definition let H be ZF-formula; assume A1: ( H is conjunctive or H is disjunctive ) ; func the_left_argument_of H -> ZF-formula means :Def31: :: ZF_LANG:def 31 ex H1 being ZF-formula st it '&' H1 = H if H is conjunctive otherwise ex H1 being ZF-formula st it 'or' H1 = H; existence ( ( H is conjunctive implies ex b1, H1 being ZF-formula st b1 '&' H1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st b1 'or' H1 = H ) ) by A1, Def13, Def20; uniqueness for b1, b2 being ZF-formula holds ( ( H is conjunctive & ex H1 being ZF-formula st b1 '&' H1 = H & ex H1 being ZF-formula st b2 '&' H1 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st b1 'or' H1 = H & ex H1 being ZF-formula st b2 'or' H1 = H implies b1 = b2 ) ) by Th30, Th31; consistency for b1 being ZF-formula holds verum ; func the_right_argument_of H -> ZF-formula means :Def32: :: ZF_LANG:def 32 ex H1 being ZF-formula st H1 '&' it = H if H is conjunctive otherwise ex H1 being ZF-formula st H1 'or' it = H; existence ( ( H is conjunctive implies ex b1, H1 being ZF-formula st H1 '&' b1 = H ) & ( not H is conjunctive implies ex b1, H1 being ZF-formula st H1 'or' b1 = H ) ) proof thus ( H is conjunctive implies ex G, H1 being ZF-formula st H1 '&' G = H ) ::_thesis: ( not H is conjunctive implies ex b1, H1 being ZF-formula st H1 'or' b1 = H ) proof assume H is conjunctive ; ::_thesis: ex G, H1 being ZF-formula st H1 '&' G = H then consider G, F being ZF-formula such that A2: G '&' F = H by Def13; take F ; ::_thesis: ex H1 being ZF-formula st H1 '&' F = H thus ex H1 being ZF-formula st H1 '&' F = H by A2; ::_thesis: verum end; thus ( not H is conjunctive implies ex G, H1 being ZF-formula st H1 'or' G = H ) ::_thesis: verum proof assume not H is conjunctive ; ::_thesis: ex G, H1 being ZF-formula st H1 'or' G = H then consider G, F being ZF-formula such that A3: G 'or' F = H by A1, Def20; take F ; ::_thesis: ex H1 being ZF-formula st H1 'or' F = H thus ex H1 being ZF-formula st H1 'or' F = H by A3; ::_thesis: verum end; end; uniqueness for b1, b2 being ZF-formula holds ( ( H is conjunctive & ex H1 being ZF-formula st H1 '&' b1 = H & ex H1 being ZF-formula st H1 '&' b2 = H implies b1 = b2 ) & ( not H is conjunctive & ex H1 being ZF-formula st H1 'or' b1 = H & ex H1 being ZF-formula st H1 'or' b2 = H implies b1 = b2 ) ) by Th30, Th31; consistency for b1 being ZF-formula holds verum ; end; :: deftheorem Def31 defines the_left_argument_of ZF_LANG:def_31_:_ for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds for b2 being ZF-formula holds ( ( H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 '&' H1 = H ) ) & ( not H is conjunctive implies ( b2 = the_left_argument_of H iff ex H1 being ZF-formula st b2 'or' H1 = H ) ) ); :: deftheorem Def32 defines the_right_argument_of ZF_LANG:def_32_:_ for H being ZF-formula st ( H is conjunctive or H is disjunctive ) holds for b2 being ZF-formula holds ( ( H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 '&' b2 = H ) ) & ( not H is conjunctive implies ( b2 = the_right_argument_of H iff ex H1 being ZF-formula st H1 'or' b2 = H ) ) ); theorem :: ZF_LANG:38 for H, F being ZF-formula st H is conjunctive holds ( ( F = the_left_argument_of H implies ex G being ZF-formula st F '&' G = H ) & ( ex G being ZF-formula st F '&' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G '&' F = H ) & ( ex G being ZF-formula st G '&' F = H implies F = the_right_argument_of H ) ) by Def31, Def32; theorem Th39: :: ZF_LANG:39 for H, F being ZF-formula st H is disjunctive holds ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) proof let H, F be ZF-formula; ::_thesis: ( H is disjunctive implies ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) ) assume A1: H is disjunctive ; ::_thesis: ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) then ex F, G being ZF-formula st H = F 'or' G by Def20; then H . 1 = 2 by FINSEQ_1:41; then not H is conjunctive by Th21; hence ( ( F = the_left_argument_of H implies ex G being ZF-formula st F 'or' G = H ) & ( ex G being ZF-formula st F 'or' G = H implies F = the_left_argument_of H ) & ( F = the_right_argument_of H implies ex G being ZF-formula st G 'or' F = H ) & ( ex G being ZF-formula st G 'or' F = H implies F = the_right_argument_of H ) ) by A1, Def31, Def32; ::_thesis: verum end; theorem Th40: :: ZF_LANG:40 for H being ZF-formula st H is conjunctive holds H = (the_left_argument_of H) '&' (the_right_argument_of H) proof let H be ZF-formula; ::_thesis: ( H is conjunctive implies H = (the_left_argument_of H) '&' (the_right_argument_of H) ) assume A1: H is conjunctive ; ::_thesis: H = (the_left_argument_of H) '&' (the_right_argument_of H) then ex F1 being ZF-formula st H = (the_left_argument_of H) '&' F1 by Def31; hence H = (the_left_argument_of H) '&' (the_right_argument_of H) by A1, Def32; ::_thesis: verum end; theorem :: ZF_LANG:41 for H being ZF-formula st H is disjunctive holds H = (the_left_argument_of H) 'or' (the_right_argument_of H) proof let H be ZF-formula; ::_thesis: ( H is disjunctive implies H = (the_left_argument_of H) 'or' (the_right_argument_of H) ) assume A1: H is disjunctive ; ::_thesis: H = (the_left_argument_of H) 'or' (the_right_argument_of H) then ex F1 being ZF-formula st H = (the_left_argument_of H) 'or' F1 by Th39; hence H = (the_left_argument_of H) 'or' (the_right_argument_of H) by A1, Th39; ::_thesis: verum end; definition let H be ZF-formula; assume A1: ( H is universal or H is existential ) ; func bound_in H -> Variable means :Def33: :: ZF_LANG:def 33 ex H1 being ZF-formula st All (it,H1) = H if H is universal otherwise ex H1 being ZF-formula st Ex (it,H1) = H; existence ( ( H is universal implies ex b1 being Variable ex H1 being ZF-formula st All (b1,H1) = H ) & ( not H is universal implies ex b1 being Variable ex H1 being ZF-formula st Ex (b1,H1) = H ) ) by A1, Def14, Def23; uniqueness for b1, b2 being Variable holds ( ( H is universal & ex H1 being ZF-formula st All (b1,H1) = H & ex H1 being ZF-formula st All (b2,H1) = H implies b1 = b2 ) & ( not H is universal & ex H1 being ZF-formula st Ex (b1,H1) = H & ex H1 being ZF-formula st Ex (b2,H1) = H implies b1 = b2 ) ) by Th3, Th34; consistency for b1 being Variable holds verum ; func the_scope_of H -> ZF-formula means :Def34: :: ZF_LANG:def 34 ex x being Variable st All (x,it) = H if H is universal otherwise ex x being Variable st Ex (x,it) = H; existence ( ( H is universal implies ex b1 being ZF-formula ex x being Variable st All (x,b1) = H ) & ( not H is universal implies ex b1 being ZF-formula ex x being Variable st Ex (x,b1) = H ) ) proof thus ( H is universal implies ex H1 being ZF-formula ex x being Variable st All (x,H1) = H ) ::_thesis: ( not H is universal implies ex b1 being ZF-formula ex x being Variable st Ex (x,b1) = H ) proof assume H is universal ; ::_thesis: ex H1 being ZF-formula ex x being Variable st All (x,H1) = H then consider x being Variable, G being ZF-formula such that A2: All (x,G) = H by Def14; take G ; ::_thesis: ex x being Variable st All (x,G) = H thus ex x being Variable st All (x,G) = H by A2; ::_thesis: verum end; thus ( not H is universal implies ex H1 being ZF-formula ex x being Variable st Ex (x,H1) = H ) ::_thesis: verum proof assume not H is universal ; ::_thesis: ex H1 being ZF-formula ex x being Variable st Ex (x,H1) = H then consider x being Variable, G being ZF-formula such that A3: Ex (x,G) = H by A1, Def23; take G ; ::_thesis: ex x being Variable st Ex (x,G) = H thus ex x being Variable st Ex (x,G) = H by A3; ::_thesis: verum end; end; uniqueness for b1, b2 being ZF-formula holds ( ( H is universal & ex x being Variable st All (x,b1) = H & ex x being Variable st All (x,b2) = H implies b1 = b2 ) & ( not H is universal & ex x being Variable st Ex (x,b1) = H & ex x being Variable st Ex (x,b2) = H implies b1 = b2 ) ) by Th3, Th34; consistency for b1 being ZF-formula holds verum ; end; :: deftheorem Def33 defines bound_in ZF_LANG:def_33_:_ for H being ZF-formula st ( H is universal or H is existential ) holds for b2 being Variable holds ( ( H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st All (b2,H1) = H ) ) & ( not H is universal implies ( b2 = bound_in H iff ex H1 being ZF-formula st Ex (b2,H1) = H ) ) ); :: deftheorem Def34 defines the_scope_of ZF_LANG:def_34_:_ for H being ZF-formula st ( H is universal or H is existential ) holds for b2 being ZF-formula holds ( ( H is universal implies ( b2 = the_scope_of H iff ex x being Variable st All (x,b2) = H ) ) & ( not H is universal implies ( b2 = the_scope_of H iff ex x being Variable st Ex (x,b2) = H ) ) ); theorem :: ZF_LANG:42 for x being Variable for H, H1 being ZF-formula st H is universal holds ( ( x = bound_in H implies ex H1 being ZF-formula st All (x,H1) = H ) & ( ex H1 being ZF-formula st All (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st All (x,H1) = H ) & ( ex x being Variable st All (x,H1) = H implies H1 = the_scope_of H ) ) by Def33, Def34; theorem Th43: :: ZF_LANG:43 for x being Variable for H, H1 being ZF-formula st H is existential holds ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) proof let x be Variable; ::_thesis: for H, H1 being ZF-formula st H is existential holds ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) let H, H1 be ZF-formula; ::_thesis: ( H is existential implies ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) ) assume A1: H is existential ; ::_thesis: ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) then ex y being Variable ex F being ZF-formula st H = Ex (y,F) by Def23; then H . 1 = 2 by FINSEQ_1:41; then not H is universal by Th22; hence ( ( x = bound_in H implies ex H1 being ZF-formula st Ex (x,H1) = H ) & ( ex H1 being ZF-formula st Ex (x,H1) = H implies x = bound_in H ) & ( H1 = the_scope_of H implies ex x being Variable st Ex (x,H1) = H ) & ( ex x being Variable st Ex (x,H1) = H implies H1 = the_scope_of H ) ) by A1, Def33, Def34; ::_thesis: verum end; theorem Th44: :: ZF_LANG:44 for H being ZF-formula st H is universal holds H = All ((bound_in H),(the_scope_of H)) proof let H be ZF-formula; ::_thesis: ( H is universal implies H = All ((bound_in H),(the_scope_of H)) ) assume A1: H is universal ; ::_thesis: H = All ((bound_in H),(the_scope_of H)) then ex x being Variable st H = All (x,(the_scope_of H)) by Def34; hence H = All ((bound_in H),(the_scope_of H)) by A1, Def33; ::_thesis: verum end; theorem :: ZF_LANG:45 for H being ZF-formula st H is existential holds H = Ex ((bound_in H),(the_scope_of H)) proof let H be ZF-formula; ::_thesis: ( H is existential implies H = Ex ((bound_in H),(the_scope_of H)) ) assume A1: H is existential ; ::_thesis: H = Ex ((bound_in H),(the_scope_of H)) then ex x being Variable st H = Ex (x,(the_scope_of H)) by Th43; hence H = Ex ((bound_in H),(the_scope_of H)) by A1, Th43; ::_thesis: verum end; definition let H be ZF-formula; assume A1: H is conditional ; func the_antecedent_of H -> ZF-formula means :Def35: :: ZF_LANG:def 35 ex H1 being ZF-formula st H = it => H1; existence ex b1, H1 being ZF-formula st H = b1 => H1 by A1, Def21; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 => H1 & ex H1 being ZF-formula st H = b2 => H1 holds b1 = b2 by Th32; func the_consequent_of H -> ZF-formula means :Def36: :: ZF_LANG:def 36 ex H1 being ZF-formula st H = H1 => it; existence ex b1, H1 being ZF-formula st H = H1 => b1 proof consider F, G being ZF-formula such that A2: H = F => G by A1, Def21; take G ; ::_thesis: ex H1 being ZF-formula st H = H1 => G take F ; ::_thesis: H = F => G thus H = F => G by A2; ::_thesis: verum end; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 => b1 & ex H1 being ZF-formula st H = H1 => b2 holds b1 = b2 by Th32; end; :: deftheorem Def35 defines the_antecedent_of ZF_LANG:def_35_:_ for H being ZF-formula st H is conditional holds for b2 being ZF-formula holds ( b2 = the_antecedent_of H iff ex H1 being ZF-formula st H = b2 => H1 ); :: deftheorem Def36 defines the_consequent_of ZF_LANG:def_36_:_ for H being ZF-formula st H is conditional holds for b2 being ZF-formula holds ( b2 = the_consequent_of H iff ex H1 being ZF-formula st H = H1 => b2 ); theorem :: ZF_LANG:46 for H, F being ZF-formula st H is conditional holds ( ( F = the_antecedent_of H implies ex G being ZF-formula st H = F => G ) & ( ex G being ZF-formula st H = F => G implies F = the_antecedent_of H ) & ( F = the_consequent_of H implies ex G being ZF-formula st H = G => F ) & ( ex G being ZF-formula st H = G => F implies F = the_consequent_of H ) ) by Def35, Def36; theorem :: ZF_LANG:47 for H being ZF-formula st H is conditional holds H = (the_antecedent_of H) => (the_consequent_of H) proof let H be ZF-formula; ::_thesis: ( H is conditional implies H = (the_antecedent_of H) => (the_consequent_of H) ) assume A1: H is conditional ; ::_thesis: H = (the_antecedent_of H) => (the_consequent_of H) then ex F being ZF-formula st H = (the_antecedent_of H) => F by Def35; hence H = (the_antecedent_of H) => (the_consequent_of H) by A1, Def36; ::_thesis: verum end; definition let H be ZF-formula; assume A1: H is biconditional ; func the_left_side_of H -> ZF-formula means :Def37: :: ZF_LANG:def 37 ex H1 being ZF-formula st H = it <=> H1; existence ex b1, H1 being ZF-formula st H = b1 <=> H1 by A1, Def22; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = b1 <=> H1 & ex H1 being ZF-formula st H = b2 <=> H1 holds b1 = b2 by Th33; func the_right_side_of H -> ZF-formula means :Def38: :: ZF_LANG:def 38 ex H1 being ZF-formula st H = H1 <=> it; existence ex b1, H1 being ZF-formula st H = H1 <=> b1 proof consider F, G being ZF-formula such that A2: H = F <=> G by A1, Def22; take G ; ::_thesis: ex H1 being ZF-formula st H = H1 <=> G take F ; ::_thesis: H = F <=> G thus H = F <=> G by A2; ::_thesis: verum end; uniqueness for b1, b2 being ZF-formula st ex H1 being ZF-formula st H = H1 <=> b1 & ex H1 being ZF-formula st H = H1 <=> b2 holds b1 = b2 by Th33; end; :: deftheorem Def37 defines the_left_side_of ZF_LANG:def_37_:_ for H being ZF-formula st H is biconditional holds for b2 being ZF-formula holds ( b2 = the_left_side_of H iff ex H1 being ZF-formula st H = b2 <=> H1 ); :: deftheorem Def38 defines the_right_side_of ZF_LANG:def_38_:_ for H being ZF-formula st H is biconditional holds for b2 being ZF-formula holds ( b2 = the_right_side_of H iff ex H1 being ZF-formula st H = H1 <=> b2 ); theorem :: ZF_LANG:48 for H, F being ZF-formula st H is biconditional holds ( ( F = the_left_side_of H implies ex G being ZF-formula st H = F <=> G ) & ( ex G being ZF-formula st H = F <=> G implies F = the_left_side_of H ) & ( F = the_right_side_of H implies ex G being ZF-formula st H = G <=> F ) & ( ex G being ZF-formula st H = G <=> F implies F = the_right_side_of H ) ) by Def37, Def38; theorem :: ZF_LANG:49 for H being ZF-formula st H is biconditional holds H = (the_left_side_of H) <=> (the_right_side_of H) proof let H be ZF-formula; ::_thesis: ( H is biconditional implies H = (the_left_side_of H) <=> (the_right_side_of H) ) assume A1: H is biconditional ; ::_thesis: H = (the_left_side_of H) <=> (the_right_side_of H) then ex F being ZF-formula st H = (the_left_side_of H) <=> F by Def37; hence H = (the_left_side_of H) <=> (the_right_side_of H) by A1, Def38; ::_thesis: verum end; definition let H, F be ZF-formula; predH is_immediate_constituent_of F means :Def39: :: ZF_LANG:def 39 ( F = 'not' H or ex H1 being ZF-formula st ( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ); end; :: deftheorem Def39 defines is_immediate_constituent_of ZF_LANG:def_39_:_ for H, F being ZF-formula holds ( H is_immediate_constituent_of F iff ( F = 'not' H or ex H1 being ZF-formula st ( F = H '&' H1 or F = H1 '&' H ) or ex x being Variable st F = All (x,H) ) ); theorem Th50: :: ZF_LANG:50 for x, y being Variable for H being ZF-formula holds not H is_immediate_constituent_of x '=' y proof let x, y be Variable; ::_thesis: for H being ZF-formula holds not H is_immediate_constituent_of x '=' y let H be ZF-formula; ::_thesis: not H is_immediate_constituent_of x '=' y assume H is_immediate_constituent_of x '=' y ; ::_thesis: contradiction then A1: ( x '=' y = 'not' H or ex H1 being ZF-formula st ( x '=' y = H '&' H1 or x '=' y = H1 '&' H ) or ex z being Variable st x '=' y = All (z,H) ) by Def39; (x '=' y) . 1 = 0 by Th15; hence contradiction by A1, Th16, Th17, FINSEQ_1:41; ::_thesis: verum end; theorem Th51: :: ZF_LANG:51 for x, y being Variable for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y proof let x, y be Variable; ::_thesis: for H being ZF-formula holds not H is_immediate_constituent_of x 'in' y let H be ZF-formula; ::_thesis: not H is_immediate_constituent_of x 'in' y assume H is_immediate_constituent_of x 'in' y ; ::_thesis: contradiction then A1: ( x 'in' y = 'not' H or ex H1 being ZF-formula st ( x 'in' y = H '&' H1 or x 'in' y = H1 '&' H ) or ex z being Variable st x 'in' y = All (z,H) ) by Def39; (x 'in' y) . 1 = 1 by Th15; hence contradiction by A1, Th16, Th17, FINSEQ_1:41; ::_thesis: verum end; theorem Th52: :: ZF_LANG:52 for F, H being ZF-formula holds ( F is_immediate_constituent_of 'not' H iff F = H ) proof let F, H be ZF-formula; ::_thesis: ( F is_immediate_constituent_of 'not' H iff F = H ) thus ( F is_immediate_constituent_of 'not' H implies F = H ) ::_thesis: ( F = H implies F is_immediate_constituent_of 'not' H ) proof A1: now__::_thesis:_for_x_being_Variable_holds_not_'not'_H_=_All_(x,F) given x being Variable such that A2: 'not' H = All (x,F) ; ::_thesis: contradiction ('not' H) . 1 = 2 by FINSEQ_1:41; hence contradiction by A2, Th17; ::_thesis: verum end; A3: now__::_thesis:_for_H1_being_ZF-formula_holds_ (_not_'not'_H_=_F_'&'_H1_&_not_'not'_H_=_H1_'&'_F_) given H1 being ZF-formula such that A4: ( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) ; ::_thesis: contradiction ('not' H) . 1 = 2 by FINSEQ_1:41; hence contradiction by A4, Th16; ::_thesis: verum end; assume F is_immediate_constituent_of 'not' H ; ::_thesis: F = H then ( 'not' H = 'not' F or ex H1 being ZF-formula st ( 'not' H = F '&' H1 or 'not' H = H1 '&' F ) or ex x being Variable st 'not' H = All (x,F) ) by Def39; hence F = H by A3, A1, FINSEQ_1:33; ::_thesis: verum end; thus ( F = H implies F is_immediate_constituent_of 'not' H ) by Def39; ::_thesis: verum end; theorem Th53: :: ZF_LANG:53 for F, G, H being ZF-formula holds ( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) ) proof let F, G, H be ZF-formula; ::_thesis: ( F is_immediate_constituent_of G '&' H iff ( F = G or F = H ) ) thus ( not F is_immediate_constituent_of G '&' H or F = G or F = H ) ::_thesis: ( ( F = G or F = H ) implies F is_immediate_constituent_of G '&' H ) proof A1: now__::_thesis:_for_x_being_Variable_holds_not_G_'&'_H_=_All_(x,F) given x being Variable such that A2: G '&' H = All (x,F) ; ::_thesis: contradiction (G '&' H) . 1 = 3 by Th16; hence contradiction by A2, Th17; ::_thesis: verum end; A3: now__::_thesis:_not_G_'&'_H_=_'not'_F assume A4: G '&' H = 'not' F ; ::_thesis: contradiction (G '&' H) . 1 = 3 by Th16; hence contradiction by A4, FINSEQ_1:41; ::_thesis: verum end; assume F is_immediate_constituent_of G '&' H ; ::_thesis: ( F = G or F = H ) then ex H1 being ZF-formula st ( G '&' H = F '&' H1 or G '&' H = H1 '&' F ) by A3, A1, Def39; hence ( F = G or F = H ) by Th30; ::_thesis: verum end; assume ( F = G or F = H ) ; ::_thesis: F is_immediate_constituent_of G '&' H hence F is_immediate_constituent_of G '&' H by Def39; ::_thesis: verum end; theorem Th54: :: ZF_LANG:54 for x being Variable for F, H being ZF-formula holds ( F is_immediate_constituent_of All (x,H) iff F = H ) proof let x be Variable; ::_thesis: for F, H being ZF-formula holds ( F is_immediate_constituent_of All (x,H) iff F = H ) let F, H be ZF-formula; ::_thesis: ( F is_immediate_constituent_of All (x,H) iff F = H ) thus ( F is_immediate_constituent_of All (x,H) implies F = H ) ::_thesis: ( F = H implies F is_immediate_constituent_of All (x,H) ) proof A1: now__::_thesis:_for_G_being_ZF-formula_holds_ (_not_All_(x,H)_=_F_'&'_G_&_not_All_(x,H)_=_G_'&'_F_) given G being ZF-formula such that A2: ( All (x,H) = F '&' G or All (x,H) = G '&' F ) ; ::_thesis: contradiction ( (F '&' G) . 1 = 3 & (G '&' F) . 1 = 3 ) by Th16; hence contradiction by A2, Th17; ::_thesis: verum end; A3: now__::_thesis:_not_All_(x,H)_=_'not'_F assume A4: All (x,H) = 'not' F ; ::_thesis: contradiction (All (x,H)) . 1 = 4 by Th17; hence contradiction by A4, FINSEQ_1:41; ::_thesis: verum end; assume F is_immediate_constituent_of All (x,H) ; ::_thesis: F = H then ex y being Variable st All (x,H) = All (y,F) by A3, A1, Def39; hence F = H by Th3; ::_thesis: verum end; thus ( F = H implies F is_immediate_constituent_of All (x,H) ) by Def39; ::_thesis: verum end; theorem :: ZF_LANG:55 for H, F being ZF-formula st H is atomic holds not F is_immediate_constituent_of H proof let H, F be ZF-formula; ::_thesis: ( H is atomic implies not F is_immediate_constituent_of H ) A1: now__::_thesis:_(_H_is_being_equality_&_H_is_atomic_implies_not_F_is_immediate_constituent_of_H_) assume H is being_equality ; ::_thesis: ( H is atomic implies not F is_immediate_constituent_of H ) then H = (Var1 H) '=' (Var2 H) by Th36; hence ( H is atomic implies not F is_immediate_constituent_of H ) by Th50; ::_thesis: verum end; A2: now__::_thesis:_(_H_is_being_membership_&_H_is_atomic_implies_not_F_is_immediate_constituent_of_H_) assume H is being_membership ; ::_thesis: ( H is atomic implies not F is_immediate_constituent_of H ) then H = (Var1 H) 'in' (Var2 H) by Th37; hence ( H is atomic implies not F is_immediate_constituent_of H ) by Th51; ::_thesis: verum end; assume H is atomic ; ::_thesis: not F is_immediate_constituent_of H hence not F is_immediate_constituent_of H by A1, A2, Def15; ::_thesis: verum end; theorem Th56: :: ZF_LANG:56 for H, F being ZF-formula st H is negative holds ( F is_immediate_constituent_of H iff F = the_argument_of H ) proof let H, F be ZF-formula; ::_thesis: ( H is negative implies ( F is_immediate_constituent_of H iff F = the_argument_of H ) ) assume H is negative ; ::_thesis: ( F is_immediate_constituent_of H iff F = the_argument_of H ) then H = 'not' (the_argument_of H) by Def30; hence ( F is_immediate_constituent_of H iff F = the_argument_of H ) by Th52; ::_thesis: verum end; theorem Th57: :: ZF_LANG:57 for H, F being ZF-formula st H is conjunctive holds ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) proof let H, F be ZF-formula; ::_thesis: ( H is conjunctive implies ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) ) assume H is conjunctive ; ::_thesis: ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th40; hence ( F is_immediate_constituent_of H iff ( F = the_left_argument_of H or F = the_right_argument_of H ) ) by Th53; ::_thesis: verum end; theorem Th58: :: ZF_LANG:58 for H, F being ZF-formula st H is universal holds ( F is_immediate_constituent_of H iff F = the_scope_of H ) proof let H, F be ZF-formula; ::_thesis: ( H is universal implies ( F is_immediate_constituent_of H iff F = the_scope_of H ) ) assume H is universal ; ::_thesis: ( F is_immediate_constituent_of H iff F = the_scope_of H ) then H = All ((bound_in H),(the_scope_of H)) by Th44; hence ( F is_immediate_constituent_of H iff F = the_scope_of H ) by Th54; ::_thesis: verum end; definition let H, F be ZF-formula; predH is_subformula_of F means :Def40: :: ZF_LANG:def 40 ex n being Element of NAT ex L being FinSequence st ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ); end; :: deftheorem Def40 defines is_subformula_of ZF_LANG:def_40_:_ for H, F being ZF-formula holds ( H is_subformula_of F iff ex n being Element of NAT ex L being FinSequence st ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) ); theorem Th59: :: ZF_LANG:59 for H being ZF-formula holds H is_subformula_of H proof let H be ZF-formula; ::_thesis: H is_subformula_of H take 1 ; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st ( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) take <*H*> ; ::_thesis: ( 1 <= 1 & len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds ex H1, F1 being ZF-formula st ( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus 1 <= 1 ; ::_thesis: ( len <*H*> = 1 & <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds ex H1, F1 being ZF-formula st ( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus len <*H*> = 1 by FINSEQ_1:40; ::_thesis: ( <*H*> . 1 = H & <*H*> . 1 = H & ( for k being Element of NAT st 1 <= k & k < 1 holds ex H1, F1 being ZF-formula st ( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus ( <*H*> . 1 = H & <*H*> . 1 = H ) by FINSEQ_1:def_8; ::_thesis: for k being Element of NAT st 1 <= k & k < 1 holds ex H1, F1 being ZF-formula st ( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) thus for k being Element of NAT st 1 <= k & k < 1 holds ex H1, F1 being ZF-formula st ( <*H*> . k = H1 & <*H*> . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; ::_thesis: verum end; definition let H, F be ZF-formula; predH is_proper_subformula_of F means :Def41: :: ZF_LANG:def 41 ( H is_subformula_of F & H <> F ); end; :: deftheorem Def41 defines is_proper_subformula_of ZF_LANG:def_41_:_ for H, F being ZF-formula holds ( H is_proper_subformula_of F iff ( H is_subformula_of F & H <> F ) ); theorem Th60: :: ZF_LANG:60 for H, F being ZF-formula st H is_immediate_constituent_of F holds len H < len F proof let H, F be ZF-formula; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F ) A1: now__::_thesis:_(_F_=_'not'_H_&_H_is_immediate_constituent_of_F_implies_len_H_<_len_F_) assume F = 'not' H ; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F ) then len F = (len <*2*>) + (len H) by FINSEQ_1:22 .= (len H) + 1 by FINSEQ_1:40 ; hence ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; ::_thesis: verum end; A2: now__::_thesis:_(_ex_H1_being_ZF-formula_st_ (_F_=_H_'&'_H1_or_F_=_H1_'&'_H_)_&_H_is_immediate_constituent_of_F_implies_len_H_<_len_F_) given H1 being ZF-formula such that A3: ( F = H '&' H1 or F = H1 '&' H ) ; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F ) A4: len ((<*3*> ^ H1) ^ H) = len (<*3*> ^ (H1 ^ H)) by FINSEQ_1:32 .= (len <*3*>) + (len (H1 ^ H)) by FINSEQ_1:22 .= 1 + (len (H1 ^ H)) by FINSEQ_1:40 .= 1 + ((len H) + (len H1)) by FINSEQ_1:22 .= (1 + (len H)) + (len H1) ; len ((<*3*> ^ H) ^ H1) = (len (<*3*> ^ H)) + (len H1) by FINSEQ_1:22 .= ((len <*3*>) + (len H)) + (len H1) by FINSEQ_1:22 .= (1 + (len H)) + (len H1) by FINSEQ_1:40 ; then 1 + (len H) <= len F by A3, A4, NAT_1:11; hence ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; ::_thesis: verum end; A5: now__::_thesis:_(_ex_x_being_Variable_st_F_=_All_(x,H)_&_H_is_immediate_constituent_of_F_implies_len_H_<_len_F_) given x being Variable such that A6: F = All (x,H) ; ::_thesis: ( H is_immediate_constituent_of F implies len H < len F ) len F = (len (<*4*> ^ <*x*>)) + (len H) by A6, FINSEQ_1:22 .= ((len <*4*>) + (len <*x*>)) + (len H) by FINSEQ_1:22 .= (1 + (len <*x*>)) + (len H) by FINSEQ_1:40 .= (1 + 1) + (len H) by FINSEQ_1:40 .= (1 + (len H)) + 1 ; then 1 + (len H) <= len F by NAT_1:11; hence ( H is_immediate_constituent_of F implies len H < len F ) by NAT_1:13; ::_thesis: verum end; assume H is_immediate_constituent_of F ; ::_thesis: len H < len F hence len H < len F by A1, A2, A5, Def39; ::_thesis: verum end; theorem Th61: :: ZF_LANG:61 for H, F being ZF-formula st H is_immediate_constituent_of F holds H is_proper_subformula_of F proof let H, F be ZF-formula; ::_thesis: ( H is_immediate_constituent_of F implies H is_proper_subformula_of F ) assume A1: H is_immediate_constituent_of F ; ::_thesis: H is_proper_subformula_of F thus H is_subformula_of F :: according to ZF_LANG:def_41 ::_thesis: H <> F proof take n = 2; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) take L = <*H,F*>; ::_thesis: ( 1 <= n & len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus 1 <= n ; ::_thesis: ( len L = n & L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus len L = n by FINSEQ_1:44; ::_thesis: ( L . 1 = H & L . n = F & ( for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus ( L . 1 = H & L . n = F ) by FINSEQ_1:44; ::_thesis: for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) let k be Element of NAT ; ::_thesis: ( 1 <= k & k < n implies ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) assume that A2: 1 <= k and A3: k < n ; ::_thesis: ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) take H ; ::_thesis: ex F1 being ZF-formula st ( L . k = H & L . (k + 1) = F1 & H is_immediate_constituent_of F1 ) take F ; ::_thesis: ( L . k = H & L . (k + 1) = F & H is_immediate_constituent_of F ) k < 1 + 1 by A3; then k <= 1 by NAT_1:13; then k = 1 by A2, XXREAL_0:1; hence ( L . k = H & L . (k + 1) = F ) by FINSEQ_1:44; ::_thesis: H is_immediate_constituent_of F thus H is_immediate_constituent_of F by A1; ::_thesis: verum end; assume H = F ; ::_thesis: contradiction then len H = len F ; hence contradiction by A1, Th60; ::_thesis: verum end; theorem Th62: :: ZF_LANG:62 for H, F being ZF-formula st H is_proper_subformula_of F holds len H < len F proof let H, F be ZF-formula; ::_thesis: ( H is_proper_subformula_of F implies len H < len F ) assume H is_subformula_of F ; :: according to ZF_LANG:def_41 ::_thesis: ( not H <> F or len H < len F ) then consider n being Element of NAT , L being FinSequence such that A1: 1 <= n and len L = n and A2: L . 1 = H and A3: L . n = F and A4: for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by Def40; defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 < n implies for H1 being ZF-formula st L . ($1 + 1) = H1 holds len H < len H1 ); A5: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume that A6: ( 1 <= k & k < n implies for H1 being ZF-formula st L . (k + 1) = H1 holds len H < len H1 ) and A7: 1 <= k + 1 and A8: k + 1 < n ; ::_thesis: for H1 being ZF-formula st L . ((k + 1) + 1) = H1 holds len H < len H1 consider F1, G being ZF-formula such that A9: L . (k + 1) = F1 and A10: ( L . ((k + 1) + 1) = G & F1 is_immediate_constituent_of G ) by A4, A7, A8; let H1 be ZF-formula; ::_thesis: ( L . ((k + 1) + 1) = H1 implies len H < len H1 ) assume A11: L . ((k + 1) + 1) = H1 ; ::_thesis: len H < len H1 A12: now__::_thesis:_(_ex_m_being_Nat_st_k_=_m_+_1_implies_len_H_<_len_H1_) given m being Nat such that A13: k = m + 1 ; ::_thesis: len H < len H1 len H < len F1 by A6, A8, A9, A13, NAT_1:11, NAT_1:13; hence len H < len H1 by A11, A10, Th60, XXREAL_0:2; ::_thesis: verum end; ( k = 0 implies len H < len H1 ) by A2, A11, A9, A10, Th60; hence len H < len H1 by A12, NAT_1:6; ::_thesis: verum end; assume H <> F ; ::_thesis: len H < len F then 1 < n by A1, A2, A3, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then consider k being Nat such that A14: n = 2 + k by NAT_1:10; A15: S1[ 0 ] ; A16: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A5); reconsider k = k as Element of NAT by ORDINAL1:def_12; A17: (1 + 1) + k = (1 + k) + 1 ; then 1 + k < n by A14, NAT_1:13; hence len H < len F by A3, A16, A14, A17, NAT_1:11; ::_thesis: verum end; theorem Th63: :: ZF_LANG:63 for H, F being ZF-formula st H is_proper_subformula_of F holds ex G being ZF-formula st G is_immediate_constituent_of F proof let H, F be ZF-formula; ::_thesis: ( H is_proper_subformula_of F implies ex G being ZF-formula st G is_immediate_constituent_of F ) assume H is_subformula_of F ; :: according to ZF_LANG:def_41 ::_thesis: ( not H <> F or ex G being ZF-formula st G is_immediate_constituent_of F ) then consider n being Element of NAT , L being FinSequence such that A1: 1 <= n and len L = n and A2: L . 1 = H and A3: L . n = F and A4: for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by Def40; assume H <> F ; ::_thesis: ex G being ZF-formula st G is_immediate_constituent_of F then 1 < n by A1, A2, A3, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then consider k being Nat such that A5: n = 2 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; (1 + 1) + k = (1 + k) + 1 ; then 1 + k < n by A5, NAT_1:13; then consider H1, F1 being ZF-formula such that L . (1 + k) = H1 and A6: ( L . ((1 + k) + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A4, NAT_1:11; take H1 ; ::_thesis: H1 is_immediate_constituent_of F thus H1 is_immediate_constituent_of F by A3, A5, A6; ::_thesis: verum end; theorem Th64: :: ZF_LANG:64 for F, G, H being ZF-formula st F is_proper_subformula_of G & G is_proper_subformula_of H holds F is_proper_subformula_of H proof let F, G, H be ZF-formula; ::_thesis: ( F is_proper_subformula_of G & G is_proper_subformula_of H implies F is_proper_subformula_of H ) assume that A1: F is_subformula_of G and A2: F <> G and A3: G is_subformula_of H and A4: G <> H ; :: according to ZF_LANG:def_41 ::_thesis: F is_proper_subformula_of H consider m being Element of NAT , L9 being FinSequence such that A5: 1 <= m and A6: len L9 = m and A7: L9 . 1 = G and A8: L9 . m = H and A9: for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L9 . k = H1 & L9 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A3, Def40; consider n being Element of NAT , L being FinSequence such that A10: 1 <= n and A11: len L = n and A12: L . 1 = F and A13: L . n = G and A14: for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40; 1 < n by A2, A10, A12, A13, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then consider k being Nat such that A15: n = 2 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15; thus F is_subformula_of H :: according to ZF_LANG:def_41 ::_thesis: F <> H proof take l = (1 + k) + m; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st ( 1 <= l & len L = l & L . 1 = F & L . l = H & ( for k being Element of NAT st 1 <= k & k < l holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) take K = L1 ^ L9; ::_thesis: ( 1 <= l & len K = l & K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds ex H1, F1 being ZF-formula st ( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) A16: ((1 + k) + m) - (1 + k) = m ; m <= m + (1 + k) by NAT_1:11; hence 1 <= l by A5, XXREAL_0:2; ::_thesis: ( len K = l & K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds ex H1, F1 being ZF-formula st ( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) (1 + 1) + k = (1 + k) + 1 ; then A17: 1 + k <= n by A15, NAT_1:11; then A18: len L1 = 1 + k by A11, FINSEQ_1:17; hence A19: len K = l by A6, FINSEQ_1:22; ::_thesis: ( K . 1 = F & K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds ex H1, F1 being ZF-formula st ( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) A20: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_1_+_k_holds_ K_._j_=_L_._j let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= 1 + k implies K . j = L . j ) assume ( 1 <= j & j <= 1 + k ) ; ::_thesis: K . j = L . j then A21: j in Seg (1 + k) by FINSEQ_1:1; then j in dom L1 by A11, A17, FINSEQ_1:17; then K . j = L1 . j by FINSEQ_1:def_7; hence K . j = L . j by A21, FUNCT_1:49; ::_thesis: verum end; 1 <= 1 + k by NAT_1:11; hence K . 1 = F by A12, A20; ::_thesis: ( K . l = H & ( for k being Element of NAT st 1 <= k & k < l holds ex H1, F1 being ZF-formula st ( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) (len L1) + 1 <= (len L1) + m by A5, XREAL_1:7; then len L1 < l by A18, NAT_1:13; then K . l = L9 . (l - (len L1)) by A19, FINSEQ_1:24; hence K . l = H by A11, A8, A17, A16, FINSEQ_1:17; ::_thesis: for k being Element of NAT st 1 <= k & k < l holds ex H1, F1 being ZF-formula st ( K . k = H1 & K . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) let j be Element of NAT ; ::_thesis: ( 1 <= j & j < l implies ex H1, F1 being ZF-formula st ( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) assume that A22: 1 <= j and A23: j < l ; ::_thesis: ex H1, F1 being ZF-formula st ( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) j + 0 <= j + 1 by XREAL_1:7; then A24: 1 <= j + 1 by A22, XXREAL_0:2; A25: now__::_thesis:_(_j_<_1_+_k_implies_ex_F1,_G1_being_ZF-formula_st_ (_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_) assume A26: j < 1 + k ; ::_thesis: ex F1, G1 being ZF-formula st ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) then A27: j + 1 <= 1 + k by NAT_1:13; then j + 1 <= n by A17, XXREAL_0:2; then j < n by NAT_1:13; then consider F1, G1 being ZF-formula such that A28: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A14, A22; take F1 = F1; ::_thesis: ex G1 being ZF-formula st ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) thus ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A20, A22, A24, A26, A27, A28; ::_thesis: verum end; A29: now__::_thesis:_(_1_+_k_<_j_implies_ex_F1,_G1_being_ZF-formula_st_ (_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_) A30: j + 1 <= l by A23, NAT_1:13; assume A31: 1 + k < j ; ::_thesis: ex F1, G1 being ZF-formula st ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) then A32: 1 + k < j + 1 by NAT_1:13; (1 + k) + 1 <= j by A31, NAT_1:13; then consider j1 being Nat such that A33: j = ((1 + k) + 1) + j1 by NAT_1:10; reconsider j1 = j1 as Element of NAT by ORDINAL1:def_12; j - (1 + k) < l - (1 + k) by A23, XREAL_1:9; then consider F1, G1 being ZF-formula such that A34: ( L9 . (1 + j1) = F1 & L9 . ((1 + j1) + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A9, A33, NAT_1:11; take F1 = F1; ::_thesis: ex G1 being ZF-formula st ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) A35: ((1 + j1) + (1 + k)) - (1 + k) = ((1 + j1) + (1 + k)) + (- (1 + k)) ; (j + 1) - (len L1) = 1 + (j + (- (len L1))) .= (1 + j1) + 1 by A11, A17, A33, A35, FINSEQ_1:17 ; hence ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A18, A19, A23, A31, A32, A30, A35, A34, FINSEQ_1:24; ::_thesis: verum end; now__::_thesis:_(_j_=_1_+_k_implies_ex_F1,_G1_being_ZF-formula_st_ (_K_._j_=_F1_&_K_._(j_+_1)_=_G1_&_F1_is_immediate_constituent_of_G1_)_) A36: ( j + 1 <= l & (j + 1) - j = (j + 1) + (- j) ) by A23, NAT_1:13; assume A37: j = 1 + k ; ::_thesis: ex F1, G1 being ZF-formula st ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) then j < (1 + k) + 1 by NAT_1:13; then consider F1, G1 being ZF-formula such that A38: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A14, A15, A22; take F1 = F1; ::_thesis: ex G1 being ZF-formula st ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) take G1 = G1; ::_thesis: ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) 1 + k < j + 1 by A37, NAT_1:13; hence ( K . j = F1 & K . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A13, A7, A15, A18, A19, A20, A22, A37, A36, A38, FINSEQ_1:24; ::_thesis: verum end; hence ex H1, F1 being ZF-formula st ( K . j = H1 & K . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A25, A29, XXREAL_0:1; ::_thesis: verum end; assume A39: F = H ; ::_thesis: contradiction F is_proper_subformula_of G by A1, A2, Def41; then A40: len F < len G by Th62; G is_proper_subformula_of H by A3, A4, Def41; hence contradiction by A39, A40, Th62; ::_thesis: verum end; theorem Th65: :: ZF_LANG:65 for F, G, H being ZF-formula st F is_subformula_of G & G is_subformula_of H holds F is_subformula_of H proof let F, G, H be ZF-formula; ::_thesis: ( F is_subformula_of G & G is_subformula_of H implies F is_subformula_of H ) assume that A1: F is_subformula_of G and A2: G is_subformula_of H ; ::_thesis: F is_subformula_of H now__::_thesis:_(_F_<>_G_implies_F_is_subformula_of_H_) assume F <> G ; ::_thesis: F is_subformula_of H then A3: F is_proper_subformula_of G by A1, Def41; now__::_thesis:_(_G_<>_H_implies_F_is_subformula_of_H_) assume G <> H ; ::_thesis: F is_subformula_of H then G is_proper_subformula_of H by A2, Def41; then F is_proper_subformula_of H by A3, Th64; hence F is_subformula_of H by Def41; ::_thesis: verum end; hence F is_subformula_of H by A1; ::_thesis: verum end; hence F is_subformula_of H by A2; ::_thesis: verum end; theorem :: ZF_LANG:66 for G, H being ZF-formula st G is_subformula_of H & H is_subformula_of G holds G = H proof let G, H be ZF-formula; ::_thesis: ( G is_subformula_of H & H is_subformula_of G implies G = H ) assume that A1: G is_subformula_of H and A2: H is_subformula_of G ; ::_thesis: G = H assume A3: G <> H ; ::_thesis: contradiction then G is_proper_subformula_of H by A1, Def41; then A4: len G < len H by Th62; H is_proper_subformula_of G by A2, A3, Def41; hence contradiction by A4, Th62; ::_thesis: verum end; theorem Th67: :: ZF_LANG:67 for x, y being Variable for F being ZF-formula holds not F is_proper_subformula_of x '=' y proof let x, y be Variable; ::_thesis: for F being ZF-formula holds not F is_proper_subformula_of x '=' y let F be ZF-formula; ::_thesis: not F is_proper_subformula_of x '=' y assume F is_proper_subformula_of x '=' y ; ::_thesis: contradiction then ex G being ZF-formula st G is_immediate_constituent_of x '=' y by Th63; hence contradiction by Th50; ::_thesis: verum end; theorem Th68: :: ZF_LANG:68 for x, y being Variable for F being ZF-formula holds not F is_proper_subformula_of x 'in' y proof let x, y be Variable; ::_thesis: for F being ZF-formula holds not F is_proper_subformula_of x 'in' y let F be ZF-formula; ::_thesis: not F is_proper_subformula_of x 'in' y assume F is_proper_subformula_of x 'in' y ; ::_thesis: contradiction then ex G being ZF-formula st G is_immediate_constituent_of x 'in' y by Th63; hence contradiction by Th51; ::_thesis: verum end; theorem Th69: :: ZF_LANG:69 for F, H being ZF-formula st F is_proper_subformula_of 'not' H holds F is_subformula_of H proof let F, H be ZF-formula; ::_thesis: ( F is_proper_subformula_of 'not' H implies F is_subformula_of H ) assume that A1: F is_subformula_of 'not' H and A2: F <> 'not' H ; :: according to ZF_LANG:def_41 ::_thesis: F is_subformula_of H consider n being Element of NAT , L being FinSequence such that A3: 1 <= n and A4: len L = n and A5: L . 1 = F and A6: L . n = 'not' H and A7: for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40; 1 < n by A2, A3, A5, A6, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then consider k being Nat such that A8: n = 2 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15; take m = 1 + k; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st ( 1 <= m & len L = m & L . 1 = F & L . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus A9: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) 1 + k <= (1 + k) + 1 by NAT_1:11; hence len L1 = m by A4, A8, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) A10: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_ L1_._j_=_L_._j let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j ) assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j then j in { j1 where j1 is Element of NAT : ( 1 <= j1 & j1 <= 1 + k ) } ; then j in Seg (1 + k) by FINSEQ_1:def_1; hence L1 . j = L . j by FUNCT_1:49; ::_thesis: verum end; hence L1 . 1 = F by A5, A9; ::_thesis: ( L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) m < m + 1 by NAT_1:13; then consider F1, G1 being ZF-formula such that A11: L . m = F1 and A12: ( L . (m + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A8, NAT_1:11; F1 = H by A6, A8, A12, Th52; hence L1 . m = H by A9, A10, A11; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex H1, F1 being ZF-formula st ( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) assume that A13: 1 <= j and A14: j < m ; ::_thesis: ex H1, F1 being ZF-formula st ( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) m <= m + 1 by NAT_1:11; then j < n by A8, A14, XXREAL_0:2; then consider F1, G1 being ZF-formula such that A15: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A13; take F1 ; ::_thesis: ex F1 being ZF-formula st ( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 ) take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) ( 1 <= 1 + j & j + 1 <= m ) by A13, A14, NAT_1:13; hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A10, A13, A14, A15; ::_thesis: verum end; theorem Th70: :: ZF_LANG:70 for F, G, H being ZF-formula holds ( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H ) proof let F, G, H be ZF-formula; ::_thesis: ( not F is_proper_subformula_of G '&' H or F is_subformula_of G or F is_subformula_of H ) assume that A1: F is_subformula_of G '&' H and A2: F <> G '&' H ; :: according to ZF_LANG:def_41 ::_thesis: ( F is_subformula_of G or F is_subformula_of H ) consider n being Element of NAT , L being FinSequence such that A3: 1 <= n and A4: len L = n and A5: L . 1 = F and A6: L . n = G '&' H and A7: for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40; 1 < n by A2, A3, A5, A6, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then consider k being Nat such that A8: n = 2 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; (1 + 1) + k = (1 + k) + 1 ; then 1 + k < n by A8, NAT_1:13; then consider H1, G1 being ZF-formula such that A9: L . (1 + k) = H1 and A10: ( L . ((1 + k) + 1) = G1 & H1 is_immediate_constituent_of G1 ) by A7, NAT_1:11; reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15; F is_subformula_of H1 proof take m = 1 + k; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st ( 1 <= m & len L = m & L . 1 = F & L . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus A11: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) 1 + k <= (1 + k) + 1 by NAT_1:11; hence len L1 = m by A4, A8, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) A12: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_ L1_._j_=_L_._j let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j ) assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j then j in { j1 where j1 is Element of NAT : ( 1 <= j1 & j1 <= 1 + k ) } ; then j in Seg (1 + k) by FINSEQ_1:def_1; hence L1 . j = L . j by FUNCT_1:49; ::_thesis: verum end; hence L1 . 1 = F by A5, A11; ::_thesis: ( L1 . m = H1 & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus L1 . m = H1 by A9, A11, A12; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex H1, F1 being ZF-formula st ( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) assume that A13: 1 <= j and A14: j < m ; ::_thesis: ex H1, F1 being ZF-formula st ( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) m <= m + 1 by NAT_1:11; then j < n by A8, A14, XXREAL_0:2; then consider F1, G1 being ZF-formula such that A15: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A13; take F1 ; ::_thesis: ex F1 being ZF-formula st ( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 ) take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) ( 1 <= 1 + j & j + 1 <= m ) by A13, A14, NAT_1:13; hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A12, A13, A14, A15; ::_thesis: verum end; hence ( F is_subformula_of G or F is_subformula_of H ) by A6, A8, A10, Th53; ::_thesis: verum end; theorem Th71: :: ZF_LANG:71 for x being Variable for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds F is_subformula_of H proof let x be Variable; ::_thesis: for F, H being ZF-formula st F is_proper_subformula_of All (x,H) holds F is_subformula_of H let F, H be ZF-formula; ::_thesis: ( F is_proper_subformula_of All (x,H) implies F is_subformula_of H ) assume that A1: F is_subformula_of All (x,H) and A2: F <> All (x,H) ; :: according to ZF_LANG:def_41 ::_thesis: F is_subformula_of H consider n being Element of NAT , L being FinSequence such that A3: 1 <= n and A4: len L = n and A5: L . 1 = F and A6: L . n = All (x,H) and A7: for k being Element of NAT st 1 <= k & k < n holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) by A1, Def40; 1 < n by A2, A3, A5, A6, XXREAL_0:1; then 1 + 1 <= n by NAT_1:13; then consider k being Nat such that A8: n = 2 + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:15; take m = 1 + k; :: according to ZF_LANG:def_40 ::_thesis: ex L being FinSequence st ( 1 <= m & len L = m & L . 1 = F & L . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) take L1 ; ::_thesis: ( 1 <= m & len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) thus A9: 1 <= m by NAT_1:11; ::_thesis: ( len L1 = m & L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) 1 + k <= (1 + k) + 1 by NAT_1:11; hence len L1 = m by A4, A8, FINSEQ_1:17; ::_thesis: ( L1 . 1 = F & L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) A10: now__::_thesis:_for_j_being_Element_of_NAT_st_1_<=_j_&_j_<=_m_holds_ L1_._j_=_L_._j let j be Element of NAT ; ::_thesis: ( 1 <= j & j <= m implies L1 . j = L . j ) assume ( 1 <= j & j <= m ) ; ::_thesis: L1 . j = L . j then j in { j1 where j1 is Element of NAT : ( 1 <= j1 & j1 <= 1 + k ) } ; then j in Seg (1 + k) by FINSEQ_1:def_1; hence L1 . j = L . j by FUNCT_1:49; ::_thesis: verum end; hence L1 . 1 = F by A5, A9; ::_thesis: ( L1 . m = H & ( for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) ) m < m + 1 by NAT_1:13; then consider F1, G1 being ZF-formula such that A11: L . m = F1 and A12: ( L . (m + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A8, NAT_1:11; F1 = H by A6, A8, A12, Th54; hence L1 . m = H by A9, A10, A11; ::_thesis: for k being Element of NAT st 1 <= k & k < m holds ex H1, F1 being ZF-formula st ( L1 . k = H1 & L1 . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) let j be Element of NAT ; ::_thesis: ( 1 <= j & j < m implies ex H1, F1 being ZF-formula st ( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) ) assume that A13: 1 <= j and A14: j < m ; ::_thesis: ex H1, F1 being ZF-formula st ( L1 . j = H1 & L1 . (j + 1) = F1 & H1 is_immediate_constituent_of F1 ) m <= m + 1 by NAT_1:11; then j < n by A8, A14, XXREAL_0:2; then consider F1, G1 being ZF-formula such that A15: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A7, A13; take F1 ; ::_thesis: ex F1 being ZF-formula st ( L1 . j = F1 & L1 . (j + 1) = F1 & F1 is_immediate_constituent_of F1 ) take G1 ; ::_thesis: ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) ( 1 <= 1 + j & j + 1 <= m ) by A13, A14, NAT_1:13; hence ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A10, A13, A14, A15; ::_thesis: verum end; theorem :: ZF_LANG:72 for H, F being ZF-formula st H is atomic holds not F is_proper_subformula_of H proof let H, F be ZF-formula; ::_thesis: ( H is atomic implies not F is_proper_subformula_of H ) assume H is atomic ; ::_thesis: not F is_proper_subformula_of H then ( H is being_equality or H is being_membership ) by Def15; then ( H = (Var1 H) '=' (Var2 H) or H = (Var1 H) 'in' (Var2 H) ) by Th36, Th37; hence not F is_proper_subformula_of H by Th67, Th68; ::_thesis: verum end; theorem :: ZF_LANG:73 for H being ZF-formula st H is negative holds the_argument_of H is_proper_subformula_of H proof let H be ZF-formula; ::_thesis: ( H is negative implies the_argument_of H is_proper_subformula_of H ) assume H is negative ; ::_thesis: the_argument_of H is_proper_subformula_of H then the_argument_of H is_immediate_constituent_of H by Th56; hence the_argument_of H is_proper_subformula_of H by Th61; ::_thesis: verum end; theorem :: ZF_LANG:74 for H being ZF-formula st H is conjunctive holds ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) proof let H be ZF-formula; ::_thesis: ( H is conjunctive implies ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) ) assume H is conjunctive ; ::_thesis: ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) then ( the_left_argument_of H is_immediate_constituent_of H & the_right_argument_of H is_immediate_constituent_of H ) by Th57; hence ( the_left_argument_of H is_proper_subformula_of H & the_right_argument_of H is_proper_subformula_of H ) by Th61; ::_thesis: verum end; theorem :: ZF_LANG:75 for H being ZF-formula st H is universal holds the_scope_of H is_proper_subformula_of H proof let H be ZF-formula; ::_thesis: ( H is universal implies the_scope_of H is_proper_subformula_of H ) assume H is universal ; ::_thesis: the_scope_of H is_proper_subformula_of H then the_scope_of H is_immediate_constituent_of H by Th58; hence the_scope_of H is_proper_subformula_of H by Th61; ::_thesis: verum end; theorem Th76: :: ZF_LANG:76 for x, y being Variable for H being ZF-formula holds ( H is_subformula_of x '=' y iff H = x '=' y ) proof let x, y be Variable; ::_thesis: for H being ZF-formula holds ( H is_subformula_of x '=' y iff H = x '=' y ) let H be ZF-formula; ::_thesis: ( H is_subformula_of x '=' y iff H = x '=' y ) thus ( H is_subformula_of x '=' y implies H = x '=' y ) ::_thesis: ( H = x '=' y implies H is_subformula_of x '=' y ) proof assume A1: H is_subformula_of x '=' y ; ::_thesis: H = x '=' y assume H <> x '=' y ; ::_thesis: contradiction then H is_proper_subformula_of x '=' y by A1, Def41; then ex F being ZF-formula st F is_immediate_constituent_of x '=' y by Th63; hence contradiction by Th50; ::_thesis: verum end; thus ( H = x '=' y implies H is_subformula_of x '=' y ) by Th59; ::_thesis: verum end; theorem Th77: :: ZF_LANG:77 for x, y being Variable for H being ZF-formula holds ( H is_subformula_of x 'in' y iff H = x 'in' y ) proof let x, y be Variable; ::_thesis: for H being ZF-formula holds ( H is_subformula_of x 'in' y iff H = x 'in' y ) let H be ZF-formula; ::_thesis: ( H is_subformula_of x 'in' y iff H = x 'in' y ) thus ( H is_subformula_of x 'in' y implies H = x 'in' y ) ::_thesis: ( H = x 'in' y implies H is_subformula_of x 'in' y ) proof assume A1: H is_subformula_of x 'in' y ; ::_thesis: H = x 'in' y assume H <> x 'in' y ; ::_thesis: contradiction then H is_proper_subformula_of x 'in' y by A1, Def41; then ex F being ZF-formula st F is_immediate_constituent_of x 'in' y by Th63; hence contradiction by Th51; ::_thesis: verum end; assume H = x 'in' y ; ::_thesis: H is_subformula_of x 'in' y hence H is_subformula_of x 'in' y by Th59; ::_thesis: verum end; definition let H be ZF-formula; func Subformulae H -> set means :Def42: :: ZF_LANG:def 42 for a being set holds ( a in it iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ); existence ex b1 being set st for a being set holds ( a in b1 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) proof defpred S1[ set ] means ex F being ZF-formula st ( F = $1 & F is_subformula_of H ); consider X being set such that A1: for a being set holds ( a in X iff ( a in NAT * & S1[a] ) ) from XBOOLE_0:sch_1(); take X ; ::_thesis: for a being set holds ( a in X iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) let a be set ; ::_thesis: ( a in X iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) thus ( a in X implies ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) by A1; ::_thesis: ( ex F being ZF-formula st ( F = a & F is_subformula_of H ) implies a in X ) given F being ZF-formula such that A2: ( F = a & F is_subformula_of H ) ; ::_thesis: a in X F in NAT * by FINSEQ_1:def_11; hence a in X by A1, A2; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for a being set holds ( a in b1 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ) & ( for a being set holds ( a in b2 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ) holds b1 = b2 proof let X, Y be set ; ::_thesis: ( ( for a being set holds ( a in X iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ) & ( for a being set holds ( a in Y iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ) implies X = Y ) assume that A3: for a being set holds ( a in X iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) and A4: for a being set holds ( a in Y iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ; ::_thesis: X = Y now__::_thesis:_for_a_being_set_holds_ (_(_a_in_X_implies_a_in_Y_)_&_(_a_in_Y_implies_a_in_X_)_) let a be set ; ::_thesis: ( ( a in X implies a in Y ) & ( a in Y implies a in X ) ) thus ( a in X implies a in Y ) ::_thesis: ( a in Y implies a in X ) proof assume a in X ; ::_thesis: a in Y then ex F being ZF-formula st ( F = a & F is_subformula_of H ) by A3; hence a in Y by A4; ::_thesis: verum end; assume a in Y ; ::_thesis: a in X then ex F being ZF-formula st ( F = a & F is_subformula_of H ) by A4; hence a in X by A3; ::_thesis: verum end; hence X = Y by TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def42 defines Subformulae ZF_LANG:def_42_:_ for H being ZF-formula for b2 being set holds ( b2 = Subformulae H iff for a being set holds ( a in b2 iff ex F being ZF-formula st ( F = a & F is_subformula_of H ) ) ); theorem Th78: :: ZF_LANG:78 for G, H being ZF-formula st G in Subformulae H holds G is_subformula_of H proof let G, H be ZF-formula; ::_thesis: ( G in Subformulae H implies G is_subformula_of H ) assume G in Subformulae H ; ::_thesis: G is_subformula_of H then ex F being ZF-formula st ( F = G & F is_subformula_of H ) by Def42; hence G is_subformula_of H ; ::_thesis: verum end; theorem :: ZF_LANG:79 for F, H being ZF-formula st F is_subformula_of H holds Subformulae F c= Subformulae H proof let F, H be ZF-formula; ::_thesis: ( F is_subformula_of H implies Subformulae F c= Subformulae H ) assume A1: F is_subformula_of H ; ::_thesis: Subformulae F c= Subformulae H let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in Subformulae F or a in Subformulae H ) assume a in Subformulae F ; ::_thesis: a in Subformulae H then consider F1 being ZF-formula such that A2: F1 = a and A3: F1 is_subformula_of F by Def42; F1 is_subformula_of H by A1, A3, Th65; hence a in Subformulae H by A2, Def42; ::_thesis: verum end; theorem Th80: :: ZF_LANG:80 for x, y being Variable holds Subformulae (x '=' y) = {(x '=' y)} proof let x, y be Variable; ::_thesis: Subformulae (x '=' y) = {(x '=' y)} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_Subformulae_(x_'='_y)_implies_a_in_{(x_'='_y)}_)_&_(_a_in_{(x_'='_y)}_implies_a_in_Subformulae_(x_'='_y)_)_) let a be set ; ::_thesis: ( ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) & ( a in {(x '=' y)} implies a in Subformulae (x '=' y) ) ) thus ( a in Subformulae (x '=' y) implies a in {(x '=' y)} ) ::_thesis: ( a in {(x '=' y)} implies a in Subformulae (x '=' y) ) proof assume a in Subformulae (x '=' y) ; ::_thesis: a in {(x '=' y)} then consider F being ZF-formula such that A1: F = a and A2: F is_subformula_of x '=' y by Def42; F = x '=' y by A2, Th76; hence a in {(x '=' y)} by A1, TARSKI:def_1; ::_thesis: verum end; assume a in {(x '=' y)} ; ::_thesis: a in Subformulae (x '=' y) then A3: a = x '=' y by TARSKI:def_1; x '=' y is_subformula_of x '=' y by Th59; hence a in Subformulae (x '=' y) by A3, Def42; ::_thesis: verum end; hence Subformulae (x '=' y) = {(x '=' y)} by TARSKI:1; ::_thesis: verum end; theorem Th81: :: ZF_LANG:81 for x, y being Variable holds Subformulae (x 'in' y) = {(x 'in' y)} proof let x, y be Variable; ::_thesis: Subformulae (x 'in' y) = {(x 'in' y)} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_Subformulae_(x_'in'_y)_implies_a_in_{(x_'in'_y)}_)_&_(_a_in_{(x_'in'_y)}_implies_a_in_Subformulae_(x_'in'_y)_)_) let a be set ; ::_thesis: ( ( a in Subformulae (x 'in' y) implies a in {(x 'in' y)} ) & ( a in {(x 'in' y)} implies a in Subformulae (x 'in' y) ) ) thus ( a in Subformulae (x 'in' y) implies a in {(x 'in' y)} ) ::_thesis: ( a in {(x 'in' y)} implies a in Subformulae (x 'in' y) ) proof assume a in Subformulae (x 'in' y) ; ::_thesis: a in {(x 'in' y)} then consider F being ZF-formula such that A1: F = a and A2: F is_subformula_of x 'in' y by Def42; F = x 'in' y by A2, Th77; hence a in {(x 'in' y)} by A1, TARSKI:def_1; ::_thesis: verum end; assume a in {(x 'in' y)} ; ::_thesis: a in Subformulae (x 'in' y) then A3: a = x 'in' y by TARSKI:def_1; x 'in' y is_subformula_of x 'in' y by Th59; hence a in Subformulae (x 'in' y) by A3, Def42; ::_thesis: verum end; hence Subformulae (x 'in' y) = {(x 'in' y)} by TARSKI:1; ::_thesis: verum end; theorem Th82: :: ZF_LANG:82 for H being ZF-formula holds Subformulae ('not' H) = (Subformulae H) \/ {('not' H)} proof let H be ZF-formula; ::_thesis: Subformulae ('not' H) = (Subformulae H) \/ {('not' H)} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_Subformulae_('not'_H)_implies_a_in_(Subformulae_H)_\/_{('not'_H)}_)_&_(_a_in_(Subformulae_H)_\/_{('not'_H)}_implies_a_in_Subformulae_('not'_H)_)_) let a be set ; ::_thesis: ( ( a in Subformulae ('not' H) implies a in (Subformulae H) \/ {('not' H)} ) & ( a in (Subformulae H) \/ {('not' H)} implies a in Subformulae ('not' H) ) ) A1: now__::_thesis:_(_a_in_{('not'_H)}_implies_a_in_Subformulae_('not'_H)_) assume a in {('not' H)} ; ::_thesis: a in Subformulae ('not' H) then A2: a = 'not' H by TARSKI:def_1; 'not' H is_subformula_of 'not' H by Th59; hence a in Subformulae ('not' H) by A2, Def42; ::_thesis: verum end; thus ( a in Subformulae ('not' H) implies a in (Subformulae H) \/ {('not' H)} ) ::_thesis: ( a in (Subformulae H) \/ {('not' H)} implies a in Subformulae ('not' H) ) proof assume a in Subformulae ('not' H) ; ::_thesis: a in (Subformulae H) \/ {('not' H)} then consider F being ZF-formula such that A3: F = a and A4: F is_subformula_of 'not' H by Def42; now__::_thesis:_(_F_<>_'not'_H_implies_a_in_Subformulae_H_) assume F <> 'not' H ; ::_thesis: a in Subformulae H then F is_proper_subformula_of 'not' H by A4, Def41; then F is_subformula_of H by Th69; hence a in Subformulae H by A3, Def42; ::_thesis: verum end; then ( a in Subformulae H or a in {('not' H)} ) by A3, TARSKI:def_1; hence a in (Subformulae H) \/ {('not' H)} by XBOOLE_0:def_3; ::_thesis: verum end; A5: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_('not'_H)_) assume a in Subformulae H ; ::_thesis: a in Subformulae ('not' H) then consider F being ZF-formula such that A6: F = a and A7: F is_subformula_of H by Def42; H is_immediate_constituent_of 'not' H by Th52; then H is_proper_subformula_of 'not' H by Th61; then H is_subformula_of 'not' H by Def41; then F is_subformula_of 'not' H by A7, Th65; hence a in Subformulae ('not' H) by A6, Def42; ::_thesis: verum end; assume a in (Subformulae H) \/ {('not' H)} ; ::_thesis: a in Subformulae ('not' H) hence a in Subformulae ('not' H) by A5, A1, XBOOLE_0:def_3; ::_thesis: verum end; hence Subformulae ('not' H) = (Subformulae H) \/ {('not' H)} by TARSKI:1; ::_thesis: verum end; theorem Th83: :: ZF_LANG:83 for H, F being ZF-formula holds Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} proof let H, F be ZF-formula; ::_thesis: Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_Subformulae_(H_'&'_F)_implies_a_in_((Subformulae_H)_\/_(Subformulae_F))_\/_{(H_'&'_F)}_)_&_(_a_in_((Subformulae_H)_\/_(Subformulae_F))_\/_{(H_'&'_F)}_implies_a_in_Subformulae_(H_'&'_F)_)_) let a be set ; ::_thesis: ( ( a in Subformulae (H '&' F) implies a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ) & ( a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} implies a in Subformulae (H '&' F) ) ) A1: ( not a in (Subformulae H) \/ (Subformulae F) or a in Subformulae H or a in Subformulae F ) by XBOOLE_0:def_3; thus ( a in Subformulae (H '&' F) implies a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ) ::_thesis: ( a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} implies a in Subformulae (H '&' F) ) proof assume a in Subformulae (H '&' F) ; ::_thesis: a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} then consider G being ZF-formula such that A2: G = a and A3: G is_subformula_of H '&' F by Def42; now__::_thesis:_(_G_<>_H_'&'_F_implies_a_in_(Subformulae_H)_\/_(Subformulae_F)_) assume G <> H '&' F ; ::_thesis: a in (Subformulae H) \/ (Subformulae F) then G is_proper_subformula_of H '&' F by A3, Def41; then ( G is_subformula_of H or G is_subformula_of F ) by Th70; then ( a in Subformulae H or a in Subformulae F ) by A2, Def42; hence a in (Subformulae H) \/ (Subformulae F) by XBOOLE_0:def_3; ::_thesis: verum end; then ( a in (Subformulae H) \/ (Subformulae F) or a in {(H '&' F)} ) by A2, TARSKI:def_1; hence a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by XBOOLE_0:def_3; ::_thesis: verum end; A4: now__::_thesis:_(_a_in_{(H_'&'_F)}_implies_a_in_Subformulae_(H_'&'_F)_) assume a in {(H '&' F)} ; ::_thesis: a in Subformulae (H '&' F) then A5: a = H '&' F by TARSKI:def_1; H '&' F is_subformula_of H '&' F by Th59; hence a in Subformulae (H '&' F) by A5, Def42; ::_thesis: verum end; A6: now__::_thesis:_(_a_in_Subformulae_F_implies_a_in_Subformulae_(H_'&'_F)_) assume a in Subformulae F ; ::_thesis: a in Subformulae (H '&' F) then consider G being ZF-formula such that A7: G = a and A8: G is_subformula_of F by Def42; F is_immediate_constituent_of H '&' F by Th53; then F is_proper_subformula_of H '&' F by Th61; then F is_subformula_of H '&' F by Def41; then G is_subformula_of H '&' F by A8, Th65; hence a in Subformulae (H '&' F) by A7, Def42; ::_thesis: verum end; A9: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_(H_'&'_F)_) assume a in Subformulae H ; ::_thesis: a in Subformulae (H '&' F) then consider G being ZF-formula such that A10: G = a and A11: G is_subformula_of H by Def42; H is_immediate_constituent_of H '&' F by Th53; then H is_proper_subformula_of H '&' F by Th61; then H is_subformula_of H '&' F by Def41; then G is_subformula_of H '&' F by A11, Th65; hence a in Subformulae (H '&' F) by A10, Def42; ::_thesis: verum end; assume a in ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} ; ::_thesis: a in Subformulae (H '&' F) hence a in Subformulae (H '&' F) by A1, A9, A6, A4, XBOOLE_0:def_3; ::_thesis: verum end; hence Subformulae (H '&' F) = ((Subformulae H) \/ (Subformulae F)) \/ {(H '&' F)} by TARSKI:1; ::_thesis: verum end; theorem Th84: :: ZF_LANG:84 for x being Variable for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))} proof let x be Variable; ::_thesis: for H being ZF-formula holds Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))} let H be ZF-formula; ::_thesis: Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))} now__::_thesis:_for_a_being_set_holds_ (_(_a_in_Subformulae_(All_(x,H))_implies_a_in_(Subformulae_H)_\/_{(All_(x,H))}_)_&_(_a_in_(Subformulae_H)_\/_{(All_(x,H))}_implies_a_in_Subformulae_(All_(x,H))_)_) let a be set ; ::_thesis: ( ( a in Subformulae (All (x,H)) implies a in (Subformulae H) \/ {(All (x,H))} ) & ( a in (Subformulae H) \/ {(All (x,H))} implies a in Subformulae (All (x,H)) ) ) A1: now__::_thesis:_(_a_in_{(All_(x,H))}_implies_a_in_Subformulae_(All_(x,H))_) assume a in {(All (x,H))} ; ::_thesis: a in Subformulae (All (x,H)) then A2: a = All (x,H) by TARSKI:def_1; All (x,H) is_subformula_of All (x,H) by Th59; hence a in Subformulae (All (x,H)) by A2, Def42; ::_thesis: verum end; thus ( a in Subformulae (All (x,H)) implies a in (Subformulae H) \/ {(All (x,H))} ) ::_thesis: ( a in (Subformulae H) \/ {(All (x,H))} implies a in Subformulae (All (x,H)) ) proof assume a in Subformulae (All (x,H)) ; ::_thesis: a in (Subformulae H) \/ {(All (x,H))} then consider F being ZF-formula such that A3: F = a and A4: F is_subformula_of All (x,H) by Def42; now__::_thesis:_(_F_<>_All_(x,H)_implies_a_in_Subformulae_H_) assume F <> All (x,H) ; ::_thesis: a in Subformulae H then F is_proper_subformula_of All (x,H) by A4, Def41; then F is_subformula_of H by Th71; hence a in Subformulae H by A3, Def42; ::_thesis: verum end; then ( a in Subformulae H or a in {(All (x,H))} ) by A3, TARSKI:def_1; hence a in (Subformulae H) \/ {(All (x,H))} by XBOOLE_0:def_3; ::_thesis: verum end; A5: now__::_thesis:_(_a_in_Subformulae_H_implies_a_in_Subformulae_(All_(x,H))_) assume a in Subformulae H ; ::_thesis: a in Subformulae (All (x,H)) then consider F being ZF-formula such that A6: F = a and A7: F is_subformula_of H by Def42; H is_immediate_constituent_of All (x,H) by Th54; then H is_proper_subformula_of All (x,H) by Th61; then H is_subformula_of All (x,H) by Def41; then F is_subformula_of All (x,H) by A7, Th65; hence a in Subformulae (All (x,H)) by A6, Def42; ::_thesis: verum end; assume a in (Subformulae H) \/ {(All (x,H))} ; ::_thesis: a in Subformulae (All (x,H)) hence a in Subformulae (All (x,H)) by A5, A1, XBOOLE_0:def_3; ::_thesis: verum end; hence Subformulae (All (x,H)) = (Subformulae H) \/ {(All (x,H))} by TARSKI:1; ::_thesis: verum end; theorem :: ZF_LANG:85 for H being ZF-formula holds ( H is atomic iff Subformulae H = {H} ) proof let H be ZF-formula; ::_thesis: ( H is atomic iff Subformulae H = {H} ) thus ( H is atomic implies Subformulae H = {H} ) ::_thesis: ( Subformulae H = {H} implies H is atomic ) proof assume H is atomic ; ::_thesis: Subformulae H = {H} then ( H is being_equality or H is being_membership ) by Def15; then ( H = (Var1 H) '=' (Var2 H) or H = (Var1 H) 'in' (Var2 H) ) by Th36, Th37; hence Subformulae H = {H} by Th80, Th81; ::_thesis: verum end; assume A1: Subformulae H = {H} ; ::_thesis: H is atomic A2: now__::_thesis:_not_H_=_'not'_(the_argument_of_H) assume H = 'not' (the_argument_of H) ; ::_thesis: contradiction then A3: the_argument_of H is_immediate_constituent_of H by Th52; then the_argument_of H is_proper_subformula_of H by Th61; then the_argument_of H is_subformula_of H by Def41; then A4: the_argument_of H in Subformulae H by Def42; len (the_argument_of H) <> len H by A3, Th60; hence contradiction by A1, A4, TARSKI:def_1; ::_thesis: verum end; A5: now__::_thesis:_not_H_=_(the_left_argument_of_H)_'&'_(the_right_argument_of_H) assume H = (the_left_argument_of H) '&' (the_right_argument_of H) ; ::_thesis: contradiction then A6: the_left_argument_of H is_immediate_constituent_of H by Th53; then the_left_argument_of H is_proper_subformula_of H by Th61; then the_left_argument_of H is_subformula_of H by Def41; then A7: the_left_argument_of H in Subformulae H by Def42; len (the_left_argument_of H) <> len H by A6, Th60; hence contradiction by A1, A7, TARSKI:def_1; ::_thesis: verum end; assume not H is atomic ; ::_thesis: contradiction then ( H is negative or H is conjunctive or H is universal ) by Th10; then ( H = 'not' (the_argument_of H) or H = (the_left_argument_of H) '&' (the_right_argument_of H) or H = All ((bound_in H),(the_scope_of H)) ) by Def30, Th40, Th44; then A8: the_scope_of H is_immediate_constituent_of H by A2, A5, Th54; then the_scope_of H is_proper_subformula_of H by Th61; then the_scope_of H is_subformula_of H by Def41; then A9: the_scope_of H in Subformulae H by Def42; len (the_scope_of H) <> len H by A8, Th60; hence contradiction by A1, A9, TARSKI:def_1; ::_thesis: verum end; theorem :: ZF_LANG:86 for H being ZF-formula st H is negative holds Subformulae H = (Subformulae (the_argument_of H)) \/ {H} proof let H be ZF-formula; ::_thesis: ( H is negative implies Subformulae H = (Subformulae (the_argument_of H)) \/ {H} ) assume H is negative ; ::_thesis: Subformulae H = (Subformulae (the_argument_of H)) \/ {H} then H = 'not' (the_argument_of H) by Def30; hence Subformulae H = (Subformulae (the_argument_of H)) \/ {H} by Th82; ::_thesis: verum end; theorem :: ZF_LANG:87 for H being ZF-formula st H is conjunctive holds Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} proof let H be ZF-formula; ::_thesis: ( H is conjunctive implies Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} ) assume H is conjunctive ; ::_thesis: Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th40; hence Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by Th83; ::_thesis: verum end; theorem :: ZF_LANG:88 for H being ZF-formula st H is universal holds Subformulae H = (Subformulae (the_scope_of H)) \/ {H} proof let H be ZF-formula; ::_thesis: ( H is universal implies Subformulae H = (Subformulae (the_scope_of H)) \/ {H} ) assume H is universal ; ::_thesis: Subformulae H = (Subformulae (the_scope_of H)) \/ {H} then H = All ((bound_in H),(the_scope_of H)) by Th44; hence Subformulae H = (Subformulae (the_scope_of H)) \/ {H} by Th84; ::_thesis: verum end; theorem :: ZF_LANG:89 for H, G, F being ZF-formula st ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F holds H in Subformulae F proof let H, G, F be ZF-formula; ::_thesis: ( ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) & G in Subformulae F implies H in Subformulae F ) assume that A1: ( H is_immediate_constituent_of G or H is_proper_subformula_of G or H is_subformula_of G ) and A2: G in Subformulae F ; ::_thesis: H in Subformulae F ( H is_proper_subformula_of G or H is_subformula_of G ) by A1, Th61; then A3: H is_subformula_of G by Def41; G is_subformula_of F by A2, Th78; then H is_subformula_of F by A3, Th65; hence H in Subformulae F by Def42; ::_thesis: verum end; scheme :: ZF_LANG:sch 1 ZFInd{ P1[ ZF-formula] } : for H being ZF-formula holds P1[H] provided A1: for H being ZF-formula st H is atomic holds P1[H] and A2: for H being ZF-formula st H is negative & P1[ the_argument_of H] holds P1[H] and A3: for H being ZF-formula st H is conjunctive & P1[ the_left_argument_of H] & P1[ the_right_argument_of H] holds P1[H] and A4: for H being ZF-formula st H is universal & P1[ the_scope_of H] holds P1[H] proof defpred S1[ Nat] means for H being ZF-formula st len H = $1 holds P1[H]; A5: for n being Nat st ( for k being Nat st k < n holds S1[k] ) holds S1[n] proof let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds S1[k] ) implies S1[n] ) assume A6: for k being Nat st k < n holds for H being ZF-formula st len H = k holds P1[H] ; ::_thesis: S1[n] let H be ZF-formula; ::_thesis: ( len H = n implies P1[H] ) assume A7: len H = n ; ::_thesis: P1[H] A8: now__::_thesis:_(_H_is_conjunctive_implies_P1[H]_) assume A9: H is conjunctive ; ::_thesis: P1[H] then A10: H = (the_left_argument_of H) '&' (the_right_argument_of H) by Th40; then the_right_argument_of H is_immediate_constituent_of H by Th53; then len (the_right_argument_of H) < len H by Th60; then A11: P1[ the_right_argument_of H] by A6, A7; the_left_argument_of H is_immediate_constituent_of H by A10, Th53; then len (the_left_argument_of H) < len H by Th60; then P1[ the_left_argument_of H] by A6, A7; hence P1[H] by A3, A9, A11; ::_thesis: verum end; A12: now__::_thesis:_(_H_is_universal_implies_P1[H]_) assume A13: H is universal ; ::_thesis: P1[H] then H = All ((bound_in H),(the_scope_of H)) by Th44; then the_scope_of H is_immediate_constituent_of H by Th54; then len (the_scope_of H) < len H by Th60; hence P1[H] by A4, A6, A7, A13; ::_thesis: verum end; now__::_thesis:_(_H_is_negative_implies_P1[H]_) assume A14: H is negative ; ::_thesis: P1[H] then H = 'not' (the_argument_of H) by Def30; then the_argument_of H is_immediate_constituent_of H by Th52; then len (the_argument_of H) < len H by Th60; hence P1[H] by A2, A6, A7, A14; ::_thesis: verum end; hence P1[H] by A1, A8, A12, Th10; ::_thesis: verum end; A15: for n being Nat holds S1[n] from NAT_1:sch_4(A5); let H be ZF-formula; ::_thesis: P1[H] len H = len H ; hence P1[H] by A15; ::_thesis: verum end; scheme :: ZF_LANG:sch 2 ZFCompInd{ P1[ ZF-formula] } : for H being ZF-formula holds P1[H] provided A1: for H being ZF-formula st ( for F being ZF-formula st F is_proper_subformula_of H holds P1[F] ) holds P1[H] proof defpred S1[ Nat] means for H being ZF-formula st len H = $1 holds P1[H]; A2: for n being Nat st ( for k being Nat st k < n holds S1[k] ) holds S1[n] proof let n be Nat; ::_thesis: ( ( for k being Nat st k < n holds S1[k] ) implies S1[n] ) assume A3: for k being Nat st k < n holds for H being ZF-formula st len H = k holds P1[H] ; ::_thesis: S1[n] let H be ZF-formula; ::_thesis: ( len H = n implies P1[H] ) assume A4: len H = n ; ::_thesis: P1[H] now__::_thesis:_for_F_being_ZF-formula_st_F_is_proper_subformula_of_H_holds_ P1[F] let F be ZF-formula; ::_thesis: ( F is_proper_subformula_of H implies P1[F] ) assume F is_proper_subformula_of H ; ::_thesis: P1[F] then len F < len H by Th62; hence P1[F] by A3, A4; ::_thesis: verum end; hence P1[H] by A1; ::_thesis: verum end; A5: for n being Nat holds S1[n] from NAT_1:sch_4(A2); let H be ZF-formula; ::_thesis: P1[H] len H = len H ; hence P1[H] by A5; ::_thesis: verum end;