:: Predicate Calculus for Boolean Valued Functions, { VI }
:: by Shunichi Kobayashi
::
:: Received October 19, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem Th1: :: BVFUNC14:1
theorem :: BVFUNC14:2
Lm1:
for B, C, D, b, c, d being set holds dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D}
Lm2:
for f being Function
for C, D, c, d being set st C <> D holds
((f +* (C .--> c)) +* (D .--> d)) . C = c
Lm3:
for B, C, D, b, c, d being set st B <> C & D <> B holds
(((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b
Lm4:
for B, C, D, b, c, d being set
for h being Function st h = ((B .--> b) +* (C .--> c)) +* (D .--> d) holds
rng h = {(h . B),(h . C),(h . D)}
theorem :: BVFUNC14:3
theorem Th4: :: BVFUNC14:4
theorem Th5: :: BVFUNC14:5
theorem :: BVFUNC14:6
theorem Th7: :: BVFUNC14:7
theorem Th8: :: BVFUNC14:8
theorem :: BVFUNC14:9
theorem :: BVFUNC14:10
theorem :: BVFUNC14:11
canceled;
theorem :: BVFUNC14:12
canceled;
theorem :: BVFUNC14:13
canceled;
theorem :: BVFUNC14:14
theorem TH15: :: BVFUNC14:15
theorem :: BVFUNC14:16
theorem :: BVFUNC14:17
theorem Th18: :: BVFUNC14:18
theorem Th19: :: BVFUNC14:19
theorem Th20: :: BVFUNC14:20
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D being
a_partition of
Y for
h being
Function for
A',
B',
C',
D' being
set st
G = {A,B,C,D} &
h = (((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D)}
theorem :: BVFUNC14:21
theorem :: BVFUNC14:22
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D} &
A <> B &
A <> C &
A <> D &
B <> C &
B <> D &
C <> D &
EqClass z,
(C '/\' D) = EqClass u,
(C '/\' D) holds
EqClass u,
(CompF A,G) meets EqClass z,
(CompF B,G)
theorem :: BVFUNC14:23
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C} &
A <> B &
B <> C &
C <> A &
EqClass z,
C = EqClass u,
C holds
EqClass u,
(CompF A,G) meets EqClass z,
(CompF B,G)
theorem Th24: :: BVFUNC14:24
theorem Th25: :: BVFUNC14:25
theorem Th26: :: BVFUNC14:26
theorem Th27: :: BVFUNC14:27
theorem :: BVFUNC14:28
theorem Th29: :: BVFUNC14:29
theorem Th30: :: BVFUNC14:30
for
A,
B,
C,
D,
E being
set for
h being
Function for
A',
B',
C',
D',
E' being
set st
h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') holds
dom h = {A,B,C,D,E}
theorem Th31: :: BVFUNC14:31
for
A,
B,
C,
D,
E being
set for
h being
Function for
A',
B',
C',
D',
E' being
set st
h = ((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E)}
theorem :: BVFUNC14:32
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E being
a_partition of
Y for
z,
u being
Element of
Y for
h being
Function st
G is
independent &
G = {A,B,C,D,E} &
A <> B &
A <> C &
A <> D &
A <> E &
B <> C &
B <> D &
B <> E &
C <> D &
C <> E &
D <> E holds
EqClass u,
(((B '/\' C) '/\' D) '/\' E) meets EqClass z,
A
theorem :: BVFUNC14:33
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D,E} &
A <> B &
A <> C &
A <> D &
A <> E &
B <> C &
B <> D &
B <> E &
C <> D &
C <> E &
D <> E &
EqClass z,
((C '/\' D) '/\' E) = EqClass u,
((C '/\' D) '/\' E) holds
EqClass u,
(CompF A,G) meets EqClass z,
(CompF B,G)
theorem Th34: :: BVFUNC14:34
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y st
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F holds
CompF A,
G = (((B '/\' C) '/\' D) '/\' E) '/\' F
theorem Th35: :: BVFUNC14:35
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y st
G is
independent &
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F holds
CompF B,
G = (((A '/\' C) '/\' D) '/\' E) '/\' F
theorem Th36: :: BVFUNC14:36
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y st
G is
independent &
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F holds
CompF C,
G = (((A '/\' B) '/\' D) '/\' E) '/\' F
theorem Th37: :: BVFUNC14:37
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y st
G is
independent &
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F holds
CompF D,
G = (((A '/\' B) '/\' C) '/\' E) '/\' F
theorem Th38: :: BVFUNC14:38
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y st
G is
independent &
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F holds
CompF E,
G = (((A '/\' B) '/\' C) '/\' D) '/\' F
theorem :: BVFUNC14:39
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y st
G is
independent &
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F holds
CompF F,
G = (((A '/\' B) '/\' C) '/\' D) '/\' E
theorem Th40: :: BVFUNC14:40
for
A,
B,
C,
D,
E,
F being
set for
h being
Function for
A',
B',
C',
D',
E',
F' being
set st
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F &
h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
(
h . A = A' &
h . B = B' &
h . C = C' &
h . D = D' &
h . E = E' &
h . F = F' )
theorem Th41: :: BVFUNC14:41
for
A,
B,
C,
D,
E,
F being
set for
h being
Function for
A',
B',
C',
D',
E',
F' being
set st
h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F}
theorem Th42: :: BVFUNC14:42
for
A,
B,
C,
D,
E,
F being
set for
h being
Function for
A',
B',
C',
D',
E',
F' being
set st
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F &
h = (((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F)}
theorem :: BVFUNC14:43
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y for
z,
u being
Element of
Y for
h being
Function st
G is
independent &
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F holds
EqClass u,
((((B '/\' C) '/\' D) '/\' E) '/\' F) meets EqClass z,
A
theorem :: BVFUNC14:44
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F being
a_partition of
Y for
z,
u being
Element of
Y for
h being
Function st
G is
independent &
G = {A,B,C,D,E,F} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
B <> C &
B <> D &
B <> E &
B <> F &
C <> D &
C <> E &
C <> F &
D <> E &
D <> F &
E <> F &
EqClass z,
(((C '/\' D) '/\' E) '/\' F) = EqClass u,
(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,
(CompF A,G) meets EqClass z,
(CompF B,G)
theorem TH1: :: BVFUNC14:45
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF A,
G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
theorem Th2: :: BVFUNC14:46
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF B,
G = ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
theorem Th3: :: BVFUNC14:47
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF C,
G = ((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J
theorem Th4: :: BVFUNC14:48
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF D,
G = ((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J
theorem Th5: :: BVFUNC14:49
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF E,
G = ((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J
theorem Th6: :: BVFUNC14:50
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF F,
G = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J
theorem :: BVFUNC14:51
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y st
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
CompF J,
G = ((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F
theorem Th8: :: BVFUNC14:52
for
A,
B,
C,
D,
E,
F,
J being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J' being
set st
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J &
h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
(
h . A = A' &
h . B = B' &
h . C = C' &
h . D = D' &
h . E = E' &
h . F = F' &
h . J = J' )
theorem Th9: :: BVFUNC14:53
for
A,
B,
C,
D,
E,
F,
J being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J' being
set st
h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J}
theorem Th10: :: BVFUNC14:54
for
A,
B,
C,
D,
E,
F,
J being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J' being
set st
h = ((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J)}
theorem :: BVFUNC14:55
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J holds
EqClass u,
(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,
A
theorem :: BVFUNC14:56
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D,E,F,J} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
C <> D &
C <> E &
C <> F &
C <> J &
D <> E &
D <> F &
D <> J &
E <> F &
E <> J &
F <> J &
EqClass z,
((((C '/\' D) '/\' E) '/\' F) '/\' J) = EqClass u,
((((C '/\' D) '/\' E) '/\' F) '/\' J) holds
EqClass u,
(CompF A,G) meets EqClass z,
(CompF B,G)
theorem Th13: :: BVFUNC14:57
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF A,
G = (((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
theorem Th14: :: BVFUNC14:58
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF B,
G = (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
theorem Th15: :: BVFUNC14:59
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF C,
G = (((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
theorem Th16: :: BVFUNC14:60
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF D,
G = (((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J) '/\' M
theorem Th17: :: BVFUNC14:61
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF E,
G = (((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J) '/\' M
theorem Th18: :: BVFUNC14:62
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF F,
G = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J) '/\' M
theorem Th19: :: BVFUNC14:63
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF J,
G = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' M
theorem :: BVFUNC14:64
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
CompF M,
G = (((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J
theorem Th21: :: BVFUNC14:65
for
A,
B,
C,
D,
E,
F,
J,
M being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J',
M' being
set st
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M &
h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
(
h . B = B' &
h . C = C' &
h . D = D' &
h . E = E' &
h . F = F' &
h . J = J' )
theorem Th22: :: BVFUNC14:66
for
A,
B,
C,
D,
E,
F,
J,
M being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J',
M' being
set st
h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J,M}
theorem Th23: :: BVFUNC14:67
for
A,
B,
C,
D,
E,
F,
J,
M being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J',
M' being
set st
h = (((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M)}
theorem :: BVFUNC14:68
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M holds
(EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) /\ (EqClass z,A) <> {}
theorem :: BVFUNC14:69
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D,E,F,J,M} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
D <> E &
D <> F &
D <> J &
D <> M &
E <> F &
E <> J &
E <> M &
F <> J &
F <> M &
J <> M &
EqClass z,
(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,
(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) holds
EqClass u,
(CompF A,G) meets EqClass z,
(CompF B,G)
definition
canceled;
end;
:: deftheorem BVFUNC14:def 1 :
canceled;
Lm1:
for x1, x2, x3, x4, x5, x6, x7, x8, x9 being set holds {x1,x2,x3,x4,x5,x6,x7,x8,x9} = {x1,x2,x3,x4} \/ {x5,x6,x7,x8,x9}
theorem :: BVFUNC14:70
canceled;
theorem :: BVFUNC14:71
canceled;
theorem :: BVFUNC14:72
canceled;
theorem :: BVFUNC14:73
canceled;
theorem :: BVFUNC14:74
canceled;
theorem :: BVFUNC14:75
canceled;
theorem :: BVFUNC14:76
canceled;
theorem :: BVFUNC14:77
canceled;
theorem :: BVFUNC14:78
canceled;
theorem Th35: :: BVFUNC14:79
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF A,
G = ((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
theorem Th36: :: BVFUNC14:80
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF B,
G = ((((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
theorem Th37: :: BVFUNC14:81
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF C,
G = ((((((A '/\' B) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
theorem Th38: :: BVFUNC14:82
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF D,
G = ((((((A '/\' B) '/\' C) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N
theorem Th39: :: BVFUNC14:83
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF E,
G = ((((((A '/\' B) '/\' C) '/\' D) '/\' F) '/\' J) '/\' M) '/\' N
theorem Th40: :: BVFUNC14:84
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF F,
G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' J) '/\' M) '/\' N
theorem Th41: :: BVFUNC14:85
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF J,
G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' M) '/\' N
theorem Th42: :: BVFUNC14:86
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF M,
G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' N
theorem :: BVFUNC14:87
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y st
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
CompF N,
G = ((((((A '/\' B) '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M
theorem Th44: :: BVFUNC14:88
for
A,
B,
C,
D,
E,
F,
J,
M,
N being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J',
M',
N' being
set st
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N &
h = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
(
h . A = A' &
h . B = B' &
h . C = C' &
h . D = D' &
h . E = E' &
h . F = F' &
h . J = J' &
h . M = M' &
h . N = N' )
theorem Th45: :: BVFUNC14:89
for
A,
B,
C,
D,
E,
F,
J,
M,
N being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J',
M',
N' being
set st
h = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
dom h = {A,B,C,D,E,F,J,M,N}
theorem Th46: :: BVFUNC14:90
for
A,
B,
C,
D,
E,
F,
J,
M,
N being
set for
h being
Function for
A',
B',
C',
D',
E',
F',
J',
M',
N' being
set st
h = ((((((((B .--> B') +* (C .--> C')) +* (D .--> D')) +* (E .--> E')) +* (F .--> F')) +* (J .--> J')) +* (M .--> M')) +* (N .--> N')) +* (A .--> A') holds
rng h = {(h . A),(h . B),(h . C),(h . D),(h . E),(h . F),(h . J),(h . M),(h . N)}
theorem :: BVFUNC14:91
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N holds
(EqClass u,(((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N)) /\ (EqClass z,A) <> {}
theorem :: BVFUNC14:92
for
Y being non
empty set for
G being
Subset of
(PARTITIONS Y) for
A,
B,
C,
D,
E,
F,
J,
M,
N being
a_partition of
Y for
z,
u being
Element of
Y st
G is
independent &
G = {A,B,C,D,E,F,J,M,N} &
A <> B &
A <> C &
A <> D &
A <> E &
A <> F &
A <> J &
A <> M &
A <> N &
B <> C &
B <> D &
B <> E &
B <> F &
B <> J &
B <> M &
B <> N &
C <> D &
C <> E &
C <> F &
C <> J &
C <> M &
C <> N &
D <> E &
D <> F &
D <> J &
D <> M &
D <> N &
E <> F &
E <> J &
E <> M &
E <> N &
F <> J &
F <> M &
F <> N &
J <> M &
J <> N &
M <> N &
EqClass z,
((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) = EqClass u,
((((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) '/\' N) holds
EqClass u,
(CompF A,G) meets EqClass z,
(CompF B,G)