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
for v1 being Element of VAR st Diagram H,E in X holds
Diagram (All v1,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
for v1 being Element of VAR st Diagram H,E in X holds
Diagram (All v1,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
for v1 being Element of VAR st Diagram H,E in X holds
Diagram (All v1,H),E in X )
assume A1:
( X is closed_wrt_A1-A7 & E in X )
; :: thesis: for H being ZF-formula
for v1 being Element of VAR st Diagram H,E in X holds
Diagram (All v1,H),E in X
let H be ZF-formula; :: thesis: for v1 being Element of VAR st Diagram H,E in X holds
Diagram (All v1,H),E in X
let v1 be Element of VAR ; :: thesis: ( Diagram H,E in X implies Diagram (All v1,H),E in X )
assume A2:
Diagram H,E in X
; :: thesis: Diagram (All v1,H),E in X
per cases
( not v1 in Free H or v1 in Free H )
;
suppose A3:
not
v1 in Free H
;
:: thesis: Diagram (All v1,H),E in Xthen
Free H = (Free H) \ {v1}
by ZFMISC_1:65;
then A4:
Free (All v1,H) = Free H
by ZF_LANG1:67;
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: Diagram H,E c= Diagram (All v1,H),Eproof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in Diagram (All v1,H),E or p in Diagram H,E )
assume
p in Diagram (All v1,H),
E
;
:: thesis: p in Diagram H,E
then consider f being
Function of
VAR ,
E such that A5:
(
p = (f * decode ) | (code (Free (All v1,H))) &
f in St (All v1,H),
E )
by Def5;
f in St H,
E
by A5, ZF_MODEL:6;
hence
p in Diagram H,
E
by A4, A5, Def5;
:: thesis: verum
end;
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in Diagram H,E or p in Diagram (All v1,H),E )
assume
p in Diagram H,
E
;
:: thesis: p in Diagram (All v1,H),E
then consider f being
Function of
VAR ,
E such that A6:
(
p = (f * decode ) | (code (Free H)) &
f in St H,
E )
by Def5;
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
then
f in St (All v1,H),
E
by A6, ZF_MODEL:6;
hence
p in Diagram (All v1,H),
E
by A4, A6, Def5;
:: thesis: verum
end; hence
Diagram (All v1,H),
E in X
by A2;
:: thesis: verum end; suppose A8:
v1 in Free H
;
:: thesis: Diagram (All v1,H),E in Xset n =
x". v1;
set fs =
code (Free H);
A9:
Diagram ('not' H),
E in X
by A1, A2, Th19;
then reconsider Dn =
Diagram ('not' H),
E as
Element of
V ;
A10:
x". v1 in code (Free H)
by A8, Lm5;
{v1} c= Free H
by A8, ZFMISC_1:37;
then
Free H = ((Free H) \ {v1}) \/ {v1}
by XBOOLE_1:45;
then A11:
code (Free H) =
(code ((Free H) \ {v1})) \/ (code {v1})
by RELAT_1:153
.=
(code ((Free H) \ {v1})) \/ {(x". v1)}
by Lm6
;
A12:
(code (Free H)) \ {(x". v1)} =
(code (Free H)) \ (code {v1})
by Lm6
.=
code ((Free H) \ {v1})
by Lm1, FUNCT_1:123
;
then A13:
(code (Free H)) \ {(x". v1)} = code (Free (All v1,H))
by ZF_LANG1:67;
A14:
Diagram ('not' H),
E c= Funcs (code (Free H)),
E
reconsider m =
E as
Element of
V by A1;
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 ) } ;
A16:
{ 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, A9, A10, A14, Th11;
A17:
Funcs ((code (Free H)) \ {(x". v1)}),
m in X
by A1, Th9;
(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: Diagram (All v1,H),E c= (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 ) } proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not 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 ) } or p in Diagram (All v1,H),E )
assume A18:
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: p in Diagram (All v1,H),E
then A19:
(
p in Funcs ((code (Free H)) \ {(x". v1)}),
m & 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 XBOOLE_0:def 5;
consider h being
Function such that A20:
(
p = h &
dom h = (code (Free H)) \ {(x". v1)} &
rng h c= E )
by A18, FUNCT_2:def 2;
consider f being
Function of
VAR ,
E such that A21:
h = (f * decode ) | ((code (Free H)) \ {(x". v1)})
by A18, A20, Lm11;
f in St (All v1,H),
E
proof
A22:
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: ( p = (ff * decode ) | (code (Free (All v1,H))) implies ff in St H,E )
assume A23:
p = (ff * decode ) | (code (Free (All v1,H)))
;
:: thesis: ff in St H,E
assume
not
ff in St H,
E
;
:: thesis: contradiction
then
ff in St ('not' H),
E
by ZF_MODEL:4;
then
(ff * decode ) | (code (Free ('not' H))) in Dn
by Def5;
then
(ff * decode ) | (((code (Free H)) \ {(x". v1)}) \/ {(x". v1)}) in Dn
by A11, A12, ZF_LANG1:65;
then A24:
((ff * decode ) | ((code (Free H)) \ {(x". v1)})) \/ ((ff * decode ) | {(x". v1)}) in Dn
by RELAT_1:107;
(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;
dom ((ff * decode ) | {(x". v1)}) = {(x". v1)}
by Lm3;
then
{[(x". v1),(((ff * decode ) | {(x". v1)}) . (x". v1))]} \/ x in Dn
by A24, GRFUNC_1:18;
hence
contradiction
by A13, A19, A23;
:: thesis: verum
end;
then A25:
f in St H,
E
by A13, A20, A21;
assume
not
f in St (All v1,H),
E
;
:: thesis: contradiction
then consider e being
Function of
VAR ,
E such that A26:
( ( for
v2 being
Element of
VAR st
e . v2 <> f . v2 holds
v2 = v1 ) & not
e in St H,
E )
by A25, ZF_MODEL:6;
(e * decode ) | ((code (Free H)) \ {(x". v1)}) = (f * decode ) | ((code (Free H)) \ {(x". v1)})
hence
contradiction
by A13, A20, A21, A22, A26;
:: thesis: verum
end;
hence
p in Diagram (All v1,H),
E
by A13, A20, A21, Def5;
:: thesis: verum
end;
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in Diagram (All v1,H),E or 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 ) } )
assume
p in Diagram (All v1,H),
E
;
:: thesis: 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 ) }
then consider f being
Function of
VAR ,
E such that A32:
(
p = (f * decode ) | (code (Free (All v1,H))) &
f in St (All v1,H),
E )
by Def5;
A33:
p in Funcs ((code (Free H)) \ {(x". v1)}),
m
by A13, A32, Lm3;
then reconsider x =
p as
Element of
V by A17, Th1;
A34:
now given u being
set such that A35:
{[(x". v1),u]} \/ x in Dn
;
:: thesis: contradictionconsider h being
Function of
VAR ,
E such that A36:
{[(x". v1),u]} \/ x = (h * decode ) | (code (Free H))
by A14, A35, Lm11;
A37:
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 A35, Def5;
code (Free H) = code (Free ('not' H))
by ZF_LANG1:65;
then
h in St ('not' H),
E
by A36, A37, Lm10;
then A38:
not
h in St H,
E
by ZF_MODEL:4;
(h * decode ) | ((code (Free H)) \ {(x". v1)}) = (f * decode ) | ((code (Free H)) \ {(x". v1)})
proof
now thus A39:
(
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: for q being set st q in (code (Free H)) \ {(x". v1)} holds
((h * decode ) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode ) | ((code (Free H)) \ {(x". v1)})) . qlet q be
set ;
:: thesis: ( q in (code (Free H)) \ {(x". v1)} implies ((h * decode ) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode ) | ((code (Free H)) \ {(x". v1)})) . q )assume A40:
q in (code (Free H)) \ {(x". v1)}
;
:: thesis: ((h * decode ) | ((code (Free H)) \ {(x". v1)})) . q = ((f * decode ) | ((code (Free H)) \ {(x". v1)})) . qreconsider g =
{[(x". v1),u]} as
Function by GRFUNC_1:15;
A41:
g = {[(x". v1),u]}
;
(h * decode ) | ((code (Free H)) \ {(x". v1)}) c= (h * decode ) | (code (Free H))
by RELAT_1:104, XBOOLE_1:36;
hence ((h * decode ) | ((code (Free H)) \ {(x". v1)})) . q =
((h * decode ) | (code (Free H))) . q
by A39, A40, GRFUNC_1:8
.=
((f * decode ) | ((code (Free H)) \ {(x". v1)})) . q
by A13, A32, A36, A39, A40, A41, GRFUNC_1:35
;
:: thesis: verum end;
hence
(h * decode ) | ((code (Free H)) \ {(x". v1)}) = (f * decode ) | ((code (Free H)) \ {(x". v1)})
by FUNCT_1:9;
:: thesis: verum
end; then
h in St (All v1,H),
E
by A13, A32, Lm10;
hence
contradiction
by A38, ZF_MODEL:6;
:: thesis: verum 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 A33, XBOOLE_0:def 5;
:: thesis: verum
end; hence
Diagram (All v1,H),
E in X
by A1, A16, A17, Th4;
:: thesis: verum end;