let V be Universe; :: thesis:
let X be Subclass of V; :: thesis:
let E be non empty set ; :: thesis:
assume that
A1: X is closed_wrt_A1-A7 and
A2: E in X ; :: thesis:
let H be ZF-formula; :: thesis:
let v1 be Element of VAR ; :: thesis:
assume A3: Diagram (H,E) in X ; :: thesis:

per cases ;

suppose A4: not v1 in Free H ; :: thesis:

then Free H = (Free H) \ {v1} by ZFMISC_1:57;
then A5: Free (All (v1,H)) = Free H by ZF_LANG1:62;
Diagram ((All (v1,H)),E) = Diagram (H,E)

proof

thus Diagram ((All (v1,H)),E) c= Diagram (H,E) :: according to XBOOLE_0:def 10 :: thesis:

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram ((All (v1,H)),E) ; :: thesis:
then consider f being Function of VAR,E such that
A6: p = (f * decode) | (code (Free (All (v1,H)))) and
A7: f in St ((All (v1,H)),E) by Def4;
f in St (H,E) by A7, ZF_MODEL:6;
hence p in Diagram (H,E) by A5, A6, Def4; :: thesis:

end;

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram (H,E) ; :: thesis:
then consider f being Function of VAR,E such that
A8: p = (f * decode) | (code (Free H)) and
A9: f in St (H,E) by Def4;
for g being Function of VAR,E st ( for v2 being Element of VAR st g . v2 <> f . v2 holds
v1 = v2 ) holds
g in St (H,E)

proof

let g be Function of VAR,E; :: thesis:
assume for v2 being Element of VAR st g . v2 <> f . v2 holds
v1 = v2 ; :: thesis:
then A10: for v2 being Element of VAR st v2 in Free H holds
f . v2 = g . v2 by A4;
E,f |= H by A9, ZF_MODEL:def 4;
then E,g |= H by A10, ZF_LANG1:75;
hence g in St (H,E) by ZF_MODEL:def 4; :: thesis:

end;

then f in St ((All (v1,H)),E) by A9, ZF_MODEL:6;
hence p in Diagram ((All (v1,H)),E) by A5, A8, Def4; :: thesis:

end;

hence Diagram ((All (v1,H)),E) in X by A3; :: thesis:

end;

suppose A11: v1 in Free H ; :: thesis:

reconsider m = E as Element of V by A2;
set n = x". v1;
set fs = code (Free H);
A12: Diagram (('not' H),E) c= Funcs ((code (Free H)),E)

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram (('not' H),E) ; :: thesis:
then A13: ex f being Function of VAR,E st
( p = (f * decode) | (code (Free ('not' H))) & f in St (('not' H),E) ) by Def4;
Free ('not' H) = Free H by ZF_LANG1:60;
hence p in Funcs ((code (Free H)),E) by A13, Lm3; :: thesis:

end;

