The Mizar article:

Predicate Calculus for Boolean Valued Functions. Part VII

by
Shunichi Kobayashi

Received October 19, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: BVFUNC15
[ MML identifier index ]


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;

Back to top