:: BVFUNC13 semantic presentation
theorem E1: :: 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 E2: :: 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;
:: uses BVFUNC_1:def 15
assume E4:
Pj (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
Pj (All ('not' c2),c4,c3),b
1 = TRUE )
;
then
Pj (B_INF (All ('not' c2),c4,c3),(CompF c5,c3)),c
6 = FALSE
by BVFUNC_1:def 19;
then
Pj (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:
Pj (All ('not' c2),c4,c3),c
6 = TRUE
by E6;
then
Pj ('not' c2),c
6 = TRUE
by E5;
then
'not' (Pj c2,c6) = TRUE
by VALUAT_1:def 5;
then
Pj c
2,c
6 = FALSE
by MARGREL1:41;
then
Pj c
2,c
6 <> TRUE
by MARGREL1:43;
then
Pj (B_INF c2,(CompF c5,c3)),c
6 = FALSE
by E6, BVFUNC_1:def 19;
then
Pj (All c2,c5,c3),c
6 = FALSE
by BVFUNC_2:def 9;
then
Pj (All c2,c5,c3),c
6 <> TRUE
by MARGREL1:43;
then
Pj (B_INF (All c2,c5,c3),(CompF c4,c3)),c
6 = FALSE
by E5, BVFUNC_1:def 19;
then
Pj (All (All c2,c5,c3),c4,c3),c
6 = FALSE
by BVFUNC_2:def 9;
then
'not' (Pj (All (All c2,c5,c3),c4,c3),c6) = TRUE
by MARGREL1:41;
hence
Pj ('not' (All (All c2,c5,c3),c4,c3)),c
6 = TRUE
by VALUAT_1:def 5;
end;
theorem E3: :: 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 E2;
end;
theorem E4: :: 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 :: BVFUNC13:5
canceled;
theorem :: 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, E4;
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 E5: :: 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 :: BVFUNC13:8
canceled;
theorem E6: :: 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 E7: :: 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 E8: :: 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;
:: uses BVFUNC_1:def 15
assume
Pj ('not' (Ex (Ex c2,c4,c3),c5,c3)),c
6 = TRUE
;
then
'not' (Pj (Ex (Ex c2,c4,c3),c5,c3),c6) = TRUE
by VALUAT_1:def 5;
then E10:
Pj (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) &
Pj (Ex c2,c4,c3),b
1 = TRUE )
;
then
Pj (B_SUP (Ex c2,c4,c3),(CompF c5,c3)),c
6 = TRUE
by BVFUNC_1:def 20;
then
Pj (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
Pj 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
Pj c
2,b
1 <> TRUE )
then
Pj (B_SUP c2,(CompF c5,c3)),c
6 = FALSE
by BVFUNC_1:def 20;
then
Pj (Ex c2,c5,c3),c
6 = FALSE
by BVFUNC_2:def 10;
then
Pj (Ex c2,c5,c3),c
6 <> TRUE
by MARGREL1:43;
then
Pj (B_INF (Ex c2,c5,c3),(CompF c4,c3)),c
6 = FALSE
by E13, BVFUNC_1:def 19;
then
Pj (All (Ex c2,c5,c3),c4,c3),c
6 = FALSE
by BVFUNC_2:def 9;
then
'not' (Pj (All (Ex c2,c5,c3),c4,c3),c6) = TRUE
by MARGREL1:41;
hence
Pj ('not' (All (Ex c2,c5,c3),c4,c3)),c
6 = TRUE
by VALUAT_1:def 5;
end;
theorem :: BVFUNC13:12
canceled;
theorem :: BVFUNC13:13
canceled;
theorem :: 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 E1;
hence
'not' (Ex (All c2,c4,c3),c5,c3) '<' 'not' (All (All c2,c5,c3),c4,c3)
by BVFUNC_2:21;
end;
theorem :: 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 E5;
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 :: 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 E3;
hence
'not' (Ex (Ex c2,c4,c3),c5,c3) '<' 'not' (All (All c2,c5,c3),c4,c3)
by BVFUNC_2:21;
end;
theorem E9: :: 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 E1;
'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 E10: :: 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 E5;
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 E11: :: 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 E3;
'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 E12: :: 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 E6;
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 E13: :: 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 E7;
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 E14: :: 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 E8;
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 E15: :: 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 E16: :: 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 E10;
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 E17: :: 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 E11;
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 E18: :: 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 E12;
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 E19: :: 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 E13;
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 E20: :: 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 E14;
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 E21: :: 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 E15;
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 :: 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 E6;
'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 :: 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 = B_INF ('not' (Ex c2,c4,c3)),
(CompF c5,c3)
by BVFUNC_2:def 9;
E24:
All c
2,c
5,c
3 = B_INF c
2,
(CompF c5,c3)
by BVFUNC_2:def 9;
E25:
Ex (All c2,c5,c3),c
4,c
3 = B_SUP (All c2,c5,c3),
(CompF c4,c3)
by BVFUNC_2:def 10;
let c
6 be
Element of c
1;
:: uses BVFUNC_1:def 15
assume E26:
Pj (All ('not' (Ex c2,c4,c3)),c5,c3),c
6 = TRUE
;
E27:
( 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
Pj ('not' (Ex c2,c4,c3)),b
1 = TRUE )
;
then
Pj (All ('not' (Ex c2,c4,c3)),c5,c3),c
6 = FALSE
by E23, BVFUNC_1:def 19;
hence
not verum
by E26, MARGREL1:43;
end;
then
Pj ('not' (Ex c2,c4,c3)),c
6 = TRUE
by E27;
then
'not' (Pj (Ex c2,c4,c3),c6) = TRUE
by VALUAT_1:def 5;
then E28:
Pj (Ex c2,c4,c3),c
6 = FALSE
by MARGREL1:41;
for b
1 being
Element of c
1 holds
not ( b
1 in EqClass c
6,
(CompF c4,c3) & not
Pj (All c2,c5,c3),b
1 <></