The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part VI

by

Shunichi Kobayashi

Received October 19, 1999

MML identifier: BVFUNC14

[ Mizar article, MML identifier index ]

environ

 vocabulary EQREL_1, T_1TOPSP, PARTIT1, BOOLE, SETFAM_1, FUNCOP_1, RELAT_1,
      FUNCT_1, CANTOR_1, CAT_1, FUNCT_4, BVFUNC_2;
 notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
      SETFAM_1, EQREL_1, CANTOR_1, CQC_LANG, PARTIT1, BVFUNC_1, BVFUNC_2,
      FUNCT_4;
 constructors DOMAIN_1, CANTOR_1, BVFUNC_2, BVFUNC_1, FUNCT_4;
 clusters PARTIT1, SUBSET_1, FUNCT_4, CQC_LANG, XBOOLE_0;
 requirements SUBSET, BOOLE;


begin :: Chap. 1  Preliminaries

reserve Y for non empty set,

        G for Subset of PARTITIONS(Y),
        A,B,C,D for a_partition of Y;

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

theorem :: BVFUNC14:2
  G={A,B} & A<>B implies
'/\' G = A '/\' B;

theorem :: BVFUNC14:3
  G={B,C,D} & B<>C & C<>D & D<>B implies
'/\' G = B '/\' C '/\' D;

theorem :: BVFUNC14:4
G={A,B,C} & A<>B & C<>A implies
CompF(A,G) = B '/\' C;

theorem :: BVFUNC14:5
G={A,B,C} & A<>B & B<>C implies CompF(B,G) = C '/\' A;

theorem :: BVFUNC14:6
  G={A,B,C} & B<>C & C<>A implies CompF(C,G) = A '/\' B;

theorem :: BVFUNC14:7
G={A,B,C,D} & A<>B & A<>C & A<>D implies
CompF(A,G) = B '/\' C '/\' D;

theorem :: BVFUNC14:8
G={A,B,C,D} & A<>B & B<>C & B<>D implies
CompF(B,G) = A '/\' C '/\' D;

theorem :: BVFUNC14:9
  G={A,B,C,D} & A<>C & B<>C & C<>D implies
CompF(C,G) = A '/\' B '/\' D;

theorem :: BVFUNC14:10
  G={A,B,C,D} & A<>D & B<>D & C<>D implies
CompF(D,G) = A '/\' C '/\' B;

canceled 3;

theorem :: BVFUNC14:14
   for B,C,D,b,c,d being set
  holds dom((B .--> b) +* (C .--> c) +* (D .--> d)) = {B,C,D};

theorem :: BVFUNC14:15
   for f being Function, C,D,c,d being set st C<>D
  holds (f +* (C .--> c) +* (D .--> d)).C = c;

theorem :: BVFUNC14:16
   for B,C,D,b,c,d being set st B<>C & D<>B
  holds ((B .--> b) +* (C .--> c) +* (D .--> d)).B = b;

theorem :: BVFUNC14:17
   for B,C,D,b,c,d being set, h being Function
  st h = (B .--> b) +* (C .--> c) +* (D .--> d)
 holds rng h = {h.B,h.C,h.D};

:: from BVFUNC20

theorem :: BVFUNC14:18
for h being Function, A',B',C',D' being set st
G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds h.B = B' & h.C = C' & h.D = D';

theorem :: BVFUNC14:19
for A,B,C,D being set,h being Function, A',B',C',D' being set st
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds dom h = {A,B,C,D};

theorem :: BVFUNC14:20
for h being Function,A',B',C',D' being set st G={A,B,C,D} &
h = (B .--> B') +* (C .--> C') +* (D .--> D') +* (A .--> A')
holds rng h = {h.A,h.B,h.C,h.D};

theorem :: BVFUNC14:21
  for z,u being Element of Y, h being Function
st G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D
holds EqClass(u,B '/\' C '/\' D) meets EqClass(z,A);

theorem :: BVFUNC14:22
  for z,u being Element of Y
st G is independent & G={A,B,C,D} & A<>B & A<>C & A<>D & B<>C & B<>D & C<>D &
EqClass(z,C '/\' D)=EqClass(u,C '/\' D)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G));

theorem :: BVFUNC14:23
   for z,u being Element of Y st
 G is independent & G={A,B,C} & A<>B & B<>C & C<>A &
EqClass(z,C)=EqClass(u,C)
holds EqClass(u,CompF(A,G)) meets EqClass(z,CompF(B,G));