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

### Predicate Calculus for Boolean Valued Functions. Part V

by
Shunichi Kobayashi, and
Yatsuka Nakamura

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

```environ

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

begin :: Chap. 1  Predicate Calculus

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

theorem :: BVFUNC13:1
G is independent implies
All('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

theorem :: BVFUNC13:2
All(All('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

theorem :: BVFUNC13:3
All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

theorem :: BVFUNC13:4
G is independent implies
All(Ex('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

canceled;

theorem :: BVFUNC13:6
G is independent implies
Ex(All('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

theorem :: BVFUNC13:7
G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

canceled;

theorem :: BVFUNC13:9
G is independent implies
'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);

theorem :: BVFUNC13:10
G is independent implies
'not' Ex(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);

theorem :: BVFUNC13:11
'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G);

canceled 2;

theorem :: BVFUNC13:14
G is independent implies
'not' Ex(All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

theorem :: BVFUNC13:15
G is independent implies
'not' All(Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

theorem :: BVFUNC13:16
'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G);

theorem :: BVFUNC13:17
G is independent implies
'not' Ex(All(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:18
G is independent implies
'not' All(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:19
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:20
G is independent implies
'not' All(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G);

theorem :: BVFUNC13:21
G is independent implies
'not' Ex(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G);

theorem :: BVFUNC13:22
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G);

theorem :: BVFUNC13:23
G is independent implies
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G);

theorem :: BVFUNC13:24
G is independent implies
'not' All(Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:25
'not' Ex(Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:26
G is independent implies
'not' All(Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:27
G is independent implies
'not' Ex(Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:28
'not' Ex(Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G);

theorem :: BVFUNC13:29
G is independent implies
'not' Ex(Ex(a,A,G),B,G) = All(All('not' a,B,G),A,G);

theorem :: BVFUNC13:30
G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);

theorem :: BVFUNC13:31
All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);

theorem :: BVFUNC13:32
All('not' Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G);

theorem :: BVFUNC13:33
G is independent implies
All('not' Ex(a,A,G),B,G) = 'not' Ex(Ex(a,B,G),A,G);

theorem :: BVFUNC13:34
G is independent implies
Ex('not' All(a,A,G),B,G) = Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:35
G is independent implies
All('not' All(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:36
G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:37
All('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:38
G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G);

theorem :: BVFUNC13:39
G is independent implies
All('not' Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G);

theorem :: BVFUNC13:40
All('not' Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G);

theorem :: BVFUNC13:41
G is independent implies
All('not' Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G);

theorem :: BVFUNC13:42
G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:43
All('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:44
G is independent implies
Ex('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:45
G is independent implies
All('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:46
All('not' Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G);

theorem :: BVFUNC13:47
G is independent implies
All('not' Ex(a,A,G),B,G) = All(All('not' a,B,G),A,G);

theorem :: BVFUNC13:48
G is independent implies
Ex(All('not' a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);

theorem :: BVFUNC13:49
G is independent implies
All(All('not' a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G);

theorem :: BVFUNC13:50
All(All('not' a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G);

theorem :: BVFUNC13:51
G is independent implies
All(All('not' a,A,G),B,G) '<' 'not' Ex(Ex(a,B,G),A,G);

theorem :: BVFUNC13:52
G is independent implies
Ex(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:53
G is independent implies
All(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:54
G is independent implies
Ex(All('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:55
All(All('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G);

theorem :: BVFUNC13:56
G is independent implies
Ex(All('not' a,A,G),B,G) '<' All('not' All(a,B,G),A,G);

theorem :: BVFUNC13:57
G is independent implies
All(All('not' a,A,G),B,G) '<' All('not' All(a,B,G),A,G);

theorem :: BVFUNC13:58
All(All('not' a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G);

theorem :: BVFUNC13:59
G is independent implies
All(All('not' a,A,G),B,G) = All('not' Ex(a,B,G),A,G);

canceled;

theorem :: BVFUNC13:61
All(Ex('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

theorem :: BVFUNC13:62
G is independent implies
Ex(All('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G);

```