:: Predicate Calculus for Boolean Valued Functions, V
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received August 17, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem Th1: :: BVFUNC13:1
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 '<' 'not' (All (All a,B,G),A,G)
theorem Th2: :: BVFUNC13:2
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 ('not' a),A,G),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem Th3: :: BVFUNC13:3
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 ('not' (Ex a,A,G)),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem Th4: :: BVFUNC13:4
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 (Ex ('not' a),A,G),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem :: BVFUNC13:5
canceled;
theorem :: BVFUNC13:6
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 ('not' a),A,G),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem Th7: :: BVFUNC13:7
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' (Ex a,A,G)),
B,
G '<' 'not' (All (All a,B,G),A,G)
theorem :: BVFUNC13:8
canceled;
theorem :: BVFUNC13:9
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 (Ex a,A,G),B,G) '<' 'not' (Ex (All a,B,G),A,G) by PARTIT_2:11, PARTIT_2:19;
theorem Th10: :: BVFUNC13:10
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' (Ex (Ex a,A,G),B,G) '<' 'not' (Ex (All a,B,G),A,G)
theorem Th11: :: BVFUNC13: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 holds
'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (Ex a,B,G),A,G)
theorem :: BVFUNC13:12
canceled;
theorem :: BVFUNC13:13
canceled;
theorem :: BVFUNC13: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 st
G is
independent holds
'not' (Ex (All a,A,G),B,G) '<' 'not' (All (All a,B,G),A,G)
theorem :: BVFUNC13: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 st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' 'not' (All (All a,B,G),A,G)
theorem :: BVFUNC13: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 holds
'not' (Ex (Ex a,A,G),B,G) '<' 'not' (All (All a,B,G),A,G)
theorem Th17: :: BVFUNC13: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' (Ex (All a,A,G),B,G) '<' Ex ('not' (All a,B,G)),
A,
G
theorem Th18: :: BVFUNC13: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
'not' (All (Ex a,A,G),B,G) '<' Ex ('not' (All a,B,G)),
A,
G
theorem Th19: :: BVFUNC13: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 holds
'not' (Ex (Ex a,A,G),B,G) '<' Ex ('not' (All a,B,G)),
A,
G
theorem Th20: :: BVFUNC13: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 (Ex a,A,G),B,G) '<' All ('not' (All a,B,G)),
A,
G
theorem Th21: :: BVFUNC13: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 st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) '<' All ('not' (All a,B,G)),
A,
G
theorem Th22: :: BVFUNC13: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 (Ex a,A,G),B,G) '<' Ex ('not' (Ex a,B,G)),
A,
G
theorem Th23: :: BVFUNC13: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 st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) = All ('not' (Ex a,B,G)),
A,
G
theorem Th24: :: BVFUNC13: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
'not' (All (Ex a,A,G),B,G) '<' Ex (Ex ('not' a),B,G),
A,
G
theorem Th25: :: BVFUNC13: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
'not' (Ex (Ex a,A,G),B,G) '<' Ex (Ex ('not' a),B,G),
A,
G
theorem Th26: :: BVFUNC13: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 st
G is
independent holds
'not' (All (Ex a,A,G),B,G) '<' All (Ex ('not' a),B,G),
A,
G
theorem Th27: :: BVFUNC13: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 st
G is
independent holds
'not' (Ex (Ex a,A,G),B,G) '<' All (Ex ('not' a),B,G),
A,
G
theorem Th28: :: BVFUNC13:28
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 (Ex a,A,G),B,G) '<' Ex (All ('not' a),B,G),
A,
G
theorem Th29: :: BVFUNC13:29
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' (Ex (Ex a,A,G),B,G) = All (All ('not' a),B,G),
A,
G
theorem :: BVFUNC13:30
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' (Ex a,A,G)),
B,
G '<' 'not' (Ex (All a,B,G),A,G)
theorem :: BVFUNC13:31
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 ('not' (Ex a,A,G)),
B,
G '<' 'not' (Ex (All a,B,G),A,G)
theorem :: BVFUNC13:32
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 ('not' (Ex a,A,G)),
B,
G '<' 'not' (All (Ex a,B,G),A,G)
theorem :: BVFUNC13:33
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' (Ex a,A,G)),
B,
G = 'not' (Ex (Ex a,B,G),A,G)
theorem :: BVFUNC13:34
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 ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:35
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 ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:36
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' (Ex a,A,G)),
B,
G '<' Ex ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:37
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 ('not' (Ex a,A,G)),
B,
G '<' Ex ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:38
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' (Ex a,A,G)),
B,
G '<' All ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:39
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' (Ex a,A,G)),
B,
G '<' All ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:40
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 ('not' (Ex a,A,G)),
B,
G '<' Ex ('not' (Ex a,B,G)),
A,
G
theorem :: BVFUNC13:41
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' (Ex a,A,G)),
B,
G = All ('not' (Ex a,B,G)),
A,
G
theorem :: BVFUNC13:42
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' (Ex a,A,G)),
B,
G '<' Ex (Ex ('not' a),B,G),
A,
G
theorem :: BVFUNC13:43
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 ('not' (Ex a,A,G)),
B,
G '<' Ex (Ex ('not' a),B,G),
A,
G
theorem :: BVFUNC13:44
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' (Ex a,A,G)),
B,
G '<' All (Ex ('not' a),B,G),
A,
G
theorem :: BVFUNC13:45
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' (Ex a,A,G)),
B,
G '<' All (Ex ('not' a),B,G),
A,
G
theorem :: BVFUNC13:46
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 ('not' (Ex a,A,G)),
B,
G '<' Ex (All ('not' a),B,G),
A,
G
theorem :: BVFUNC13:47
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' (Ex a,A,G)),
B,
G = All (All ('not' a),B,G),
A,
G
theorem :: BVFUNC13:48
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 ('not' a),A,G),
B,
G '<' 'not' (Ex (All a,B,G),A,G)
theorem :: BVFUNC13:49
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 ('not' a),A,G),
B,
G '<' 'not' (Ex (All a,B,G),A,G)
theorem :: BVFUNC13:50
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 ('not' a),A,G),
B,
G '<' 'not' (All (Ex a,B,G),A,G)
theorem :: BVFUNC13:51
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 ('not' a),A,G),
B,
G '<' 'not' (Ex (Ex a,B,G),A,G)
theorem :: BVFUNC13:52
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 (Ex ('not' a),A,G),
B,
G '<' Ex ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:53
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 (Ex ('not' a),A,G),
B,
G '<' Ex ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:54
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 ('not' a),A,G),
B,
G '<' Ex ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:55
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 ('not' a),A,G),
B,
G '<' Ex ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:56
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 ('not' a),A,G),
B,
G '<' All ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:57
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 ('not' a),A,G),
B,
G '<' All ('not' (All a,B,G)),
A,
G
theorem :: BVFUNC13:58
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 ('not' a),A,G),
B,
G '<' Ex ('not' (Ex a,B,G)),
A,
G
theorem :: BVFUNC13:59
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 ('not' a),A,G),
B,
G = All ('not' (Ex a,B,G)),
A,
G
theorem :: BVFUNC13:60
canceled;
theorem :: BVFUNC13:61
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 ('not' a),A,G),
B,
G '<' Ex (Ex ('not' a),B,G),
A,
G
theorem :: BVFUNC13:62
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 ('not' a),A,G),
B,
G '<' Ex (Ex ('not' a),B,G),
A,
G