Copyright (c) 2001 Association of Mizar Users
environ
vocabulary TAXONOM2, TAXONOM1, ABIAN, EQREL_1, TARSKI, PUA2MSS1, REALSET1,
SETFAM_1, YELLOW_1, WELLORD2, HAHNBAN, ZFMISC_1, BOOLE, ORDERS_1,
RELAT_1, RELAT_2, PARTIT1, ORDERS_2, LATTICES, TREES_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, REALSET1, RELAT_1,
ORDINAL1, RELSET_1, STRUCT_0, ORDERS_1, EQREL_1, ABIAN, PARTIT1,
ORDERS_2, YELLOW_1, TAXONOM1;
constructors ORDERS_2, PUA2MSS1, TAXONOM1, ABIAN, YELLOW_1;
clusters SUBSET_1, RELSET_1, PARTIT1, YELLOW_1, XBOOLE_0, PARTFUN1;
requirements BOOLE, SUBSET;
definitions TARSKI, EQREL_1, TAXONOM1, SETFAM_1, XBOOLE_0;
theorems TARSKI, TAXONOM1, PARTIT1, EQREL_1, ZFMISC_1, ORDERS_1, ORDERS_2,
RELAT_1, RELSET_1, SETFAM_1, REALSET1, ABIAN, T_1TOPSP, YELLOW_1,
WELLORD2, ORDINAL1, XBOOLE_0, XBOOLE_1;
schemes XBOOLE_0;
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 R' = RelIncl A;
reconsider R = R' as Relation of A;
A1: RelStr(#A,R#) = InclPoset A by YELLOW_1:def 1;
set L = RelStr(#A,R#);
A2: L is with_superior
proof
set max = {a};
{a} in A by TARSKI:def 1;
then reconsider max' = max as Element of L;
take max';
[max',max'] in R by WELLORD2:def 1;
then A3: max' in field R by RELAT_1:30;
for y be set st y in field R & y <> max' holds [y,max'] in R
proof
let y be set such that
A4: y in field R & y <> max';
field R c= A \/ A by RELSET_1:19;
hence [y,max'] in R by A4,TARSKI:def 1;
end;
hence thesis by A3,ORDERS_2:def 11;
end;
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;
x = {a} & y = {a} by TARSKI:def 1;
then [x,y] in R by WELLORD2:def 1;
hence (x <= y or y <= x) by ORDERS_1:def 9;
end;
hence thesis by A1,A2,Def2;
end;
definition
cluster non empty reflexive transitive antisymmetric with_superior
with_comparable_down strict RelStr;
existence
proof take InclPoset {{{}}};
thus thesis by Th1;
end;
end;
definition
mode Tree is with_superior with_comparable_down Poset;
end;
theorem Th2:
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 A1: z in Class(EqR,x) & z in Class(EqR,y);
then A2: [z,x] in EqR by EQREL_1:27;
A3: [z,y] in EqR by A1,EQREL_1:27;
thus Class(EqR,x) = Class(EqR,z)
by A1,A2,EQREL_1:44
.= Class(EqR,y) by A1,A3,EQREL_1:44;
end;
theorem Th3:
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
proof
let P be a_partition of X,
x,y,z being set such that
A1: x in P & y in P & z in x & z in y;
consider EqR being Equivalence_Relation of X such that
A2: P = Class EqR by EQREL_1:43;
consider x' being Element of X such that
A3: x = Class(EqR,x') by A1,A2,EQREL_1:45;
consider y' being Element of X such that
A4: y = Class(EqR,y') by A1,A2,EQREL_1:45;
thus x = y by A1,A3,A4,Th2;
end;
theorem Th4:
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 & x in union C;
now
let a be set such that
A2: a in x;
consider Y be set such that
A3: x in Y & Y in C by A1,TARSKI:def 4;
reconsider Y' = Y as a_partition of X by A1,A3,PARTIT1:def 3;
a in union Y' by A2,A3,TARSKI:def 4;
hence a in X;
end;
hence x c= X by TARSKI:def 3;
end;
theorem
for C being set st
C is Strong_Classification of X
holds InclPoset union C is Tree
proof
let C being set such that
A1: C is Strong_Classification of X;
set B = union C;
A2: X in {X} by TARSKI:def 1;
{X} in C by A1,TAXONOM1:def 2;
then A3: B <> {} by A2,TARSKI:def 4;
set R' = RelIncl B;
reconsider R = R' as Relation of B;
A4: RelStr(#B,R#) = InclPoset B by YELLOW_1:def 1;
set D = RelStr(#B,R#);
A5: C is Classification of X by A1,TAXONOM1:def 2;
A6: {X} in C by A1,TAXONOM1:def 2;
A7: X in {X} by TARSKI:def 1;
then A8: X in B by A6,TARSKI:def 4;
reconsider B' = B as non empty set by A6,A7,TARSKI:def 4;
A9: D is with_superior
proof
reconsider s = X as Element of D by A8;
consider x be set such that
A10: x in SmallestPartition X by XBOOLE_0:def 1;
reconsider C' = C as Strong_Classification of X by A1;
SmallestPartition X in C' by TAXONOM1:def 2;
then x is Element of B' by A10,TARSKI:def 4;
then reconsider x' = x as Element of D;
take s;
[x',s] in R by A3,A10,WELLORD2:def 1;
then A11: s in field R by RELAT_1:30;
now
let y be set such that A12: y in field R & y <> s;
A13: y in dom R \/ rng R by A12,RELAT_1:def 6;
per cases by A13,XBOOLE_0:def 2;
suppose y in dom R;
then reconsider y' = y as Element of B';
y' c= s by A5,Th4;
hence [y,s] in R by WELLORD2:def 1;
suppose y in rng R;
then reconsider y' = y as Element of B';
y' c= s by A5,Th4;
hence [y,s] in R by WELLORD2:def 1;
end;
hence thesis by A11,ORDERS_2:def 11;
end;
now
let x,y be Element of D;
assume ex z be Element of D st (z <= x & z <= y);
then consider z be Element of D such that A14: z <= x & z <= y;
reconsider z' = z as Element of B';
consider Z be set such that
A15: z' in Z & Z in C by TARSKI:def 4;
reconsider z'' = z' as Subset of X by A5,Th4;
reconsider Z' = Z as a_partition of X
by A1,A15,PARTIT1:def 3;
z'' in Z' by A15;
then z'' <> {} by EQREL_1:def 6;
then consider a be set such that A16: a in z by XBOOLE_0:def 1;
[z,x] in R by A14,ORDERS_1:def 9;
then A17: z c= x by A3,WELLORD2:def 1;
then A18:a in x by A16;
[z,y] in R by A14,ORDERS_1:def 9;
then A19: z c= y by A3,WELLORD2:def 1;
then A20:a in y by A16;
reconsider x' = x, y' = y as Element of B';
consider S be set such that
A21: x' in S & S in C by TARSKI:def 4;
reconsider S' = S as a_partition of X
by A1,A21,PARTIT1:def 3;
consider T be set such that
A22: y' in T & T in C by TARSKI:def 4;
reconsider T' = T as a_partition of X
by A1,A22,PARTIT1:def 3;
A23: C is Classification of X by A1,TAXONOM1:def 2;
now per cases by A21,A22,A23,TAXONOM1:def 1;
suppose S' is_finer_than T';
then consider Y be set such that A24: Y in T' & x' c= Y
by A21,SETFAM_1:def 2;
thus x' c= y' or y' c= x' by A16,A18,A19,A22,A24,Th3;
suppose T' is_finer_than S';
then consider Y be set such that A25: Y in S' & y' c= Y
by A22,SETFAM_1:def 2;
thus x' c= y' or y' c= x' by A16,A17,A20,A21,A25,Th3;
end;
then [x',y'] in R or [y',x'] in R by WELLORD2:def 1;
hence x <= y or y <= x by ORDERS_1:def 9;
end;
hence InclPoset B is Tree by A4,A9,Def2;
end;
begin
definition let Y;
attr Y is hierarchic means :Def3:
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;
definition
cluster trivial -> hierarchic set;
coherence
proof
let X be set such that
A1: X is trivial;
per cases by A1,REALSET1:def 12;
suppose A2: X is empty;
for x,y be set st x in {} & y in {} holds
x c= y or y c= x or x misses y;
hence thesis by A2,Def3;
suppose ex a being set st X = {a};
then consider a be set such that A3: X = {a};
X is hierarchic
proof
let x,y be set such that
A4: x in X & y in X;
x = a & y = a by A3,A4,TARSKI:def 1;
hence x c= y or y c= x or x misses y;
end;
hence thesis;
end;
end;
definition
cluster non trivial hierarchic set;
existence
proof
consider A be non empty set;
consider B be empty set;
consider C be set such that A1: C = {A,B};
take C;
A2: C is hierarchic
proof
let x,y be set such that
A3: x in C & y in C;
per cases by A1,A3,TARSKI:def 2;
suppose A4: x = A;
now per cases by A1,A3,TARSKI:def 2;
suppose y = A;
hence x c= y or y c= x or x misses y by A4;
suppose y = B;
hence x c= y or y c= x or x misses y by XBOOLE_1:65;
end;
hence x c= y or y c= x or x misses y;
suppose x = B;
hence x c= y or y c= x or x misses y by XBOOLE_1:65;
end;
now
assume A5:C is trivial;
per cases by A5,REALSET1:def 12;
suppose C is empty;
hence contradiction by A1;
suppose ex x being set st C = {x};
then consider a be set such that A6: C = {a};
thus contradiction by A1,A6,ZFMISC_1:9;
end;
hence thesis by A2;
end;
end;
theorem Th6:
{} is hierarchic
proof
let x,y be set such that A1: x in {} & y in {};
thus thesis by A1;
end;
theorem
{{}} is hierarchic
proof
let x,y be set such that
A1: x in {{}} & y in {{}};
x = {} & y = {} by A1,TARSKI:def 1;
hence x c= y or y c= x or (x misses y);
end;
definition let Y;
mode Hierarchy of Y -> Subset-Family of Y means :Def4:
it is hierarchic;
existence
proof
set H = {};
{} c= bool Y by XBOOLE_1:2;
then reconsider H' = H as Subset-Family of Y by SETFAM_1:def 7;
take H';
thus thesis by Th6;
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;
Lm1: now
let x,y be set such that
A1: x in {{}} & y in {{}} & x <> y;
x = {} & y = {} by A1,TARSKI:def 1;
hence x misses y by A1;
end;
definition let Y;
cluster mutually-disjoint Subset-Family of Y;
existence
proof
set e = {{}};
now
let x be set such that A1: x in {{}};
x = {} by A1,TARSKI:def 1;
then x c= Y by XBOOLE_1:2;
hence x in bool Y;
end;
then {{}} c= bool Y by TARSKI:def 3;
then reconsider e' = e as Subset-Family of Y by SETFAM_1:def 7;
take e';
thus thesis by Def5,Lm1;
end;
end;
theorem
{} is mutually-disjoint
proof
let x,y be set such that A1: x in {} & y in {};
thus thesis by A1;
end;
theorem
{{}} is mutually-disjoint by Def5,Lm1;
theorem Th10:
{a} is mutually-disjoint
proof
let x,y be set such that
A1: x in {a} & y in {a} & x <> y;
x = a by A1,TARSKI:def 1;
hence thesis by A1,TARSKI:def 1;
end;
Lm2:
now
let Y;
let H being Hierarchy of Y such that
A1: H is covering;
let B being mutually-disjoint Subset-Family of Y such that
A2: B c= H &
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
proof
thus union B c= Y;
thus Y c= union B
proof
let y be set such that A3: y in Y;
y in union H by A1,A3,ABIAN:4;
then consider x be set such that
A4: y in x & x in H by TARSKI:def 4;
now
assume A5: not y in union B;
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 Separation;
set C = (B \ D) \/ {x};
x in {x} by TARSKI:def 1;
then A7: x in C by XBOOLE_0:def 2;
A8: (B \ D) c= C by XBOOLE_1:7;
(B \ D) c= B by XBOOLE_1:36;
then A9: (B \ D) c= H by A2,XBOOLE_1:1;
{x} c= H
proof
let s be set such that A10: s in {x};
thus thesis by A4,A10,TARSKI:def 1;
end;
then A11: C c= H by A9,XBOOLE_1:8;
then A12: C c= bool Y by XBOOLE_1:1;
A13: for p being set st p in B & not p in D & p <> x holds p misses x
proof
let p be set such that
A14: p in B & not p in D & p <> x;
A15: not p c= x by A6,A14;
A16: not x c= p by A4,A5,A14,TARSKI:def 4;
H is hierarchic by Def4;
hence p misses x by A2,A4,A14,A15,A16,Def3;
end;
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
A17: p in C & q in C & p <> q;
per cases by A17,XBOOLE_0:def 2;
suppose p in (B \ D);
then A18: p in B & not p in D by XBOOLE_0:def 4;
now per cases by A17,XBOOLE_0:def 2;
suppose q in (B \ D);
then q in B & not q in D by XBOOLE_0:def 4;
hence p misses q by A17,A18,Def5;
suppose q in {x};
then q = x by TARSKI:def 1;
hence p misses q by A13,A17,A18;
end;
hence thesis;
suppose p in {x};
then A19: p = x by TARSKI:def 1;
now per cases by A17,XBOOLE_0:def 2;
suppose q in (B \ D);
then q in B & not q in D by XBOOLE_0:def 4;
hence p misses q by A13,A17,A19;
suppose q in {x};
hence thesis by A17,A19,TARSKI:def 1;
end;
hence thesis;
end;
then A20: C is mutually-disjoint Subset-Family of Y
by A12,Def5,SETFAM_1:def 7;
union B c= union C
proof
let s be set such that A21:s in union B;
consider t be set such that
A22: s in t & t in B by A21,TARSKI:def 4;
per cases;
suppose t in D;
then t c= x by A6;
hence thesis by A7,A22,TARSKI:def 4;
suppose not t in D;
then t in (B \ D) by A22,XBOOLE_0:def 4;
hence s in union C by A8,A22,TARSKI:def 4;
end;
then A23: B = C by A2,A11,A20;
A24: {x} c= (B \ D) \/ {x} by XBOOLE_1:7;
x in {x} by TARSKI:def 1;
hence contradiction by A4,A5,A23,A24,TARSKI:def 4;
end;
hence y in union B;
end;
end;
end;
Lm3:
now
let Y;
let H being Hierarchy of Y;
let B being mutually-disjoint Subset-Family of Y such that
A1: B c= H &
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 A2: S1 in B;
now
assume A3: S1 = {};
set C = B \ {{}};
A4: union B c= union C
proof
let x be set such that A5: x in union B;
consider y be set such that A6: x in y & y in B by A5,TARSKI:def 4;
not y in {{}} by A6,TARSKI:def 1;
then y in C by A6,XBOOLE_0:def 4;
hence thesis by A6,TARSKI:def 4;
end;
A7: C c= B by XBOOLE_1:36;
then A8: C c= H by A1,XBOOLE_1:1;
C c= bool Y by A7,XBOOLE_1:1;
then A9: C is Subset-Family of Y by SETFAM_1:def 7;
C is mutually-disjoint
proof
let x,y be set such that
A10: x in C & y in C & x <> y;
x in B & y in B by A10,XBOOLE_0:def 4;
hence x misses y by A10,Def5;
end;
then B = C by A1,A4,A8,A9;
then not {} in {{}} by A2,A3,XBOOLE_0:def 4;
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 Th11:
for F be Subset-Family of Y st F = {} holds F is T_3
proof
let F be Subset-Family of Y such that
A1: F = {};
thus F is T_3
proof
let A be Subset of Y such that
A2: A in F;
let x be Element of Y such that not x in A;
thus ex B be Subset of Y st x in B & B in F & A misses B by A1,A2;
end;
end;
definition let Y;
cluster covering T_3 Hierarchy of Y;
existence
proof
per cases;
suppose A1: Y <> {};
set H' = {Y};
H' c= bool Y by ZFMISC_1:80;
then reconsider H = H' as Subset-Family of Y by SETFAM_1:def 7;
H is hierarchic
proof
let x,y be set such that A2: x in H & y in H;
x = Y & y = Y by A2,TARSKI:def 1;
hence x c= y or y c= x or x misses y;
end;
then reconsider H as Hierarchy of Y by Def4;
take H;
union H = Y by ZFMISC_1:31;
hence H is covering by ABIAN:4;
thus H is T_3
proof
let A be Subset of Y such that
A3: A in H;
A4: A = Y by A3,TARSKI:def 1;
let x be Element of Y such that
A5: not x in A;
thus ex B be Subset of Y st x in B & B in H & A misses B by A1,A4,A5;
end;
suppose A6: Y = {};
set H' = {};
{} c= bool Y by XBOOLE_1:2;
then reconsider H = H' as Subset-Family of Y by SETFAM_1:def 7;
reconsider H1 = H as Hierarchy of Y by Def4,Th6;
take H1;
thus H1 is covering by A6,ABIAN:4,ZFMISC_1:2;
thus H1 is T_3 by Th11;
end;
end;
definition let Y; let F be Subset-Family of Y;
attr F is lower-bounded means
:Def7:
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 Th12:
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};
{S1} c= bool Y
proof
let p be set such that A2: p in {S1};
p = S1 by A2,TARSKI:def 1;
hence p in bool Y;
end;
then A3: C c= bool Y by XBOOLE_1:8;
now
let c1,c2 be set such that
A4: c1 in C and
A5: c2 in C and
A6: c1 <> c2;
per cases by A4,XBOOLE_0:def 2;
suppose A7:c1 in B;
now per cases by A5,XBOOLE_0:def 2;
suppose c2 in B;
hence c1 misses c2 by A6,A7,Def5;
suppose c2 in {S1};
then c2 = S1 by TARSKI:def 1;
hence c1 misses c2 by A1,A7;
end;
hence c1 misses c2;
suppose c1 in {S1};
then A8: c1 = S1 by TARSKI:def 1;
then not c2 in {S1} by A6,TARSKI:def 1;
then c2 in B by A5,XBOOLE_0:def 2;
hence c1 misses c2 by A1,A8;
end;
hence C is mutually-disjoint Subset-Family of Y by A3,Def5,SETFAM_1:def 7;
thus S1 <> {} implies union C <> union B
proof
assume A9: S1 <> {};
not union C c= union B
proof
assume A10: union C c= union B;
consider p be set such that
A11: p in S1 by A9,XBOOLE_0:def 1;
A12: S1 in {S1} by TARSKI:def 1;
{S1} c= C by XBOOLE_1:7;
then p in union C by A11,A12,TARSKI:def 4;
then consider S2 be set such that
A13: p in S2 & S2 in B by A10,TARSKI:def 4;
S1 misses S2 by A1,A13;
hence contradiction by A11,A13,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
:Def8:
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 P' = {};
{} c= bool Y by XBOOLE_1:2;
then reconsider P = P' as Subset-Family of Y by SETFAM_1:def 7;
take P;
thus thesis by A2,EQREL_1:def 6,XBOOLE_1:2;
suppose A3: Y <> {};
now per cases;
suppose A4: Y in H;
set P = {Y};
A5: P is a_partition of Y by A3,T_1TOPSP:7;
P c= H
proof
let p be set such that A6: p in P;
thus p in H by A4,A6,TARSKI:def 1;
end;
hence thesis by A5;
suppose A7: 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 P' be set such that
A8: for T be set holds T in P' iff T in H & X[T] from Separation;
A9: union H = Y by ABIAN:4;
A10: P' c= H
proof
let p be set such that A11: p in P';
thus p in H by A8,A11;
end;
then P' c= bool Y by XBOOLE_1:1;
then reconsider P = P' as Subset-Family of Y by SETFAM_1:def 7;
A12: union P = Y
proof
thus union P c= Y;
thus Y c= union P
proof
let p be set such that A13:p in Y;
consider h' be set such that
A14: p in h' & h' in H by A9,A13,TARSKI:def 4;
reconsider h = h' as Subset of Y by A14;
consider T be Subset of Y such that
A15: h c= T & T in H & for V being Subset of Y st T c= V & V in H holds V = Y
by A1,A14,Def8;
T in P by A8,A15;
hence p in union P by A14,A15,TARSKI:def 4;
end;
end;
now
let S1 such that
A16: S1 in P;
thus S1 <> {}
proof
assume A17: S1 = {};
consider S be Subset of Y such that
A18: S in H and
A19: S c= S1 and
A20: for V being Subset of Y st S1 c= V & V in H holds V = Y by A8,A16;
A21: S1 c= S by A17,XBOOLE_1:2;
then S1 = S by A19,XBOOLE_0:def 10
.= Y by A18,A20,A21;
hence contradiction by A3,A17;
end;
thus for S2 st S2 in P holds S1 = S2 or S1 misses S2
proof
let S2 such that
A22: S2 in P;
A23: S2 in H by A8,A22;
consider T be Subset of Y such that
T in H and
T c= S2 and
A24: for V being Subset of Y st S2 c= V & V in H holds V = Y by A8,A22;
thus S1 = S2 or S1 misses S2 by A7,A23,A24;
end;
end;
then P is a_partition of Y by A3,A12,EQREL_1:def 6;
hence thesis by A10;
end;
hence thesis;
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 being covering Hierarchy of Y;
let B being mutually-disjoint Subset-Family of Y such that
A1: B c= H & for C being mutually-disjoint Subset-Family of Y st
C c= H & union B c= union C holds B = C;
thus B is a_partition of Y
proof
per cases;
case Y <> {};
thus union B = Y by A1,Lm2;
thus for S1 st S1 in B holds
S1 <> {} & for S2 st S2 in B holds
S1 = S2 or S1 misses S2 by A1,Def5,Lm3;
case A2: Y = {};
now per cases by A2,ZFMISC_1:1,39;
suppose H = {};
hence B = {} by A1,XBOOLE_1:3;
suppose A3: H = {{}};
not B = {{}}
proof
assume B = {{}};
then {} in B by TARSKI:def 1;
hence contradiction by A1,Lm3;
end;
hence thesis by A1,A3,ZFMISC_1:39;
end;
hence thesis;
end;
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 being covering T_3 Hierarchy of Y such that
A1: H is lower-bounded & not {} in H;
let A being Subset of Y;
let B being mutually-disjoint Subset-Family of Y such that
A2: A in B and
A3: B c= H and
A4: 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;
A5: union H = Y by ABIAN:4;
A6: H is hierarchic by Def4;
per cases;
suppose A7: Y <> {};
Y c= union B
proof
assume not Y c= union B;
then consider x be set such that
A8: x in Y and
A9: not x in union B by TARSKI:def 3;
defpred X[set] means x in $1;
consider D be set such that
A10: for h be set holds h in D iff h in H & X[h] from Separation;
consider xx be set such that A11: x in xx & xx in H by A5,A8,TARSKI:def 4;
A12: xx in D by A10,A11;
A13: D c= H
proof
let d be set such that A14: d in D;
thus d in H by A10,A14;
end;
now
let h1,h2 be set such that A15: h1 in D & h2 in D;
now
assume A16: h1 misses h2;
x in h1 & x in h2 by A10,A15;
hence contradiction by A16,XBOOLE_0:3;
end;
then h1 c= h2 or h2 c= h1 by A6,A13,A15,Def3;
hence h1,h2 are_c=-comparable by XBOOLE_0:def 9;
end;
then D is c=-linear by ORDINAL1:def 9;
then consider min be set such that
A17: min in H and
A18: min c= meet D by A1,A12,A13,Def7;
reconsider min' = min as Subset of Y by A17;
now
let b1 be set such that A19: b1 in B;
reconsider b1' = b1 as Subset of Y by A19;
reconsider x' = x as Element of Y by A8;
A20: not x' in b1' by A9,A19,TARSKI:def 4;
A21: not min' c= b1
proof
assume A22: min' c= b1;
consider k be Subset of Y such that
A23: x' in k and
A24: k in H and
A25: k misses b1' by A3,A19,A20,Def6;
k in D by A10,A23,A24;
then meet D c= k by SETFAM_1:4;
then A26: min' c= k by A18,XBOOLE_1:1;
consider y be set such that
A27: y in min' by A1,A17,XBOOLE_0:def 1;
thus contradiction by A22,A25,A26,A27,XBOOLE_0:3;
end;
not b1 c= min'
proof
assume A28: b1 c= min';
reconsider b1' = b1 as Subset of Y by A19;
consider k be Subset of Y such that
A29: x' in k and
A30: k in H and
A31: k misses b1' by A3,A19,A20,Def6;
A32: b1 <> {} by A1,A3,A19;
k in D by A10,A29,A30;
then meet D c= k by SETFAM_1:4;
then min' c= k by A18,XBOOLE_1:1;
then A33: b1' c= k by A28,XBOOLE_1:1;
consider y be set such that
A34: y in b1' by A32,XBOOLE_0:def 1;
thus contradiction by A31,A33,A34,XBOOLE_0:3;
end;
hence b1 misses min' by A3,A6,A17,A19,A21,Def3;
end;
then A35: for b be set st b in B holds min' misses b & Y <> {} by A7;
set C = B \/ {min'};
A36: C is mutually-disjoint Subset-Family of Y
& union C <> union B by A1,A17,A35,Th12;
{min'} c= H
proof
let s be set such that A37: s in {min'};
thus s in H by A17,A37,TARSKI:def 1;
end;
then A38:C c= H by A3,XBOOLE_1:8;
A39: B c= C by XBOOLE_1:7;
B c= C by XBOOLE_1:7;
then union B c= union C by ZFMISC_1:95;
hence contradiction by A2,A4,A36,A38,A39;
end;
then A40: 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 A1,A3,Def5;
hence thesis by A7,A40,EQREL_1:def 6;
suppose A41: Y = {};
now per cases by A41,ZFMISC_1:1,39;
suppose H = {};
hence B = {} by A3,XBOOLE_1:3;
suppose A42: H = {{}};
not B = {{}}
proof
assume B = {{}};
then {} in B by TARSKI:def 1;
hence contradiction by A1,A3;
end;
hence B = {} by A3,A42,ZFMISC_1:39;
end;
hence thesis by A41,EQREL_1:def 6;
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
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 being covering T_3 Hierarchy of Y such that
A1: H is lower-bounded & not {} in H;
let A being Subset of Y;
let B being mutually-disjoint Subset-Family of Y such that
A2: A in B and
A3: B c= H and
A4: for C being mutually-disjoint Subset-Family of Y st
A in C & C c= H & B c= C holds B = C;
A5: union H = Y by ABIAN:4;
A6: H is hierarchic by Def4;
per cases;
suppose A7: Y <> {};
Y c= union B
proof
assume not Y c= union B;
then consider x be set such that
A8: x in Y and
A9: not x in union B by TARSKI:def 3;
defpred X[set] means x in $1;
consider D be set such that
A10: for h be set holds h in D iff h in H & X[h] from Separation;
consider xx be set such that A11: x in xx & xx in H by A5,A8,TARSKI:def 4;
A12: xx in D by A10,A11;
A13: D c= H
proof
let d be set such that A14: d in D;
thus d in H by A10,A14;
end;
now
let h1,h2 be set such that A15: h1 in D & h2 in D;
now
assume A16: h1 misses h2;
x in h1 & x in h2 by A10,A15;
hence contradiction by A16,XBOOLE_0:3;
end;
then h1 c= h2 or h2 c= h1 by A6,A13,A15,Def3;
hence h1,h2 are_c=-comparable by XBOOLE_0:def 9;
end;
then D is c=-linear by ORDINAL1:def 9;
then consider min be set such that
A17: min in H and
A18: min c= meet D by A1,A12,A13,Def7;
reconsider min' = min as Subset of Y by A17;
now
let b1 be set such that A19: b1 in B;
reconsider b1' = b1 as Subset of Y by A19;
reconsider x' = x as Element of Y by A8;
A20: not x' in b1' by A9,A19,TARSKI:def 4;
A21: not min' c= b1
proof
assume A22: min' c= b1;
consider k be Subset of Y such that
A23: x' in k and
A24: k in H and
A25: k misses b1' by A3,A19,A20,Def6;
k in D by A10,A23,A24;
then meet D c= k by SETFAM_1:4;
then A26: min' c= k by A18,XBOOLE_1:1;
consider y be set such that
A27: y in min' by A1,A17,XBOOLE_0:def 1;
thus contradiction by A22,A25,A26,A27,XBOOLE_0:3;
end;
not b1 c= min'
proof
assume A28: b1 c= min';
reconsider b1' = b1 as Subset of Y by A19;
consider k be Subset of Y such that
A29: x' in k and
A30: k in H and
A31: k misses b1' by A3,A19,A20,Def6;
A32: b1 <> {} by A1,A3,A19;
k in D by A10,A29,A30;
then meet D c= k by SETFAM_1:4;
then min' c= k by A18,XBOOLE_1:1;
then A33: b1' c= k by A28,XBOOLE_1:1;
consider y be set such that
A34: y in b1' by A32,XBOOLE_0:def 1;
thus contradiction by A31,A33,A34,XBOOLE_0:3;
end;
hence b1 misses min' by A3,A6,A17,A19,A21,Def3;
end;
then A35: for b be set st b in B holds min' misses b & Y <> {} by A7;
set C = B \/ {min'};
A36: C is mutually-disjoint Subset-Family of Y
& union C <> union B by A1,A17,A35,Th12;
{min'} c= H
proof
let s be set such that A37: s in {min'};
thus s in H by A17,A37,TARSKI:def 1;
end;
then A38:C c= H by A3,XBOOLE_1:8;
B c= C by XBOOLE_1:7;
hence contradiction by A2,A4,A36,A38;
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 A1,A3,Def5;
hence thesis by A7,A39,EQREL_1:def 6;
suppose A40: Y = {};
now per cases by A40,ZFMISC_1:1,39;
suppose H = {};
hence B = {} by A3,XBOOLE_1:3;
suppose A41: H = {{}};
not B = {{}}
proof
assume B = {{}};
then {} in B by TARSKI:def 1;
hence contradiction by A1,A3;
end;
hence B = {} by A3,A41,ZFMISC_1:39;
end;
hence thesis by A40,EQREL_1:def 6;
end;
theorem Th17:
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;
defpred X[set] means
A in $1 & $1 is mutually-disjoint & $1 c= H;
consider K be set such that
A4: for S be set holds S in K iff S in bool bool Y & X[S] from Separation;
set k1 = {A};
A5: A in k1 by TARSKI:def 1;
A6: k1 is mutually-disjoint by Th10;
A7: k1 c= H by A3,ZFMISC_1:37;
k1 c= bool Y by ZFMISC_1:37;
then A8: k1 in K by A4,A5,A6,A7;
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: now
let X1,X2 be set;
assume X1 in Z & X2 in Z;
then X1,X2 are_c=-comparable by A10,ORDINAL1:def 9;
hence X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
end;
per cases;
suppose A12: Z <> {};
set X3 = union Z;
take X3;
now
consider z be set such that
A13: z in Z by A12,XBOOLE_0:def 1;
A in z by A4,A9,A13;
hence A in X3 by A13,TARSKI:def 4;
A14: for a st a in Z holds a c= H by A4,A9;
then X3 c= H by ZFMISC_1:94;
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 & v1 in Z by A15,TARSKI:def 4;
consider v2 be set such that
A19: t2 in v2 & v2 in Z by A16,TARSKI:def 4;
A20: v1 is mutually-disjoint by A4,A9,A18;
A21: v2 is mutually-disjoint by A4,A9,A19;
per cases by A11,A18,A19;
suppose v1 c= v2;
hence t1 misses t2 by A17,A18,A19,A21,Def5;
suppose v2 c= v1;
hence t1 misses t2 by A17,A18,A19,A20,Def5;
end;
thus X3 c= H by A14,ZFMISC_1:94;
end;
hence X3 in K by A4;
thus for X1 be set st X1 in Z holds X1 c= X3 by ZFMISC_1:92;
suppose A22: Z = {};
consider a be set such that
A23: a in K by A8;
take a;
thus a in K by A23;
thus for X1 be set st X1 in Z holds X1 c= a by A22;
end;
then consider M be set such that
A24: M in K and
A25:for Z be set st Z in K & Z <> M holds not M c= Z by A8,ORDERS_2:77;
A26: M c= H by A4,A24;
then M c= bool Y by XBOOLE_1:1;
then A27: M is mutually-disjoint Subset-Family of Y by A4,A24,SETFAM_1:def 7;
A28: A in M by A4,A24;
A29: now
let C be mutually-disjoint Subset-Family of Y such that
A30: A in C & C c= H & M c= C;
C in K by A4,A30;
hence M = C by A25,A30;
end;
take M;
thus thesis by A1,A2,A26,A27,A28,A29,Th16;
end;
Lm4:
now
let x be non empty set;let y such that A1: x c= y;
consider a be set such that A2: a in x by XBOOLE_0:def 1;
thus not x misses y by A1,A2,XBOOLE_0:3;
end;
theorem Th18:
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 & h c= hw;
let PS being a_partition of X such that
A2: h in PS and
A3: for x st x in PS holds (x c= hw or hw c= x or hw misses x);
let PT be set such that
A4: for a holds a in PT iff a in PS & a c= hw;
A5:union Pmin = X by EQREL_1:def 6;
A6:union PS = X by EQREL_1:def 6;
set P = PT \/ (Pmin \ {hw});
A7: PT c= P by XBOOLE_1:7;
A8: h in PT by A1,A2,A4;
A9:Pmin \ {hw} c= P by XBOOLE_1:7;
A10:PT c= PS
proof
let a such that A11: a in PT;
thus a in PS by A4,A11;
end;
then A12: PT c= bool X by XBOOLE_1:1;
A13:Pmin \ {hw} c= Pmin by XBOOLE_1:36;
then Pmin \ {hw} c= bool X by XBOOLE_1:1;
then A14: P c= bool X by A12,XBOOLE_1:8;
then A15: P is Subset-Family of X by SETFAM_1:def 7;
A16: now
let x,y such that
A17: x in PT & y in Pmin \ {hw};
A18: x c= hw by A4,A17;
A19: y in Pmin & not y in {hw} by A17,XBOOLE_0:def 4;
then A20: y <> hw by TARSKI:def 1;
now
assume not x misses y;
then consider a such that A21: a in x & a in y by XBOOLE_0:3;
not hw misses y by A18,A21,XBOOLE_0:3;
hence contradiction by A1,A19,A20,EQREL_1:def 6;
end;
hence x misses y;
end;
A22: union P = X
proof
thus union P c= X
proof
let a such that A23: a in union P;
consider b such that A24: a in b & b in P by A23,TARSKI:def 4;
thus a in X by A14,A24;
end;
thus X c= union P
proof
let a such that
A25: a in X;
consider b such that
A26: a in b & b in Pmin by A5,A25,TARSKI:def 4;
per cases;
suppose A27: b = hw;
consider c such that
A28: a in c & c in PS by A6,A25,TARSKI:def 4;
A29: not hw misses c by A26,A27,A28,XBOOLE_0:3;
now per cases by A3,A28,A29;
suppose hw c= c;
then A30: h c= c by A1,XBOOLE_1:1;
not h misses c
proof
assume A31:h misses c;
consider x such that A32: x in h by XBOOLE_0:def 1;
thus contradiction by A30,A31,A32,XBOOLE_0:3;
end;
then h = c by A2,A28,EQREL_1:def 6;
hence a in union P by A7,A8,A28,TARSKI:def 4;
suppose c c= hw;
then c in PT by A4,A28;
hence a in union P by A7,A28,TARSKI:def 4;
end;
hence a in union P;
suppose b <> hw;
then not b in {hw} by TARSKI:def 1;
then b in Pmin \ {hw} by A26,XBOOLE_0:def 4;
hence a in union P by A9,A26,TARSKI:def 4;
end;
end;
now
let A be Subset of X such that
A33: A in P;
now per cases by A33,XBOOLE_0:def 2;
suppose A in PT;
hence A <> {} by A10,EQREL_1:def 6;
suppose A in Pmin \ {hw};
hence A <> {} by A13,EQREL_1:def 6;
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
A34: B in P;
per cases by A33,XBOOLE_0:def 2;
suppose A35: A in PT;
now per cases by A34,XBOOLE_0:def 2;
suppose B in PT;
hence A = B or A misses B by A10,A35,EQREL_1:def 6;
suppose B in Pmin \ {hw};
hence A = B or A misses B by A16,A35;
end;
hence A = B or A misses B;
suppose A36: A in Pmin \ {hw};
now per cases by A34,XBOOLE_0:def 2;
suppose B in PT;
hence A = B or A misses B by A16,A36;
suppose B in Pmin \ {hw};
hence A = B or A misses B by A13,A36,EQREL_1:def 6;
end;
hence A = B or A misses B;
end;
end;
hence PT \/ (Pmin \ {hw}) is a_partition of X by A15,A22,EQREL_1:def 6;
thus PT \/ (Pmin \ {hw}) is_finer_than Pmin
proof
let a such that
A37: a in P;
per cases by A37,XBOOLE_0:def 2;
suppose a in PT;
then a c= hw by A4;
hence ex b st b in Pmin & a c= b by A1;
suppose a in Pmin \ {hw};
hence ex b st b in Pmin & a c= b by A13;
end;
end;
theorem Th19:
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 being non empty set such that
A1: h c= X;
let Pmax being a_partition of X such that
A2: ex hy be set st (hy in Pmax & hy c= h) and
A3: for x st x in Pmax holds (x c= h or h c= x or h misses x);
A4: union Pmax = X by EQREL_1:def 6;
let Pb be set such that
A5: for x holds x in Pb iff (x in Pmax & x misses h);
set P = Pb \/ {h};
A6: Pb c= P by XBOOLE_1:7;
A7: h in {h} by TARSKI:def 1;
A8: {h} c= P by XBOOLE_1:7;
A9:now
let s be set such that A10: s in Pmax & h c= s;
consider hy be set such that
A11: hy in Pmax & hy c= h by A2;
A12: hy c= s by A10,A11,XBOOLE_1:1;
hy <> {} by A11,EQREL_1:def 6;
then not hy misses s by A12,Lm4;
then s = hy by A10,A11,EQREL_1:def 6;
hence h = s by A10,A11,XBOOLE_0:def 10;
end;
A13:Pb c= Pmax
proof
let s be set such that A14: s in Pb;
thus s in Pmax by A5,A14;
end;
then A15: Pb c= bool X by XBOOLE_1:1;
{h} c= bool X
proof
let s be set such that A16: s in {h};
s = h by A16,TARSKI:def 1;
hence s in bool X by A1;
end;
then A17: P c= bool X by A15,XBOOLE_1:8;
then A18: P is Subset-Family of X by SETFAM_1:def 7;
A19: union P = X
proof
thus union P c= X
proof
let s be set such that
A20: s in union P;
consider t be set such that
A21: s in t & t in P by A20,TARSKI:def 4;
thus s in X by A17,A21;
end;
thus X c= union P
proof
let s be set such that
A22: s in X;
consider t be set such that
A23: s in t & t in Pmax by A4,A22,TARSKI:def 4;
per cases;
suppose t in Pb;
hence s in union P by A6,A23,TARSKI:def 4;
suppose not t in Pb;
then A24: not t misses h by A5,A23;
now per cases by A3,A23,A24;
suppose h c= t;
then t = h by A9,A23;
hence s in union P by A7,A8,A23,TARSKI:def 4;
suppose A25: t c= h;
h in {h} by TARSKI:def 1;
hence s in union P by A8,A23,A25,TARSKI:def 4;
end;
hence s in union P;
end;
end;
now
let A be Subset of X such that
A26: A in P;
now
per cases by A26,XBOOLE_0:def 2;
suppose A in Pb;
then A in Pmax by A5;
hence A <> {} by EQREL_1:def 6;
suppose A in {h};
hence A <> {} by TARSKI:def 1;
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
A27: B in P;
per cases by A26,XBOOLE_0:def 2;
suppose A28: A in Pb;
now per cases by A27,XBOOLE_0:def 2;
suppose B in Pb;
hence A = B or A misses B by A13,A28,EQREL_1:def 6;
suppose B in {h};
then B = h by TARSKI:def 1;
hence A = B or A misses B by A5,A28;
end;
hence A = B or A misses B;
suppose A29: A in {h};
now per cases by A27,XBOOLE_0:def 2;
suppose A30: B in Pb;
A = h by A29,TARSKI:def 1;
hence A = B or A misses B by A5,A30;
suppose B in {h};
then B = h by TARSKI:def 1;
hence A = B or A misses B by A29,TARSKI:def 1;
end;
hence A = B or A misses B;
end;
end;
hence Pb \/ {h} is a_partition of X by A18,A19,EQREL_1:def 6;
thus Pmax is_finer_than (Pb \/ {h})
proof
let x be set such that
A31: x in Pmax;
per cases;
suppose x c= h;
hence ex y be set st y in P & x c= y by A7,A8;
suppose A32: not x c= h;
now per cases by A3,A31,A32;
suppose h c= x;
then h = x by A9,A31;
hence ex y be set st y in P & x c= y by A7,A8;
suppose h misses x;
then x in Pb by A5,A31;
hence ex y be set st y in P & x c= y by A6;
end;
hence ex y be set st y in P & x c= y;
end;
thus
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 Pmin be a_partition of X such that
A33: Pmax is_finer_than Pmin;
let hw be set such that
A34: hw in Pmin & h c= hw;
thus (Pb \/ {h}) is_finer_than Pmin
proof
let s be set such that A35: s in P;
per cases by A35,XBOOLE_0:def 2;
suppose s in Pb;
then s in Pmax by A5;
then consider t be set such that
A36: t in Pmin & s c= t by A33,SETFAM_1:def 2;
thus ex s1 be set st s1 in Pmin & s c= s1 by A36;
suppose s in {h};
then s = h by TARSKI:def 1;
hence ex s1 be set st s1 in Pmin & s c= s1 by A34;
end;
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)));
A4: 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
A5: for L be set holds L in RL iff L in bool PARTITIONS X & X[L]
from Separation;
union H = X by ABIAN:4;
then consider h be set such that
A6: h in H by XBOOLE_0:def 1,ZFMISC_1:2;
reconsider h as Subset of X by A6;
consider PX being a_partition of X such that
h in PX and
A7: PX c= H by A1,A2,A6,Th17;
set L = {PX};
A8: L c= PARTITIONS(X)
proof
let l be set such that
A9: l in L;
l = PX by A9,TARSKI:def 1;
hence l in PARTITIONS(X) by PARTIT1:def 3;
end;
A10: for a st a in L holds a c= H by A7,TARSKI:def 1;
now
let P1,P2 be set;
assume P1 in L & P2 in L;
then P1 = PX & P2 = PX by TARSKI:def 1;
hence P1 is_finer_than P2 or P2 is_finer_than P1;
end;
then A11: L in RL by A5,A8,A10;
now
let Z be set such that
A12: Z c= RL and
A13: Z is c=-linear;
A14:now
let X1,X2 be set;
assume X1 in Z & X2 in Z;
then X1,X2 are_c=-comparable by A13,ORDINAL1:def 9;
hence X1 c= X2 or X2 c= X1 by XBOOLE_0:def 9;
end;
set Y = union Z;
take Y;
A15: Y c= PARTITIONS(X)
proof
let P be set such that
A16: P in Y;
consider L4 be set such that
A17: P in L4 & L4 in Z by A16,TARSKI:def 4;
L4 in bool PARTITIONS(X) by A5,A12,A17;
hence P in PARTITIONS(X) by A17;
end;
A18: now
let P be set;
assume P in Y;
then consider L3 be set such that
A19: P in L3 & L3 in Z by TARSKI:def 4;
thus P c= H by A5,A12,A19;
end;
now
let P1,P2 be set;
assume A20: P1 in Y & P2 in Y;
then consider L1 be set such that
A21: P1 in L1 & L1 in Z by TARSKI:def 4;
consider L2 be set such that
A22: P2 in L2 & L2 in Z by A20,TARSKI:def 4;
per cases by A14,A21,A22;
suppose L1 c= L2;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A5,A12,A21,A22;
suppose L2 c= L1;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A5,A12,A21,A22;
end;
hence Y in RL by A5,A15,A18;
thus for X1 be set st X1 in Z holds X1 c= Y by ZFMISC_1:92;
end;
then consider C be set such that
A23: C in RL and
A24: for Z be set st Z in RL & Z <> C holds not C c= Z by A11,ORDERS_2:77;
reconsider C as Subset of PARTITIONS(X) by A5,A23;
take C;
A25: C is Classification of X
proof
let P1,P2 be a_partition of X such that
A26: P1 in C and
A27: P2 in C;
thus P1 is_finer_than P2 or P2 is_finer_than P1 by A5,A23,A26,A27;
end;
A28: now
assume A29: C = {};
then C c= L by XBOOLE_1:2;
hence contradiction by A11,A24,A29;
end;
union C = H
proof
thus union C c= H
proof
let h be set such that
A30: h in union C;
consider P be set such that
A31: h in P & P in C by A30,TARSKI:def 4;
P c= H by A5,A23,A31;
hence h in H by A31;
end;
thus H c= union C
proof
let h be set such that
A32: h in H;
per cases;
suppose A33: not h in union C;
consider PS be a_partition of X such that
A34: h in PS and
A35: PS c= H by A1,A2,A32,Th17;
A36: h <> {} by A34,EQREL_1:def 6;
defpred X[set] means ex hx be set st (hx in $1 & h c= hx & h <> hx);
consider Ca be set such that
A37: for p be set holds p in Ca iff p in C & X[p] from Separation;
A38: Ca c= C
proof
let s be set such that A39: s in Ca;
thus s in C by A37,A39;
end;
defpred X[set] means ex hx be set st (hx in $1 & hx c= h & h <> hx);
consider Cb be set such that
A40: for p be set holds
p in Cb iff p in C & X[p] from Separation;
A41: Cb c= C
proof
let s be set such that A42: s in Cb;
thus s in C by A40,A42;
end;
A43: now
let p be set such that
A44:p in C;
assume A45: for hv be set st hv in p holds hv misses h;
consider t be set such that
A46: t in h by A36,XBOOLE_0:def 1;
p is a_partition of X by A44,PARTIT1:def 3;
then union p = X by EQREL_1:def 6;
then consider v be set such that
A47: t in v & v in p by A32,A46,TARSKI:def 4;
not v misses h by A46,A47,XBOOLE_0:3;
hence contradiction by A45,A47;
end;
A48: C = Ca \/ Cb
proof
thus C c= Ca \/ Cb
proof
let p be set such that
A49: p in C;
consider hv be set such that
A50: hv in p & not hv misses h by A43,A49;
A51: p c= H by A5,A23,A49;
A52: h <> hv by A33,A49,A50,TARSKI:def 4;
per cases by A4,A32,A50,A51,Def3;
suppose hv c= h;
then p in Cb by A40,A49,A50,A52;
hence p in Ca \/ Cb by XBOOLE_0:def 2;
suppose h c= hv;
then p in Ca by A37,A49,A50,A52;
hence p in Ca \/ Cb by XBOOLE_0:def 2;
end;
thus Ca \/ Cb c= C by A38,A41,XBOOLE_1:8;
end;
then A53: Ca c= C by XBOOLE_1:7;
A54: Cb c= C by A48,XBOOLE_1:7;
A55: Ca c= PARTITIONS(X) by A53,XBOOLE_1:1;
A56: now
let P1,P2 be set such that
A57: P1 in Ca & P2 in Ca;
P1 in C & P2 in C by A53,A57;
then P1 is a_partition of X & P2 is a_partition of X
by PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1
by A25,A53,A57,TAXONOM1:def 1;
end;
A58: Cb c= PARTITIONS(X) by A54,XBOOLE_1:1;
A59: now
let P1,P2 be set such that
A60: P1 in Cb & P2 in Cb;
P1 in C & P2 in C by A54,A60;
then P1 is a_partition of X & P2 is a_partition of X
by PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1
by A25,A54,A60,TAXONOM1:def 1;
end;
now per cases;
suppose Cb <> {};
then consider PX,Pmax be set such that
A61: PX in Cb & Pmax in Cb and
A62: for PZ st PZ in Cb holds
PZ is_finer_than Pmax & PX is_finer_than PZ by A3,A58,A59;
A63: Pmax c= H by A5,A23,A54,A61;
Pmax in C by A54,A61;
then A64: Pmax is a_partition of X by PARTIT1:def 3;
defpred X[set] means $1 misses h;
consider Pb be set such that
A65: for x holds x in Pb iff x in Pmax & X[x] from Separation;
set PS1 = Pb \/ {h};
Pb c= Pmax
proof
let s be set such that A66: s in Pb;
thus s in Pmax by A65,A66;
end;
then A67: Pb c= H by A63,XBOOLE_1:1;
A68: for a st a in Pmax holds a c= h or h c= a or h misses a
by A4,A32,A63,Def3;
A69: ex hx be set st (hx in Pmax & hx c= h & h <> hx) by A40,A61;
then A70: PS1 is a_partition of X by A32,A36,A64,A65,A68,Th19;
A71: {PS1} c= PARTITIONS(X)
proof
let s be set such that A72: s in {PS1};
s = PS1 by A72,TARSKI:def 1;
hence s in PARTITIONS(X) by A70,PARTIT1:def 3;
end;
A73: {h} c= H
proof
let s be set such that A74: s in {h};
thus s in H by A32,A74,TARSKI:def 1;
end;
h in {h} by TARSKI:def 1;
then A75: h in PS1 by XBOOLE_0:def 2;
A76: PS1 c= H by A67,A73,XBOOLE_1:8;
set C1 = C \/ {PS1};
PS1 in {PS1} by TARSKI:def 1;
then A77: PS1 in C1 by XBOOLE_0:def 2;
A78: C1 c= PARTITIONS(X) by A71,XBOOLE_1:8;
A79: now
let P3 be set;
assume A80: P3 in C1;
per cases by A80,XBOOLE_0:def 2;
suppose P3 in C;
hence P3 c= H by A5,A23;
suppose P3 in {PS1};
hence P3 c= H by A76,TARSKI:def 1;
end;
A81:Pmax is_finer_than PS1 by A32,A36,A64,A65,A68,A69,Th19;
A82: now
let P3 be set such that A83: P3 in C;
per cases;
suppose Ca = {};
then P3 is_finer_than Pmax by A48,A62,A83;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A81,SETFAM_1:23;
suppose A84: Ca <> {};
now per cases by A48,A83,XBOOLE_0:def 2;
suppose A85: P3 in Ca;
consider Pmin,PY be set such that
A86: Pmin in Ca & PY in Ca and
A87: for PZ st PZ in Ca holds
PZ is_finer_than PY & Pmin is_finer_than PZ by A3,A55,A56,A84;
Pmin in C by A53,A86;
then A88: Pmin is a_partition of X by PARTIT1:def 3;
consider hw be set such that
A89: hw in Pmin & h c= hw & h <> hw by A37,A86;
Pmax is_finer_than Pmin
proof
A90: Pmin in C & Pmax in C by A48,A61,A86,XBOOLE_0:def 2;
then A91: Pmin is a_partition of X & Pmax is a_partition of X
by PARTIT1:def 3;
now
assume A92: Pmin is_finer_than Pmax;
consider hx be set such that A93:(hx in Pmin & h c= hx & h <> hx) by A37,A86;
consider hy be set such that A94:(hy in Pmax & hy c= h & h <> hy) by A40,A61;
A95: hy c= hx by A93,A94,XBOOLE_1:1;
consider hz be set such that
A96: hz in Pmax & hx c= hz by A92,A93,SETFAM_1:def 2;
A97: hy c= hz by A95,A96,XBOOLE_1:1;
hy is non empty by A64,A94,EQREL_1:def 6;
then not hy misses hz by A97,Lm4;
then hy = hz by A64,A94,A96,EQREL_1:def 6;
then hx c= h by A94,A96,XBOOLE_1:1;
hence contradiction by A93,XBOOLE_0:def 10;
end;
hence thesis by A25,A90,A91,TAXONOM1:def 1;
end;
then A98: PS1 is_finer_than Pmin by A32,A36,A64,A65,A68,A69,A88,A89,Th19;
Pmin is_finer_than P3 by A85,A87;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A98,SETFAM_1:23;
suppose P3 in Cb;
then P3 is_finer_than Pmax by A62;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A81,SETFAM_1:23;
end;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1;
end;
now
let P1,P2 be set;
assume A99: P1 in C1 & P2 in C1;
per cases by A99,XBOOLE_0:def 2;
suppose A100: P1 in C;
now per cases by A99,XBOOLE_0:def 2;
suppose A101: P2 in C;
A102: P1 is a_partition of X by A100,PARTIT1:def 3;
P2 is a_partition of X by A101,PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1
by A25,A100,A101,A102,TAXONOM1:def 1;
suppose P2 in {PS1};
then P2 = PS1 by TARSKI:def 1;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A82,A100;
end;
hence P1 is_finer_than P2 or P2 is_finer_than P1;
suppose P1 in {PS1};
then A103: P1 = PS1 by TARSKI:def 1;
now per cases by A99,XBOOLE_0:def 2;
suppose P2 in C;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A82,A103;
suppose P2 in {PS1};
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A103,TARSKI:def 1
;
end;
hence P1 is_finer_than P2 or P2 is_finer_than P1;
end;
then A104: C1 in RL by A5,A78,A79;
C c= C1 by XBOOLE_1:7;
then C = C1 by A24,A104;
hence h in union C by A75,A77,TARSKI:def 4;
suppose A105: Cb = {};
then consider Pmin,PY be set such that
A106: Pmin in Ca & PY in Ca and
A107: for PZ st PZ in Ca holds
PZ is_finer_than PY & Pmin is_finer_than PZ by A3,A28,A48,A56;
A108:Pmin c= H by A5,A23,A53,A106;
Pmin in C by A53,A106;
then A109: Pmin is a_partition of X by PARTIT1:def 3;
consider hw be set such that
A110: hw in Pmin & h c= hw & h <> hw by A37,A106;
Pmin \ {hw} c= Pmin by XBOOLE_1:36;
then A111: Pmin \ {hw} c= H by A108,XBOOLE_1:1;
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 Separation;
set PS1 = PT \/ (Pmin \ {hw});
A113: PT c= PS1 by XBOOLE_1:7;
A114:h in PT by A34,A110,A112;
PT c= PS
proof
let s be set such that A115: s in PT;
thus s in PS by A112,A115;
end;
then PT c= H by A35,XBOOLE_1:1;
then A116: PS1 c= H by A111,XBOOLE_1:8;
A117: for a st a in PS holds a c= hw or hw c= a or hw misses a
by A4,A35,A108,A110,Def3;
then A118: PS1 is a_partition of X by A34,A36,A109,A110,A112,Th18;
A119: {PS1} c= PARTITIONS(X)
proof
let s be set such that A120: s in {PS1};
s = PS1 by A120,TARSKI:def 1;
hence s in PARTITIONS(X) by A118,PARTIT1:def 3;
end;
set C1 = C \/ {PS1};
A121: {PS1} c= C1 by XBOOLE_1:7;
A122: PS1 in {PS1} by TARSKI:def 1;
A123: PS1 is_finer_than Pmin by A34,A36,A109,A110,A112,A117,Th18;
A124: C1 c= PARTITIONS(X) by A119,XBOOLE_1:8;
A125: now
let P3 be set;
assume A126: P3 in C1;
per cases by A126,XBOOLE_0:def 2;
suppose P3 in C;
hence P3 c= H by A5,A23;
suppose P3 in {PS1};
hence P3 c= H by A116,TARSKI:def 1;
end;
A127:now
let P3 be set such that A128: P3 in C;
Pmin is_finer_than P3 by A48,A105,A107,A128;
hence PS1 is_finer_than P3 or P3 is_finer_than PS1 by A123,SETFAM_1:23;
end;
now
let P1,P2 be set;
assume A129: P1 in C1 & P2 in C1;
per cases by A129,XBOOLE_0:def 2;
suppose A130: P1 in C;
now per cases by A129,XBOOLE_0:def 2;
suppose A131: P2 in C;
A132: P1 is a_partition of X by A130,PARTIT1:def 3;
P2 is a_partition of X by A131,PARTIT1:def 3;
hence P1 is_finer_than P2 or P2 is_finer_than P1
by A25,A130,A131,A132,TAXONOM1:def 1;
suppose P2 in {PS1};
then P2 = PS1 by TARSKI:def 1;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A127,A130;
end;
hence P1 is_finer_than P2 or P2 is_finer_than P1;
suppose P1 in {PS1};
then A133: P1 = PS1 by TARSKI:def 1;
now per cases by A129,XBOOLE_0:def 2;
suppose P2 in C;
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A127,A133;
suppose P2 in {PS1};
hence P1 is_finer_than P2 or P2 is_finer_than P1 by A133,TARSKI:def 1;
end;
hence P1 is_finer_than P2 or P2 is_finer_than P1;
end;
then A134: C1 in RL by A5,A124,A125;
C c= C1 by XBOOLE_1:7;
then C = C1 by A24,A134;
hence h in union C by A113,A114,A121,A122,TARSKI:def 4;
end;
hence h in union C;
suppose h in union C;
hence thesis;
end;
end;
hence thesis by A25;
end;