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 that
A1: X is closed_wrt_A1-A7 and
A2: E in X ; :: thesis: for H being ZF-formula st Diagram H,E in X holds
Diagram ('not' H),E in X
reconsider m = E as Element of V by A2;
let H be ZF-formula; :: thesis: ( Diagram H,E in X implies Diagram ('not' H),E in X )
assume A3: Diagram H,E in X ; :: thesis: Diagram ('not' H),E in X
set fs = code (Free H);
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)) and
A7: 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 A7, ZF_MODEL:4; :: thesis: verum

end;

end;

now

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

then A12: Diagram ('not' H),E = (Funcs (code (Free H)),E) \ (Diagram H,E) by XBOOLE_0:def 5;
Funcs (code (Free H)),m in X by A1, A2, Th9;
hence Diagram ('not' H),E in X by A1, A3, A12, Th4; :: thesis: verum