:: Predicate Calculus for Boolean Valued Functions, III
:: by Shunichi Kobayashi and Yatsuka Nakamura
::
:: Received July 14, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, MARGREL1, PARTIT1, EQREL_1, TARSKI, BVFUNC_2,
FUNCOP_1, FUNCT_1, ZFMISC_1, SETFAM_1, RELAT_1, BVFUNC_1, XBOOLEAN;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MARGREL1, RELAT_1, SETFAM_1,
FUNCT_1, FUNCT_2, EQREL_1, FUNCOP_1, PARTIT1, BVFUNC_1, BVFUNC_2,
FUNCT_4;
constructors SETFAM_1, FUNCT_4, XCMPLX_0, BVFUNC_1, BVFUNC_2, RELSET_1,
NUMBERS, FUNCOP_1;
registrations XBOOLE_0, FUNCOP_1, FUNCT_4, EQREL_1, MARGREL1, ORDINAL1;
requirements SUBSET, BOOLE, ARITHM, NUMERALS;
definitions TARSKI, BVFUNC_1, XBOOLE_0;
equalities XBOOLEAN, FUNCOP_1;
expansions XBOOLE_0;
theorems TARSKI, FUNCT_1, SETFAM_1, EQREL_1, ZFMISC_1, PARTIT1, BVFUNC_1,
BVFUNC_2, ENUMSET1, FUNCT_4, FUNCOP_1, MSSUBFAM, PARTIT_2, BVFUNC_4,
XBOOLE_0, XBOOLE_1, XBOOLEAN, MARGREL1;
begin :: Chap. 1 Preliminaries
reserve Y for non empty set,
a, b for Function of Y,BOOLEAN,
G for Subset of PARTITIONS(Y),
A, B for a_partition of Y;
theorem Th1:
for z being Element of Y, PA,PB being a_partition of Y st PA '<'
PB holds EqClass(z,PA) c= EqClass(z,PB)
proof
let z be Element of Y;
let PA,PB be a_partition of Y;
assume PA '<' PB;
then
A1: ex b being set st b in PB & EqClass(z,PA) c= b by SETFAM_1:def 2;
z in EqClass(z,PA) by EQREL_1:def 6;
hence thesis by A1,EQREL_1:def 6;
end;
theorem
for z being Element of Y, PA,PB being a_partition of Y holds EqClass(z
,PA) c= EqClass(z,PA '\/' PB) by Th1,PARTIT1:16;
theorem
for z being Element of Y, PA,PB being a_partition of Y holds EqClass(z
,PA '/\' PB) c= EqClass(z,PA) by Th1,PARTIT1:15;
theorem
for z being Element of Y, PA being a_partition of Y holds EqClass(z,PA
) c= EqClass(z,%O(Y)) & EqClass(z,%I(Y)) c= EqClass(z,PA) by Th1,PARTIT1:32;
theorem
for G being Subset of PARTITIONS(Y), A,B being a_partition of Y st G
is independent & G={A,B} & A<>B holds for a,b being set st a in A & b in B
holds a meets b
proof
let G be Subset of PARTITIONS(Y);
let A,B be a_partition of Y;
assume that
A1: G is independent and
A2: G={A,B} and
A3: A<>B;
let a,b be set;
assume that
A4: a in A and
A5: b in B;
set h2 = (A,B) --> (a,b);
A6: for d being set st d in G holds h2.d in d
proof
let d be set;
assume d in G;
then d = A or d = B by A2,TARSKI:def 2;
hence thesis by A3,A4,A5,FUNCT_4:63;
end;
{a,b} c= bool Y
proof
let x be object;
assume x in {a,b};
then x = a or x = b by TARSKI:def 2;
hence thesis by A4,A5;
end;
then reconsider SS = {a,b} as Subset-Family of Y;
A7: dom h2 = {A,B} by FUNCT_4:62;
rng h2 = SS by A3,FUNCT_4:64;
then Intersect SS <> {} by A1,A2,A7,A6,BVFUNC_2:def 5;
hence a /\ b <> {} by A4,A5,MSSUBFAM:10;
end;
theorem
for G being Subset of PARTITIONS(Y), A,B being a_partition of Y st G
is independent & G={A,B} & A <> B holds '/\' G = A '/\' B
proof
let G be Subset of PARTITIONS(Y);
let A,B be a_partition of Y;
assume that
A1: G is independent and
A2: G={A,B} and
A3: A <> B;
A4: '/\' G c= A '/\' B
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in '/\' G;
then consider h being Function, F being Subset-Family of Y such that
A5: dom h=G and
A6: rng h = F and
A7: for d being set st d in G holds h.d in d and
A8: x=Intersect F and
A9: x<>{} by BVFUNC_2:def 1;
A10: not x in {{}} by A9,TARSKI:def 1;
A11: A in G by A2,TARSKI:def 2;
then
A12: h.A in rng h by A5,FUNCT_1:def 3;
then
A13: Intersect F = meet (rng h) by A6,SETFAM_1:def 9;
A14: h.A /\ h.B c= xx
proof
A15: rng h = {h.A,h.B}
proof
thus rng h c= {h.A,h.B}
proof
let m be object;
assume m in rng h;
then consider w being object such that
A16: w in dom h and
A17: m = h.w by FUNCT_1:def 3;
w = A or w = B by A2,A5,A16,TARSKI:def 2;
hence thesis by A17,TARSKI:def 2;
end;
let m be object;
assume m in {h.A,h.B};
then
A18: m = h.A or m = h.B by TARSKI:def 2;
A19: B in dom h by A2,A5,TARSKI:def 2;
A in dom h by A2,A5,TARSKI:def 2;
hence thesis by A18,A19,FUNCT_1:def 3;
end;
let m be object;
assume
A20: m in h.A /\ h.B;
then
A21: m in h.B by XBOOLE_0:def 4;
m in h.A by A20,XBOOLE_0:def 4;
then for y being set holds y in rng h implies m in y by A21,A15,
TARSKI:def 2;
hence thesis by A8,A12,A13,SETFAM_1:def 1;
end;
A22: B in G by A2,TARSKI:def 2;
then
A23: h.B in B by A7;
A24: h.B in rng h by A5,A22,FUNCT_1:def 3;
xx c= h.A /\ h.B
proof
let m be object;
assume
A25: m in xx;
then
A26: m in h.B by A8,A24,A13,SETFAM_1:def 1;
m in h.A by A8,A12,A13,A25,SETFAM_1:def 1;
hence thesis by A26,XBOOLE_0:def 4;
end;
then
A27: h.A /\ h.B = x by A14,XBOOLE_0:def 10;
h.A in A by A7,A11;
then x in INTERSECTION(A,B) by A23,A27,SETFAM_1:def 5;
then x in INTERSECTION(A,B) \ {{}} by A10,XBOOLE_0:def 5;
hence thesis by PARTIT1:def 4;
end;
A '/\' B c= '/\' G
proof
let x be object;
assume x in A '/\' B;
then x in INTERSECTION(A,B) \ {{}} by PARTIT1:def 4;
then consider X,Z being set such that
A28: X in A and
A29: Z in B and
A30: x = X /\ Z by SETFAM_1:def 5;
{X,Z} c= bool Y
proof
let m be object;
assume m in {X,Z};
then m = X or m = Z by TARSKI:def 2;
hence thesis by A28,A29;
end;
then reconsider SS = {X,Z} as Subset-Family of Y;
A31: X /\ Z = Intersect SS by A28,A29,MSSUBFAM:10;
set h = (A,B) --> (X,Z);
A32: for d being set st d in G holds h.d in d
proof
let d be set;
assume d in G;
then d = A or d = B by A2,TARSKI:def 2;
hence thesis by A3,A28,A29,FUNCT_4:63;
end;
A33: dom h = {A,B} by FUNCT_4:62;
A34: rng h = SS by A3,FUNCT_4:64;
then Intersect SS <> {} by A1,A2,A33,A32,BVFUNC_2:def 5;
hence thesis by A2,A30,A33,A34,A32,A31,BVFUNC_2:def 1;
end;
hence thesis by A4;
end;
theorem
for G being Subset of PARTITIONS(Y), A,B being a_partition of Y st G={
A,B} & A<>B holds CompF(A,G) = B
proof
let G be Subset of PARTITIONS(Y);
let A,B be a_partition of Y;
assume that
A1: G={A,B} and
A2: A<>B;
A3: '/\' {B} c= B
proof
let x be object;
assume x in '/\' {B};
then consider h being Function, F being Subset-Family of Y such that
A4: dom h={B} and
A5: rng h = F and
A6: for d being set st d in {B} holds h.d in d and
A7: x=Intersect F and
x<>{} by BVFUNC_2:def 1;
rng h = {h.B} by A4,FUNCT_1:4;
then
A8: x=meet ({h.B}) by A5,A7,SETFAM_1:def 9;
B in {B} by TARSKI:def 1;
then h.B in B by A6;
hence thesis by A8,SETFAM_1:10;
end;
A9: B c= '/\' {B}
proof
let x be object;
set h0 = B .--> x;
A10: dom h0 = {B};
assume
A11: x in B;
A12: for d being set st d in {B} holds h0.d in d
proof
let d be set;
assume d in {B};
then d=B by TARSKI:def 1;
hence thesis by A11,FUNCOP_1:72;
end;
A13: rng h0 = {x} by FUNCOP_1:8;
A14: x is set by TARSKI:1;
rng h0 c= bool Y
proof
let m be object;
assume m in rng h0;
then m=x by A13,TARSKI:def 1;
hence thesis by A11;
end;
then reconsider F0 = rng h0 as Subset-Family of Y;
meet F0 = Intersect F0 by A13,SETFAM_1:def 9;
then
A15: x=Intersect F0 by A13,SETFAM_1:10,A14;
x<>{} by A11,EQREL_1:def 4;
hence thesis by A10,A12,A15,BVFUNC_2:def 1;
end;
A in {A} by TARSKI:def 1;
then
A16: {A} \ {A}={} by ZFMISC_1:60;
G \ {A}={A} \/ {B} \ {A} by A1,ENUMSET1:1
.= ({A} \ {A}) \/ ({B} \ {A}) by XBOOLE_1:42
.= ({A} \ {A}) \/ {B} by A2,ZFMISC_1:14;
then CompF(A,G)='/\' {B} by A16,BVFUNC_2:def 7;
hence thesis by A3,A9;
end;
begin
theorem Th8:
a '<' b implies All(a,A,G) '<' Ex(b,A,G)
proof
assume a '<' b;
then
A1: All(a,A,G) '<' All(b,A,G) by PARTIT_2:12;
All(b,A,G) '<' Ex(b,A,G) by BVFUNC_4:17;
hence thesis by A1,BVFUNC_1:15;
end;
theorem Th9:
G is independent implies All(All(a,A,G),B,G) '<' Ex(All(a,B,G),A,G)
proof
assume G is independent;
then All(All(a,A,G),B,G) = All(All(a,B,G),A,G) by PARTIT_2:15;
hence thesis by Th8;
end;
theorem
All(All(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G)
proof
A1: All(All(a,A,G),B,G) '<' All(a,A,G) by BVFUNC_2:11;
All(a,A,G) '<' Ex(Ex(a,B,G),A,G) by Th8,BVFUNC_2:12;
hence thesis by A1,BVFUNC_1:15;
end;
theorem
G is independent implies All(All(a,A,G),B,G) '<' All(Ex(a,B,G),A,G)
proof
assume G is independent;
then
A1: All(All(a,A,G),B,G) = All(All(a,B,G),A,G) by PARTIT_2:15;
All(a,B,G) '<' Ex(a,B,G) by Th8;
hence thesis by A1,PARTIT_2:12;
end;
theorem
All(Ex(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G)
proof
A1: Ex(a,B,G) = B_SUP(a,CompF(B,G)) by BVFUNC_2:def 10;
let z be Element of Y;
assume
A2: (All(Ex(a,A,G),B,G)).z=TRUE;
A3: now
assume not (for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
(Ex(a,A,G)).x=TRUE);
then (B_INF(Ex(a,A,G),CompF(B,G))).z = FALSE by BVFUNC_1:def 16;
hence contradiction by A2,BVFUNC_2:def 9;
end;
A4: z in EqClass(z,CompF(B,G)) by EQREL_1:def 6;
now assume
not (ex x being Element of Y st x in EqClass(z,CompF(A,G)) & (a). x=TRUE);
then (B_SUP(a,CompF(A,G))).z = FALSE by BVFUNC_1:def 17;
then (Ex(a,A,G)).z=FALSE by BVFUNC_2:def 10;
hence contradiction by A4,A3;
end;
then consider x1 being Element of Y such that
A5: x1 in EqClass(z,CompF(A,G)) and
A6: (a).x1=TRUE;
x1 in EqClass(x1,CompF(B,G)) by EQREL_1:def 6;
then (Ex(a,B,G)).x1=TRUE by A1,A6,BVFUNC_1:def 17;
then (B_SUP(Ex(a,B,G),CompF(A,G))).z = TRUE by A5,BVFUNC_1:def 17;
hence thesis by BVFUNC_2:def 10;
end;
theorem Th13:
'not' Ex(All(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
A1: All(a,A,G) = B_INF(a,CompF(A,G)) by BVFUNC_2:def 9;
let z be Element of Y;
A2: z in EqClass(z,CompF(B,G)) by EQREL_1:def 6;
assume ('not' Ex(All(a,A,G),B,G)).z=TRUE;
then
A3: 'not' (Ex(All(a,A,G),B,G)).z=TRUE by MARGREL1:def 19;
Ex(All(a,A,G),B,G) = B_SUP(All(a,A,G),CompF(B,G)) by BVFUNC_2:def 10;
then (All(a,A,G)).z<>TRUE by A3,A2,BVFUNC_1:def 17;
then consider x1 being Element of Y such that
A4: x1 in EqClass(z,CompF(A,G)) and
A5: (a).x1<>TRUE by A1,BVFUNC_1:def 16;
(a).x1=FALSE by A5,XBOOLEAN:def 3;
then
A6: ('not' a).x1='not' FALSE by MARGREL1:def 19;
A7: Ex('not' a,B,G) = B_SUP('not' a,CompF(B,G)) by BVFUNC_2:def 10;
x1 in EqClass(x1,CompF(B,G)) by EQREL_1:def 6;
then (Ex('not' a,B,G)).x1=TRUE by A7,A6,BVFUNC_1:def 17;
then (B_SUP(Ex('not' a,B,G),CompF(A,G))).z = TRUE by A4,BVFUNC_1:def 17;
hence thesis by BVFUNC_2:def 10;
end;
theorem Th14:
G is independent implies Ex('not' All(a,A,G),B,G) '<' Ex(Ex(
'not' a,B,G),A,G)
proof
assume G is independent;
then Ex(Ex('not' a,B,G),A,G) = Ex(Ex('not' a,A,G),B,G) by PARTIT_2:16;
hence thesis by BVFUNC_2:18;
end;
theorem Th15:
G is independent implies 'not' All(All(a,A,G),B,G) = Ex('not' All(a,B,G),A,G)
proof
assume G is independent;
then All(All(a,A,G),B,G) = All(All(a,B,G),A,G) by PARTIT_2:15;
hence thesis by BVFUNC_2:18;
end;
theorem
G is independent implies All('not' All(a,A,G),B,G) '<' Ex(Ex('not' a,B
,G),A,G)
proof
assume G is independent;
then
A1: Ex(Ex('not' a,B,G),A,G) = Ex(Ex('not' a,A,G),B,G) by PARTIT_2:16;
'not' All(a,A,G) = Ex('not' a,A,G) by BVFUNC_2:18;
hence thesis by A1,Th8;
end;
theorem
G is independent implies 'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,B,G ),A,G)
proof
A1: Ex('not' a,B,G) = 'not' All(a,B,G) by BVFUNC_2:18;
assume G is independent;
hence thesis by A1,Th15;
end;
theorem
G is independent implies 'not' All(All(a,A,G),B,G) '<' Ex(Ex('not' a,A
,G),B,G)
proof
assume
A1: G is independent;
then Ex('not' All(a,B,G),A,G) '<' Ex(Ex('not' a,A,G),B,G) by Th14;
hence thesis by A1,Th15;
end;
:: from BVFUNC12
theorem Th19:
'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G)
proof
'not' All(Ex(a,A,G),B,G) = Ex('not' Ex(a,A,G),B,G) by BVFUNC_2:18;
hence thesis by BVFUNC_2:19;
end;
theorem Th20:
'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G)
proof
'not' Ex(All(a,A,G),B,G) = All('not' All(a,A,G),B,G) by BVFUNC_2:19;
hence thesis by BVFUNC_2:18;
end;
theorem Th21:
'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G)
proof
Ex('not' All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G) by BVFUNC_2:18;
hence thesis by BVFUNC_2:18;
end;
theorem
G is independent implies Ex(All(a,A,G),B,G) '<' Ex(Ex(a,B,G),A,G)
proof
assume G is independent; then
A1: Ex(Ex(a,B,G),A,G) = Ex(Ex(a,A,G),B,G) by PARTIT_2:16;
All(a,A,G) '<' Ex(a,A,G) by Th8;
hence thesis by A1,PARTIT_2:13;
end;
theorem
All(All(a,A,G),B,G) '<' All(Ex(a,A,G),B,G)
proof
All(a,A,G) '<' Ex(a,A,G) by Th8;
hence thesis by PARTIT_2:12;
end;
theorem
All(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G)
proof
All(a,A,G) '<' Ex(a,A,G) by Th8;
hence thesis by Th8;
end;
theorem
Ex(All(a,A,G),B,G) '<' Ex(Ex(a,A,G),B,G)
proof
All(a,A,G) '<' Ex(a,A,G) by Th8;
hence thesis by PARTIT_2:13;
end;
:: BVFUNC13
theorem Th26:
G is independent implies All('not' All(a,A,G),B,G) '<' 'not' All(
All(a,B,G),A,G)
proof
assume G is independent;
then All(All(a,B,G),A,G) = All(All(a,A,G),B,G) by PARTIT_2:15;
then
All('not' All(a,A,G),B,G) = 'not' Ex(All(a,A,G),B,G) & All(All(a,B,G),A,
G) '<' Ex(All(a,A,G),B,G) by Th8,BVFUNC_2:19;
hence thesis by PARTIT_2:11;
end;
theorem Th27:
All(All('not' a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
let z be Element of Y;
A1: z in EqClass(z,CompF(A,G)) by EQREL_1:def 6;
A2: z in EqClass(z,CompF(B,G)) by EQREL_1:def 6;
assume
A3: (All(All('not' a,A,G),B,G)).z=TRUE;
now
assume not (for x being Element of Y st x in EqClass(z,CompF(B,G)) holds
(All('not' a,A,G)).x=TRUE);
then (B_INF(All('not' a,A,G),CompF(B,G))).z = FALSE by BVFUNC_1:def 16;
hence contradiction by A3,BVFUNC_2:def 9;
end;
then All('not' a,A,G) = B_INF('not' a,CompF(A,G)) & (All('not' a,A,G)).z=
TRUE by A2,BVFUNC_2:def 9;
then ('not' a).z=TRUE by A1,BVFUNC_1:def 16;
then 'not' (a).z=TRUE by MARGREL1:def 19;
then (B_INF(a,CompF(B,G))).z = FALSE by A2,BVFUNC_1:def 16;
then (All(a,B,G)).z=FALSE by BVFUNC_2:def 9;
then (B_INF(All(a,B,G),CompF(A,G))).z = FALSE by A1,BVFUNC_1:def 16;
then (All(All(a,B,G),A,G)).z=FALSE by BVFUNC_2:def 9;
then 'not' (All(All(a,B,G),A,G)).z=TRUE;
hence thesis by MARGREL1:def 19;
end;
theorem Th28:
All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
All('not' Ex(a,A,G),B,G) = All(All('not' a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th27;
end;
theorem Th29:
G is independent implies All(Ex('not' a,A,G),B,G) '<' 'not' All(
All(a,B,G),A,G)
proof
Ex('not' a,A,G) = 'not' All(a,A,G) by BVFUNC_2:18;
then
A1: All(Ex('not' a,A,G),B,G) = 'not' Ex(All(a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th9,PARTIT_2:11;
end;
theorem
G is independent implies Ex(All('not' a,A,G),B,G) '<' 'not' All(All(a,
B,G),A,G)
proof
assume
A1: G is independent;
then
Ex(All('not' a,A,G),B,G) '<' All(Ex('not' a,B,G),A,G) & All(Ex('not' a,B
,G), A,G) '<' 'not' All(All(a,A,G),B,G) by Th29,PARTIT_2:17;
then Ex(All('not' a,A,G),B,G) '<' 'not' All(All(a,A,G),B,G) by BVFUNC_1:15;
hence thesis by A1,PARTIT_2:15;
end;
theorem Th31:
G is independent implies Ex('not' Ex(a,A,G),B,G) '<' 'not' All(
All(a,B,G),A,G)
proof
All(a,A,G) '<' Ex(a,A,G) by Th8;
then
A1: All(All(a,A,G),B,G) '<' All(Ex(a,A,G),B,G) by PARTIT_2:12;
assume G is independent;
then
Ex('not' Ex(a,A,G),B,G) = 'not' All(Ex(a,A,G),B,G) & All(All(a,B,G),A,G)
= All(All(a,A,G),B,G) by BVFUNC_2:18,PARTIT_2:15;
hence thesis by A1,PARTIT_2:11;
end;
theorem
G is independent implies 'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B
,G),A,G) by PARTIT_2:11,17;
theorem Th33:
G is independent implies 'not' Ex(Ex(a,A,G),B,G) '<' 'not' Ex(
All(a,B,G),A,G)
proof
assume G is independent;
then
A1: Ex(Ex(a,A,G),B,G) = Ex(Ex(a,B,G),A,G) by PARTIT_2:16;
All(a,B,G) '<' Ex(a,B,G) by Th8;
then Ex(All(a,B,G),A,G) '<' Ex(Ex(a,A,G),B,G) by A1,PARTIT_2:13;
hence thesis by PARTIT_2:11;
end;
theorem Th34:
'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G)
proof
let z be Element of Y;
assume ('not' Ex(Ex(a,A,G),B,G)).z=TRUE;
then
A1: 'not' (Ex(Ex(a,A,G),B,G)).z=TRUE by MARGREL1:def 19;
A2: now
assume ex x being Element of Y st x in EqClass(z,CompF(B,G)) & (Ex(a,A,G)
).x=TRUE;
then (B_SUP(Ex(a,A,G),CompF(B,G))).z = TRUE by BVFUNC_1:def 17;
then (Ex(Ex(a,A,G),B,G)).z=TRUE by BVFUNC_2:def 10;
hence contradiction by A1;
end;
A3: Ex(a,A,G) = B_SUP(a,CompF(A,G)) by BVFUNC_2:def 10;
A4: for x being Element of Y st x in EqClass(z,CompF(B,G)) holds for y being
Element of Y st y in EqClass(x,CompF(A,G)) holds a.y<>TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(B,G));
then (Ex(a,A,G)).x<>TRUE by A2;
hence thesis by A3,BVFUNC_1:def 17;
end;
for x being Element of Y st x in EqClass(z,CompF(B,G)) holds (a).x<> TRUE
proof
let x be Element of Y;
A5: x in EqClass(x,CompF(A,G)) by EQREL_1:def 6;
assume x in EqClass(z,CompF(B,G));
hence thesis by A4,A5;
end;
then (B_SUP(a,CompF(B,G))).z = FALSE by BVFUNC_1:def 17;
then z in EqClass(z,CompF(A,G)) & (Ex(a,B,G)).z=FALSE by BVFUNC_2:def 10
,EQREL_1:def 6;
then (B_INF(Ex(a,B,G),CompF(A,G))).z = FALSE by BVFUNC_1:def 16;
then (All(Ex(a,B,G),A,G)).z=FALSE by BVFUNC_2:def 9;
then 'not' (All(Ex(a,B,G),A,G)).z=TRUE;
hence thesis by MARGREL1:def 19;
end;
theorem
G is independent implies 'not' Ex(All(a,A,G),B,G) '<' 'not' All(All(a,
B,G),A,G)
proof
assume G is independent;
then All('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th26;
hence thesis by BVFUNC_2:19;
end;
theorem
G is independent implies 'not' All(Ex(a,A,G),B,G) '<' 'not' All(All(a,
B,G),A,G)
proof
assume G is independent;
then
A1: Ex('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th31;
Ex('not' Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by BVFUNC_2:19;
hence thesis by A1,Th19;
end;
theorem
'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G)
proof
All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th28;
hence thesis by BVFUNC_2:19;
end;
theorem Th38:
G is independent implies 'not' Ex(All(a,A,G),B,G) '<' Ex('not'
All(a,B,G),A,G)
proof
assume G is independent;
then
A1: All('not' All(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th26;
'not' Ex(All(a,A,G),B,G) = All('not' All(a,A,G),B,G) by BVFUNC_2:19;
hence thesis by A1,BVFUNC_2:18;
end;
theorem Th39:
G is independent implies 'not' All(Ex(a,A,G),B,G) '<' Ex('not'
All(a,B,G),A,G)
proof
assume G is independent;
then
A1: Ex('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) by Th31;
'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) & Ex('not' Ex(a,A,G)
,B,G ) = Ex(All('not' a,A,G),B,G) by Th19,BVFUNC_2:19;
hence thesis by A1,BVFUNC_2:18;
end;
theorem Th40:
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
All('not' Ex(a,A,G),B,G) '<' 'not' All(All(a,B,G),A,G) & 'not' Ex(Ex(a,A
,G), B,G) = All('not' Ex(a,A,G),B,G) by Th28,BVFUNC_2:19;
hence thesis by BVFUNC_2:18;
end;
theorem Th41:
G is independent implies 'not' All(Ex(a,A,G),B,G) '<' All('not'
All(a,B,G),A,G)
proof
assume G is independent;
then 'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G) by PARTIT_2:11,17;
hence thesis by BVFUNC_2:19;
end;
theorem Th42:
G is independent implies 'not' Ex(Ex(a,A,G),B,G) '<' All('not'
All(a,B,G),A,G)
proof
assume G is independent;
then 'not' Ex(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G) by Th33;
hence thesis by BVFUNC_2:19;
end;
theorem Th43:
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G) & Ex('not' Ex(a,B,G
),A, G) = Ex(All('not' a,B,G),A,G) by Th34,BVFUNC_2:19;
hence thesis by Th19;
end;
theorem Th44:
G is independent implies 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex( a,B,G),A,G)
proof
assume G is independent;
then 'not' Ex(Ex(a,A,G),B,G) = 'not' Ex(Ex(a,B,G),A,G) by PARTIT_2:16;
hence thesis by BVFUNC_2:19;
end;
theorem Th45:
G is independent implies 'not' All(Ex(a,A,G),B,G) '<' Ex(Ex(
'not' a,B,G),A,G)
proof
assume G is independent;
then 'not' All(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G) by Th39;
hence thesis by BVFUNC_2:18;
end;
theorem Th46:
'not' Ex(Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G) by Th40;
hence thesis by BVFUNC_2:18;
end;
theorem Th47:
G is independent implies 'not' All(Ex(a,A,G),B,G) '<' All(Ex(
'not' a,B,G),A,G)
proof
assume G is independent;
then 'not' All(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G) by Th41;
hence thesis by BVFUNC_2:18;
end;
theorem Th48:
G is independent implies 'not' Ex(Ex(a,A,G),B,G) '<' All(Ex(
'not' a,B,G),A,G)
proof
assume G is independent;
then 'not' Ex(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G) by Th42;
hence thesis by BVFUNC_2:18;
end;
theorem Th49:
'not' Ex(Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G) by Th43;
hence thesis by BVFUNC_2:19;
end;
theorem Th50:
G is independent implies 'not' Ex(Ex(a,A,G),B,G) = All(All('not' a,B,G),A,G)
proof
assume G is independent;
then 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,B,G),A,G) by Th44;
hence thesis by BVFUNC_2:19;
end;
theorem
G is independent implies Ex('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,
G),A,G)
proof
assume G is independent; then
A1: 'not' All(Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G) by PARTIT_2:11,17;
'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by Th19;
hence thesis by A1,BVFUNC_2:19;
end;
theorem
All('not' Ex(a,A,G),B,G) '<' 'not' Ex(All(a,B,G),A,G)
proof
let z be Element of Y;
A1: All('not' Ex(a,A,G),B,G) = B_INF('not' Ex(a,A,G),CompF(B,G)) & z in
EqClass( z,CompF(B,G)) by BVFUNC_2:def 9,EQREL_1:def 6;
assume (All('not' Ex(a,A,G),B,G)).z=TRUE;
then ('not' Ex(a,A,G)).z=TRUE by A1,BVFUNC_1:def 16;
then
A2: Ex(a,A,G) = B_SUP(a,CompF(A,G)) & 'not' (Ex(a,A,G)).z=TRUE by
BVFUNC_2:def 10,MARGREL1:def 19;
A3: All(a,B,G) = B_INF(a,CompF(B,G)) by BVFUNC_2:def 9;
for x being Element of Y st x in EqClass(z,CompF(A,G)) holds (All(a,B,G
)).x<>TRUE
proof
let x be Element of Y;
assume x in EqClass(z,CompF(A,G)); then
A4: (a).x<>TRUE by A2,BVFUNC_1:def 17;
x in EqClass(x,CompF(B,G)) by EQREL_1:def 6;
hence thesis by A3,A4,BVFUNC_1:def 16;
end;
then Ex(All(a,B,G),A,G) = B_SUP(All(a,B,G),CompF(A,G)) & (B_SUP(All(a,B,G),
CompF( A,G))).z = FALSE by BVFUNC_1:def 17,BVFUNC_2:def 10;
then 'not' (Ex(All(a,B,G),A,G)).z=TRUE;
hence thesis by MARGREL1:def 19;
end;
theorem
All('not' Ex(a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th34;
end;
theorem
G is independent implies All('not' Ex(a,A,G),B,G) = 'not' Ex(Ex(a,B,G) ,A,G)
proof
A1: 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,PARTIT_2:16;
end;
theorem
G is independent implies Ex('not' All(a,A,G),B,G) = Ex('not' All(a,B,G ),A,G)
proof
A1: 'not' All(All(a,A,G),B,G) = Ex('not' All(a,A,G),B,G) by BVFUNC_2:18;
assume G is independent;
hence thesis by A1,Th15;
end;
theorem
G is independent implies All('not' All(a,A,G),B,G) '<' Ex('not' All(a,
B,G),A,G)
proof
A1: 'not' Ex(All(a,A,G),B,G) = All('not' All(a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th38;
end;
theorem
G is independent implies Ex('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B,
G),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) & Ex('not' Ex(a,A,G)
,B,G ) = Ex(All('not' a,A,G),B,G) by Th19,BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th39;
end;
theorem
All('not' Ex(a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th40;
end;
theorem
G is independent implies Ex('not' Ex(a,A,G),B,G) '<' All('not' All(a,B
,G),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) & Ex('not' Ex(a,A,G)
,B,G ) = Ex(All('not' a,A,G),B,G) by Th19,BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th41;
end;
theorem
G is independent implies All('not' Ex(a,A,G),B,G) '<' All('not' All(a,
B,G),A,G)
proof
assume G is independent;
then 'not' Ex(Ex(a,A,G),B,G) '<' All('not' All(a,B,G),A,G) by Th42;
hence thesis by BVFUNC_2:19;
end;
theorem
All('not' Ex(a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th43;
end;
theorem
G is independent implies All('not' Ex(a,A,G),B,G) = All('not' Ex(a,B,G ),A,G)
proof
A1: 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th44;
end;
theorem
G is independent implies Ex('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G ),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) & Ex('not' Ex(a,A,G)
,B,G ) = Ex(All('not' a,A,G),B,G) by Th19,BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th45;
end;
theorem
All('not' Ex(a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th46;
end;
theorem
G is independent implies Ex('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B,
G),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) & Ex('not' Ex(a,A,G)
,B,G ) = Ex(All('not' a,A,G),B,G) by Th19,BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th47;
end;
theorem
G is independent implies All('not' Ex(a,A,G),B,G) '<' All(Ex('not' a,B
,G),A,G)
proof
A1: 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th48;
end;
theorem
All('not' Ex(a,A,G),B,G) '<' Ex(All('not' a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th49;
end;
theorem
G is independent implies All('not' Ex(a,A,G),B,G) = All(All('not' a,B,
G),A,G)
proof
A1: 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th50;
end;
theorem
G is independent implies Ex(All('not' a,A,G),B,G) '<' 'not' Ex(All(a,B
,G),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by Th19;
assume G is independent;
hence thesis by A1,PARTIT_2:11,17;
end;
theorem
G is independent implies All(All('not' a,A,G),B,G) '<' 'not' Ex(All(a,
B,G),A,G)
proof
A1: 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) & All('not' Ex(a,A,G)
,B,G ) = All(All('not' a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th33;
end;
theorem
All(All('not' a,A,G),B,G) '<' 'not' All(Ex(a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) & All('not' Ex(a,A,G)
,B,G ) = All(All('not' a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th34;
end;
theorem
G is independent implies All(All('not' a,A,G),B,G) '<' 'not' Ex(Ex(a,B
,G),A,G)
proof
A1: 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) & All('not' Ex(a,A,G)
,B,G ) = All(All('not' a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,PARTIT_2:16;
end;
theorem
G is independent implies Ex(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B,
G),A,G)
proof
A1: 'not' All(All(a,A,G),B,G) = Ex(Ex('not' a,A,G),B,G) by Th21;
assume G is independent;
hence thesis by A1,Th15;
end;
theorem
G is independent implies All(Ex('not' a,A,G),B,G) '<' Ex('not' All(a,B
,G),A,G)
proof
A1: 'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G) by Th20;
assume G is independent;
hence thesis by A1,Th38;
end;
theorem
G is independent implies Ex(All('not' a,A,G),B,G) '<' Ex('not' All(a,B
,G),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by Th19;
assume G is independent;
hence thesis by A1,Th39;
end;
theorem
All(All('not' a,A,G),B,G) '<' Ex('not' All(a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) & All('not' Ex(a,A,G)
,B,G ) = All(All('not' a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th40;
end;
theorem
G is independent implies Ex(All('not' a,A,G),B,G) '<' All('not' All(a,
B,G),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by Th19;
assume G is independent;
hence thesis by A1,Th41;
end;
theorem
G is independent implies All(All('not' a,A,G),B,G) '<' All('not' All(a
,B,G),A,G)
proof
A1: 'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) & All('not' Ex(a,A,G)
,B,G ) = All(All('not' a,A,G),B,G) by BVFUNC_2:19;
assume G is independent;
hence thesis by A1,Th42;
end;
theorem
All(All('not' a,A,G),B,G) '<' Ex('not' Ex(a,B,G),A,G)
proof
'not' Ex(Ex(a,A,G),B,G) = All('not' Ex(a,A,G),B,G) & All('not' Ex(a,A,G)
,B,G ) = All(All('not' a,A,G),B,G) by BVFUNC_2:19;
hence thesis by Th43;
end;
theorem
G is independent implies All(All('not' a,A,G),B,G) = All('not' Ex(a,B,
G),A,G)
proof
assume G is independent;
then All(All('not' a,A,G),B,G) = All(All('not' a,B,G),A,G) by PARTIT_2:15;
hence thesis by BVFUNC_2:19;
end;
theorem
All(Ex('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
'not' Ex(All(a,A,G),B,G) = All(Ex('not' a,A,G),B,G) by Th20;
hence thesis by Th13;
end;
theorem
G is independent implies
Ex(All('not' a,A,G),B,G) '<' Ex(Ex('not' a,B,G),A,G)
proof
A1: 'not' All(Ex(a,A,G),B,G) = Ex(All('not' a,A,G),B,G) by Th19;
assume G is independent;
hence thesis by A1,Th45;
end;