A14: (code (Free H)) \ {(x". v1)} = (code (Free H)) \ (code {v1}) by Lm6
.= code ((Free H) \ {v1}) by Lm1, FUNCT_1:64 ;
then A15: (code (Free H)) \ {(x". v1)} = code (Free (All (v1,H))) by ZF_LANG1:62;
A16: Diagram (('not' H),E) in X by A1, A2, A3, Th19;
then reconsider Dn = Diagram (('not' H),E) as Element of V ;
set C = { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ;
A17: Funcs (((code (Free H)) \ {(x". v1)}),m) in X by A1, A2, Th9;
{v1} c= Free H by A11, ZFMISC_1:31;
then Free H = ((Free H) \ {v1}) \/ {v1} by XBOOLE_1:45;
then A18: code (Free H) = (code ((Free H) \ {v1})) \/ (code {v1}) by RELAT_1:120
.= (code ((Free H) \ {v1})) \/ {(x". v1)} by Lm6 ;
A19: (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } = Diagram ((All (v1,H)),E)

proof

thus (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } c= Diagram ((All (v1,H)),E) :: according to XBOOLE_0:def 10 :: thesis:

proof

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume A20: p in (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ; :: thesis:
then consider h being Function such that
A21: p = h and
dom h = (code (Free H)) \ {(x". v1)} and
rng h c= E by FUNCT_2:def 2;
consider f being Function of VAR,E such that
A22: h = (f * decode) | ((code (Free H)) \ {(x". v1)}) by A20, A21, Lm11;
A23: not p in { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } by A20, XBOOLE_0:def 5;
f in St ((All (v1,H)),E)

proof

assume A24: not f in St ((All (v1,H)),E) ; :: thesis:
A25: for ff being Function of VAR,E st p = (ff * decode) | (code (Free (All (v1,H)))) holds
ff in St (H,E)

proof

let ff be Function of VAR,E; :: thesis:
assume A26: p = (ff * decode) | (code (Free (All (v1,H)))) ; :: thesis:
(ff * decode) | ((code (Free H)) \ {(x". v1)}) in Funcs (((code (Free H)) \ {(x". v1)}),m) by Lm3;
then reconsider x = (ff * decode) | ((code (Free H)) \ {(x". v1)}) as Element of V by A17, Th1;
assume not ff in St (H,E) ; :: thesis:
then ff in St (('not' H),E) by ZF_MODEL:4;
then (ff * decode) | (code (Free ('not' H))) in Dn by Def4;
then (ff * decode) | (((code (Free H)) \ {(x". v1)}) \/ {(x". v1)}) in Dn by A18, A14, ZF_LANG1:60;
then A27: ((ff * decode) | ((code (Free H)) \ {(x". v1)})) \/ ((ff * decode) | {(x". v1)}) in Dn by RELAT_1:78;
dom ((ff * decode) | {(x". v1)}) = {(x". v1)} by Lm3;
then {[(x". v1),(((ff * decode) | {(x". v1)}) . (x". v1))]} \/ x in Dn by A27, GRFUNC_1:7;
hence contradiction by A15, A20, A23, A26; :: thesis:

end;

then f in St (H,E) by A15, A21, A22;
then consider e being Function of VAR,E such that
A28: for v2 being Element of VAR st e . v2 <> f . v2 holds
v2 = v1 and
A29: not e in St (H,E) by A24, ZF_MODEL:6;

now :: thesis:

thus A30: ( (code (Free H)) \ {(x". v1)} = dom ((e * decode) | ((code (Free H)) \ {(x". v1)})) & (code (Free H)) \ {(x". v1)} = dom ((f * decode) | ((code (Free H)) \ {(x". v1)})) ) by Lm3; :: thesis:
let q be object ; :: thesis:
assume A31: q in (code (Free H)) \ {(x". v1)} ; :: thesis:
then reconsider p99 = q as Element of omega ;
A32: q = x". (x. (card p99)) by Lm2;
not q in {(x". v1)} by A31, XBOOLE_0:def 5;
then A33: x. (card p99) <> v1 by A32, TARSKI:def 1;
thus ((e * decode) | ((code (Free H)) \ {(x". v1)})) . q = (e * decode) . q by A30, A31, FUNCT_1:47
.= e . (x. (card p99)) by A32, Lm4
.= f . (x. (card p99)) by A28, A33
.= (f * decode) . q by A32, Lm4
.= ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q by A30, A31, FUNCT_1:47 ; :: thesis:

end;

hence contradiction by A15, A21, A22, A25, A29, FUNCT_1:2; :: thesis:

end;

hence p in Diagram ((All (v1,H)),E) by A15, A21, A22, Def4; :: thesis:

end;

let p be object ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram ((All (v1,H)),E) ; :: thesis:
then consider f being Function of VAR,E such that
A34: p = (f * decode) | (code (Free (All (v1,H)))) and
A35: f in St ((All (v1,H)),E) by Def4;
A36: p in Funcs (((code (Free H)) \ {(x". v1)}),m) by A15, A34, Lm3;
then reconsider x = p as Element of V by A17, Th1;

A37: now :: thesis:

A38: code (Free H) = code (Free ('not' H)) by ZF_LANG1:60;
given u being set such that A39: {[(x". v1),u]} \/ x in Dn ; :: thesis:
consider h being Function of VAR,E such that
A40: {[(x". v1),u]} \/ x = (h * decode) | (code (Free H)) by A12, A39, Lm11;

now :: thesis:

reconsider g = {[(x". v1),u]} as Function ;
thus A41: ( dom ((h * decode) | ((code (Free H)) \ {(x". v1)})) = (code (Free H)) \ {(x". v1)} & dom ((f * decode) | ((code (Free H)) \ {(x". v1)})) = (code (Free H)) \ {(x". v1)} ) by Lm3; :: thesis:
let q be object ; :: thesis:
assume A42: q in (code (Free H)) \ {(x". v1)} ; :: thesis:
(h * decode) | ((code (Free H)) \ {(x". v1)}) c= (h * decode) | (code (Free H)) by RELAT_1:75, XBOOLE_1:36;
hence ((h * decode) | ((code (Free H)) \ {(x". v1)})) . q = ((h * decode) | (code (Free H))) . q by A41, A42, GRFUNC_1:2
.= ((f * decode) | ((code (Free H)) \ {(x". v1)})) . q by A15, A34, A40, A41, A42, GRFUNC_1:15 ;
:: thesis:

end;

then A43: h in St ((All (v1,H)),E) by A15, A35, Lm10, FUNCT_1:2;
ex hh being Function of VAR,E st
( {[(x". v1),u]} \/ x = (hh * decode) | (code (Free ('not' H))) & hh in St (('not' H),E) ) by A39, Def4;
then h in St (('not' H),E) by A40, A38, Lm10;
then not h in St (H,E) by ZF_MODEL:4;
hence contradiction by A43, ZF_MODEL:6; :: thesis:

end;

now :: thesis:

assume x in { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ; :: thesis:
then ex y being Element of V st
( y = x & y in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ y in Dn ) ;
hence contradiction by A37; :: thesis:

end;

hence p in (Funcs (((code (Free H)) \ {(x". v1)}),m)) \ { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } by A36, XBOOLE_0:def 5; :: thesis:

end;

x". v1 in code (Free H) by A11, Lm5;
then { x where x is Element of V : ( x in Funcs (((code (Free H)) \ {(x". v1)}),m) & ex u being set st {[(x". v1),u]} \/ x in Dn ) } in X by A1, A2, A16, A12, Th11;
hence Diagram ((All (v1,H)),E) in X by A1, A17, A19, Th4; :: thesis:

end;