The Mizar article:

Predicate Calculus for Boolean Valued Functions. Part XI

by

Shunichi Kobayashi

Received November 15, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: BVFUNC19

[ MML identifier index ]

environ

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

begin

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

canceled 5;

theorem
G is independent implies
All('not' Ex(a,A,G),B,G) '<' All(All('not' a,B,G),A,G)
proof
  assume G is independent;then
A1:All(All('not' a,B,G),A,G) = All(All('not' a,A,G),B,G) by PARTIT_2:17;
  All('not' Ex(a,A,G),B,G) '<' All(All('not' a,A,G),B,G) by BVFUNC_2:21;
  hence thesis by A1;
end;