The abstract of the Mizar article:

Five Variable Predicate Calculus for Boolean Valued Functions. Part I

by

Shunichi Kobayashi

Received December 27, 1999

MML identifier: BVFUNC22

[ 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 for a_partition of Y;

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

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

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

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

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

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

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

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

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

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