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

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;
then (All (a 'or' b),PA,G) . z = FALSE by BVFUNC_2:def 9;
hence contradiction by A1; :: 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;
then (All (a 'imp' b),PA,G) . z = FALSE by BVFUNC_2:def 9;
hence contradiction by A1; :: 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;