let V be Universe; :: thesis: for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H being ZF-formula st Diagram H,E in X holds
Diagram ('not' H),E in X
let X be Subclass of V; :: thesis: for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H being ZF-formula st Diagram H,E in X holds
Diagram ('not' H),E in X
let E be non empty set ; :: thesis: ( X is closed_wrt_A1-A7 & E in X implies for H being ZF-formula st Diagram H,E in X holds
Diagram ('not' H),E in X )
assume A1: ( X is closed_wrt_A1-A7 & E in X ) ; :: thesis: for H being ZF-formula st Diagram H,E in X holds
Diagram ('not' H),E in X
let H be ZF-formula; :: thesis: ( Diagram H,E in X implies Diagram ('not' H),E in X )
assume A2: Diagram H,E in X ; :: thesis: Diagram ('not' H),E in X
set fs = code (Free H);
reconsider m = E as Element of V by A1;
A3: Funcs (code (Free H)),m in X by A1, Th9;
Diagram ('not' H),E = (Funcs (code (Free H)),E) \ (Diagram H,E)

proof

A4: code (Free H) = code (Free ('not' H)) by ZF_LANG1:65;

now

let p be set ; :: thesis: ( p in Diagram ('not' H),E iff ( p in Funcs (code (Free H)),E & not p in Diagram H,E ) )

A5: now

assume p in Diagram ('not' H),E ; :: thesis: ( p in Funcs (code (Free H)),E & not p in Diagram H,E )
then consider f being Function of VAR ,E such that
A6: ( p = (f * decode ) | (code (Free H)) & f in St ('not' H),E ) by A4, Def5;
thus p in Funcs (code (Free H)),E by A6, Lm3; :: thesis: not p in Diagram H,E
thus not p in Diagram H,E :: thesis: verum

proof

assume p in Diagram H,E ; :: thesis: contradiction
then ex g being Function of VAR ,E st
( p = (g * decode ) | (code (Free H)) & g in St H,E ) by Def5;
then f in St H,E by A6, Lm10;
hence contradiction by A6, ZF_MODEL:4; :: thesis: verum

end;

end;

now

assume A7: ( p in Funcs (code (Free H)),E & not p in Diagram H,E ) ; :: thesis: p in Diagram ('not' H),E
then consider e being Function such that
A8: ( p = e & dom e = code (Free H) & rng e c= E ) by FUNCT_2:def 2;
consider f being Function of VAR ,E such that
A9: e = (f * decode ) | (code (Free H)) by A7, A8, Lm11;
A10: Free ('not' H) = Free H by ZF_LANG1:65;
not f in St H,E by A7, A8, A9, Def5;
then f in St ('not' H),E by ZF_MODEL:4;
hence p in Diagram ('not' H),E by A8, A9, A10, Def5; :: thesis: verum

end;

hence ( p in Diagram ('not' H),E iff ( p in Funcs (code (Free H)),E & not p in Diagram H,E ) ) by A5; :: thesis: verum

end;

hence Diagram ('not' H),E = (Funcs (code (Free H)),E) \ (Diagram H,E) by XBOOLE_0:def 5; :: thesis: verum

end;

hence Diagram ('not' H),E in X by A1, A2, A3, Th4; :: thesis: verum