The abstract of the Mizar article:

Predicate Calculus for Boolean Valued Functions. Part II

by

Shunichi Kobayashi, and

Yatsuka Nakamura

Received March 13, 1999

MML identifier: BVFUNC_4

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, PARTIT1, BVFUNC_1, ZF_LANG, FUNCT_1, RELAT_1,
      BINARITH, EQREL_1, BVFUNC_2, T_1TOPSP;
 notation TARSKI, XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, RELAT_1, FUNCT_1,
      FRAENKEL, EQREL_1, BINARITH, BVFUNC_1, BVFUNC_2;
 constructors BINARITH, BVFUNC_2, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;
 requirements SUBSET, BOOLE;


begin

::Chap. 1  Preliminaries

reserve Y for non empty set;

theorem :: BVFUNC_4:1
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a '<' (b 'imp' c) implies a '&' b '<' c;

theorem :: BVFUNC_4:2
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
a '&' b '<' c implies a '<' (b 'imp' c);

theorem :: BVFUNC_4:3
for a,b being Element of Funcs(Y,BOOLEAN) holds
  a 'or' (a '&' b) = a;

theorem :: BVFUNC_4:4
for a,b being Element of Funcs(Y,BOOLEAN) holds
  a '&' (a 'or' b) = a;

theorem :: BVFUNC_4:5
for a being Element of Funcs(Y,BOOLEAN) holds
a '&' 'not' a = O_el(Y);

theorem :: BVFUNC_4:6
for a being Element of Funcs(Y,BOOLEAN) holds
a 'or' 'not' a = I_el(Y);

theorem :: BVFUNC_4:7
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' b = (a 'imp' b) '&' (b 'imp' a);

theorem :: BVFUNC_4:8
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'imp' b = 'not' a 'or' b;

theorem :: BVFUNC_4:9
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'xor' b = ('not' a '&' b) 'or' (a '&' 'not' b);

theorem :: BVFUNC_4:10
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) iff ((a 'imp' b)=I_el(Y) & (b 'imp' a)=I_el(Y));

theorem :: BVFUNC_4:11
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) & (b 'eqv' c)=I_el(Y) implies (a 'eqv' c)=I_el(Y);

theorem :: BVFUNC_4:12
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'eqv' b=I_el(Y) implies 'not' a 'eqv' 'not' b=I_el(Y);

theorem :: BVFUNC_4:13
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) & (c 'eqv' d)=I_el(Y) implies
((a '&' c) 'eqv' (b '&' d))=I_el(Y);

theorem :: BVFUNC_4:14
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) & (c 'eqv' d)=I_el(Y) implies
((a 'imp' c) 'eqv' (b 'imp' d))=I_el(Y);

theorem :: BVFUNC_4:15
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) & (c 'eqv' d)=I_el(Y) implies
((a 'or' c) 'eqv' (b 'or' d))=I_el(Y);

theorem :: BVFUNC_4:16
for a,b,c,d being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b)=I_el(Y) & (c 'eqv' d)=I_el(Y) implies
((a 'eqv' c) 'eqv' (b 'eqv' d))=I_el(Y);

begin

::Chap. 2  Predicate Calculus

theorem :: BVFUNC_4:17
for a,b being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
PA being a_partition of Y holds
All(a 'eqv' b,PA,G) = All(a 'imp' b,PA,G) '&' All(b 'imp' a,PA,G);

theorem :: BVFUNC_4:18
for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA,PB being a_partition of Y holds
All(a,PA,G) '<' Ex(a,PB,G);

theorem :: BVFUNC_4:19
for a,u being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA being a_partition of Y
st G is independent & PA in G & u is_independent_of PA,G holds
a 'imp' u = I_el(Y) implies All(a,PA,G) 'imp' u = I_el(Y);

theorem :: BVFUNC_4:20
for u being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA being a_partition of Y
st u is_independent_of PA,G holds
Ex(u,PA,G) '<' u;

theorem :: BVFUNC_4:21
for u being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA being a_partition of Y
st u is_independent_of PA,G holds
u '<' All(u,PA,G);

theorem :: BVFUNC_4:22
for u being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA,PB being a_partition of Y
st u is_independent_of PB,G holds
All(u,PA,G) '<' All(u,PB,G);

theorem :: BVFUNC_4:23
for u being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA,PB being a_partition of Y
st u is_independent_of PA,G holds
Ex(u,PA,G) '<' Ex(u,PB,G);

theorem :: BVFUNC_4:24
for a,b being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
PA being a_partition of Y holds
All(a 'eqv' b,PA,G) '<' All(a,PA,G) 'eqv' All(b,PA,G);

theorem :: BVFUNC_4:25
for a,b being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
PA being a_partition of Y holds
All(a '&' b,PA,G) '<' a '&' All(b,PA,G);

theorem :: BVFUNC_4:26
for a,u being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
PA being a_partition of Y holds
All(a,PA,G) 'imp' u '<' Ex(a 'imp' u,PA,G);

theorem :: BVFUNC_4:27
for a,b being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA being a_partition of Y holds
(a 'eqv' b)=I_el(Y) implies (All(a,PA,G) 'eqv' All(b,PA,G))=I_el(Y);

theorem :: BVFUNC_4:28
for a,b being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y), PA being a_partition of Y holds
(a 'eqv' b)=I_el(Y) implies (Ex(a,PA,G) 'eqv' Ex(b,PA,G))=I_el(Y);