Copyright (c) 1999 Association of Mizar Users
environ vocabulary FUNCT_2, MARGREL1, PARTIT1, EQREL_1, ZF_LANG, BVFUNC_2; notation XBOOLE_0, SUBSET_1, MARGREL1, VALUAT_1, FRAENKEL, EQREL_1, BVFUNC_1, BVFUNC_2; constructors BVFUNC_2, BVFUNC_1; clusters MARGREL1, XBOOLE_0; theorems BVFUNC_1, BVFUNC_2, PARTIT_2, BVFUNC_4; begin :: Chap. 1 Predicate Calculus reserve Y for non empty set; canceled 4; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) proof let a be Element of Funcs(Y,BOOLEAN); let G be Subset of PARTITIONS(Y); let A,B be a_partition of Y; 'not' All(Ex(a,A,G),B,G) = Ex('not' Ex(a,A,G),B,G) by BVFUNC_2:20; hence thesis by BVFUNC_2:21; end; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds 'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G) proof let a be Element of Funcs(Y,BOOLEAN); let G be Subset of PARTITIONS(Y); let A,B be a_partition of Y; 'not' Ex(All(a,A,G),B,G) = All('not' All(a,A,G),B,G) by BVFUNC_2:21; hence thesis by BVFUNC_2:20; end; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds 'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G) proof let a be Element of Funcs(Y,BOOLEAN); let G be Subset of PARTITIONS(Y); let A,B be a_partition of Y; Ex('not' All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G) by BVFUNC_2:20; hence thesis by BVFUNC_2:20; end; Lm1: for a,b being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), P being a_partition of Y st a '<' b holds All(a,P,G) '<' Ex(b,P,G) proof let a,b be Element of Funcs(Y,BOOLEAN), G be Subset of PARTITIONS(Y), P be a_partition of Y; assume a '<' b; then A1:All(a,P,G) '<' All(b,P,G) by PARTIT_2:13; All(b,P,G) '<' Ex(b,P,G) by BVFUNC_4:18; hence thesis by A1,BVFUNC_1:18; end; canceled 3; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y st G is independent holds Ex(All(a,A,G),B,G) '<' Ex(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 be a_partition of Y; assume G is independent; then A1:Ex(Ex(a,B,G),A,G) = Ex(Ex(a,A,G),B,G) by PARTIT_2:18; All(a,A,G) '<' Ex(a,A,G) by Lm1; hence thesis by A1,PARTIT_2:15; end; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds All(All(a,A,G),B,G) '<' All(Ex(a,A,G),B,G) proof let a be Element of Funcs(Y,BOOLEAN); let G be Subset of PARTITIONS(Y); let A,B be a_partition of Y; All(a,A,G) '<' Ex(a,A,G) by Lm1; hence thesis by PARTIT_2:13; end; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds All(All(a,A,G),B,G) '<' Ex(All(a,A,G),B,G) by Lm1; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds All(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G) proof let a be Element of Funcs(Y,BOOLEAN); let G be Subset of PARTITIONS(Y); let A,B be a_partition of Y; All(a,A,G) '<' Ex(a,A,G) by Lm1; hence thesis by Lm1; end; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds All(Ex(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G) by Lm1; theorem for a being Element of Funcs(Y,BOOLEAN), G being Subset of PARTITIONS(Y), A,B being a_partition of Y holds Ex(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G) proof let a be Element of Funcs(Y,BOOLEAN); let G be Subset of PARTITIONS(Y); let A,B be a_partition of Y; All(a,A,G) '<' Ex(a,A,G) by Lm1; hence thesis by PARTIT_2:15; end;