:: Hierarchies and Classifications of Sets
:: by Mariusz Giero
::
:: Received December 28, 2001
:: Copyright (c) 2001-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 ORDERS_2, XBOOLE_0, SUBSET_1, ORDERS_1, XXREAL_0, YELLOW_1,
RELAT_2, WELLORD2, RELAT_1, TARSKI, TREES_1, EQREL_1, TAXONOM1, SETFAM_1,
ZFMISC_1, ABIAN, PRE_TOPC, LATTICES, ORDINAL1, PARTIT1, TAXONOM2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, ORDINAL1,
RELSET_1, STRUCT_0, ORDERS_2, EQREL_1, ABIAN, PARTIT1, ORDERS_1,
YELLOW_1, TAXONOM1;
constructors ABIAN, YELLOW_1, TAXONOM1, RELSET_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, EQREL_1, YELLOW_1;
requirements BOOLE, SUBSET;
definitions TARSKI, EQREL_1, TAXONOM1, SETFAM_1;
expansions TARSKI, SETFAM_1;
theorems TARSKI, TAXONOM1, PARTIT1, EQREL_1, ZFMISC_1, ORDERS_2, ORDERS_1,
RELAT_1, RELSET_1, SETFAM_1, ABIAN, YELLOW_1, WELLORD2, ORDINAL1,
XBOOLE_0, XBOOLE_1;
schemes XFAMILY;
begin
reserve A for RelStr;
reserve X for non empty set;
reserve PX,PY,PZ,Y,a,b,c,x,y for set;
reserve S1,S2 for Subset of Y;
definition
let A;
attr A is with_superior means
ex x be Element of A st x is_superior_of the InternalRel of A;
end;
definition
let A;
attr A is with_comparable_down means
:Def2:
for x,y be Element of A holds (
ex z be Element of A st z <= x & z <= y) implies (x <= y or y <= x);
end;
theorem Th1:
for a being set holds InclPoset {{a}} is non empty reflexive
transitive antisymmetric with_superior with_comparable_down
proof
let a be set;
set A = {{a}};
set R9 = RelIncl A;
reconsider R = R9 as Relation of A;
set L = RelStr(#A,R#);
A1: L is with_superior
proof
set max1 = {a};
reconsider max9 = max1 as Element of L by TARSKI:def 1;
take max9;
A2: for y be set st y in field R & y <> max9 holds [y,max9] in R
proof
let y be set such that
A3: y in field R and
A4: y <> max9;
field R c= A \/ A by RELSET_1:8;
hence thesis by A3,A4,TARSKI:def 1;
end;
[max9,max9] in R by WELLORD2:def 1;
then max9 in field R by RELAT_1:15;
hence thesis by A2,ORDERS_1:def 14;
end;
A5: for x,y be Element of L holds (ex z be Element of L st z <= x & z <= y)
implies x <= y or y <= x
proof
let x,y be Element of L;
assume ex z be Element of L st z <= x & z <= y;
A6: y = {a} by TARSKI:def 1;
x = {a} by TARSKI:def 1;
then [x,y] in R by A6,WELLORD2:def 1;
hence thesis by ORDERS_2:def 5;
end;
RelStr(#A,R#) = InclPoset A by YELLOW_1:def 1;
hence thesis by A1,A5;
end;
registration
cluster non empty reflexive transitive antisymmetric with_superior
with_comparable_down strict for RelStr;
existence
proof
take InclPoset {{{}}};
thus thesis by Th1;
end;
end;
definition
mode Tree is with_superior with_comparable_down Poset;
end;
theorem
for EqR being Equivalence_Relation of X, x,y,z be set holds z in
Class(EqR,x) & z in Class(EqR,y) implies Class(EqR,x) = Class(EqR,y)
proof
let EqR being Equivalence_Relation of X, x,y,z be set;
assume that
A1: z in Class(EqR,x) and
A2: z in Class(EqR,y);
A3: [z,y] in EqR by A2,EQREL_1:19;
[z,x] in EqR by A1,EQREL_1:19;
hence Class(EqR,x) = Class(EqR,z) by A1,EQREL_1:35
.= Class(EqR,y) by A1,A3,EQREL_1:35;
end;
::$CT
Lm1:
for P being a_partition of X, x,y,z being set st x in P & y in P
& z in x & z in y holds x = y by EQREL_1:70;
theorem Th3:
for C,x be set st C is Classification of X & x in union C holds x c= X
proof
let C,x be set such that
A1: C is Classification of X and
A2: x in union C;
consider Y be set such that
A3: x in Y and
A4: Y in C by A2,TARSKI:def 4;
reconsider Y9 = Y as a_partition of X by A1,A4,PARTIT1:def 3;
let a be object;
assume a in x;
then a in union Y9 by A3,TARSKI:def 4;
hence thesis;
end;
theorem
for C being set st C is Strong_Classification of X holds InclPoset
union C is Tree
proof
A1: X in {X} by TARSKI:def 1;
A2: X in {X} by TARSKI:def 1;
let C being set such that
A3: C is Strong_Classification of X;
A4: C is Classification of X by A3,TAXONOM1:def 2;
set B = union C;
A5: {X} in C by A3,TAXONOM1:def 2;
then reconsider B9 = B as non empty set by A2,TARSKI:def 4;
set R9 = RelIncl B;
reconsider R = R9 as Relation of B;
set D = RelStr(#B,R#);
{X} in C by A3,TAXONOM1:def 2;
then
A6: B <> {} by A1,TARSKI:def 4;
A7: now
let x,y be Element of D;
given z be Element of D such that
A8: z <= x and
A9: z <= y;
reconsider z9 = z as Element of B9;
reconsider z99 = z9 as Subset of X by A4,Th3;
consider Z be set such that
A10: z9 in Z and
A11: Z in C by TARSKI:def 4;
reconsider Z9 = Z as a_partition of X by A3,A11,PARTIT1:def 3;
z99 in Z9 by A10;
then z99 <> {} by EQREL_1:def 4;
then consider a be object such that
A12: a in z by XBOOLE_0:def 1;
[z,y] in R by A9,ORDERS_2:def 5;
then
A13: z c= y by A6,WELLORD2:def 1;
then
A14: a in y by A12;
A15: C is Classification of X by A3,TAXONOM1:def 2;
reconsider x9 = x, y9 = y as Element of B9;
consider S be set such that
A16: x9 in S and
A17: S in C by TARSKI:def 4;
reconsider S9 = S as a_partition of X by A3,A17,PARTIT1:def 3;
consider T be set such that
A18: y9 in T and
A19: T in C by TARSKI:def 4;
reconsider T9 = T as a_partition of X by A3,A19,PARTIT1:def 3;
[z,x] in R by A8,ORDERS_2:def 5;
then
A20: z c= x by A6,WELLORD2:def 1;
then
A21: a in x by A12;
now
per cases by A17,A19,A15,TAXONOM1:def 1;
suppose
S9 is_finer_than T9;
then ex Y be set st Y in T9 & x9 c= Y by A16;
hence x9 c= y9 or y9 c= x9 by A12,A21,A13,A18,Lm1;
end;
suppose
T9 is_finer_than S9;
then ex Y be set st Y in S9 & y9 c= Y by A18;
hence x9 c= y9 or y9 c= x9 by A12,A20,A14,A16,Lm1;
end;
end;
then [x9,y9] in R or [y9,x9] in R by WELLORD2:def 1;
hence x <= y or y <= x by ORDERS_2:def 5;
end;
A22: D is with_superior
proof
reconsider C9 = C as Strong_Classification of X by A3;
reconsider s = X as Element of D by A5,A2,TARSKI:def 4;
consider x be object such that
A23: x in SmallestPartition X by XBOOLE_0:def 1;
SmallestPartition X in C9 by TAXONOM1:def 2;
then reconsider x9 = x as Element of D by A23,TARSKI:def 4;
take s;
A24: now
let y be set such that
A25: y in field R and
y <> s;
A26: y in dom R \/ rng R by A25,RELAT_1:def 6;
per cases by A26,XBOOLE_0:def 3;
suppose
y in dom R;
then reconsider y9 = y as Element of B9;
y9 c= s by A4,Th3;
hence [y,s] in R by WELLORD2:def 1;
end;
suppose
y in rng R;
then reconsider y9 = y as Element of B9;
y9 c= s by A4,Th3;
hence [y,s] in R by WELLORD2:def 1;
end;
end;
[x9,s] in R by A6,A23,WELLORD2:def 1;
then s in field R by RELAT_1:15;
hence thesis by A24,ORDERS_1:def 14;
end;
RelStr(#B,R#) = InclPoset B by YELLOW_1:def 1;
hence thesis by A22,A7,Def2;
end;
begin
definition
let Y;
attr Y is hierarchic means
for x,y be set st x in Y & y in Y holds (x c= y or y c= x or x misses y);
end;
registration
cluster trivial -> hierarchic for set;
coherence
proof
let X be set such that
A1: X is trivial;
per cases by A1,ZFMISC_1:131;
suppose
A2: X is empty;
thus thesis by A2;
end;
suppose
ex a being object st X = {a};
then consider a be object such that
A3: X = {a};
X is hierarchic
proof
let x,y be set such that
A4: x in X and
A5: y in X;
x = a by A3,A4,TARSKI:def 1;
hence thesis by A3,A5,TARSKI:def 1;
end;
hence thesis;
end;
end;
end;
registration
cluster non trivial hierarchic for set;
existence
proof
set B = the empty set;
set A = the non empty set;
consider C be set such that
A1: C = {A,B};
A2: C is hierarchic
proof
let x,y be set such that
A3: x in C and
A4: y in C;
per cases by A1,A3,TARSKI:def 2;
suppose
A5: x = A;
per cases by A1,A4,TARSKI:def 2;
suppose
y = A;
hence thesis by A5;
end;
suppose
y = B;
hence thesis;
end;
end;
suppose
x = B;
hence thesis;
end;
end;
take C;
now
assume
A6: C is trivial;
per cases by A6,ZFMISC_1:131;
suppose
C is empty;
hence contradiction by A1;
end;
suppose
ex x being object st C = {x};
hence contradiction by A1,ZFMISC_1:5;
end;
end;
hence thesis by A2;
end;
end;
theorem Th5:
{} is hierarchic;
theorem
{{}} is hierarchic
proof
let x,y be set such that
A1: x in {{}} and
y in {{}};
x = {} by A1,TARSKI:def 1;
hence thesis;
end;
definition
let Y;
mode Hierarchy of Y -> Subset-Family of Y means
:Def4:
it is hierarchic;
existence
proof
set H = {};
reconsider H9 = H as Subset-Family of Y by XBOOLE_1:2;
take H9;
thus thesis;
end;
end;
definition
let Y;
attr Y is mutually-disjoint means
:Def5:
for x,y be set st x in Y & y in Y & x <> y holds x misses y;
end;
Lm2: now
let x,y be set such that
A1: x in {{}} and
A2: y in {{}} and
A3: x <> y;
x = {} by A1,TARSKI:def 1;
hence x misses y by A2,A3,TARSKI:def 1;
end;
registration
let Y;
cluster mutually-disjoint for Subset-Family of Y;
existence
proof
set e = {{}};
now
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in {{}};
then x = {} by TARSKI:def 1;
then xx c= Y;
hence x in bool Y;
end;
then reconsider e9 = e as Subset-Family of Y by TARSKI:def 3;
take e9;
thus thesis by Lm2;
end;
end;
theorem
{} is mutually-disjoint;
theorem
{{}} is mutually-disjoint by Lm2;
theorem Th9:
{a} is mutually-disjoint
proof
let x,y be set such that
A1: x in {a} and
A2: y in {a} and
A3: x <> y;
x = a by A1,TARSKI:def 1;
hence thesis by A2,A3,TARSKI:def 1;
end;
Lm3: now
let Y;
let H be Hierarchy of Y such that
A1: H is covering;
let B be mutually-disjoint Subset-Family of Y such that
A2: B c= H and
A3: for C being mutually-disjoint Subset-Family of Y st C c= H & union B
c= union C holds B = C;
Y c= union B
proof
let y be object;
assume y in Y;
then y in union H by A1,ABIAN:4;
then consider x be set such that
A4: y in x and
A5: x in H by TARSKI:def 4;
now
defpred X[set] means $1 c= x;
consider D be set such that
A6: for a be set holds a in D iff a in B & X[a] from XFAMILY:sch 1;
set C = (B \ D) \/ {x};
A7: (B \ D) c= C by XBOOLE_1:7;
A8: {x} c= H
by A5,TARSKI:def 1;
assume
A9: not y in union B;
A10: for p being set st p in B & not p in D & p <> x holds p misses x
proof
A11: H is hierarchic by Def4;
let p be set such that
A12: p in B and
A13: not p in D and
p <> x;
A14: not x c= p by A4,A9,A12,TARSKI:def 4;
not p c= x by A6,A12,A13;
hence thesis by A2,A5,A12,A14,A11;
end;
A15: for p,q be set st p in C & q in C & p <> q holds p misses q
proof
let p,q be set such that
A16: p in C and
A17: q in C and
A18: p <> q;
per cases by A16,XBOOLE_0:def 3;
suppose
A19: p in (B \ D);
then
A20: not p in D by XBOOLE_0:def 5;
A21: p in B by A19,XBOOLE_0:def 5;
per cases by A17,XBOOLE_0:def 3;
suppose
q in (B \ D);
then q in B by XBOOLE_0:def 5;
hence thesis by A18,A21,Def5;
end;
suppose
q in {x};
then q = x by TARSKI:def 1;
hence thesis by A10,A18,A21,A20;
end;
end;
suppose
p in {x};
then
A22: p = x by TARSKI:def 1;
per cases by A17,XBOOLE_0:def 3;
suppose
A23: q in (B \ D);
then
A24: not q in D by XBOOLE_0:def 5;
q in B by A23,XBOOLE_0:def 5;
hence thesis by A10,A18,A22,A24;
end;
suppose
q in {x};
hence thesis by A18,A22,TARSKI:def 1;
end;
end;
end;
x in {x} by TARSKI:def 1;
then
A25: x in C by XBOOLE_0:def 3;
A26: union B c= union C
proof
let s be object;
assume s in union B;
then consider t be set such that
A27: s in t and
A28: t in B by TARSKI:def 4;
per cases;
suppose
t in D;
then t c= x by A6;
hence thesis by A25,A27,TARSKI:def 4;
end;
suppose
not t in D;
then t in (B \ D) by A28,XBOOLE_0:def 5;
hence thesis by A7,A27,TARSKI:def 4;
end;
end;
A29: x in {x} by TARSKI:def 1;
(B \ D) c= B by XBOOLE_1:36;
then
A30: (B \ D) c= H by A2;
then C c= H by A8,XBOOLE_1:8;
then C is mutually-disjoint Subset-Family of Y by A15,Def5,XBOOLE_1:1;
then
A31: B = C by A3,A30,A8,A26,XBOOLE_1:8;
{x} c= (B \ D) \/ {x} by XBOOLE_1:7;
hence contradiction by A4,A9,A31,A29,TARSKI:def 4;
end;
hence thesis;
end;
hence union B = Y by XBOOLE_0:def 10;
end;
Lm4: now
let Y;
let H be Hierarchy of Y;
let B be mutually-disjoint Subset-Family of Y such that
A1: B c= H and
A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B
c= union C holds B = C;
let S1 such that
A3: S1 in B;
now
set C = B \ {{}};
assume
A4: S1 = {};
A5: union B c= union C
proof
let x be object;
assume x in union B;
then consider y be set such that
A6: x in y and
A7: y in B by TARSKI:def 4;
not y in {{}} by A6,TARSKI:def 1;
then y in C by A7,XBOOLE_0:def 5;
hence thesis by A6,TARSKI:def 4;
end;
A8: C is mutually-disjoint
proof
let x,y be set such that
A9: x in C and
A10: y in C and
A11: x <> y;
A12: y in B by A10,XBOOLE_0:def 5;
x in B by A9,XBOOLE_0:def 5;
hence thesis by A11,A12,Def5;
end;
C c= B by XBOOLE_1:36;
then C c= H by A1;
then B = C by A2,A5,A8;
then not {} in {{}} by A3,A4,XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
hence S1 <> {};
end;
definition
let Y;
let F be Subset-Family of Y;
attr F is T_3 means
:Def6:
for A be Subset of Y st A in F for x be Element
of Y st not x in A ex B be Subset of Y st x in B & B in F & A misses B;
end;
theorem
for F be Subset-Family of Y st F = {} holds F is T_3;
registration
let Y;
cluster covering T_3 for Hierarchy of Y;
existence
proof
per cases;
suppose
A1: Y <> {};
set H9 = {Y};
reconsider H = H9 as Subset-Family of Y by ZFMISC_1:68;
H is hierarchic
proof
let x,y be set such that
A2: x in H and
A3: y in H;
x = Y by A2,TARSKI:def 1;
hence thesis by A3;
end;
then reconsider H as Hierarchy of Y by Def4;
take H;
union H = Y by ZFMISC_1:25;
hence H is covering by ABIAN:4;
thus H is T_3
proof
let A be Subset of Y;
assume A in H;
then
A4: A = Y by TARSKI:def 1;
let x be Element of Y;
assume not x in A;
hence thesis by A1,A4;
end;
end;
suppose
A5: Y = {};
set H9 = {};
reconsider H = H9 as Subset-Family of Y by XBOOLE_1:2;
reconsider H1 = H as Hierarchy of Y by Def4,Th5;
take H1;
thus H1 is covering by A5,ABIAN:4,ZFMISC_1:2;
thus thesis;
end;
end;
end;
definition
let Y;
let F be Subset-Family of Y;
attr F is lower-bounded means
for B being set st B <> {} & B c= F & B
is c=-linear ex c st c in F & c c= meet B;
end;
theorem Th11:
for B being mutually-disjoint Subset-Family of Y st for b be set
st b in B holds S1 misses b & Y <> {} holds B \/ {S1} is mutually-disjoint
Subset-Family of Y & (S1 <> {} implies union (B \/ {S1}) <> union B)
proof
let B being mutually-disjoint Subset-Family of Y such that
A1: for b be set st b in B holds S1 misses b & Y <> {};
set C = B \/ {S1};
A2: now
let c1,c2 be set such that
A3: c1 in C and
A4: c2 in C and
A5: c1 <> c2;
per cases by A3,XBOOLE_0:def 3;
suppose
A6: c1 in B;
per cases by A4,XBOOLE_0:def 3;
suppose
c2 in B;
hence c1 misses c2 by A5,A6,Def5;
end;
suppose
c2 in {S1};
then c2 = S1 by TARSKI:def 1;
hence c1 misses c2 by A1,A6;
end;
end;
suppose
c1 in {S1};
then
A7: c1 = S1 by TARSKI:def 1;
then not c2 in {S1} by A5,TARSKI:def 1;
then c2 in B by A4,XBOOLE_0:def 3;
hence c1 misses c2 by A1,A7;
end;
end;
{S1} c= bool Y
proof
let p be object;
assume p in {S1};
then p = S1 by TARSKI:def 1;
hence thesis;
end;
hence C is mutually-disjoint Subset-Family of Y by A2,Def5,XBOOLE_1:8;
thus S1 <> {} implies union C <> union B
proof
assume
A8: S1 <> {};
not union C c= union B
proof
A9: {S1} c= C by XBOOLE_1:7;
assume
A10: union C c= union B;
consider p be object such that
A11: p in S1 by A8,XBOOLE_0:def 1;
S1 in {S1} by TARSKI:def 1;
then p in union C by A11,A9,TARSKI:def 4;
then consider S2 be set such that
A12: p in S2 and
A13: S2 in B by A10,TARSKI:def 4;
S1 misses S2 by A1,A13;
hence contradiction by A11,A12,XBOOLE_0:3;
end;
hence thesis;
end;
end;
definition
let Y;
let F be Subset-Family of Y;
attr F is with_max's means
for S being Subset of Y st S in F ex T
being Subset of Y st S c= T & T in F & for V being Subset of Y st T c= V & V in
F holds V = Y;
end;
begin
theorem
for H being covering Hierarchy of Y st H is with_max's ex P being
a_partition of Y st P c= H
proof
let H be covering Hierarchy of Y such that
A1: H is with_max's;
per cases;
suppose
A2: Y = {};
set P9 = {};
reconsider P = P9 as Subset-Family of Y by XBOOLE_1:2;
take P;
thus thesis by A2,EQREL_1:45;
end;
suppose
A3: Y <> {};
now
per cases;
suppose
A4: Y in H;
set P = {Y};
A5: P c= H
by A4,TARSKI:def 1;
P is a_partition of Y by A3,EQREL_1:39;
hence thesis by A5;
end;
suppose
A6: not Y in H;
defpred X[set] means ex S be Subset of Y st (S in H & S c= $1 & for V
being Subset of Y st $1 c= V & V in H holds V = Y);
consider P9 be set such that
A7: for T be set holds T in P9 iff T in H & X[T] from XFAMILY:
sch 1;
A8: P9 c= H
by A7;
then reconsider P = P9 as Subset-Family of Y by XBOOLE_1:1;
A9: now
let S1 such that
A10: S1 in P;
thus S1 <> {}
proof
consider S be Subset of Y such that
A11: S in H and
A12: S c= S1 and
A13: for V being Subset of Y st S1 c= V & V in H holds V = Y by A7,A10;
assume
A14: S1 = {};
then S1 = S by A12
.= Y by A14,A11,A13,XBOOLE_1:2;
hence contradiction by A3,A14;
end;
thus for S2 st S2 in P holds S1 = S2 or S1 misses S2
proof
let S2 such that
A15: S2 in P;
A16: ex T be Subset of Y st T in H & T c= S2 & for V being
Subset of Y st S2 c= V & V in H holds V = Y by A7,A15;
S2 in H by A7,A15;
hence thesis by A6,A16;
end;
end;
A17: union H = Y by ABIAN:4;
Y c= union P
proof
let p be object;
assume p in Y;
then consider h9 be set such that
A18: p in h9 and
A19: h9 in H by A17,TARSKI:def 4;
reconsider h = h9 as Subset of Y by A19;
consider T be Subset of Y such that
A20: h c= T and
A21: T in H and
A22: for V being Subset of Y st T c= V & V in H holds V = Y by A1,A19;
T in P by A7,A21,A22;
hence thesis by A18,A20,TARSKI:def 4;
end;
then union P = Y by XBOOLE_0:def 10;
then P is a_partition of Y by A9,EQREL_1:def 4;
hence thesis by A8;
end;
end;
hence thesis;
end;
end;
theorem
for H being covering Hierarchy of Y for B being mutually-disjoint
Subset-Family of Y st B c= H & for C being mutually-disjoint Subset-Family of Y
st C c= H & union B c= union C holds B = C holds B is a_partition of Y
proof
let H be covering Hierarchy of Y;
let B be mutually-disjoint Subset-Family of Y such that
A1: B c= H and
A2: for C being mutually-disjoint Subset-Family of Y st C c= H & union B
c= union C holds B = C;
thus union B = Y by A1,A2,Lm3;
thus thesis by A1,A2,Def5,Lm4;
end;
theorem
for H being covering T_3 Hierarchy of Y st H is lower-bounded & not {}
in H for A being Subset of Y for B being mutually-disjoint Subset-Family of Y
st A in B & B c= H & for C being mutually-disjoint Subset-Family of Y st A in C
& C c= H & union B c= union C holds union B = union C holds B is a_partition of
Y
proof
let H be covering T_3 Hierarchy of Y such that
A1: H is lower-bounded and
A2: not {} in H;
let A be Subset of Y;
let B be mutually-disjoint Subset-Family of Y such that
A3: A in B and
A4: B c= H and
A5: for C being mutually-disjoint Subset-Family of Y st A in C & C c= H
& union B c= union C holds union B = union C;
A6: union H = Y by ABIAN:4;
A7: H is hierarchic by Def4;
per cases;
suppose
A8: Y <> {};
Y c= union B
proof
assume not Y c= union B;
then consider x be object such that
A9: x in Y and
A10: not x in union B;
consider xx be set such that
A11: x in xx and
A12: xx in H by A6,A9,TARSKI:def 4;
defpred X[set] means x in $1;
consider D be set such that
A13: for h be set holds h in D iff h in H & X[h] from XFAMILY:sch 1;
A14: D c= H
by A13;
now
let h1,h2 be set such that
A15: h1 in D and
A16: h2 in D;
now
A17: x in h2 by A13,A16;
assume
A18: h1 misses h2;
x in h1 by A13,A15;
hence contradiction by A18,A17,XBOOLE_0:3;
end;
then h1 c= h2 or h2 c= h1 by A7,A14,A15,A16;
hence h1,h2 are_c=-comparable by XBOOLE_0:def 9;
end;
then
A19: D is c=-linear by ORDINAL1:def 8;
xx in D by A13,A11,A12;
then consider min1 be set such that
A20: min1 in H and
A21: min1 c= meet D by A1,A14,A19;
reconsider min9 = min1 as Subset of Y by A20;
set C = B \/ {min9};
A22: B c= C by XBOOLE_1:7;
now
reconsider x9 = x as Element of Y by A9;
let b1 be set such that
A23: b1 in B;
reconsider b19 = b1 as Subset of Y by A23;
A24: not x9 in b19 by A10,A23,TARSKI:def 4;
A25: not b1 c= min9
proof
reconsider b19 = b1 as Subset of Y by A23;
consider k be Subset of Y such that
A26: x9 in k and
A27: k in H and
A28: k misses b19 by A4,A23,A24,Def6;
k in D by A13,A26,A27;
then meet D c= k by SETFAM_1:3;
then
A29: min9 c= k by A21;
b1 <> {} by A2,A4,A23;
then
A30: ex y be object st y in b19 by XBOOLE_0:def 1;
assume b1 c= min9;
then b19 c= k by A29;
hence contradiction by A28,A30,XBOOLE_0:3;
end;
not min9 c= b1
proof
consider k be Subset of Y such that
A31: x9 in k and
A32: k in H and
A33: k misses b19 by A4,A23,A24,Def6;
k in D by A13,A31,A32;
then meet D c= k by SETFAM_1:3;
then
A34: min9 c= k by A21;
assume
A35: min9 c= b1;
ex y be object st y in min9 by A2,A20,XBOOLE_0:def 1;
hence contradiction by A35,A33,A34,XBOOLE_0:3;
end;
hence b1 misses min9 by A4,A7,A20,A23,A25;
end;
then
A36: for b be set st b in B holds min9 misses b & Y <> {} by A8;
then
A37: C is mutually-disjoint Subset-Family of Y by Th11;
{min9} c= H
by A20,TARSKI:def 1;
then
A38: C c= H by A4,XBOOLE_1:8;
union C <> union B by A2,A20,A36,Th11;
hence contradiction by A3,A5,A37,A38,A22,ZFMISC_1:77;
end;
then
A39: union B = Y by XBOOLE_0:def 10;
for A be Subset of Y st A in B holds (A <> {} & for E be Subset of Y
st E in B holds A = E or A misses E) by A2,A4,Def5;
hence thesis by A39,EQREL_1:def 4;
end;
suppose
A40: Y = {};
now
per cases by A40,ZFMISC_1:1,33;
suppose
H = {};
hence B = {} by A4;
end;
suppose
A41: H = {{}};
B <> {{}}
proof
assume B = {{}};
then {} in B by TARSKI:def 1;
hence contradiction by A2,A4;
end;
hence B = {} by A4,A41,ZFMISC_1:33;
end;
end;
hence thesis by A40,EQREL_1:45;
end;
end;
theorem Th15:
for H being covering T_3 Hierarchy of Y st H is lower-bounded &
not {} in H for A being Subset of Y for B being mutually-disjoint Subset-Family
of Y st A in B & B c= H & for C being mutually-disjoint Subset-Family of Y st A
in C & C c= H & B c= C holds B = C holds B is a_partition of Y
proof
let H be covering T_3 Hierarchy of Y such that
A1: H is lower-bounded and
A2: not {} in H;
let A be Subset of Y;
let B be mutually-disjoint Subset-Family of Y such that
A3: A in B and
A4: B c= H and
A5: for C being mutually-disjoint Subset-Family of Y st A in C & C c= H
& B c= C holds B = C;
A6: union H = Y by ABIAN:4;
A7: H is hierarchic by Def4;
per cases;
suppose
A8: Y <> {};
Y c= union B
proof
assume not Y c= union B;
then consider x be object such that
A9: x in Y and
A10: not x in union B;
consider xx be set such that
A11: x in xx and
A12: xx in H by A6,A9,TARSKI:def 4;
defpred X[set] means x in $1;
consider D be set such that
A13: for h be set holds h in D iff h in H & X[h] from XFAMILY:sch 1;
A14: D c= H
by A13;
now
let h1,h2 be set such that
A15: h1 in D and
A16: h2 in D;
now
A17: x in h2 by A13,A16;
assume
A18: h1 misses h2;
x in h1 by A13,A15;
hence contradiction by A18,A17,XBOOLE_0:3;
end;
then h1 c= h2 or h2 c= h1 by A7,A14,A15,A16;
hence h1,h2 are_c=-comparable by XBOOLE_0:def 9;
end;
then
A19: D is c=-linear by ORDINAL1:def 8;
xx in D by A13,A11,A12;
then consider min1 be set such that
A20: min1 in H and
A21: min1 c= meet D by A1,A14,A19;
reconsider min9 = min1 as Subset of Y by A20;
A22: {min9} c= H
by A20,TARSKI:def 1;
set C = B \/ {min9};
now
reconsider x9 = x as Element of Y by A9;
let b1 be set such that
A23: b1 in B;
reconsider b19 = b1 as Subset of Y by A23;
A24: not x9 in b19 by A10,A23,TARSKI:def 4;
A25: not b1 c= min9
proof
reconsider b19 = b1 as Subset of Y by A23;
consider k be Subset of Y such that
A26: x9 in k and
A27: k in H and
A28: k misses b19 by A4,A23,A24,Def6;
k in D by A13,A26,A27;
then meet D c= k by SETFAM_1:3;
then
A29: min9 c= k by A21;
b1 <> {} by A2,A4,A23;
then
A30: ex y be object st y in b19 by XBOOLE_0:def 1;
assume b1 c= min9;
then b19 c= k by A29;
hence contradiction by A28,A30,XBOOLE_0:3;
end;
not min9 c= b1
proof
consider k be Subset of Y such that
A31: x9 in k and
A32: k in H and
A33: k misses b19 by A4,A23,A24,Def6;
k in D by A13,A31,A32;
then meet D c= k by SETFAM_1:3;
then
A34: min9 c= k by A21;
assume
A35: min9 c= b1;
ex y be object st y in min9 by A2,A20,XBOOLE_0:def 1;
hence contradiction by A35,A33,A34,XBOOLE_0:3;
end;
hence b1 misses min9 by A4,A7,A20,A23,A25;
end;
then
A36: for b be set st b in B holds min9 misses b & Y <> {} by A8;
then
A37: C is mutually-disjoint Subset-Family of Y by Th11;
A38: B c= C by XBOOLE_1:7;
union C <> union B by A2,A20,A36,Th11;
hence contradiction by A3,A4,A5,A37,A22,A38,XBOOLE_1:8;
end;
then
A39: union B = Y by XBOOLE_0:def 10;
for A be Subset of Y st A in B holds (A <> {} & for E be Subset of Y
st E in B holds A = E or A misses E) by A2,A4,Def5;
hence thesis by A39,EQREL_1:def 4;
end;
suppose
A40: Y = {};
now
per cases by A40,ZFMISC_1:1,33;
suppose
H = {};
hence B = {} by A4;
end;
suppose
A41: H = {{}};
B <> {{}}
proof
assume B = {{}};
then {} in B by TARSKI:def 1;
hence contradiction by A2,A4;
end;
hence B = {} by A4,A41,ZFMISC_1:33;
end;
end;
hence thesis by A40,EQREL_1:45;
end;
end;
theorem Th16:
for H being covering T_3 Hierarchy of Y st H is lower-bounded &
not {} in H for A being Subset of Y st A in H ex P being a_partition of Y st A
in P & P c= H
proof
let H be covering T_3 Hierarchy of Y such that
A1: H is lower-bounded and
A2: not {} in H;
let A be Subset of Y such that
A3: A in H;
set k1 = {A};
A4: k1 c= H by A3,ZFMISC_1:31;
A5: A in k1 by TARSKI:def 1;
A6: k1 c= bool Y by ZFMISC_1:31;
defpred X[set] means A in $1 & $1 is mutually-disjoint & $1 c= H;
consider K be set such that
A7: for S be set holds S in K iff S in bool bool Y & X[S] from XFAMILY:
sch 1;
k1 is mutually-disjoint by Th9;
then
A8: k1 in K by A7,A5,A4,A6;
for Z be set st Z c= K & Z is c=-linear ex X3 be set st X3 in K & for
X1 be set st X1 in Z holds X1 c= X3
proof
let Z be set such that
A9: Z c= K and
A10: Z is c=-linear;
A11: for X1,X2 being set st X1 in Z & X2 in Z holds X1 c= X2 or X2 c= X1
by XBOOLE_0:def 9,A10,ORDINAL1:def 8;
per cases;
suppose
A12: Z <> {};
set X3 = union Z;
take X3;
now
consider z be object such that
A13: z in Z by A12,XBOOLE_0:def 1;
reconsider z as set by TARSKI:1;
A in z by A7,A9,A13;
hence A in X3 by A13,TARSKI:def 4;
A14: for a st a in Z holds a c= H by A7,A9;
then X3 c= H by ZFMISC_1:76;
then X3 c= bool Y by XBOOLE_1:1;
hence X3 in bool bool Y;
thus X3 is mutually-disjoint
proof
let t1,t2 be set such that
A15: t1 in X3 and
A16: t2 in X3 and
A17: t1 <> t2;
consider v1 be set such that
A18: t1 in v1 and
A19: v1 in Z by A15,TARSKI:def 4;
A20: v1 is mutually-disjoint by A7,A9,A19;
consider v2 be set such that
A21: t2 in v2 and
A22: v2 in Z by A16,TARSKI:def 4;
A23: v2 is mutually-disjoint by A7,A9,A22;
per cases by A11,A19,A22;
suppose
v1 c= v2;
hence thesis by A17,A18,A21,A23;
end;
suppose
v2 c= v1;
hence thesis by A17,A18,A21,A20;
end;
end;
thus X3 c= H by A14,ZFMISC_1:76;
end;
hence X3 in K by A7;
thus thesis by ZFMISC_1:74;
end;
suppose
A24: Z = {};
consider a be set such that
A25: a in K by A8;
take a;
thus a in K by A25;
thus thesis by A24;
end;
end;
then consider M be set such that
A26: M in K and
A27: for Z be set st Z in K & Z <> M holds not M c= Z by A8,ORDERS_1:65;
A28: M is mutually-disjoint Subset-Family of Y by A7,A26;
A29: for C being mutually-disjoint Subset-Family of Y
st A in C & C c= H & M c= C
holds M = C by A27,A7;
A30: A in M by A7,A26;
take M;
M c= H by A7,A26;
hence thesis by A1,A2,A28,A30,A29,Th15;
end;
Lm5: now
let x be non empty set;
A1: ex a be object st a in x by XBOOLE_0:def 1;
let y;
assume x c= y;
hence x meets y by A1,XBOOLE_0:3;
end;
theorem Th17:
for h being non empty set for Pmin being a_partition of X for hw
being set st hw in Pmin & h c= hw for PS being a_partition of X st h in PS &
for x st x in PS holds (x c= hw or hw c= x or hw misses x) for PT be set st (
for a holds a in PT iff a in PS & a c= hw) holds PT \/ (Pmin \ {hw}) is
a_partition of X & PT \/ (Pmin \ {hw}) is_finer_than Pmin
proof
let h be non empty set;
let Pmin be a_partition of X;
let hw be set such that
A1: hw in Pmin and
A2: h c= hw;
let PS being a_partition of X such that
A3: h in PS and
A4: for x st x in PS holds (x c= hw or hw c= x or hw misses x);
let PT be set such that
A5: for a holds a in PT iff a in PS & a c= hw;
A6: PT c= PS
by A5;
A7: union PS = X by EQREL_1:def 4;
A8: union Pmin = X by EQREL_1:def 4;
set P = PT \/ (Pmin \ {hw});
A9: PT c= P by XBOOLE_1:7;
A10: Pmin \ {hw} c= P by XBOOLE_1:7;
A11: h in PT by A2,A3,A5;
A12: X c= union P
proof
let a be object such that
A13: a in X;
consider b such that
A14: a in b and
A15: b in Pmin by A8,A13,TARSKI:def 4;
per cases;
suppose
A16: b = hw;
consider c such that
A17: a in c and
A18: c in PS by A7,A13,TARSKI:def 4;
A19: hw meets c by A14,A16,A17,XBOOLE_0:3;
per cases by A4,A18,A19;
suppose
hw c= c;
then
A20: h c= c by A2;
h meets c
proof
A21: ex x being object st x in h by XBOOLE_0:def 1;
assume h misses c;
hence contradiction by A20,A21,XBOOLE_0:3;
end;
then h = c by A3,A18,EQREL_1:def 4;
hence thesis by A9,A11,A17,TARSKI:def 4;
end;
suppose
c c= hw;
then c in PT by A5,A18;
hence thesis by A9,A17,TARSKI:def 4;
end;
end;
suppose
b <> hw;
then not b in {hw} by TARSKI:def 1;
then b in Pmin \ {hw} by A15,XBOOLE_0:def 5;
hence thesis by A10,A14,TARSKI:def 4;
end;
end;
A22: Pmin \ {hw} c= Pmin by XBOOLE_1:36;
A23: now
let x,y such that
A24: x in PT and
A25: y in Pmin \ {hw};
A26: y in Pmin by A25,XBOOLE_0:def 5;
not y in {hw} by A25,XBOOLE_0:def 5;
then
A27: y <> hw by TARSKI:def 1;
A28: x c= hw by A5,A24;
now
assume x meets y;
then ex a being object st a in x & a in y by XBOOLE_0:3;
then hw meets y by A28,XBOOLE_0:3;
hence contradiction by A1,A26,A27,EQREL_1:def 4;
end;
hence x misses y;
end;
A29: now
let A be Subset of X such that
A30: A in P;
now
per cases by A30,XBOOLE_0:def 3;
suppose
A in PT;
hence A <> {} by A6,EQREL_1:def 4;
end;
suppose
A in Pmin \ {hw};
hence A <> {} by A22,EQREL_1:def 4;
end;
end;
hence A <> {};
thus for B be Subset of X st B in P holds A = B or A misses B
proof
let B be Subset of X such that
A31: B in P;
per cases by A30,XBOOLE_0:def 3;
suppose
A32: A in PT;
per cases by A31,XBOOLE_0:def 3;
suppose
B in PT;
hence thesis by A6,A32,EQREL_1:def 4;
end;
suppose
B in Pmin \ {hw};
hence thesis by A23,A32;
end;
end;
suppose
A33: A in Pmin \ {hw};
per cases by A31,XBOOLE_0:def 3;
suppose
B in PT;
hence thesis by A23,A33;
end;
suppose
B in Pmin \ {hw};
hence thesis by A22,A33,EQREL_1:def 4;
end;
end;
end;
end;
PT c= bool X by A6,XBOOLE_1:1;
then
A34: P c= bool X by XBOOLE_1:8;
union P c= X
proof
let a be object;
assume a in union P;
then ex b st a in b & b in P by TARSKI:def 4;
hence thesis by A34;
end;
then union P = X by A12,XBOOLE_0:def 10;
hence PT \/ (Pmin \ {hw}) is a_partition of X by A34,A29,EQREL_1:def 4;
let a such that
A35: a in P;
per cases by A35,XBOOLE_0:def 3;
suppose
a in PT;
then a c= hw by A5;
hence thesis by A1;
end;
suppose
a in Pmin \ {hw};
hence thesis by A22;
end;
end;
theorem Th18:
for h being non empty set st h c= X for Pmax being a_partition
of X st ( (ex hy be set st hy in Pmax & hy c= h) & for x st x in Pmax holds (x
c= h or h c= x or h misses x)) for Pb be set st (for x holds x in Pb iff (x in
Pmax & x misses h)) holds Pb \/ {h} is a_partition of X & Pmax is_finer_than (
Pb \/ {h})& for Pmin being a_partition of X st Pmax is_finer_than Pmin for hw
being set st hw in Pmin & h c= hw holds (Pb \/ {h}) is_finer_than Pmin
proof
let h be non empty set such that
A1: h c= X;
A2: {h} c= bool X
proof
let s be object;
assume s in {h};
then s = h by TARSKI:def 1;
hence thesis by A1;
end;
A3: h in {h} by TARSKI:def 1;
let Pmax be a_partition of X such that
A4: ex hy be set st hy in Pmax & hy c= h and
A5: for x st x in Pmax holds (x c= h or h c= x or h misses x);
A6: now
let s be set such that
A7: s in Pmax and
A8: h c= s;
consider hy be set such that
A9: hy in Pmax and
A10: hy c= h by A4;
hy <> {} by A9,EQREL_1:def 4;
then hy meets s by A8,A10,Lm5,XBOOLE_1:1;
then s = hy by A7,A9,EQREL_1:def 4;
hence h = s by A8,A10,XBOOLE_0:def 10;
end;
let Pb be set such that
A11: for x holds x in Pb iff x in Pmax & x misses h;
set P = Pb \/ {h};
A12: Pb c= P by XBOOLE_1:7;
A13: Pb c= Pmax
by A11;
A14: now
let A be Subset of X such that
A15: A in P;
now
per cases by A15,XBOOLE_0:def 3;
suppose
A in Pb;
then A in Pmax by A11;
hence A <> {} by EQREL_1:def 4;
end;
suppose
A in {h};
hence A <> {} by TARSKI:def 1;
end;
end;
hence A<>{};
thus for B be Subset of X st B in P holds A = B or A misses B
proof
let B be Subset of X such that
A16: B in P;
per cases by A15,XBOOLE_0:def 3;
suppose
A17: A in Pb;
per cases by A16,XBOOLE_0:def 3;
suppose
B in Pb;
hence thesis by A13,A17,EQREL_1:def 4;
end;
suppose
B in {h};
then B = h by TARSKI:def 1;
hence thesis by A11,A17;
end;
end;
suppose
A18: A in {h};
per cases by A16,XBOOLE_0:def 3;
suppose
A19: B in Pb;
A = h by A18,TARSKI:def 1;
hence thesis by A11,A19;
end;
suppose
B in {h};
then B = h by TARSKI:def 1;
hence thesis by A18,TARSKI:def 1;
end;
end;
end;
end;
A20: {h} c= P by XBOOLE_1:7;
A21: union Pmax = X by EQREL_1:def 4;
A22: X c= union P
proof
let s be object;
assume s in X;
then consider t be set such that
A23: s in t and
A24: t in Pmax by A21,TARSKI:def 4;
per cases;
suppose
t in Pb;
hence thesis by A12,A23,TARSKI:def 4;
end;
suppose
not t in Pb;
then
A25: t meets h by A11,A24;
per cases by A5,A24,A25;
suppose
h c= t;
then t = h by A6,A24;
hence thesis by A3,A20,A23,TARSKI:def 4;
end;
suppose
A26: t c= h;
h in {h} by TARSKI:def 1;
hence thesis by A20,A23,A26,TARSKI:def 4;
end;
end;
end;
Pb c= bool X by A13,XBOOLE_1:1;
then
A27: P c= bool X by A2,XBOOLE_1:8;
union P c= X
proof
let s be object;
assume s in union P;
then ex t be set st s in t & t in P by TARSKI:def 4;
hence thesis by A27;
end;
then union P = X by A22,XBOOLE_0:def 10;
hence Pb \/ {h} is a_partition of X by A27,A14,EQREL_1:def 4;
thus Pmax is_finer_than (Pb \/ {h})
proof
let x be set such that
A28: x in Pmax;
per cases;
suppose
x c= h;
hence thesis by A3,A20;
end;
suppose
A29: not x c= h;
per cases by A5,A28,A29;
suppose
h c= x;
then h = x by A6,A28;
hence thesis by A3,A20;
end;
suppose
h misses x;
then x in Pb by A11,A28;
hence thesis by A12;
end;
end;
end;
let Pmin be a_partition of X such that
A30: Pmax is_finer_than Pmin;
let hw be set such that
A31: hw in Pmin and
A32: h c= hw;
let s be set such that
A33: s in P;
per cases by A33,XBOOLE_0:def 3;
suppose
s in Pb;
then s in Pmax by A11;
hence thesis by A30;
end;
suppose
s in {h};
then s = h by TARSKI:def 1;
hence thesis by A31,A32;
end;
end;
theorem
for H being covering T_3 Hierarchy of X st H is lower-bounded & not {}
in H & (for C1 be set st (C1 <> {} & C1 c= PARTITIONS(X) & (for P1,P2 be set st
P1 in C1 & P2 in C1 holds P1 is_finer_than P2 or P2 is_finer_than P1)) holds (
ex PX,PY st (PX in C1 & PY in C1 & for PZ st PZ in C1 holds PZ is_finer_than PY
& PX is_finer_than PZ))) ex C being Classification of X st union C = H
proof
let H be covering T_3 Hierarchy of X such that
A1: H is lower-bounded and
A2: not {} in H and
A3: for C1 be set st C1 <> {} & C1 c= PARTITIONS(X) & (for P1,P2 be set
st P1 in C1 & P2 in C1 holds P1 is_finer_than P2 or P2 is_finer_than P1) holds
ex PX,PY st (PX in C1 & PY in C1 & for PZ st PZ in C1 holds PZ is_finer_than PY
& PX is_finer_than PZ);
union H = X by ABIAN:4;
then consider h be object such that
A4: h in H by XBOOLE_0:def 1,ZFMISC_1:2;
reconsider h as Subset of X by A4;
consider PX being a_partition of X such that
h in PX and
A5: PX c= H by A1,A2,A4,Th16;
set L = {PX};
A6: L c= PARTITIONS(X)
proof
let l be object;
assume l in L;
then l = PX by TARSKI:def 1;
hence thesis by PARTIT1:def 3;
end;
A7: now
let P1,P2 be set;
assume that
A8: P1 in L and
A9: P2 in L;
P1 = PX by A8,TARSKI:def 1;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A9,TARSKI:def 1;
end;
A10: H is hierarchic by Def4;
defpred X[set] means (for P be set holds P in $1 implies P c= H) & (for P1,
P2 be set holds P1 in $1 & P2 in $1 implies P1 is_finer_than P2 or P2
is_finer_than P1);
consider RL be set such that
A11: for L be set holds L in RL iff L in bool PARTITIONS X & X[L] from
XFAMILY:sch 1;
for a st a in L holds a c= H by A5,TARSKI:def 1;
then
A12: L in RL by A11,A6,A7;
now
let Z be set such that
A13: Z c= RL and
A14: Z is c=-linear;
set Y = union Z;
A15: for X1,X2 being set st X1 in Z & X2 in Z holds X1 c= X2 or X2 c= X1
by XBOOLE_0:def 9,A14,ORDINAL1:def 8;
A16: now
let P1,P2 be set;
assume that
A17: P1 in Y and
A18: P2 in Y;
consider L1 be set such that
A19: P1 in L1 and
A20: L1 in Z by A17,TARSKI:def 4;
consider L2 be set such that
A21: P2 in L2 and
A22: L2 in Z by A18,TARSKI:def 4;
per cases by A15,A20,A22;
suppose
L1 c= L2;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A11,A13,A19,A21,A22
;
end;
suppose
L2 c= L1;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A11,A13,A19,A20,A21
;
end;
end;
take Y;
A23: now
let P be set;
assume P in Y;
then ex L3 be set st P in L3 & L3 in Z by TARSKI:def 4;
hence P c= H by A11,A13;
end;
Y c= PARTITIONS(X)
proof
let P be object;
assume P in Y;
then consider L4 be set such that
A24: P in L4 and
A25: L4 in Z by TARSKI:def 4;
L4 in bool PARTITIONS(X) by A11,A13,A25;
hence thesis by A24;
end;
hence Y in RL by A11,A23,A16;
thus for X1 be set st X1 in Z holds X1 c= Y by ZFMISC_1:74;
end;
then consider C be set such that
A26: C in RL and
A27: for Z be set st Z in RL & Z <> C holds not C c= Z by A12,ORDERS_1:65;
reconsider C as Subset of PARTITIONS(X) by A11,A26;
A28: C is Classification of X
proof
let P1,P2 be a_partition of X such that
A29: P1 in C and
A30: P2 in C;
thus thesis by A11,A26,A29,A30;
end;
A31: C <> {} by A12,A27,XBOOLE_1:2;
A32: H c= union C
proof
let h be object such that
A33: h in H;
reconsider hh=h as set by TARSKI:1;
per cases;
suppose
A34: not h in union C;
defpred X[set] means
ex hx be set st (hx in $1 & hh c= hx & h <> hx);
consider Ca be set such that
A35: for p be set holds p in Ca iff p in C & X[p] from XFAMILY:sch
1;
A36: Ca c= C
by A35;
defpred X[set] means ex hx be set st (hx in $1 & hx c= hh & h <> hx);
consider Cb be set such that
A37: for p be set holds p in Cb iff p in C & X[p] from XFAMILY:sch
1;
consider PS be a_partition of X such that
A38: h in PS and
A39: PS c= H by A1,A2,A33,Th16;
A40: h <> {} by A38,EQREL_1:def 4;
A41: now
consider t be object such that
A42: t in hh by A40,XBOOLE_0:def 1;
let p be set;
assume p in C;
then p is a_partition of X by PARTIT1:def 3;
then union p = X by EQREL_1:def 4;
then consider v be set such that
A43: t in v and
A44: v in p by A33,A42,TARSKI:def 4;
assume
A45: for hv be set st hv in p holds hv misses hh;
not v misses hh by A42,A43,XBOOLE_0:3;
hence contradiction by A45,A44;
end;
A46: C c= Ca \/ Cb
proof
let p be object such that
A47: p in C;
reconsider pp=p as set by TARSKI:1;
consider hv be set such that
A48: hv in pp and
A49: not hv misses hh by A41,A47;
A50: h <> hv by A34,A47,A48,TARSKI:def 4;
A51: pp c= H by A11,A26,A47;
per cases by A10,A33,A48,A49,A51;
suppose
hv c= hh;
then p in Cb by A37,A47,A48,A50;
hence thesis by XBOOLE_0:def 3;
end;
suppose
hh c= hv;
then p in Ca by A35,A47,A48,A50;
hence thesis by XBOOLE_0:def 3;
end;
end;
Cb c= C
by A37;
then Ca \/ Cb c= C by A36,XBOOLE_1:8;
then
A52: C = Ca \/ Cb by A46,XBOOLE_0:def 10;
then
A53: Ca c= C by XBOOLE_1:7;
A54: now
let P1,P2 be set such that
A55: P1 in Ca and
A56: P2 in Ca;
P2 in C by A53,A56;
then
A57: P2 is a_partition of X by PARTIT1:def 3;
P1 in C by A53,A55;
then P1 is a_partition of X by PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A28,A53,A55,A56,A57
,TAXONOM1:def 1;
end;
A58: Cb c= C by A52,XBOOLE_1:7;
A59: now
let P1,P2 be set such that
A60: P1 in Cb and
A61: P2 in Cb;
P2 in C by A58,A61;
then
A62: P2 is a_partition of X by PARTIT1:def 3;
P1 in C by A58,A60;
then P1 is a_partition of X by PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A28,A58,A60,A61,A62
,TAXONOM1:def 1;
end;
now
per cases;
suppose
A63: Cb <> {};
defpred X[set] means $1 misses hh;
A64: {h} c= H
by A33,TARSKI:def 1;
consider PX,Pmax be set such that
PX in Cb and
A65: Pmax in Cb and
A66: for PZ st PZ in Cb holds PZ is_finer_than Pmax & PX
is_finer_than PZ by A3,A58,A59,A63,XBOOLE_1:1;
consider Pb be set such that
A67: for x holds x in Pb iff x in Pmax & X[x] from XFAMILY:sch
1;
set PS1 = Pb \/ {h};
set C1 = C \/ {PS1};
Pmax in C by A58,A65;
then
A68: Pmax is a_partition of X by PARTIT1:def 3;
A69: Pmax c= H by A11,A26,A58,A65;
then
A70: for a st a in Pmax holds a c= hh or hh c= a or hh misses a
by A10,A33;
Pb c= Pmax
by A67;
then Pb c= H by A69;
then
A71: PS1 c= H by A64,XBOOLE_1:8;
A72: now
let P3 be set;
assume
A73: P3 in C1;
per cases by A73,XBOOLE_0:def 3;
suppose
P3 in C;
hence P3 c= H by A11,A26;
end;
suppose
P3 in {PS1};
hence P3 c= H by A71,TARSKI:def 1;
end;
end;
PS1 in {PS1} by TARSKI:def 1;
then
A74: PS1 in C1 by XBOOLE_0:def 3;
h in {h} by TARSKI:def 1;
then
A75: h in PS1 by XBOOLE_0:def 3;
A76: ex hx be set st hx in Pmax & hx c= hh & hh <> hx by A37,A65;
then
A77: Pmax is_finer_than PS1 by A33,A40,A68,A67,A70,Th18;
A78: now
let P3 be set such that
A79: P3 in C;
per cases;
suppose
Ca = {};
then P3 is_finer_than Pmax by A46,A66,A79;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A77,
SETFAM_1:17;
end;
suppose
A80: Ca <> {};
now
per cases by A46,A79,XBOOLE_0:def 3;
suppose
A81: P3 in Ca;
consider Pmin,PY be set such that
A82: Pmin in Ca and
PY in Ca and
A83: for PZ st PZ in Ca holds PZ is_finer_than PY &
Pmin is_finer_than PZ by A3,A53,A54,A80,XBOOLE_1:1;
A84: Pmin is_finer_than P3 by A81,A83;
A85: now
consider hx be set such that
A86: hx in Pmin and
A87: hh c= hx and
A88: h <> hx by A35,A82;
assume Pmin is_finer_than Pmax;
then consider hz be set such that
A89: hz in Pmax and
A90: hx c= hz by A86;
consider hy be set such that
A91: hy in Pmax and
A92: hy c= hh and
h <> hy by A37,A65;
A93: hy is non empty by A68,A91,EQREL_1:def 4;
hy c= hx by A87,A92;
then hy meets hz by A90,A93,Lm5,XBOOLE_1:1;
then hy = hz by A68,A91,A89,EQREL_1:def 4;
then hx c= hh by A92,A90;
hence contradiction by A87,A88,XBOOLE_0:def 10;
end;
A94: Pmax in C by A52,A65,XBOOLE_0:def 3;
then
A95: Pmax is a_partition of X by PARTIT1:def 3;
Pmin in C by A53,A82;
then
A96: Pmin is a_partition of X by PARTIT1:def 3;
A97: ex hw be set st hw in Pmin & hh c= hw & h <> hw by A35,A82;
A98: Pmin in C by A52,A82,XBOOLE_0:def 3;
then Pmin is a_partition of X by PARTIT1:def 3;
then Pmax is_finer_than Pmin by A28,A98,A94,A95,A85,
TAXONOM1:def 1;
then PS1 is_finer_than Pmin by A33,A40,A68,A67,A70,A76,A96
,A97,Th18;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A84,
SETFAM_1:17;
end;
suppose
P3 in Cb;
then P3 is_finer_than Pmax by A66;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A77,
SETFAM_1:17;
end;
end;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1;
end;
end;
A99: now
let P1,P2 be set;
assume that
A100: P1 in C1 and
A101: P2 in C1;
per cases by A100,XBOOLE_0:def 3;
suppose
A102: P1 in C;
per cases by A101,XBOOLE_0:def 3;
suppose
A103: P2 in C;
then
A104: P2 is a_partition of X by PARTIT1:def 3;
P1 is a_partition of X by A102,PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A28,A102
,A103,A104,TAXONOM1:def 1;
end;
suppose
P2 in {PS1};
then P2 = PS1 by TARSKI:def 1;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A78,A102;
end;
end;
suppose
P1 in {PS1};
then
A105: P1 = PS1 by TARSKI:def 1;
per cases by A101,XBOOLE_0:def 3;
suppose
P2 in C;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A78,A105;
end;
suppose
P2 in {PS1};
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A105,
TARSKI:def 1;
end;
end;
end;
A106: PS1 is a_partition of X by A33,A40,A68,A67,A70,A76,Th18;
{PS1} c= PARTITIONS(X)
proof
let s be object;
assume s in {PS1};
then s = PS1 by TARSKI:def 1;
hence thesis by A106,PARTIT1:def 3;
end;
then C1 c= PARTITIONS(X) by XBOOLE_1:8;
then C1 in RL by A11,A72,A99;
then C = C1 by A27,XBOOLE_1:7;
hence thesis by A75,A74,TARSKI:def 4;
end;
suppose
A107: Cb = {};
then consider Pmin,PY be set such that
A108: Pmin in Ca and
PY in Ca and
A109: for PZ st PZ in Ca holds PZ is_finer_than PY & Pmin
is_finer_than PZ by A3,A31,A52,A54;
consider hw be set such that
A110: hw in Pmin and
A111: hh c= hw and
hh <> hw by A35,A108;
defpred X[set] means $1 c= hw;
consider PT be set such that
A112: for a holds a in PT iff a in PS & X[a] from XFAMILY:sch 1;
set PS1 = PT \/ (Pmin \ {hw});
set C1 = C \/ {PS1};
PT c= PS
by A112;
then
A113: PT c= H by A39;
A114: Pmin c= H by A11,A26,A53,A108;
then Pmin \ {hw} c= H;
then
A115: PS1 c= H by A113,XBOOLE_1:8;
A116: now
let P3 be set;
assume
A117: P3 in C1;
per cases by A117,XBOOLE_0:def 3;
suppose
P3 in C;
hence P3 c= H by A11,A26;
end;
suppose
P3 in {PS1};
hence P3 c= H by A115,TARSKI:def 1;
end;
end;
Pmin in C by A53,A108;
then
A118: Pmin is a_partition of X by PARTIT1:def 3;
A119: for a st a in PS holds a c= hw or hw c= a or hw misses a by A10,A39
,A114,A110;
then
A120: PS1 is_finer_than Pmin by A38,A40,A118,A110,A111,A112,Th17;
A121: now
let P3 be set;
assume P3 in C;
then Pmin is_finer_than P3 by A46,A107,A109;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A120,
SETFAM_1:17;
end;
A122: now
let P1,P2 be set;
assume that
A123: P1 in C1 and
A124: P2 in C1;
per cases by A123,XBOOLE_0:def 3;
suppose
A125: P1 in C;
per cases by A124,XBOOLE_0:def 3;
suppose
A126: P2 in C;
then
A127: P2 is a_partition of X by PARTIT1:def 3;
P1 is a_partition of X by A125,PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A28,A125
,A126,A127,TAXONOM1:def 1;
end;
suppose
P2 in {PS1};
then P2 = PS1 by TARSKI:def 1;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A121,A125;
end;
end;
suppose
P1 in {PS1};
then
A128: P1 = PS1 by TARSKI:def 1;
per cases by A124,XBOOLE_0:def 3;
suppose
P2 in C;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A121,A128;
end;
suppose
P2 in {PS1};
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A128,
TARSKI:def 1;
end;
end;
end;
A129: PS1 is a_partition of X by A38,A40,A118,A110,A111,A112,A119,Th17;
{PS1} c= PARTITIONS(X)
proof
let s be object;
assume s in {PS1};
then s = PS1 by TARSKI:def 1;
hence thesis by A129,PARTIT1:def 3;
end;
then C1 c= PARTITIONS(X) by XBOOLE_1:8;
then C1 in RL by A11,A116,A122;
then
A130: C = C1 by A27,XBOOLE_1:7;
A131: PT c= PS1 by XBOOLE_1:7;
A132: PS1 in {PS1} by TARSKI:def 1;
A133: {PS1} c= C1 by XBOOLE_1:7;
h in PT by A38,A111,A112;
hence thesis by A131,A133,A132,A130,TARSKI:def 4;
end;
end;
hence thesis;
end;
suppose
h in union C;
hence thesis;
end;
end;
take C;
union C c= H
proof
let h be object;
assume h in union C;
then consider P be set such that
A134: h in P and
A135: P in C by TARSKI:def 4;
P c= H by A11,A26,A135;
hence thesis by A134;
end;
hence thesis by A28,A32,XBOOLE_0:def 10;
end;