taxonom2.miz
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;
::
TAXONOM2:def1
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;
::
TAXONOM2:def2
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 ::
TAXONOM2:1
Th1: for a be
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 ::
TAXONOM2:2
for EqR be
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 be
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;
::$Canceled
Lm1: for P be
a_partition of X, x,y,z be
set st x
in P & y
in P & z
in x & z
in y holds x
= y by
EQREL_1: 70;
theorem ::
TAXONOM2:4
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 ::
TAXONOM2:5
for C be
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 be
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;
::
TAXONOM2:def3
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 be
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 be
object st C
=
{x};
hence contradiction by
A1,
ZFMISC_1: 5;
end;
end;
hence thesis by
A2;
end;
end
theorem ::
TAXONOM2:6
Th5:
{} is
hierarchic;
theorem ::
TAXONOM2:7
{
{} } 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;
::
TAXONOM2:def4
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;
::
TAXONOM2:def5
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 ::
TAXONOM2:8
{} is
mutually-disjoint;
theorem ::
TAXONOM2:9
{
{} } is
mutually-disjoint by
Lm2;
theorem ::
TAXONOM2:10
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 be
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 be
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 be
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;
::
TAXONOM2:def6
attr F is
T_3 means
:
Def6: for A be
Subset of Y st A
in F holds for x be
Element of Y st not x
in A holds ex B be
Subset of Y st x
in B & B
in F & A
misses B;
end
theorem ::
TAXONOM2:11
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;
::
TAXONOM2:def7
attr F is
lower-bounded means for B be
set st B
<>
{} & B
c= F & B is
c=-linear holds ex c st c
in F & c
c= (
meet B);
end
theorem ::
TAXONOM2:12
Th11: for B be
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 be
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;
::
TAXONOM2:def8
attr F is
with_max's means for S be
Subset of Y st S
in F holds ex T be
Subset of Y st S
c= T & T
in F & for V be
Subset of Y st T
c= V & V
in F holds V
= Y;
end
begin
theorem ::
TAXONOM2:13
for H be
covering
Hierarchy of Y st H is
with_max's holds ex P be
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 be
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 be
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 be
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 be
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 ::
TAXONOM2:14
for H be
covering
Hierarchy of Y holds for B be
mutually-disjoint
Subset-Family of Y st B
c= H & for C be
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 be
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 ::
TAXONOM2:15
for H be
covering
T_3
Hierarchy of Y st H is
lower-bounded & not
{}
in H holds for A be
Subset of Y holds for B be
mutually-disjoint
Subset-Family of Y st A
in B & B
c= H & for C be
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 be
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,
ZFMISC_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 ::
TAXONOM2:16
Th15: for H be
covering
T_3
Hierarchy of Y st H is
lower-bounded & not
{}
in H holds for A be
Subset of Y holds for B be
mutually-disjoint
Subset-Family of Y st A
in B & B
c= H & for C be
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 be
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,
ZFMISC_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 ::
TAXONOM2:17
Th16: for H be
covering
T_3
Hierarchy of Y st H is
lower-bounded & not
{}
in H holds for A be
Subset of Y st A
in H holds ex P be
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 holds 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 be
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 be
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 ::
TAXONOM2:18
Th17: for h be non
empty
set holds for Pmin be
a_partition of X holds for hw be
set st hw
in Pmin & h
c= hw holds for PS be
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) holds 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 be
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 be
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 be
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 ::
TAXONOM2:19
Th18: for h be non
empty
set st h
c= X holds for Pmax be
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)) holds 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 be
a_partition of X st Pmax
is_finer_than Pmin holds for hw be
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 ::
TAXONOM2:20
for H be
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))) holds ex C be
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 be
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 be
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;