:: BVFUNC13 semantic presentation
theorem Th1: :: BVFUNC13:1
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
All ('not' (All b2,b4,b3)),b
5,b
3 '<' 'not' (All (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then E2:
All (All c2,c5,c3),c
4,c
3 = All (All c2,c4,c3),c
5,c
3
by PARTIT_2:17;
E3:
All ('not' (All c2,c4,c3)),c
5,c
3 = 'not' (Ex (All c2,c4,c3),c5,c3)
by BVFUNC_2:21;
All (All c2,c5,c3),c
4,c
3 '<' Ex (All c2,c4,c3),c
5,c
3
by E2, BVFUNC11:8;
hence
All ('not' (All c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by E3, PARTIT_2:11;
end;
theorem Th2: :: BVFUNC13:2
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
All (All ('not' b2),b4,b3),b
5,b
3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
E3:
All ('not' c2),c
4,c
3 = B_INF ('not' c2),
(CompF c4,c3)
by BVFUNC_2:def 9;
let c
6 be
Element of c
1;
:: according to BVFUNC_1:def 15
assume E4:
(All (All ('not' c2),c4,c3),c5,c3) . c
6 = TRUE
;
E5:
( c
6 in EqClass c
6,
(CompF c4,c3) &
EqClass c
6,
(CompF c4,c3) in CompF c
4,c
3 )
by T_1TOPSP:def 1;
E6:
( c
6 in EqClass c
6,
(CompF c5,c3) &
EqClass c
6,
(CompF c5,c3) in CompF c
5,c
3 )
by T_1TOPSP:def 1;
now
assume
ex b
1 being
Element of c
1 st
( b
1 in EqClass c
6,
(CompF c5,c3) & not
(All ('not' c2),c4,c3) . b
1 = TRUE )
;
then
(B_INF (All ('not' c2),c4,c3),(CompF c5,c3)) . c
6 = FALSE
by BVFUNC_1:def 19;
then
(All (All ('not' c2),c4,c3),c5,c3) . c
6 = FALSE
by BVFUNC_2:def 9;
hence
not verum
by E4, MARGREL1:43;
end;
then E7:
(All ('not' c2),c4,c3) . c
6 = TRUE
by E6;
then
('not' c2) . c
6 = TRUE
by E5;
then
'not' (c2 . c6) = TRUE
by VALUAT_1:def 5;
then
c
2 . c
6 = FALSE
by MARGREL1:41;
then
c
2 . c
6 <> TRUE
by MARGREL1:43;
then
(B_INF c2,(CompF c5,c3)) . c
6 = FALSE
by E6, BVFUNC_1:def 19;
then
(All c2,c5,c3) . c
6 = FALSE
by BVFUNC_2:def 9;
then
(All c2,c5,c3) . c
6 <> TRUE
by MARGREL1:43;
then
(B_INF (All c2,c5,c3),(CompF c4,c3)) . c
6 = FALSE
by E5, BVFUNC_1:def 19;
then
(All (All c2,c5,c3),c4,c3) . c
6 = FALSE
by BVFUNC_2:def 9;
then
'not' ((All (All c2,c5,c3),c4,c3) . c6) = TRUE
by MARGREL1:41;
hence
('not' (All (All c2,c5,c3),c4,c3)) . c
6 = TRUE
by VALUAT_1:def 5;
end;
theorem Th3: :: BVFUNC13:3
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
All ('not' (Ex b2,b4,b3)),b
5,b
3 '<' 'not' (All (All b2,b5,b3),b4,b3)
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
All ('not' (Ex c2,c4,c3)),c
5,c
3 = All (All ('not' c2),c4,c3),c
5,c
3
by BVFUNC_2:21;
hence
All ('not' (Ex c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by Th2;
end;
theorem Th4: :: BVFUNC13:4
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
All (Ex ('not' b2),b4,b3),b
5,b
3 '<' 'not' (All (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume E5:
c
3 is
independent
;
Ex ('not' c2),c
4,c
3 = 'not' (All c2,c4,c3)
by BVFUNC_2:20;
then E6:
All (Ex ('not' c2),c4,c3),c
5,c
3 = 'not' (Ex (All c2,c4,c3),c5,c3)
by BVFUNC_2:21;
All (All c2,c5,c3),c
4,c
3 '<' Ex (All c2,c4,c3),c
5,c
3
by E5, BVFUNC11:11;
hence
All (Ex ('not' c2),c4,c3),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by E6, PARTIT_2:11;
end;
theorem Th5: :: BVFUNC13:5
canceled;
theorem Th6: :: BVFUNC13:6
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
Ex (All ('not' b2),b4,b3),b
5,b
3 '<' 'not' (All (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume E5:
c
3 is
independent
;
then E6:
Ex (All ('not' c2),c4,c3),c
5,c
3 '<' All (Ex ('not' c2),c5,c3),c
4,c
3
by PARTIT_2:19;
All (Ex ('not' c2),c5,c3),c
4,c
3 '<' 'not' (All (All c2,c4,c3),c5,c3)
by E5, Th4;
then
Ex (All ('not' c2),c4,c3),c
5,c
3 '<' 'not' (All (All c2,c4,c3),c5,c3)
by E6, BVFUNC_1:18;
hence
Ex (All ('not' c2),c4,c3),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by E5, PARTIT_2:17;
end;
theorem Th7: :: BVFUNC13:7
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
Ex ('not' (Ex b2,b4,b3)),b
5,b
3 '<' 'not' (All (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume E6:
c
3 is
independent
;
E7:
Ex ('not' (Ex c2,c4,c3)),c
5,c
3 = 'not' (All (Ex c2,c4,c3),c5,c3)
by BVFUNC_2:20;
E8:
All (All c2,c5,c3),c
4,c
3 = All (All c2,c4,c3),c
5,c
3
by E6, PARTIT_2:17;
All c
2,c
4,c
3 '<' Ex c
2,c
4,c
3
by BVFUNC11:8;
then
All (All c2,c4,c3),c
5,c
3 '<' All (Ex c2,c4,c3),c
5,c
3
by PARTIT_2:13;
hence
Ex ('not' (Ex c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by E7, E8, PARTIT_2:11;
end;
theorem Th8: :: BVFUNC13:8
canceled;
theorem Th9: :: BVFUNC13:9
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (All (Ex b2,b4,b3),b5,b3) '<' 'not' (Ex (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
Ex (All c2,c5,c3),c
4,c
3 '<' All (Ex c2,c4,c3),c
5,c
3
by PARTIT_2:19;
hence
'not' (All (Ex c2,c4,c3),c5,c3) '<' 'not' (Ex (All c2,c5,c3),c4,c3)
by PARTIT_2:11;
end;
theorem Th10: :: BVFUNC13:10
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' 'not' (Ex (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then E8:
Ex (Ex c2,c4,c3),c
5,c
3 = Ex (Ex c2,c5,c3),c
4,c
3
by PARTIT_2:18;
All c
2,c
5,c
3 '<' Ex c
2,c
5,c
3
by BVFUNC11:8;
then
Ex (All c2,c5,c3),c
4,c
3 '<' Ex (Ex c2,c4,c3),c
5,c
3
by E8, PARTIT_2:15;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' 'not' (Ex (All c2,c5,c3),c4,c3)
by PARTIT_2:11;
end;
theorem Th11: :: BVFUNC13:11
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' 'not' (All (Ex b2,b5,b3),b4,b3)
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
E9:
Ex c
2,c
4,c
3 = B_SUP c
2,
(CompF c4,c3)
by BVFUNC_2:def 10;
let c
6 be
Element of c
1;
:: according to BVFUNC_1:def 15
assume
('not' (Ex (Ex c2,c4,c3),c5,c3)) . c
6 = TRUE
;
then
'not' ((Ex (Ex c2,c4,c3),c5,c3) . c6) = TRUE
by VALUAT_1:def 5;
then E10:
(Ex (Ex c2,c4,c3),c5,c3) . c
6 = FALSE
by MARGREL1:41;
E11:
now
assume
ex b
1 being
Element of c
1 st
( b
1 in EqClass c
6,
(CompF c5,c3) &
(Ex c2,c4,c3) . b
1 = TRUE )
;
then
(B_SUP (Ex c2,c4,c3),(CompF c5,c3)) . c
6 = TRUE
by BVFUNC_1:def 20;
then
(Ex (Ex c2,c4,c3),c5,c3) . c
6 = TRUE
by BVFUNC_2:def 10;
hence
not verum
by E10, MARGREL1:43;
end;
E12:
for b
1 being
Element of c
1 holds
( b
1 in EqClass c
6,
(CompF c5,c3) implies for b
2 being
Element of c
1 holds
not ( b
2 in EqClass b
1,
(CompF c4,c3) & not c
2 . b
2 <> TRUE ) )
E13:
c
6 in EqClass c
6,
(CompF c4,c3)
by T_1TOPSP:def 1;
for b
1 being
Element of c
1 holds
not ( b
1 in EqClass c
6,
(CompF c5,c3) & not c
2 . b
1 <> TRUE )
then
(B_SUP c2,(CompF c5,c3)) . c
6 = FALSE
by BVFUNC_1:def 20;
then
(Ex c2,c5,c3) . c
6 = FALSE
by BVFUNC_2:def 10;
then
(Ex c2,c5,c3) . c
6 <> TRUE
by MARGREL1:43;
then
(B_INF (Ex c2,c5,c3),(CompF c4,c3)) . c
6 = FALSE
by E13, BVFUNC_1:def 19;
then
(All (Ex c2,c5,c3),c4,c3) . c
6 = FALSE
by BVFUNC_2:def 9;
then
'not' ((All (Ex c2,c5,c3),c4,c3) . c6) = TRUE
by MARGREL1:41;
hence
('not' (All (Ex c2,c5,c3),c4,c3)) . c
6 = TRUE
by VALUAT_1:def 5;
end;
theorem Th12: :: BVFUNC13:12
canceled;
theorem Th13: :: BVFUNC13:13
canceled;
theorem Th14: :: BVFUNC13:14
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (Ex (All b2,b4,b3),b5,b3) '<' 'not' (All (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
All ('not' (All c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by Th1;
hence
'not' (Ex (All c2,c4,c3),c5,c3) '<' 'not' (All (All c2,c5,c3),c4,c3)
by BVFUNC_2:21;
end;
theorem Th15: :: BVFUNC13:15
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (All (Ex b2,b4,b3),b5,b3) '<' 'not' (All (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then E9:
Ex ('not' (Ex c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by Th7;
Ex ('not' (Ex c2,c4,c3)),c
5,c
3 = Ex (All ('not' c2),c4,c3),c
5,c
3
by BVFUNC_2:21;
hence
'not' (All (Ex c2,c4,c3),c5,c3) '<' 'not' (All (All c2,c5,c3),c4,c3)
by E9, BVFUNC11:21;
end;
theorem Th16: :: BVFUNC13:16
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' 'not' (All (All b2,b5,b3),b4,b3)
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
All ('not' (Ex c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by Th3;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' 'not' (All (All c2,c5,c3),c4,c3)
by BVFUNC_2:21;
end;
theorem Th17: :: BVFUNC13:17
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (Ex (All b2,b4,b3),b5,b3) '<' Ex ('not' (All b2,b5,b3)),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then E10:
All ('not' (All c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by Th1;
'not' (Ex (All c2,c4,c3),c5,c3) = All ('not' (All c2,c4,c3)),c
5,c
3
by BVFUNC_2:21;
hence
'not' (Ex (All c2,c4,c3),c5,c3) '<' Ex ('not' (All c2,c5,c3)),c
4,c
3
by E10, BVFUNC_2:20;
end;
theorem Th18: :: BVFUNC13:18
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (All (Ex b2,b4,b3),b5,b3) '<' Ex ('not' (All b2,b5,b3)),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then E11:
Ex ('not' (Ex c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by Th7;
E12:
'not' (All (Ex c2,c4,c3),c5,c3) = Ex (All ('not' c2),c4,c3),c
5,c
3
by BVFUNC11:21;
Ex ('not' (Ex c2,c4,c3)),c
5,c
3 = Ex (All ('not' c2),c4,c3),c
5,c
3
by BVFUNC_2:21;
hence
'not' (All (Ex c2,c4,c3),c5,c3) '<' Ex ('not' (All c2,c5,c3)),c
4,c
3
by E11, E12, BVFUNC_2:20;
end;
theorem Th19: :: BVFUNC13:19
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex ('not' (All b2,b5,b3)),b
4,b
3
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
E12:
All ('not' (Ex c2,c4,c3)),c
5,c
3 '<' 'not' (All (All c2,c5,c3),c4,c3)
by Th3;
'not' (Ex (Ex c2,c4,c3),c5,c3) = All ('not' (Ex c2,c4,c3)),c
5,c
3
by BVFUNC_2:21;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' Ex ('not' (All c2,c5,c3)),c
4,c
3
by E12, BVFUNC_2:20;
end;
theorem Th20: :: BVFUNC13:20
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (All (Ex b2,b4,b3),b5,b3) '<' All ('not' (All b2,b5,b3)),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
'not' (All (Ex c2,c4,c3),c5,c3) '<' 'not' (Ex (All c2,c5,c3),c4,c3)
by Th9;
hence
'not' (All (Ex c2,c4,c3),c5,c3) '<' All ('not' (All c2,c5,c3)),c
4,c
3
by BVFUNC_2:21;
end;
theorem Th21: :: BVFUNC13:21
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' All ('not' (All b2,b5,b3)),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' 'not' (Ex (All c2,c5,c3),c4,c3)
by Th10;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' All ('not' (All c2,c5,c3)),c
4,c
3
by BVFUNC_2:21;
end;
theorem Th22: :: BVFUNC13:22
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex ('not' (Ex b2,b5,b3)),b
4,b
3
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
E15:
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' 'not' (All (Ex c2,c5,c3),c4,c3)
by Th11;
Ex ('not' (Ex c2,c5,c3)),c
4,c
3 = Ex (All ('not' c2),c5,c3),c
4,c
3
by BVFUNC_2:21;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' Ex ('not' (Ex c2,c5,c3)),c
4,c
3
by E15, BVFUNC11:21;
end;
theorem Th23: :: BVFUNC13:23
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (Ex (Ex b2,b4,b3),b5,b3) = All ('not' (Ex b2,b5,b3)),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
'not' (Ex (Ex c2,c4,c3),c5,c3) = 'not' (Ex (Ex c2,c5,c3),c4,c3)
by PARTIT_2:18;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) = All ('not' (Ex c2,c5,c3)),c
4,c
3
by BVFUNC_2:21;
end;
theorem Th24: :: BVFUNC13:24
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (All (Ex b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b5,b3),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
'not' (All (Ex c2,c4,c3),c5,c3) '<' Ex ('not' (All c2,c5,c3)),c
4,c
3
by Th18;
hence
'not' (All (Ex c2,c4,c3),c5,c3) '<' Ex (Ex ('not' c2),c5,c3),c
4,c
3
by BVFUNC_2:20;
end;
theorem Th25: :: BVFUNC13:25
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex (Ex ('not' b2),b5,b3),b
4,b
3
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' Ex ('not' (All c2,c5,c3)),c
4,c
3
by Th19;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' Ex (Ex ('not' c2),c5,c3),c
4,c
3
by BVFUNC_2:20;
end;
theorem Th26: :: BVFUNC13:26
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (All (Ex b2,b4,b3),b5,b3) '<' All (Ex ('not' b2),b5,b3),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
'not' (All (Ex c2,c4,c3),c5,c3) '<' All ('not' (All c2,c5,c3)),c
4,c
3
by Th20;
hence
'not' (All (Ex c2,c4,c3),c5,c3) '<' All (Ex ('not' c2),c5,c3),c
4,c
3
by BVFUNC_2:20;
end;
theorem Th27: :: BVFUNC13:27
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' All (Ex ('not' b2),b5,b3),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' All ('not' (All c2,c5,c3)),c
4,c
3
by Th21;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' All (Ex ('not' c2),c5,c3),c
4,c
3
by BVFUNC_2:20;
end;
theorem Th28: :: BVFUNC13:28
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
'not' (Ex (Ex b2,b4,b3),b5,b3) '<' Ex (All ('not' b2),b5,b3),b
4,b
3
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' Ex ('not' (Ex c2,c5,c3)),c
4,c
3
by Th22;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' Ex (All ('not' c2),c5,c3),c
4,c
3
by BVFUNC_2:21;
end;
theorem Th29: :: BVFUNC13:29
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
'not' (Ex (Ex b2,b4,b3),b5,b3) = All (All ('not' b2),b5,b3),b
4,b
3 )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then
'not' (Ex (Ex c2,c4,c3),c5,c3) = All ('not' (Ex c2,c5,c3)),c
4,c
3
by Th23;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) = All (All ('not' c2),c5,c3),c
4,c
3
by BVFUNC_2:21;
end;
theorem Th30: :: BVFUNC13:30
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
( b
3 is
independent implies
Ex ('not' (Ex b2,b4,b3)),b
5,b
3 '<' 'not' (Ex (All b2,b5,b3),b4,b3) )
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
assume
c
3 is
independent
;
then E22:
'not' (All (Ex c2,c4,c3),c5,c3) '<' 'not' (Ex (All c2,c5,c3),c4,c3)
by Th9;
'not' (All (Ex c2,c4,c3),c5,c3) = Ex (All ('not' c2),c4,c3),c
5,c
3
by BVFUNC11:21;
hence
Ex ('not' (Ex c2,c4,c3)),c
5,c
3 '<' 'not' (Ex (All c2,c5,c3),c4,c3)
by E22, BVFUNC_2:21;
end;
theorem Th31: :: BVFUNC13:31
for b
1 being non
empty set for b
2 being
Element of
Funcs b
1,
BOOLEAN for b
3 being
Subset of
(PARTITIONS b1)for b
4, b
5 being
a_partition of b
1 holds
All ('not' (Ex b2,b4,b3)),b
5,b
3 '<' 'not' (Ex (All b2,b5,b3),b4,b3)
proof
let c
1 be non
empty set ;
let c
2 be
Element of
Funcs c
1,
BOOLEAN ;
let c
3 be
Subset of
(PARTITIONS c1);
let c
4, c
5 be
a_partition of c
1;
E22:
Ex c
2,c
4,c
3 = B_SUP c
2,
(CompF c4,c3)
by BVFUNC_2:def 10;
E23:
All ('not' (Ex c2,c4,c3)),c
5,c
3 =