:: Predicate Calculus for Boolean Valued Functions, III
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received July 14, 1999
:: Copyright (c) 1999 Association of Mizar Users

theorem Th1: :: BVFUNC11:1

for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y st PA '<' PB holds
EqClass z,PA c= EqClass z,PB

proof end;

theorem :: BVFUNC11:2

for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass z,PA c= EqClass z,(PA '\/' PB) by Th1, PARTIT1:19;

theorem :: BVFUNC11:3

for Y being non empty set
for z being Element of Y
for PA, PB being a_partition of Y holds EqClass z,(PA '/\' PB) c= EqClass z,PA by Th1, PARTIT1:17;

theorem :: BVFUNC11:4

for Y being non empty set
for z being Element of Y
for PA being a_partition of Y holds
( EqClass z,PA c= EqClass z,(%O Y) & EqClass z,(%I Y) c= EqClass z,PA ) by Th1, PARTIT1:36;

theorem :: BVFUNC11:5

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds
for a, b being set st a in A & b in B holds
a meets b

proof end;

theorem :: BVFUNC11:6

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent & G = {A,B} & A <> B holds
'/\' G = A '/\' B

proof end;

theorem :: BVFUNC11:7

for Y being non empty set
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G = {A,B} & A <> B holds
CompF A,G = B

proof end;

theorem Th8: :: BVFUNC11:8

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

proof end;

theorem :: BVFUNC11:9

canceled;

theorem :: BVFUNC11:10

canceled;

theorem :: BVFUNC11:11

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (All a,A,G),B,G '<' Ex (All a,B,G),A,G

proof end;

theorem :: BVFUNC11:12

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (All a,A,G),B,G '<' Ex (Ex a,B,G),A,G

proof end;

theorem :: BVFUNC11:13

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All (All a,A,G),B,G '<' All (Ex a,B,G),A,G

proof end;

theorem :: BVFUNC11:14

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (Ex a,A,G),B,G '<' Ex (Ex a,B,G),A,G

proof end;

theorem :: BVFUNC11:15

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

proof end;

theorem Th16: :: BVFUNC11:16

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex ('not' (All a,A,G)),B,G '<' Ex (Ex ('not' a),B,G),A,G

proof end;

theorem Th17: :: BVFUNC11:17

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (All a,A,G),B,G) = Ex ('not' (All a,B,G)),A,G

proof end;

theorem :: BVFUNC11:18

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
All ('not' (All a,A,G)),B,G '<' Ex (Ex ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC11:19

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (All a,A,G),B,G) = Ex (Ex ('not' a),B,G),A,G

proof end;

theorem :: BVFUNC11:20

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
'not' (All (All a,A,G),B,G) '<' Ex (Ex ('not' a),A,G),B,G

proof end;

theorem :: BVFUNC11:21

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

proof end;

theorem :: BVFUNC11:22

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

proof end;

theorem :: BVFUNC11:23

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

proof end;

theorem :: BVFUNC11:24

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent holds
Ex (All a,A,G),B,G '<' Ex (Ex a,B,G),A,G

proof end;

theorem :: BVFUNC11:25

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (All a,A,G),B,G '<' All (Ex a,A,G),B,G

proof end;

theorem :: BVFUNC11:26

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds All (All a,A,G),B,G '<' Ex (Ex a,A,G),B,G

proof end;

theorem :: BVFUNC11:27

for Y being non empty set
for a being Element of Funcs Y,BOOLEAN
for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y holds Ex (All a,A,G),B,G '<' Ex (Ex a,A,G),B,G

proof end;