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