The abstract of the Mizar article:

Six Variable Predicate Calculus for Boolean Valued Functions. Part I

by

Shunichi Kobayashi

Received December 27, 1999

MML identifier: BVFUNC23

[ Mizar article, MML identifier index ]

environ

 vocabulary PARTIT1, EQREL_1, BVFUNC_2, BOOLE, SETFAM_1, CAT_1, FUNCT_4,
      RELAT_1, FUNCT_1, CANTOR_1, T_1TOPSP;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
      FUNCT_1, CQC_LANG, FUNCT_4, EQREL_1, PARTIT1, CANTOR_1, BVFUNC_1,
      BVFUNC_2;
 constructors BVFUNC_2, SETWISEO, CANTOR_1, FUNCT_7, BVFUNC_1;
 clusters SUBSET_1, PARTIT1, CQC_LANG, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Chap. 1  Preliminaries

reserve Y for non empty set,

        G for Subset of PARTITIONS(Y),
        A, B, C, D, E, F for a_partition of Y;

theorem :: BVFUNC23:1
 G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F
implies
CompF(A,G) = B '/\' C '/\' D '/\' E '/\' F;

theorem :: BVFUNC23:2
G is independent & G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F
implies
CompF(B,G) = A '/\' C '/\' D '/\' E '/\' F;

theorem :: BVFUNC23:3
G is independent & G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F
implies
CompF(C,G) = A '/\' B '/\' D '/\' E '/\' F;

theorem :: BVFUNC23:4
G is independent & G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F
implies
CompF(D,G) = A '/\' B '/\' C '/\' E '/\' F;

theorem :: BVFUNC23:5
G is independent & G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F
implies
CompF(E,G) = A '/\' B '/\' C '/\' D '/\' F;

theorem :: BVFUNC23:6
  G is independent & G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F
implies
CompF(F,G) = A '/\' B '/\' C '/\' D '/\' E;

theorem :: BVFUNC23:7
for A,B,C,D,E,F being set, h being Function,
A',B',C',D',E',F' being set st
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (A .--> A')
holds h.A = A' & h.B = B' & h.C = C' &
      h.D = D' & h.E = E' & h.F = F';

theorem :: BVFUNC23:8
for A,B,C,D,E,F being set, h being Function,
A',B',C',D',E',F' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (A .--> A')
holds dom h = {A,B,C,D,E,F};

theorem :: BVFUNC23:9
for A,B,C,D,E,F being set, h being Function,
A',B',C',D',E',F' being set st
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +*
    (E .--> E') +* (F .--> F') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D,h.E,h.F};

theorem :: BVFUNC23:10
  for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F being a_partition of Y, z,u being Element of Y, h being Function
st G is independent & G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F
holds EqClass(u,B '/\' C '/\' D '/\' E '/\' F) meets EqClass(z,A);

theorem :: BVFUNC23:11
for G being Subset of PARTITIONS(Y),
A,B,C,D,E,F being a_partition of Y, z,u being Element of Y, h being Function
st G is independent & G={A,B,C,D,E,F} &
A<>B & A<>C & A<>D & A<>E & A<>F & B<>C & B<>D & B<>E & B<>F &
C<>D & C<>E & C<>F & D<>E & D<>F & E<>F &
EqClass(z,C '/\' D '/\' E '/\' F)=EqClass(u,C '/\' D '/\' E '/\' F)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G));