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;