The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part V

by

Shunichi Kobayashi, and

Yatsuka Nakamura

Received August 17, 1999

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);