let W be Universe; :: thesis: for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds
Y is predicatively_closed
let Y be Subclass of W; :: thesis: ( Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is predicatively_closed )
assume A1: ( Y is closed_wrt_A1-A7 & Y is epsilon-transitive ) ; :: thesis: Y is predicatively_closed
let H be ZF-formula; :: according to ZF_FUND2:def 2 :: thesis: for E being non empty set
for f being Function of VAR ,E st E in Y holds
Section H,f in Y
let E be non empty set ; :: thesis: for f being Function of VAR ,E st E in Y holds
Section H,f in Y
let f be Function of VAR ,E; :: thesis: ( E in Y implies Section H,f in Y )
assume A2: E in Y ; :: thesis: Section H,f in Y

now

per cases ( not x. 0 in Free H or x. 0 in Free H ) ;

suppose not x. 0 in Free H ; :: thesis: Section H,f in Y

then Section H,f = {} by Def1;
hence Section H,f in Y by A1, ZF_FUND1:3; :: thesis: verum

end;

suppose A3: x. 0 in Free H ; :: thesis: Section H,f in Y

reconsider n = {} as Element of omega by ORDINAL1:def 12;
set fs = (code (Free H)) \ {n};
reconsider a = E as Element of W by A2;
A4: Diagram H,E in Y by A1, A2, ZF_FUND1:22;
then reconsider b = Diagram H,E as Element of W ;
A5: Funcs ((code (Free H)) \ {n}),a in Y by A1, A2, ZF_FUND1:9;
A6: (f * decode ) | ((code (Free H)) \ {n}) in Funcs ((code (Free H)) \ {n}),a by ZF_FUND1:32;
then reconsider y = (f * decode ) | ((code (Free H)) \ {n}) as Element of W by A5, ZF_FUND1:1;
set A = { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ;
set B = { e where e is Element of E : {[n,e]} \/ y in b } ;
A7: { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } = { e where e is Element of E : {[n,e]} \/ y in b }

proof

thus { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } c= { e where e is Element of E : {[n,e]} \/ y in b } :: according to XBOOLE_0:def 10 :: thesis: { e where e is Element of E : {[n,e]} \/ y in b } c= { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } or u in { e where e is Element of E : {[n,e]} \/ y in b } )
assume u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ; :: thesis: u in { e where e is Element of E : {[n,e]} \/ y in b }
then ex w being Element of W st
( u = w & w in a & {[n,w]} \/ y in b ) ;
hence u in { e where e is Element of E : {[n,e]} \/ y in b } ; :: thesis: verum

end;

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { e where e is Element of E : {[n,e]} \/ y in b } or u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } )
assume u in { e where e is Element of E : {[n,e]} \/ y in b } ; :: thesis: u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }
then consider e being Element of E such that
A8: ( u = e & {[n,e]} \/ y in b ) ;
reconsider e = e as Element of W by A2, ZF_FUND1:1;
e in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A8;
hence u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } by A8; :: thesis: verum

end;

n in {n} by TARSKI:def 1;
then A9: not n in (code (Free H)) \ {n} by XBOOLE_0:def 5;
A10: a c= Y by A1, A2, ORDINAL1:def 2;
b c= Funcs (((code (Free H)) \ {n}) \/ {n}),a

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in b or u in Funcs (((code (Free H)) \ {n}) \/ {n}),a )
assume u in b ; :: thesis: u in Funcs (((code (Free H)) \ {n}) \/ {n}),a
then A11: ex f1 being Function of VAR ,E st
( u = (f1 * decode ) | (code (Free H)) & f1 in St H,E ) by ZF_FUND1:def 5;
x". (x. 0 ) in code (Free H) by A3, ZF_FUND1:34;
then n in code (Free H) by ZF_FUND1:def 3;
then A12: {n} c= code (Free H) by ZFMISC_1:37;
u in Funcs (code (Free H)),a by A11, ZF_FUND1:32;
hence u in Funcs (((code (Free H)) \ {n}) \/ {n}),a by A12, XBOOLE_1:45; :: thesis: verum

end;

then { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } in Y by A1, A2, A4, A6, A9, A10, ZF_FUND1:16;
hence Section H,f in Y by A7, Th4; :: thesis: verum

end;

end;

end;

hence Section H,f in Y ; :: thesis: verum