The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part III

by

Shunichi Kobayashi, and

Yatsuka Nakamura

Received July 14, 1999

MML identifier: BVFUNC11

[ Mizar article, MML identifier index ]

environ

 vocabulary EQREL_1, PARTIT1, T_1TOPSP, BOOLE, BVFUNC_2, FUNCOP_1, SETFAM_1,
      RELAT_1, FUNCT_1, CANTOR_1, CAT_1, FUNCT_2, MARGREL1, ZF_LANG, BVFUNC_1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1,
      SETFAM_1, FUNCT_1, FRAENKEL, EQREL_1, CANTOR_1, CQC_LANG, PARTIT1,
      BVFUNC_1, BVFUNC_2, FUNCT_4;
 constructors CANTOR_1, BVFUNC_2, PUA2MSS1, BVFUNC_1, FUNCT_4, MEMBERED;
 clusters FUNCT_7, PARTIT1, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL;
 requirements SUBSET, BOOLE;


begin

::Chap. 1  Preliminaries

reserve Y for non empty set;

theorem :: BVFUNC11:1
for z being Element of Y, PA,PB being a_partition of Y
st PA '<' PB holds EqClass(z,PA) c= EqClass(z,PB);

theorem :: BVFUNC11:2
for z being Element of Y, PA,PB being a_partition of Y
holds EqClass(z,PA) c= EqClass(z,PA '\/' PB);

theorem :: BVFUNC11:3
for z being Element of Y, PA,PB being a_partition of Y
holds EqClass(z,PA '/\' PB) c= EqClass(z,PA);

theorem :: BVFUNC11:4
for z being Element of Y, PA being a_partition of Y holds
EqClass(z,PA) c= EqClass(z,%O(Y)) & EqClass(z,%I(Y)) c= EqClass(z,PA);

theorem :: BVFUNC11:5
for G being Subset of PARTITIONS(Y),
A,B being a_partition of Y
st G is independent & G={A,B} & A<>B holds
for a,b being set st a in A & b in B holds a meets b;

theorem :: BVFUNC11:6
for G being Subset of PARTITIONS(Y),
A,B being a_partition of Y
st G is independent & G={A,B} & A <> B holds
'/\' G = A '/\' B;

theorem :: BVFUNC11:7
   for G being Subset of PARTITIONS(Y), A,B being a_partition of Y
   st G={A,B} & A<>B
  holds CompF(A,G) = B;

begin

canceled 3;

theorem :: BVFUNC11:11
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
All(All(a,A,G),B,G) '<' Ex(All(a,B,G),A,G);

theorem :: BVFUNC11:12
  for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
All(All(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G);

theorem :: BVFUNC11:13
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
All(All(a,A,G),B,G) '<' All(Ex(a,B,G),A,G);

theorem :: BVFUNC11:14
  for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds All(Ex(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G);

theorem :: BVFUNC11:15
  for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y holds
'not' Ex(All(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC11:16
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
Ex('not' All(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC11:17
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
'not' All(All(a,A,G),B,G) = Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC11:18
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
All('not' All(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC11:19
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC11:20
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B being a_partition of Y st G is independent holds
'not' All(All(a,A,G),B,G) '<' Ex(Ex('not' a,A,G),B,G);