Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, BVFUNC_2, T_1TOPSP, BOOLE,
FUNCT_1, SETFAM_1, RELAT_1, CANTOR_1, CAT_1, FUNCT_4;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
FRAENKEL, MARGREL1, SETFAM_1, EQREL_1, CANTOR_1, CQC_LANG, PARTIT1,
BVFUNC_1, BVFUNC_2, FUNCT_4;
constructors DOMAIN_1, AMI_1, CANTOR_1, BVFUNC_2, BVFUNC_1;
clusters SUBSET_1, FUNCT_7, PARTIT1, MARGREL1, XBOOLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI;
theorems TARSKI, FUNCT_1, SETFAM_1, EQREL_1, CANTOR_1, T_1TOPSP, PARTIT1,
BVFUNC_2, BVFUNC11, BVFUNC14, ENUMSET1, CQC_LANG, FUNCT_4, XBOOLE_0,
XBOOLE_1;
begin :: Predicate Calculus
theorem
for Y being non empty set,
a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B,C being a_partition of Y, z,u being Element of Y
st G is independent & G={A,B,C} & A<>B & B<>C & C<>A &
EqClass(z,C)=EqClass(u,C)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G))
proof
let Y be non empty set,
a be Element of Funcs(Y,BOOLEAN),
G be Subset of PARTITIONS(Y),
A,B,C be a_partition of Y,
z,u be Element of Y;
assume A1:G is independent & G={A,B,C} & A<>B & B<>C & C<>A &
EqClass(z,C)=EqClass(u,C);then
A2:for h being Function, F being Subset-Family of Y st
dom h=G & rng h=F &
(for d being set st d in G holds h.d in d)
holds (Intersect F)<>{} by BVFUNC_2:def 5;
A3:CompF(B,G) = A '/\' C by BVFUNC14:5,A1;
set H=EqClass(z,CompF(B,G)),
I=EqClass(z,A),
GG=EqClass(u,B '/\' C);
A4: GG=EqClass(u,CompF(A,G)) by BVFUNC14:4,A1;
set h = (B .--> EqClass(u,B)) +* (C .--> EqClass(u,C)) +*
(A .--> EqClass(z,A));
A5: dom ((B .--> EqClass(u,B)) +* (C .--> EqClass(u,C)))
= dom (B .--> EqClass(u,B)) \/ dom (C .--> EqClass(u,C))
by FUNCT_4:def 2;
A6: dom ((B .--> EqClass(u,B)) +* (C .--> EqClass(u,C)) +*
(A .--> EqClass(z,A)))
= dom (B .--> EqClass(u,B)) \/ dom (C .--> EqClass(u,C)) \/
dom (A .--> EqClass(z,A)) by A5,FUNCT_4:def 2;
A7: dom (B .--> EqClass(u,B)) = {B} by CQC_LANG:5;
A8: dom (C .--> EqClass(u,C)) = {C} by CQC_LANG:5;
A9: dom (A .--> EqClass(z,A)) = {A} by CQC_LANG:5;then
dom ((B .--> EqClass(u,B)) +* (C .--> EqClass(u,C)) +*
(A .--> EqClass(z,A)))
= {A} \/ {B} \/ {C} by A8,A6,A7,XBOOLE_1:4
.= {A,B} \/ {C} by ENUMSET1:41
.= {A,B,C} by ENUMSET1:43;then
A10: dom h = G by A1;
A11: h.A = EqClass(z,A)
proof
A in dom (A .--> EqClass(z,A)) by TARSKI:def 1,A9;then
h.A = (A .--> EqClass(z,A)).A by FUNCT_4:44;
hence thesis by CQC_LANG:6;
end;
A12: h.B = EqClass(u,B)
proof
not B in dom (A .--> EqClass(z,A)) by TARSKI:def 1,A1,A9; then
A13:h.B=((B .--> EqClass(u,B)) +* (C .--> EqClass(u,C))).B
by FUNCT_4:42;
not B in dom (C .--> EqClass(u,C)) by TARSKI:def 1,A1,A8; then
h.B=(B .--> EqClass(u,B)).B by A13,FUNCT_4:42;
hence thesis by CQC_LANG:6;
end;
A14: h.C = EqClass(u,C)
proof
not C in dom (A .--> EqClass(z,A)) by TARSKI:def 1,A1,A9; then
A15:h.C=((B .--> EqClass(u,B)) +* (C .--> EqClass(u,C))).C
by FUNCT_4:42;
C in dom (C .--> EqClass(u,C)) by A8,TARSKI:def 1;then
h.C=(C .--> EqClass(u,C)).C by A15,FUNCT_4:44;
hence thesis by CQC_LANG:6;
end;
A16: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;then
A17:d=A or d=B or d=C by A1,ENUMSET1:13;
now per cases by A17;
case d=A; hence thesis by A11;
case d=B; hence thesis by A12;
case d=C; hence thesis by A14;
end;
hence thesis;
end;
A in dom h by ENUMSET1:def 1,A1,A10;then
A18: h.A in rng h by FUNCT_1:def 5;
B in dom h by ENUMSET1:def 1,A1,A10;then
A19: h.B in rng h by FUNCT_1:def 5;
C in dom h by ENUMSET1:def 1,A1,A10;then
A20: h.C in rng h by FUNCT_1:def 5;
A21:rng h c= {h.A,h.B,h.C}
proof
let t be set;
assume t in rng h;
then consider x1 being set such that
A22: x1 in dom h & t = h.x1 by FUNCT_1:def 5;
now per cases by A22,A1,A10,ENUMSET1:def 1;
case x1=A; hence thesis by A22,ENUMSET1:def 1;
case x1=B; hence thesis by A22,ENUMSET1:def 1;
case x1=C; hence thesis by A22,ENUMSET1:def 1;
end;
hence thesis;
end;
{h.A,h.B,h.C} c= rng h
proof
let t be set;
assume t in {h.A,h.B,h.C};then
A23:t=h.A or t=h.B or t=h.C by ENUMSET1:def 1;
now per cases by A23;
case t=h.A; hence thesis by A18;
case t=h.B; hence thesis by A19;
case t=h.C; hence thesis by A20;
end;
hence thesis;
end;then
A24:rng h = {h.A,h.B,h.C} by XBOOLE_0:def 10,A21;
rng h c= bool Y
proof
let t be set;
assume t in rng h;then
A25:t=h.A or t=h.B or t=h.C by A24,ENUMSET1:def 1;
now per cases by A25;
case t=h.A;
hence thesis by A11;
case t=h.B; hence thesis by A12;
case t=h.C; hence thesis by A14;
end;
hence thesis;
end;then
reconsider FF=rng h as Subset-Family of Y by SETFAM_1:def 7;
A26: Intersect FF = meet (rng h) by A18,CANTOR_1:def 3;
A27: for x being set holds x in meet FF iff
(for y being set holds y in FF implies x in y)
by SETFAM_1:def 1,A18;
(Intersect FF)<>{} by A2,A10,A16;then
consider m being set such that
A28: m in Intersect FF by XBOOLE_0:def 1;
m in h.A & m in h.B & m in h.C by A18,A19,A20,A27,A26,A28;then
A29: m in EqClass(z,A) & m in EqClass(u,B) & m in EqClass(u,C) by A11,A12,A14;
A30: GG /\ I = EqClass(u,B) /\ EqClass(u,C) /\ EqClass(z,A) by BVFUNC14:1;
m in EqClass(u,B) /\ EqClass(u,C) by A29,XBOOLE_0:def 3;then
GG /\ I <> {} by A30,A29,XBOOLE_0:def 3;then
consider p being set such that
A31: p in GG /\ I by XBOOLE_0:def 1;
reconsider p as Element of Y by A31;
set K=EqClass(p,C);
A32: p in K & K in C by T_1TOPSP:def 1;
p in GG & p in I by A31,XBOOLE_0:def 3;then
A33:p in I /\ K by A32,XBOOLE_0:def 3;then
A34:not (I /\ K in {{}}) by TARSKI:def 1;
I /\ K in INTERSECTION(A,C) by SETFAM_1:def 5;then
I /\ K in INTERSECTION(A,C) \ {{}} by A34,XBOOLE_0:def 4;then
A35: I /\ K in A '/\' C by PARTIT1:def 4;
set L=EqClass(z,C);
A36: GG c= L by A1,BVFUNC11:3;
A37: p in GG by A31,XBOOLE_0:def 3;
p in EqClass(p,C) by T_1TOPSP:def 1;then
K meets L by A36,A37,XBOOLE_0:3;then
A38: K=L by T_1TOPSP:9;
A39: z in K by A38,T_1TOPSP:def 1;
z in I by T_1TOPSP:def 1;then
A40: z in I /\ K by XBOOLE_0:def 3,A39;
z in H by T_1TOPSP:def 1;then
I /\ K meets H by A40,XBOOLE_0:3; then
A41: I /\ K /\ H <> {} by XBOOLE_0:def 7;
I /\ K = H or I /\ K misses H by A35,A3,EQREL_1:def 6;then
I /\ K = H or I /\ K /\ H = {} by XBOOLE_0:def 7;
then EqClass(u,CompF(A,G)) /\ EqClass(z,CompF(B,G)) <> {}
by A4,A37,XBOOLE_0:def 3,A33,A41;
hence thesis by XBOOLE_0:def 7;
end;