Copyright (c) 1999 Association of Mizar Users
environ
vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, BVFUNC_2, ZF_LANG, BVFUNC_1,
T_1TOPSP;
notation XBOOLE_0, SUBSET_1, FRAENKEL, MARGREL1, VALUAT_1, EQREL_1, SETWISEO,
BVFUNC_1, BVFUNC_2;
constructors SETWISEO, BVFUNC_2, BVFUNC_1;
clusters SUBSET_1, MARGREL1, VALUAT_1, AMI_1, XBOOLE_0;
definitions BVFUNC_1;
theorems T_1TOPSP, MARGREL1, BVFUNC_1, BVFUNC_2, BVFUNC13, VALUAT_1;
begin :: Chap. 1 Predicate Calculus
reserve Y for non empty set;
canceled 3;
theorem for a being Element of Funcs(Y,BOOLEAN),
G being Subset of PARTITIONS(Y),
A,B,C being a_partition of Y holds
All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y);
let A,B,C be a_partition of Y;
A1:Ex(a,A,G) = B_SUP(a,CompF(A,G)) by BVFUNC_2:def 10;
A2:All('not' Ex(a,A,G),B,G) = B_INF('not' Ex(a,A,G),CompF(B,G))
by BVFUNC_2:def 9;
A3:for y being Element of Y holds
( (for x being Element of Y st x in EqClass(y,CompF(B,G)) holds
Pj('not' Ex(a,A,G),x)=TRUE) implies
Pj(B_INF('not' Ex(a,A,G),CompF(B,G)),y) = TRUE ) &
(not (for x being Element of Y st x in EqClass(y,CompF(B,G)) holds
Pj('not' Ex(a,A,G),x)=TRUE) implies
Pj(B_INF('not' Ex(a,A,G),CompF(B,G)),y) = FALSE)
by BVFUNC_1:def 19;
A4:All(a,B,G) = B_INF(a,CompF(B,G)) by BVFUNC_2:def 9;
A5:Ex(All(a,B,G),A,G) = B_SUP(All(a,B,G),CompF(A,G))
by BVFUNC_2:def 10;
let z be Element of Y;
assume A6:Pj(All('not' Ex(a,A,G),B,G),z)=TRUE;
A7:z in EqClass(z,CompF(B,G)) &
EqClass(z,CompF(B,G)) in CompF(B,G)
by T_1TOPSP:def 1;
now assume
not (for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
Pj('not' Ex(a,A,G),x)=TRUE);then
Pj(B_INF('not' Ex(a,A,G),CompF(B,G)),z) = FALSE by A3;then
Pj(All('not' Ex(a,A,G),B,G),z)=FALSE by A2;then
Pj(All('not' Ex(a,A,G),B,G),z)<>TRUE by MARGREL1:43;
hence contradiction by A6;
end;then
for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
Pj('not' Ex(a,A,G),x)=TRUE;then
Pj('not' Ex(a,A,G),z)=TRUE by A7;then
'not' Pj(Ex(a,A,G),z)=TRUE by VALUAT_1:def 5;then
Pj(Ex(a,A,G),z)='not' TRUE by MARGREL1:40;then
A8:Pj(Ex(a,A,G),z)=FALSE by MARGREL1:41;
now assume
ex x being Element of Y st
x in EqClass(z,CompF(A,G)) & Pj(a,x)=TRUE;then
Pj(B_SUP(a,CompF(A,G)),z) = TRUE by BVFUNC_1:def 20;then
Pj(Ex(a,A,G),z)=TRUE by A1;
hence contradiction by A8,MARGREL1:43;
end;then
A9:for x being Element of Y st
x in EqClass(z,CompF(A,G)) holds Pj(a,x)<>TRUE;
for x being Element of Y st
x in EqClass(z,CompF(A,G)) holds Pj(All(a,B,G),x)<>TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(A,G));then
A10:Pj(a,x)<>TRUE by A9;
x in EqClass(x,CompF(B,G)) & EqClass(x,CompF(B,G)) in CompF(B,G)
by T_1TOPSP:def 1;then
ex y being Element of Y st y in EqClass(x,CompF(B,G)) &
Pj(a,y)<>TRUE by A10;then
Pj(B_INF(a,CompF(B,G)),x) = FALSE by BVFUNC_1:def 19;then
Pj(All(a,B,G),x)=FALSE by A4;then
Pj(All(a,B,G),x)<>TRUE by MARGREL1:43;
hence thesis;
end;then
not (ex x being Element of Y st
x in EqClass(z,CompF(A,G)) & Pj(All(a,B,G),x)=TRUE);then
Pj(B_SUP(All(a,B,G),CompF(A,G)),z) = FALSE by BVFUNC_1:def 20;then
Pj(Ex(All(a,B,G),A,G),z)=FALSE by A5;then
'not' Pj(Ex(All(a,B,G),A,G),z)=TRUE by MARGREL1:41;
hence thesis by VALUAT_1:def 5;
end;
Lm1:for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C 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) by BVFUNC13:34;
canceled 2;
theorem
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C being a_partition of Y
st G is independent & G={A,B,C} & A<>B & B<>C & C<>A holds
Ex('not' All(a,A,G),B,G) = Ex('not' All(a,B,G),A,G)
proof
let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y);
let A,B,C be a_partition of Y;
assume A1:G is independent & G={A,B,C} & A<>B & B<>C & C<>A;then
A2:Ex('not' All(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G) by Lm1;
Ex('not' All(a,B,G),A,G) '<' Ex('not' All(a,A,G),B,G) by A1,Lm1;
hence thesis by A2,BVFUNC_1:18;
end;
canceled 6;
theorem
for a being Element of Funcs(Y,BOOLEAN),G being Subset of PARTITIONS(Y),
A,B,C being a_partition of Y
st G is independent & G={A,B,C} & A<>B & B<>C & C<>A holds
All('not' Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G)
proof
let a be Element of Funcs(Y,BOOLEAN);
let G be Subset of PARTITIONS(Y);
let A,B,C be a_partition of Y;
assume A1:G is independent & G={A,B,C} & A<>B & B<>C & C<>A;then
A2:All('not' Ex(a,A,G),B,G) '<' All('not' Ex(a,B,G),A,G) by BVFUNC13:41;
All('not' Ex(a,B,G),A,G) '<' All('not' Ex(a,A,G),B,G) by A1,BVFUNC13:41;
hence thesis by A2,BVFUNC_1:18;
end;