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:60;
now :: thesis: for p being object holds
( p in Diagram (('not' H),E) iff ( p in Funcs ((code (Free H)),E) & not p in Diagram (H,E) ) )
let p be object ; :: thesis: ( p in Diagram (('not' H),E) iff ( p in Funcs ((code (Free H)),E) & not p in Diagram (H,E) ) )
A5: now :: thesis: ( p in Diagram (('not' H),E) implies ( p in Funcs ((code (Free H)),E) & not p in Diagram (H,E) ) )
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, Def4;
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 Def4;
then f in St (H,E) by A6, Lm10;
hence contradiction by A7, ZF_MODEL:4; :: thesis: verum
end;
end;
now :: thesis: ( p in Funcs ((code (Free H)),E) & not p in Diagram (H,E) implies p in Diagram (('not' H),E) )
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, Def4;
then ( Free ('not' H) = Free H & f in St (('not' H),E) ) by ZF_LANG1:60, ZF_MODEL:4;
hence p in Diagram (('not' H),E) by A10, A11, Def4; :: 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