The abstract of the Mizar article:

Propositional Calculus for Boolean Valued Functions. Part II

by

Shunichi Kobayashi, and

Yatsuka Nakamura

Received March 13, 1999

MML identifier: BVFUNC_6

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_2, MARGREL1, BVFUNC_1, ZF_LANG, BINARITH;
 notation XBOOLE_0, SUBSET_1, FRAENKEL, MARGREL1, VALUAT_1, BINARITH, BVFUNC_1;
 constructors BINARITH, BVFUNC_1;
 clusters MARGREL1, VALUAT_1, BINARITH, FRAENKEL;


begin

::Chap. 1  Propositional Calculus

reserve Y for non empty set;

theorem :: BVFUNC_6:1
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (b 'imp' (a '&' b))=I_el(Y);

theorem :: BVFUNC_6:2
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b) 'imp' ((b 'imp' a) 'imp' (a 'eqv' b))=I_el(Y);

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

theorem :: BVFUNC_6:4
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a '&' b) 'imp' c) 'imp' (a 'imp' (b 'imp' c))=I_el(Y);

theorem :: BVFUNC_6:5
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' (b 'imp' c)) 'imp' ((a '&' b) 'imp' c)=I_el(Y);

theorem :: BVFUNC_6:6
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(c 'imp' a) 'imp' ((c 'imp' b) 'imp' (c 'imp' (a '&' b)))=I_el(Y);

theorem :: BVFUNC_6:7
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a 'or' b) 'imp' c) 'imp' ((a 'imp' c) 'or' (b 'imp' c))=I_el(Y);

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

theorem :: BVFUNC_6:9
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a 'imp' c) '&' (b 'imp' c)) 'imp' ((a 'or' b) 'imp' c)=I_el(Y);

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

theorem :: BVFUNC_6:11
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a 'or' b) '&' (a 'or' c)) 'imp' (a 'or' (b '&' c))=I_el(Y);

theorem :: BVFUNC_6:12
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a '&' (b 'or' c)) 'imp' ((a '&' b) 'or' (a '&' c))=I_el(Y);

theorem :: BVFUNC_6:13
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a 'or' c) '&' (b 'or' c)) 'imp' ((a '&' b) 'or' c)=I_el(Y);

theorem :: BVFUNC_6:14
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a 'or' b) '&' c) 'imp' ((a '&' c) 'or' (b '&' c))=I_el(Y);

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

theorem :: BVFUNC_6:16
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b)=I_el(Y) implies (a 'or' c) 'imp' (b 'or' c)=I_el(Y);

theorem :: BVFUNC_6:17
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' b)=I_el(Y) implies (a '&' c) 'imp' (b '&' c)=I_el(Y);

theorem :: BVFUNC_6:18
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(c 'imp' a)=I_el(Y) & (c 'imp' b)=I_el(Y) implies
c 'imp' (a '&' b)=I_el(Y);

theorem :: BVFUNC_6:19
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'imp' c)=I_el(Y) & (b 'imp' c)=I_el(Y) implies
(a 'or' b) 'imp' c = I_el(Y);

theorem :: BVFUNC_6:20
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'or' b)=I_el(Y) & 'not' a=I_el(Y) implies b=I_el(Y);

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

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

theorem :: BVFUNC_6:23
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a '&' 'not' b) 'imp' 'not' a=I_el(Y) implies (a 'imp' b)=I_el(Y);

canceled;

theorem :: BVFUNC_6:25
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'imp' 'not' b=I_el(Y) implies b 'imp' 'not' a=I_el(Y);

theorem :: BVFUNC_6:26
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not' a 'imp' b=I_el(Y) implies 'not' b 'imp' a=I_el(Y);

theorem :: BVFUNC_6:27
for a,b being Element of Funcs(Y,BOOLEAN) holds
a 'imp' (a 'or' b)=I_el(Y);

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

theorem :: BVFUNC_6:29
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not'( a 'or' b) 'imp' ('not' a '&' 'not' b)=I_el(Y);

theorem :: BVFUNC_6:30
for a,b being Element of Funcs(Y,BOOLEAN) holds
('not' a '&' 'not' b) 'imp' 'not'( a 'or' b)=I_el(Y);

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

theorem :: BVFUNC_6:32
for a being Element of Funcs(Y,BOOLEAN) holds
(a 'or' a) 'imp' a=I_el(Y);

theorem :: BVFUNC_6:33
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a '&' 'not' a) 'imp' b=I_el(Y);

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

theorem :: BVFUNC_6:35
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' 'not'( a 'imp' 'not' b)=I_el(Y);

theorem :: BVFUNC_6:36
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not'( a 'imp' 'not' b) 'imp' (a '&' b)=I_el(Y);

theorem :: BVFUNC_6:37
for a,b being Element of Funcs(Y,BOOLEAN) holds
'not'( a '&' b) 'imp' ('not' a 'or' 'not' b)=I_el(Y);

theorem :: BVFUNC_6:38
for a,b being Element of Funcs(Y,BOOLEAN) holds
('not' a 'or' 'not' b) 'imp' 'not'( a '&' b)=I_el(Y);

theorem :: BVFUNC_6:39
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' a=I_el(Y);

theorem :: BVFUNC_6:40
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' (a 'or' b)=I_el(Y);

theorem :: BVFUNC_6:41
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a '&' b) 'imp' b=I_el(Y);

theorem :: BVFUNC_6:42
for a being Element of Funcs(Y,BOOLEAN) holds
a 'imp' a '&' a=I_el(Y);

theorem :: BVFUNC_6:43
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) 'imp' (a 'imp' b)=I_el(Y);

theorem :: BVFUNC_6:44
for a,b being Element of Funcs(Y,BOOLEAN) holds
(a 'eqv' b) 'imp' (b 'imp' a)=I_el(Y);

theorem :: BVFUNC_6:45
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a 'or' b) 'or' c) 'imp' (a 'or' (b 'or' c))=I_el(Y);

theorem :: BVFUNC_6:46
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
((a '&' b) '&' c) 'imp' (a '&' (b '&' c))=I_el(Y);

theorem :: BVFUNC_6:47
for a,b,c being Element of Funcs(Y,BOOLEAN) holds
(a 'or' (b 'or' c)) 'imp' ((a 'or' b) 'or' c)=I_el(Y);