Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

Predicate Calculus for Boolean Valued Functions. Part IV

by
Shunichi Kobayashi, and
Yatsuka Nakamura

MML identifier: BVFUNC12
[ Mizar article, MML identifier index ]

```environ

vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, ZF_LANG, BVFUNC_2;
notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, EQREL_1, BVFUNC_1,
BVFUNC_2;
constructors BVFUNC_2, BVFUNC_1;
clusters MARGREL1, XBOOLE_0;

begin :: Chap. 1  Predicate Calculus

reserve Y for non empty set;

canceled 4;

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

theorem :: BVFUNC12:6
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) = All(Ex('not' a,A,G),B,G);

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

canceled 3;

theorem :: BVFUNC12: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
Ex(All(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G);

theorem :: BVFUNC12: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) '<' All(Ex(a,A,G),B,G);

theorem :: BVFUNC12:13
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(All(a,A,G),B,G);

theorem :: BVFUNC12:14
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,A,G),B,G);

theorem :: BVFUNC12:15
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,A,G),B,G);

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

```