let y be set ; :: thesis: for S being Language
for D being RuleSet of S
for Seqts being Subset of (S -sequents) st {y} is Seqts,D -derivable holds
ex mm being Element of NAT st y is mm,Seqts,D -derivable
let S be Language; :: thesis: for D being RuleSet of S
for Seqts being Subset of (S -sequents) 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) 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: ( {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} c= union (((OneStep D) [*]) .: {Seqts}) by DefDerivable;
then y in union (((OneStep D) [*]) .: {Seqts}) by ZFMISC_1:31;
then consider Y being set such that
B0: ( y in Y & Y in ((OneStep D) [*]) .: {Seqts} ) by TARSKI:def 4;
rng (OneStep D) c= dom (OneStep D) by Lm4;
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
B1: ( Y in Z & Z in { (R .: {Seqts}) where R is Subset of [:(bool (S -sequents)),(bool (S -sequents)):] : R in D -iterators } ) by B0, TARSKI:def 4;
consider f being Subset of [:(bool (S -sequents)),(bool (S -sequents)):] such that
B2: ( Z = f .: {Seqts} & f in D -iterators ) by B1;
consider mm being Element of NAT such that
B3: f = iter ((OneStep D),mm) by B2;
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 BB4: 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 B0, B1, B3, B2;
then ( y in Y & Y in {((iter ((OneStep D),mm)) . Seqts)} ) by BB4, FUNCT_1:59;
then y in ((mm,D) -derivables) . Seqts by TARSKI:def 1;
hence y is mm,Seqts,D -derivable by DefDerivable3; :: thesis: verum