let W be Universe; 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; ( Y is closed_wrt_A1-A7 & Y is epsilon-transitive implies Y is predicatively_closed )
assume that
A1:
Y is closed_wrt_A1-A7
and
A2:
Y is epsilon-transitive
; Y is predicatively_closed
let H be ZF-formula; ZF_FUND2:def 2 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 ; for f being Function of VAR,E st E in Y holds
Section (H,f) in Y
let f be Function of VAR,E; ( E in Y implies Section (H,f) in Y )
assume A3:
E in Y
; Section (H,f) in Y
now Section (H,f) in Yper cases
( not x. 0 in Free H or x. 0 in Free H )
;
suppose A4:
x. 0 in Free H
;
Section (H,f) in Yreconsider a =
E as
Element of
W by A3;
reconsider n =
{} as
Element of
omega by ORDINAL1:def 11;
set fs =
(code (Free H)) \ {n};
A5:
Diagram (
H,
E)
in Y
by A1, A3, ZF_FUND1:22;
then reconsider b =
Diagram (
H,
E) as
Element of
W ;
A6:
b c= Funcs (
(((code (Free H)) \ {n}) \/ {n}),
a)
n in {n}
by TARSKI:def 1;
then A8:
not
n in (code (Free H)) \ {n}
by XBOOLE_0:def 5;
A9:
(f * decode) | ((code (Free H)) \ {n}) in Funcs (
((code (Free H)) \ {n}),
a)
by ZF_FUND1:31;
Funcs (
((code (Free H)) \ {n}),
a)
in Y
by A1, A3, ZF_FUND1:9;
then reconsider y =
(f * decode) | ((code (Free H)) \ {n}) as
Element of
W by A9, ZF_FUND1:1;
set B =
{ e where e is Element of E : {[n,e]} \/ y in b } ;
set A =
{ w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } ;
A10:
{ 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 }
XBOOLE_0:def 10 { 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 ) }
let u be
object ;
TARSKI:def 3 ( 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 }
;
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 A11:
u = e
and A12:
{[n,e]} \/ y in b
;
reconsider e =
e as
Element of
W by A3, ZF_FUND1:1;
e in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }
by A12;
hence
u in { w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) }
by A11;
verum
end;
a c= Y
by A2, A3;
then
{ w where w is Element of W : ( w in a & {[n,w]} \/ y in b ) } in Y
by A1, A3, A5, A9, A8, A6, ZF_FUND1:16;
hence
Section (
H,
f)
in Y
by A10, Th4;
verum end; end; end;
hence
Section (H,f) in Y
; verum