let m be Nat; for X being set
for S being Language
for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let X be set ; for S being Language
for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let S be Language; for D being RuleSet of S st X c= S -sequents holds
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
let D be RuleSet of S; ( X c= S -sequents implies ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X}) )
set O = OneStep D;
set RH = union (((OneStep D) [*]) .: {X});
set Q = S -sequents ;
assume
X c= S -sequents
; ((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
then A1:
X in dom (iter ((OneStep D),m))
by Lm1;
reconsider f = union {(iter ((OneStep D),m))} as Function ;
A2: (iter ((OneStep D),m)) . X =
union {((iter ((OneStep D),m)) . X)}
.=
union (Im ((iter ((OneStep D),m)),X))
by FUNCT_1:59, A1
.=
union (f .: {X})
;
reconsider mm = m as Element of NAT by ORDINAL1:def 12;
iter ((OneStep D),mm) = iter ((OneStep D),m)
;
then
iter ((OneStep D),m) in D -iterators
;
then
union {(iter ((OneStep D),m))} c= union (D -iterators)
by ZFMISC_1:31, ZFMISC_1:77;
then
f .: {X} c= (union (D -iterators)) .: {X}
by RELAT_1:124;
then A3:
((m,D) -derivables) . X c= union ((union (D -iterators)) .: {X})
by A2, ZFMISC_1:77;
rng (OneStep D) c= dom (OneStep D)
by Lm1;
hence
((m,D) -derivables) . X c= union (((OneStep D) [*]) .: {X})
by A3, FOMODEL0:17; verum