The abstract of the Mizar article:

Four Variable Predicate Calculus for Boolean Valued Functions. Part I

by

Shunichi Kobayashi

Received November 26, 1999

MML identifier: BVFUNC20

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, FUNCT_1, CAT_1, FUNCT_4,
      RELAT_1, BOOLE, BVFUNC_2, T_1TOPSP, SETFAM_1, CANTOR_1, ZF_LANG,
      BVFUNC_1;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1,
      FUNCT_1, FRAENKEL, CQC_LANG, FUNCT_4, MARGREL1, VALUAT_1, 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, MARGREL1, VALUAT_1, AMI_1, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Chap. 1  Preliminaries

reserve Y for non empty set,
        a for Element of Funcs(Y,BOOLEAN),
        G for Subset of PARTITIONS(Y),
        A, B, C, D for a_partition of Y;

theorem :: BVFUNC20:1
for h being Function, A',B',C',D' being set st
G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds h.B = B' & h.C = C' & h.D = D';

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

theorem :: BVFUNC20:3
for h being Function,A',B',C',D' being set st G={A,B,C,D} &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D};

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

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

begin

canceled 14;

theorem :: BVFUNC20:20
G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D
 implies Ex('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

canceled 2;

theorem :: BVFUNC20:23
G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D
implies Ex(Ex('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);