let S be Language; :: thesis: for D being RuleSet of S
for Seqts being Subset of (S -sequents)
for y being object st {y} is Seqts,D -derivable holds
ex mm being Element of NAT st y is mm,Seqts,D -derivable
let D be RuleSet of S; :: thesis: for Seqts being Subset of (S -sequents)
for y being object st {y} is Seqts,D -derivable holds
ex mm being Element of NAT st y is mm,Seqts,D -derivable
let Seqts be Subset of (S -sequents); :: thesis: for y being object st {y} is Seqts,D -derivable holds
ex mm being Element of NAT st y is mm,Seqts,D -derivable
let y be object ; :: thesis: ( {y} is Seqts,D -derivable implies ex mm being Element of NAT st y is mm,Seqts,D -derivable )
set X = Seqts;
set Q = S -sequents ;
set O = OneStep D;
set I = D -iterators ;
assume {y} is Seqts,D -derivable ; :: thesis: ex mm being Element of NAT st y is mm,Seqts,D -derivable
then y in union (((OneStep D) [*]) .: {Seqts}) by ZFMISC_1:31;
then consider Y being set such that
A1: ( y in Y & Y in ((OneStep D) [*]) .: {Seqts} ) by TARSKI:def 4;
rng (OneStep D) c= dom (OneStep D) by Lm1;
then (OneStep D) [*] = union (D -iterators) by FOMODEL0:17;
then ((OneStep D) [*]) .: {Seqts} = union { (R .: {Seqts}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D -iterators } by RELSET_2:34;
then consider Z being set such that
A2: ( Y in Z & Z in { (R .: {Seqts}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D -iterators } ) by A1, TARSKI:def 4;
consider f being Subset of [:(bool (S -sequents)),(bool (S -sequents)):] such that
A3: ( Z = f .: {Seqts} & f in D -iterators ) by A2;
consider mm being Element of NAT such that
A4: f = iter ((OneStep D),mm) by A3;
take mm ; :: thesis: y is mm,Seqts,D -derivable
iter ((OneStep D),mm) is Function of (bool (S -sequents)),(bool (S -sequents)) by FUNCT_7:83;
then A5: dom (iter ((OneStep D),mm)) = bool (S -sequents) by FUNCT_2:def 1;
( y in Y & Y in Im ((iter ((OneStep D),mm)),Seqts) ) by A1, A2, A4, A3;
then ( y in Y & Y in {((iter ((OneStep D),mm)) . Seqts)} ) by A5, FUNCT_1:59;
then y in ((mm,D) -derivables) . Seqts by TARSKI:def 1;
hence y is mm,Seqts,D -derivable ; :: thesis: verum