:: Predicate Calculus for Boolean Valued Functions, { I }
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

theorem :: BVFUNC_3:1
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds a 'imp' b '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:2
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) '&amp;' (All (b,PA,G)) '<' a '&amp;' b
proofend;

theorem :: BVFUNC_3:3
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds a '&amp;' b '<' (Ex (a,PA,G)) '&amp;' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:4
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' ((All (a,PA,G)) '&amp;' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))
proofend;

theorem :: BVFUNC_3:5
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds 'not' ((Ex (a,PA,G)) '&amp;' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))
proofend;

theorem :: BVFUNC_3:6
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) 'or' (All (b,PA,G)) '<' a 'or' b
proofend;

theorem :: BVFUNC_3:7
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds a 'or' b '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:8
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds a 'xor' b '<' ('not' ((Ex (('not' a),PA,G)) 'xor' (Ex (b,PA,G)))) 'or' ('not' ((Ex (a,PA,G)) 'xor' (Ex (('not' b),PA,G))))
proofend;

theorem :: BVFUNC_3:9
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'or' b),PA,G) '<' (All (a,PA,G)) 'or' (Ex (b,PA,G))
proofend;

Lm1: now__::_thesis:_for_Y_being_non_empty_set_
for_a,_b_being_Function_of_Y,BOOLEAN
for_G_being_Subset_of_(PARTITIONS_Y)
for_PA_being_a_partition_of_Y
for_z_being_Element_of_Y_st_(All_((a_'or'_b),PA,G))_._z_=_TRUE_holds_
for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'or'_b)_._x_=_TRUE
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y
for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let PA be a_partition of Y; ::_thesis: for z being Element of Y st (All ((a 'or' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
let z be Element of Y; ::_thesis: ( (All ((a 'or' b),PA,G)) . z = TRUE implies for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE )
assume A1: (All ((a 'or' b),PA,G)) . z = TRUE ; ::_thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'or' b) . x = TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) &amp; not (a 'or' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'or' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A1, BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3:10
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (All (b,PA,G))
proofend;

theorem :: BVFUNC_3:11
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'or' b),PA,G) '<' (Ex (a,PA,G)) 'or' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:12
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) '&amp;' (All (b,PA,G)) '<' Ex ((a '&amp;' b),PA,G)
proofend;

theorem :: BVFUNC_3:13
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) '&amp;' (Ex (b,PA,G)) '<' Ex ((a '&amp;' b),PA,G)
proofend;

Lm2: now__::_thesis:_for_Y_being_non_empty_set_
for_a,_b_being_Function_of_Y,BOOLEAN
for_G_being_Subset_of_(PARTITIONS_Y)
for_PA_being_a_partition_of_Y
for_z_being_Element_of_Y_st_(All_((a_'imp'_b),PA,G))_._z_=_TRUE_holds_
for_x_being_Element_of_Y_st_x_in_EqClass_(z,(CompF_(PA,G)))_holds_
(a_'imp'_b)_._x_=_TRUE
let Y be non empty set ; ::_thesis: for a, b being Function of Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let a, b be Function of Y,BOOLEAN; ::_thesis: for G being Subset of (PARTITIONS Y)
for PA being a_partition of Y
for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let G be Subset of (PARTITIONS Y); ::_thesis: for PA being a_partition of Y
for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let PA be a_partition of Y; ::_thesis: for z being Element of Y st (All ((a 'imp' b),PA,G)) . z = TRUE holds
for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
let z be Element of Y; ::_thesis: ( (All ((a 'imp' b),PA,G)) . z = TRUE implies for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE )
assume A1: (All ((a 'imp' b),PA,G)) . z = TRUE ; ::_thesis: for x being Element of Y st x in EqClass (z,(CompF (PA,G))) holds
(a 'imp' b) . x = TRUE
assume  ex x being Element of Y st
( x in EqClass (z,(CompF (PA,G))) &amp; not (a 'imp' b) . x = TRUE ) ; ::_thesis: contradiction
then  (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def_16;
hence  contradiction by A1, BVFUNC_2:def_9; ::_thesis: verum
end;

theorem :: BVFUNC_3:14
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:15
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) '<' (Ex (a,PA,G)) 'imp' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:16
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (All (b,PA,G)) '<' All ((a 'imp' b),PA,G)
proofend;

