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

theorem :: BVFUNC_3:1
for Y being non empty set
for G being Subset of ()
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))
proof end;

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

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

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

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

theorem :: BVFUNC_3:6
for Y being non empty set
for G being Subset of ()
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
proof end;

theorem :: BVFUNC_3:7
for Y being non empty set
for G being Subset of ()
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))
proof end;

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

theorem :: BVFUNC_3:9
for Y being non empty set
for G being Subset of ()
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))
proof end;

Lm1: now :: thesis: for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of ()
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 ()
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 ()
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 (); :: 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))) & 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 ; :: thesis: verum
end;

theorem :: BVFUNC_3:10
for Y being non empty set
for G being Subset of ()
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))
proof end;

theorem :: BVFUNC_3:11
for Y being non empty set
for G being Subset of ()
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))
proof end;

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

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

Lm2: now :: thesis: for Y being non empty set
for a, b being Function of Y,BOOLEAN
for G being Subset of ()
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 ()
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 ()
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 (); :: 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))) & 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 ; :: thesis: verum
end;

theorem :: BVFUNC_3:14
for Y being non empty set
for G being Subset of ()
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))
proof end;

theorem :: BVFUNC_3:15
for Y being non empty set
for G being Subset of ()
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))
proof end;

theorem :: BVFUNC_3:16
for Y being non empty set
for G being Subset of ()
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)
proof end;

theorem :: BVFUNC_3:17
for Y being non empty set
for G being Subset of ()
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))
proof end;

theorem :: BVFUNC_3:18
for Y being non empty set
for G being Subset of ()
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
proof end;

theorem :: BVFUNC_3:19
for Y being non empty set
for G being Subset of ()
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))
proof end;

theorem :: BVFUNC_3:20
for Y being non empty set
for G being Subset of ()
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 '&' b),PA,G))
proof end;

theorem :: BVFUNC_3:21
for Y being non empty set
for G being Subset of ()
for a, u 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))
proof end;

theorem :: BVFUNC_3:22
for Y being non empty set
for G being Subset of ()
for a, u 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
proof end;

theorem :: BVFUNC_3:23
for Y being non empty set
for G being Subset of ()
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)
proof end;

theorem :: BVFUNC_3:24
for Y being non empty set
for G being Subset of ()
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))
proof end;

theorem :: BVFUNC_3:25
for Y being non empty set
for G being Subset of ()
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))
proof end;

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

theorem :: BVFUNC_3:27
for Y being non empty set
for G being Subset of ()
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 '&' ()),PA,G))
proof end;

theorem :: BVFUNC_3:28
for Y being non empty set
for G being Subset of ()
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)) '&' (All ((a 'imp' ()),PA,G)))
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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