:: Predicate Calculus for Boolean Valued Functions, { I }
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received December 21, 1998
:: Copyright (c) 1998-2011 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 Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds 'not' ((All (a,PA,G)) '&' (All (b,PA,G))) = (Ex (('not' a),PA,G)) 'or' (Ex (('not' b),PA,G))

proof end;

theorem :: BVFUNC_3:5

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds 'not' ((Ex (a,PA,G)) '&' (Ex (b,PA,G))) = (All (('not' a),PA,G)) 'or' (All (('not' b),PA,G))

proof end;

theorem :: BVFUNC_3:6

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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))))

proof end;

theorem :: BVFUNC_3:9

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs (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

let Y be non empty set ; :: thesis: for a, b being Element of Funcs (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 Element of Funcs (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))) & not (a 'or' b) . x = TRUE ) ; :: thesis: contradiction
then (B_INF ((a 'or' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def 19;
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 Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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

let Y be non empty set ; :: thesis: for a, b being Element of Funcs (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 Element of Funcs (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))) & not (a 'imp' b) . x = TRUE ) ; :: thesis: contradiction
then (B_INF ((a 'imp' b),(CompF (PA,G)))) . z = FALSE by BVFUNC_1:def 19;
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 Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for u, a being Element of Funcs (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 (PARTITIONS Y)
for u, a being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) = All ((('not' a) 'or' b),PA,G)

proof end;

theorem :: BVFUNC_3:27

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds All ((a 'imp' b),PA,G) = 'not' (Ex ((a '&' ('not' b)),PA,G))

proof end;

theorem :: BVFUNC_3:28

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds Ex (a,PA,G) '<' 'not' ((All ((a 'imp' b),PA,G)) '&' (All ((a 'imp' ('not' b)),PA,G)))

proof end;

theorem :: BVFUNC_3:29

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds Ex (a,PA,G) '<' 'not' (('not' (Ex ((a '&' b),PA,G))) '&' ('not' (Ex ((a '&' ('not' b)),PA,G))))

proof end;

theorem :: BVFUNC_3:30

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, b being Element of Funcs (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 (PARTITIONS Y)
for a, c, b being Element of Funcs (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 (PARTITIONS Y)
for c, b, a being Element of Funcs (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 (PARTITIONS Y)
for b, c, a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (All ((a 'imp' c),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)

proof end;

theorem :: BVFUNC_3:35

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((a 'imp' ('not' c)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)

proof end;

theorem :: BVFUNC_3:36

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds (All ((b 'imp' ('not' c)),PA,G)) '&' (Ex ((a '&' c),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)

proof end;

theorem :: BVFUNC_3:37

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (Ex ((a '&' ('not' c)),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)

proof end;

theorem :: BVFUNC_3:38

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for c, b, a being Element of Funcs (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 (PARTITIONS Y)
for b, c, a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds (All ((b 'imp' c),PA,G)) '&' (All ((c 'imp' ('not' a)),PA,G)) '<' All ((a 'imp' ('not' b)),PA,G)

proof end;

theorem :: BVFUNC_3:40

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for b, c, a being Element of Funcs (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 (PARTITIONS Y)
for c, b, a being Element of Funcs (Y,BOOLEAN)
for PA being a_partition of Y holds ((Ex (c,PA,G)) '&' (All ((b 'imp' ('not' c)),PA,G))) '&' (All ((c 'imp' a),PA,G)) '<' Ex ((a '&' ('not' b)),PA,G)

proof end;