theorem :: BVFUNC_3:17
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds a 'imp' b '<' a 'imp' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:18
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds a 'imp' b '<' (All (a,PA,G)) 'imp' b
proofend;

theorem :: BVFUNC_3:19
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex ((a 'imp' b),PA,G) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:20
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All (a,PA,G) '<' (Ex (b,PA,G)) 'imp' (Ex ((a '&amp;' b),PA,G))
proofend;

theorem :: BVFUNC_3:21
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((u 'imp' a),PA,G) '<' u 'imp' (Ex (a,PA,G))
proofend;

theorem :: BVFUNC_3:22
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for u, a being Function of Y,BOOLEAN
for PA being a_partition of Y st u is_independent_of PA,G holds
Ex ((a 'imp' u),PA,G) '<' (All (a,PA,G)) 'imp' u
proofend;

theorem :: BVFUNC_3:23
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) 'imp' (Ex (b,PA,G)) = Ex ((a 'imp' b),PA,G)
proofend;

theorem :: BVFUNC_3:24
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All (a,PA,G)) 'imp' (All (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
proofend;

theorem :: BVFUNC_3:25
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) 'imp' (Ex (b,PA,G)) '<' (All (a,PA,G)) 'imp' (Ex (b,PA,G))
proofend;

theorem Th26: :: BVFUNC_3:26
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) = All ((('not' a) 'or' b),PA,G)
proofend;

theorem :: BVFUNC_3:27
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) = 'not' (Ex ((a '&amp;' ('not' b)),PA,G))
proofend;

theorem :: BVFUNC_3:28
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex (a,PA,G) '<' 'not' ((All ((a 'imp' b),PA,G)) '&amp;' (All ((a 'imp' ('not' b)),PA,G)))
proofend;

theorem :: BVFUNC_3:29
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds Ex (a,PA,G) '<' 'not' (('not' (Ex ((a '&amp;' b),PA,G))) '&amp;' ('not' (Ex ((a '&amp;' ('not' b)),PA,G))))
proofend;

theorem :: BVFUNC_3:30
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) '&amp;' (All ((a 'imp' b),PA,G)) '<' Ex ((a '&amp;' b),PA,G)
proofend;

theorem :: BVFUNC_3:31
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (Ex (a,PA,G)) '&amp;' ('not' (Ex ((a '&amp;' b),PA,G))) '<' 'not' (All ((a 'imp' b),PA,G))
proofend;

theorem :: BVFUNC_3:32
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, c, b being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((a 'imp' c),PA,G)) '&amp;' (All ((c 'imp' b),PA,G)) '<' All ((a 'imp' b),PA,G)
proofend;

theorem :: BVFUNC_3:33
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((c 'imp' b),PA,G)) '&amp;' (Ex ((a '&amp;' c),PA,G)) '<' Ex ((a '&amp;' b),PA,G)
proofend;

theorem :: BVFUNC_3:34
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&amp;' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
proofend;

theorem :: BVFUNC_3:35
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&amp;' (All ((a 'imp' ('not' c)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
proofend;

theorem :: BVFUNC_3:36
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&amp;' (Ex ((a '&amp;' c),PA,G)) '<' Ex ((a '&amp;' ('not' b)),PA,G)
proofend;

theorem :: BVFUNC_3:37
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&amp;' (Ex ((a '&amp;' ('not' c)),PA,G)) '<' Ex ((a '&amp;' ('not' b)),PA,G)
proofend;

theorem :: BVFUNC_3:38
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&amp;' (All ((c 'imp' b),PA,G))) '&amp;' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&amp;' b),PA,G)
proofend;

theorem :: BVFUNC_3:39
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&amp;' (All ((c 'imp' ('not' a)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)
proofend;

theorem :: BVFUNC_3:40
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (b,PA,G)) '&amp;' (All ((b 'imp' c),PA,G))) '&amp;' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&amp;' b),PA,G)
proofend;

theorem :: BVFUNC_3:41
for Y being non empty set
for G being Subset of (PARTITIONS Y)
for c, b, a being Function of Y,BOOLEAN
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&amp;' (All ((b 'imp' ('not' c)),PA,G))) '&amp;' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&amp;' ('not' b)),PA,G)
proofend;