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

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

by
Shunichi Kobayashi

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

```