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 v1, v2 being Element of VAR holds
( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),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 v1, v2 being Element of VAR holds
( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),E in X )
let E be non empty set ; :: thesis: ( X is closed_wrt_A1-A7 & E in X implies for v1, v2 being Element of VAR holds
( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),E in X ) )
assume A1:
( X is closed_wrt_A1-A7 & E in X )
; :: thesis: for v1, v2 being Element of VAR holds
( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),E in X )
then A2:
X is closed_wrt_A4
by Def13;
A3:
X is closed_wrt_A1
by A1, Def13;
let v1, v2 be Element of VAR ; :: thesis: ( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),E in X )
set H = v1 '=' v2;
set H' = v1 'in' v2;
A4:
Free (v1 '=' v2) = {v1,v2}
by ZF_LANG1:63;
A5:
Free (v1 'in' v2) = {v1,v2}
by ZF_LANG1:64;
then A6:
( v1 in Free (v1 '=' v2) & v2 in Free (v1 '=' v2) & v1 in Free (v1 'in' v2) & v2 in Free (v1 'in' v2) )
by A4, TARSKI:def 2;
A7:
omega c= X
by A1, Th7;
reconsider m = E as Element of V by A1;
per cases
( v1 = v2 or v1 <> v2 )
;
suppose A8:
v1 = v2
;
:: thesis: ( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),E in X )then A9:
(
Free (v1 '=' v2) = {v1} &
Free (v1 'in' v2) = {v1} )
by A4, A5, ENUMSET1:69;
A10:
x". v1 in X
by A7, TARSKI:def 3;
then
{(x". v1)} in X
by A1, Th2;
then A11:
code (Free (v1 '=' v2)) in X
by A9, Lm6;
set a =
code (Free (v1 '=' v2));
set Z =
{ {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } ;
{ {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } = Diagram (v1 '=' v2),
E
proof
thus
{ {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } c= Diagram (v1 '=' v2),
E
:: according to XBOOLE_0:def 10 :: thesis: Diagram (v1 '=' v2),E c= { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } or p in Diagram (v1 '=' v2),E )
assume
p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) }
;
:: thesis: p in Diagram (v1 '=' v2),E
then consider z,
y being
Element of
V such that A12:
(
p = {[z,y]} &
z in code (Free (v1 '=' v2)) &
y in m )
;
z in {(x". v1)}
by A9, A12, Lm6;
then A13:
z = x". v1
by TARSKI:def 1;
reconsider f =
VAR --> y as
Function of
VAR ,
E by A12, FUNCOP_1:57;
dom ((f * decode ) | (code (Free (v1 '=' v2)))) =
code (Free (v1 '=' v2))
by Lm3
.=
{z}
by A9, A13, Lm6
;
then
(f * decode ) | (code (Free (v1 '=' v2))) = {[z,(((f * decode ) | (code (Free (v1 '=' v2)))) . z)]}
by GRFUNC_1:18;
then
(f * decode ) | (code (Free (v1 '=' v2))) = {[z,(f . v1)]}
by A6, A13, Lm9;
then A14:
(f * decode ) | (code (Free (v1 '=' v2))) = p
by A12, FUNCOP_1:13;
A15:
f . (Var1 (v1 '=' v2)) =
f . v2
by A8, ZF_LANG1:1
.=
f . (Var2 (v1 '=' v2))
by ZF_LANG1:1
;
v1 '=' v2 is
being_equality
by ZF_LANG:16;
then
f in St (v1 '=' v2),
E
by A15, ZF_MODEL:7;
hence
p in Diagram (v1 '=' v2),
E
by A14, Def5;
:: thesis: verum
end;
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in Diagram (v1 '=' v2),E or p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) } )
assume
p in Diagram (v1 '=' v2),
E
;
:: thesis: p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) }
then consider f being
Function of
VAR ,
E such that A16:
(
p = (f * decode ) | (code (Free (v1 '=' v2))) &
f in St (v1 '=' v2),
E )
by Def5;
reconsider z =
x". v1 as
Element of
V by A10;
dom ((f * decode ) | (code (Free (v1 '=' v2)))) =
code (Free (v1 '=' v2))
by Lm3
.=
{z}
by A9, Lm6
;
then A17:
(f * decode ) | (code (Free (v1 '=' v2))) = {[z,(((f * decode ) | (code (Free (v1 '=' v2)))) . z)]}
by GRFUNC_1:18;
reconsider y =
f . v1 as
Element of
V by A1, Th1;
A18:
p = {[z,y]}
by A6, A16, A17, Lm9;
z in {z}
by TARSKI:def 1;
then
z in code (Free (v1 '=' v2))
by A9, Lm6;
hence
p in { {[z,y]} where z, y is Element of V : ( z in code (Free (v1 '=' v2)) & y in m ) }
by A18;
:: thesis: verum
end; hence
Diagram (v1 '=' v2),
E in X
by A1, A2, A11, Def9;
:: thesis: Diagram (v1 'in' v2),E in X
Diagram (v1 'in' v2),
E = {}
hence
Diagram (v1 'in' v2),
E in X
by A1, Th3;
:: thesis: verum end; suppose A21:
v1 <> v2
;
:: thesis: ( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),E in X )set fs =
code (Free (v1 '=' v2));
A23:
code (Free (v1 '=' v2)) = {(x". v1),(x". v2)}
by A4, Lm7;
{[(x". v1),(0-element_of V)],[(x". v2),(1-element_of V)]} in X
proof
A24:
(
x". v1 in X &
x". v2 in X )
by A7, TARSKI:def 3;
(
0-element_of V in X &
1-element_of V in X )
by A1, Lm13;
then
(
[(x". v1),(0-element_of V)] in X &
[(x". v2),(1-element_of V)] in X )
by A1, A24, Th6;
hence
{[(x". v1),(0-element_of V)],[(x". v2),(1-element_of V)]} in X
by A1, Th6;
:: thesis: verum
end; then reconsider d =
{[(x". v1),(0-element_of V)],[(x". v2),(1-element_of V)]} as
Element of
V ;
set a =
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in m } ;
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in m } in X
by A1, Th17;
then reconsider a =
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in m } as
Element of
V ;
set b =
{ {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in m & y in m ) } ;
A26:
{ {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in m & y in m ) } in X
by A1, A3, Def6;
then reconsider b =
{ {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in m & y in m ) } as
Element of
V ;
set Y =
{ (d (#) x) where x is Element of V : x in a } ;
set Z =
{ (d (#) x) where x is Element of V : x in b } ;
A27:
d in Funcs (code (Free (v1 '=' v2))),
omega
proof
reconsider e =
d as
Function by A22, GRFUNC_1:19;
reconsider g =
{[(x". v1),(0-element_of V)]},
h =
{[(x". v2),(1-element_of V)]} as
Function by GRFUNC_1:15;
A28:
e = g \/ h
by ENUMSET1:41;
then A29:
dom e =
(dom g) \/ (dom h)
by RELAT_1:13
.=
{(x". v1)} \/ (dom h)
by RELAT_1:23
.=
{(x". v1)} \/ {(x". v2)}
by RELAT_1:23
.=
code (Free (v1 '=' v2))
by A23, ENUMSET1:41
;
A30:
rng e =
(rng g) \/ (rng h)
by A28, RELAT_1:26
.=
{(0-element_of V)} \/ (rng h)
by RELAT_1:23
.=
{(0-element_of V)} \/ {(1-element_of V)}
by RELAT_1:23
.=
{(0-element_of V),(1-element_of V)}
by ENUMSET1:41
;
(
0-element_of V in omega &
1-element_of V in omega )
by ORDINAL1:def 12;
then
rng e c= omega
by A30, ZFMISC_1:38;
hence
d in Funcs (code (Free (v1 '=' v2))),
omega
by A29, FUNCT_2:def 2;
:: thesis: verum
end;
{ (d (#) x) where x is Element of V : x in a } = Diagram (v1 '=' v2),
E
proof
thus
{ (d (#) x) where x is Element of V : x in a } c= Diagram (v1 '=' v2),
E
:: according to XBOOLE_0:def 10 :: thesis: Diagram (v1 '=' v2),E c= { (d (#) x) where x is Element of V : x in a } proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in { (d (#) x) where x is Element of V : x in a } or p in Diagram (v1 '=' v2),E )
assume
p in { (d (#) x) where x is Element of V : x in a }
;
:: thesis: p in Diagram (v1 '=' v2),E
then consider x being
Element of
V such that A31:
(
p = d (#) x &
x in a )
;
consider y being
Element of
V such that A32:
(
x = {[(0-element_of V),y],[(1-element_of V),y]} &
y in m )
by A31;
A33:
p = {[(x". v1),y],[(x". v2),y]}
by A31, A32, Lm15;
reconsider f =
VAR --> y as
Function of
VAR ,
E by A32, FUNCOP_1:57;
A34:
dom ((f * decode ) | (code (Free (v1 '=' v2)))) = {(x". v1),(x". v2)}
by A23, Lm3;
A35:
((f * decode ) | (code (Free (v1 '=' v2)))) . (x". v1) =
f . v1
by A6, Lm9
.=
y
by FUNCOP_1:13
;
((f * decode ) | (code (Free (v1 '=' v2)))) . (x". v2) =
f . v2
by A6, Lm9
.=
y
by FUNCOP_1:13
;
then A36:
(f * decode ) | (code (Free (v1 '=' v2))) = p
by A33, A34, A35, Lm16;
A37:
v1 '=' v2 is
being_equality
by ZF_LANG:16;
f . (Var1 (v1 '=' v2)) =
y
by FUNCOP_1:13
.=
f . (Var2 (v1 '=' v2))
by FUNCOP_1:13
;
then
f in St (v1 '=' v2),
E
by A37, ZF_MODEL:7;
hence
p in Diagram (v1 '=' v2),
E
by A36, Def5;
:: thesis: verum
end;
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in Diagram (v1 '=' v2),E or p in { (d (#) x) where x is Element of V : x in a } )
assume
p in Diagram (v1 '=' v2),
E
;
:: thesis: p in { (d (#) x) where x is Element of V : x in a }
then consider f being
Function of
VAR ,
E such that A38:
(
p = (f * decode ) | (code (Free (v1 '=' v2))) &
f in St (v1 '=' v2),
E )
by Def5;
A39:
dom ((f * decode ) | (code (Free (v1 '=' v2)))) = {(x". v1),(x". v2)}
by A23, Lm3;
v1 '=' v2 is
being_equality
by ZF_LANG:16;
then
f . (Var1 (v1 '=' v2)) = f . (Var2 (v1 '=' v2))
by A38, ZF_MODEL:7;
then A40:
f . v1 =
f . (Var2 (v1 '=' v2))
by ZF_LANG1:1
.=
f . v2
by ZF_LANG1:1
;
reconsider y =
f . v1 as
Element of
V by A1, Th1;
A41:
((f * decode ) | (code (Free (v1 '=' v2)))) . (x". v1) = y
by A6, Lm9;
((f * decode ) | (code (Free (v1 '=' v2)))) . (x". v2) = y
by A6, A40, Lm9;
then A42:
p = {[(x". v1),y],[(x". v2),y]}
by A38, A39, A41, Lm16;
A43:
{[(0-element_of V),y],[(1-element_of V),y]} in a
;
reconsider x =
{[(0-element_of V),y],[(1-element_of V),y]} as
Element of
V ;
p = d (#) x
by A42, Lm15;
hence
p in { (d (#) x) where x is Element of V : x in a }
by A43;
:: thesis: verum
end; hence
Diagram (v1 '=' v2),
E in X
by A1, A27, Th10, Th17;
:: thesis: Diagram (v1 'in' v2),E in X
{ (d (#) x) where x is Element of V : x in b } = Diagram (v1 'in' v2),
E
proof
thus
{ (d (#) x) where x is Element of V : x in b } c= Diagram (v1 'in' v2),
E
:: according to XBOOLE_0:def 10 :: thesis: Diagram (v1 'in' v2),E c= { (d (#) x) where x is Element of V : x in b } proof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in { (d (#) x) where x is Element of V : x in b } or p in Diagram (v1 'in' v2),E )
assume
p in { (d (#) x) where x is Element of V : x in b }
;
:: thesis: p in Diagram (v1 'in' v2),E
then consider x being
Element of
V such that A44:
(
p = d (#) x &
x in b )
;
consider y,
z being
Element of
V such that A45:
(
x = {[(0-element_of V),y],[(1-element_of V),z]} &
y in z &
y in m &
z in m )
by A44;
A46:
p = {[(x". v1),y],[(x". v2),z]}
by A44, A45, Lm15;
reconsider y' =
y,
z' =
z as
Element of
E by A45;
reconsider a1 =
v1 as
Element of
VAR ;
deffunc H1(
set )
-> Element of
E =
z';
consider f being
Function of
VAR ,
E such that A47:
(
f . a1 = y' & ( for
v3 being
Element of
VAR st
v3 <> a1 holds
f . v3 = H1(
v3) ) )
from FUNCT_2:sch 6();
A48:
dom ((f * decode ) | (code (Free (v1 'in' v2)))) = {(x". v1),(x". v2)}
by A4, A5, A23, Lm3;
A49:
((f * decode ) | (code (Free (v1 'in' v2)))) . (x". v1) = y
by A6, A47, Lm9;
((f * decode ) | (code (Free (v1 'in' v2)))) . (x". v2) =
f . v2
by A6, Lm9
.=
z
by A21, A47
;
then A50:
p = (f * decode ) | (code (Free (v1 'in' v2)))
by A46, A48, A49, Lm16;
A51:
v1 'in' v2 is
being_membership
by ZF_LANG:16;
f . v1 in f . v2
by A21, A45, A47;
then
f . (Var1 (v1 'in' v2)) in f . v2
by ZF_LANG1:2;
then
f . (Var1 (v1 'in' v2)) in f . (Var2 (v1 'in' v2))
by ZF_LANG1:2;
then
f in St (v1 'in' v2),
E
by A51, ZF_MODEL:8;
hence
p in Diagram (v1 'in' v2),
E
by A50, Def5;
:: thesis: verum
end;
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in Diagram (v1 'in' v2),E or p in { (d (#) x) where x is Element of V : x in b } )
assume
p in Diagram (v1 'in' v2),
E
;
:: thesis: p in { (d (#) x) where x is Element of V : x in b }
then consider f being
Function of
VAR ,
E such that A52:
(
p = (f * decode ) | (code (Free (v1 'in' v2))) &
f in St (v1 'in' v2),
E )
by Def5;
A53:
dom ((f * decode ) | (code (Free (v1 'in' v2)))) = {(x". v1),(x". v2)}
by A4, A5, A23, Lm3;
A54:
(
((f * decode ) | (code (Free (v1 'in' v2)))) . (x". v1) = f . v1 &
((f * decode ) | (code (Free (v1 'in' v2)))) . (x". v2) = f . v2 )
by A6, Lm9;
reconsider y =
f . v1 as
Element of
V by A1, Th1;
reconsider z =
f . v2 as
Element of
V by A1, Th1;
A55:
p = {[(x". v1),y],[(x". v2),z]}
by A52, A53, A54, Lm16;
v1 'in' v2 is
being_membership
by ZF_LANG:16;
then
f . (Var1 (v1 'in' v2)) in f . (Var2 (v1 'in' v2))
by A52, ZF_MODEL:8;
then
f . v1 in f . (Var2 (v1 'in' v2))
by ZF_LANG1:2;
then
y in z
by ZF_LANG1:2;
then A56:
{[(0-element_of V),y],[(1-element_of V),z]} in b
;
reconsider x =
{[(0-element_of V),y],[(1-element_of V),z]} as
Element of
V ;
p = d (#) x
by A55, Lm15;
hence
p in { (d (#) x) where x is Element of V : x in b }
by A56;
:: thesis: verum
end; hence
Diagram (v1 'in' v2),
E in X
by A1, A26, A27, Th10;
:: thesis: verum end;