:: Kuratowski - Zorn Lemma
:: by Wojciech A. Trybulec and Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, ORDERS_1,
SUBSET_1, XXREAL_0, ARYTM_3, TREES_2, TARSKI, WELLORD1, FUNCT_1,
ZFMISC_1, ORDERS_2, CARD_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
RELSET_1, PARTFUN1, CARD_1, WELLORD1, DOMAIN_1, STRUCT_0, ORDERS_1;
constructors RELAT_2, WELLORD1, PARTFUN1, DOMAIN_1, ORDERS_1, PRE_TOPC,
RELSET_1, SETFAM_1;
registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PARTFUN1, CARD_1,
RELAT_2;
requirements BOOLE, SUBSET;
definitions RELAT_2, TARSKI, WELLORD1, STRUCT_0, XBOOLE_0, ORDERS_1;
equalities RELAT_1, WELLORD1, STRUCT_0, ORDERS_1;
expansions RELAT_2, TARSKI, WELLORD1, XBOOLE_0, ORDERS_1;
theorems RELAT_1, RELAT_2, TARSKI, WELLORD1, ZFMISC_1, XBOOLE_0, XBOOLE_1,
PARTFUN1, ORDERS_1, XTUPLE_0, RELSET_1;
schemes XFAMILY;
begin :: Original ORDERS_1
reserve X,Y,x,y for set;
definition
struct(1-sorted) RelStr (# carrier -> set, InternalRel -> Relation of the
carrier #);
end;
registration
let X be non empty set;
let R be Relation of X;
cluster RelStr(#X,R#) -> non empty;
coherence;
end;
definition
let A be RelStr;
attr A is total means
:Def1:
the InternalRel of A is total;
attr A is reflexive means
:Def2:
the InternalRel of A is_reflexive_in the carrier of A;
attr A is transitive means
:Def3:
the InternalRel of A is_transitive_in the carrier of A;
attr A is antisymmetric means
:Def4:
the InternalRel of A is_antisymmetric_in the carrier of A;
end;
registration
cluster reflexive transitive antisymmetric strict total 1-element for RelStr;
existence
proof
set R = the Order of {{}};
take L = RelStr(#{{}},R#);
A1: field R = the carrier of L by ORDERS_1:12;
hence the InternalRel of L is_reflexive_in the carrier of L by
RELAT_2:def 9;
thus the InternalRel of L is_transitive_in the carrier of L by A1,
RELAT_2:def 16;
thus the InternalRel of L is_antisymmetric_in the carrier of L by A1,
RELAT_2:def 12;
thus L is strict;
thus the InternalRel of L is total;
thus the carrier of L is 1-element;
end;
end;
registration
cluster reflexive -> total for RelStr;
coherence
proof
let L be RelStr;
assume L is reflexive;
then the InternalRel of L is_reflexive_in the carrier of L;
then dom the InternalRel of L = the carrier of L by ORDERS_1:13;
hence the InternalRel of L is total by PARTFUN1:def 2;
end;
end;
definition
mode Poset is reflexive transitive antisymmetric RelStr;
end;
registration
let A be total RelStr;
cluster the InternalRel of A -> total;
coherence by Def1;
end;
registration
let A be reflexive RelStr;
cluster the InternalRel of A -> reflexive;
coherence
proof
set R = the InternalRel of A;
R is_reflexive_in the carrier of A by Def2;
then
A1: field R = the carrier of A by ORDERS_1:13;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
hence thesis by A1;
end;
end;
registration
let A be total antisymmetric RelStr;
cluster the InternalRel of A -> antisymmetric;
coherence
proof
set R = the InternalRel of A;
field R = the carrier of A & the InternalRel of A is_antisymmetric_in
the carrier of A by Def4,ORDERS_1:12;
hence thesis;
end;
end;
registration
let A be transitive RelStr;
cluster the InternalRel of A -> transitive;
coherence
proof
let a,b,c be object;
assume
A1: a in field the InternalRel of A & b in field the InternalRel of A &
c in field the InternalRel of A;
field the InternalRel of A c= (the carrier of A)\/the carrier of A
by RELSET_1:8;
hence thesis by A1,RELAT_2:def 8,Def3;
end;
end;
registration
let X be set;
let O be total reflexive Relation of X;
cluster RelStr(#X,O#) -> reflexive;
coherence
proof
set A = RelStr(#X,O#);
field O = X by ORDERS_1:12;
hence the InternalRel of A is_reflexive_in the carrier of A by
RELAT_2:def 9;
end;
end;
registration
let X be set;
let O be total transitive Relation of X;
cluster RelStr(#X,O#) -> transitive;
coherence
proof
set A = RelStr(#X,O#);
field O = X by ORDERS_1:12;
hence the InternalRel of A is_transitive_in the carrier of A by
RELAT_2:def 16;
end;
end;
registration
let X be set;
let O be total antisymmetric Relation of X;
cluster RelStr(#X,O#) -> antisymmetric;
coherence
proof
set A = RelStr(#X,O#);
field O = X by ORDERS_1:12;
hence the InternalRel of A is_antisymmetric_in the carrier of A by
RELAT_2:def 12;
end;
end;
reserve A for non empty Poset;
reserve a,a1,a2,a3,b,c for Element of A;
reserve S,T for Subset of A;
Lm1: x in S implies x is Element of A;
definition
let A be RelStr;
let a1,a2 be Element of A;
pred a1 <= a2 means
[a1,a2] in the InternalRel of A;
end;
notation
let A be RelStr;
let a1,a2 be Element of A;
synonym a2 >= a1 for a1 <= a2;
end;
definition
let A be RelStr;
let a1,a2 be Element of A;
pred a1 < a2 means
a1 <= a2 & a1 <> a2;
irreflexivity;
end;
notation
let A be RelStr;
let a1,a2 be Element of A;
synonym a2 > a1 for a1 < a2;
end;
theorem Th1:
for A being reflexive non empty RelStr, a being Element of A holds a <= a
proof
let A be reflexive non empty RelStr, a be Element of A;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then [a,a] in the InternalRel of A;
hence thesis;
end;
definition
let A be reflexive non empty RelStr;
let a1,a2 be Element of A;
redefine pred a1 <= a2; :: redefines <= (ORDERS_2, definition)
reflexivity by Th1;
end;
theorem Th2:
for A being antisymmetric RelStr, a1,a2 being Element of A st a1
<= a2 & a2 <= a1 holds a1 = a2
proof
let A be antisymmetric RelStr, a1,a2 be Element of A;
assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a1] in the InternalRel of A;
A3: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
a1 in the carrier of A by A1,ZFMISC_1:87;
hence thesis by A1,A2,A3;
end;
theorem Th3:
for A being transitive RelStr, a1,a2,a3 being Element of A holds
a1 <= a2 & a2 <= a3 implies a1 <= a3
proof
let A be transitive RelStr, a1,a2,a3 be Element of A;
assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a3] in the InternalRel of A;
A3: the InternalRel of A is_transitive_in the carrier of A by Def3;
a1 in the carrier of A by A1,ZFMISC_1:87;
hence [a1,a3] in the InternalRel of A by A1,A2,A3;
end;
theorem Th4:
for A being antisymmetric RelStr, a1,a2 being Element of A holds
not(a1 < a2 & a2 < a1)
by Th2;
theorem Th5:
for A being transitive antisymmetric RelStr for a1,a2,a3 being
Element of A holds a1 < a2 & a2 < a3 implies a1 < a3
by Th3,Th4;
theorem Th6:
for A being antisymmetric RelStr, a1,a2 being Element of A holds
a1 <= a2 implies not a2 < a1
by Th2;
theorem Th7:
for A being transitive antisymmetric RelStr for a1,a2,a3 being
Element of A holds a1 < a2 & a2 <= a3 or a1 <= a2 & a2 < a3 implies a1 < a3
by Th2,Th3;
::
:: Chains.
::
definition
let A be RelStr;
let IT be Subset of A;
attr IT is strongly_connected means
:Def7:
the InternalRel of A is_strongly_connected_in IT;
end;
registration
let A be RelStr;
cluster empty -> strongly_connected for Subset of A;
coherence
proof let S be Subset of A;
assume S is empty;
then
A1: S = {}A;
let x1,x2 be object;
thus thesis by A1;
end;
end;
registration
let A be RelStr;
cluster strongly_connected for Subset of A;
existence
proof
take {}A;
thus thesis;
end;
end;
definition
let A be RelStr;
mode Chain of A is strongly_connected Subset of A;
end;
theorem Th8:
for A being non empty reflexive RelStr for a being Element of A
holds {a} is Chain of A
proof
let A be non empty reflexive RelStr, a be Element of A;
A1: the InternalRel of A is_reflexive_in the carrier of A by Def2;
{a} is strongly_connected
proof
let x1,x2 be object;
assume x1 in {a} & x2 in {a};
then x1 = a & x2 = a by TARSKI:def 1;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th9:
for A being non empty reflexive RelStr, a1,a2 being Element of A
holds {a1,a2} is Chain of A iff a1 <= a2 or a2 <= a1
proof
let A be non empty reflexive RelStr, a1,a2 be Element of A;
A1: a2 <= a2;
thus {a1,a2} is Chain of A implies a1 <= a2 or a2 <= a1
proof
assume {a1,a2} is Chain of A;
then
A2: the InternalRel of A is_strongly_connected_in {a1,a2} by Def7;
a1 in {a1,a2} & a2 in {a1,a2} by TARSKI:def 2;
then
[a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A by A2;
hence thesis;
end;
assume
A3: a1 <= a2 or a2 <= a1;
A4: a1 <= a1;
{a1,a2} is strongly_connected
proof
let x,y be object;
assume
A5: x in {a1,a2} & y in {a1,a2};
now
per cases by A5,TARSKI:def 2;
suppose
x = a1 & y = a1;
hence thesis by A4;
end;
suppose
x = a1 & y = a2;
hence thesis by A3;
end;
suppose
x = a2 & y = a1;
hence thesis by A3;
end;
suppose
x = a2 & y = a2;
hence thesis by A1;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
for A being RelStr, C being Chain of A, S being Subset of A holds S c=
C implies S is Chain of A
proof
let A be RelStr, C be Chain of A, S be Subset of A;
assume
A1: S c= C;
the InternalRel of A is_strongly_connected_in C by Def7;
then the InternalRel of A is_strongly_connected_in S by A1;
hence thesis by Def7;
end;
theorem Th11:
for A being reflexive RelStr, a1,a2 being Element of A holds (ex
C being Chain of A st a1 in C & a2 in C) iff a1 <= a2 or a2 <= a1
proof
let A be reflexive RelStr;
let a1,a2 be Element of A;
thus (ex C being Chain of A st a1 in C & a2 in C) implies a1 <= a2 or a2 <=
a1
proof
given C being Chain of A such that
A1: a1 in C & a2 in C;
the InternalRel of A is_strongly_connected_in C by Def7;
then
[a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A by A1;
hence thesis;
end;
assume
A2: a1 <= a2 or a2 <= a1;
then
[a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A;
then reconsider B = A as non empty reflexive RelStr;
reconsider b1 = a1, b2 = a2 as Element of B;
reconsider Y = {b1,b2} as Chain of A by A2,Th9;
take Y;
thus thesis by TARSKI:def 2;
end;
theorem Th12:
for A being reflexive antisymmetric RelStr, a1,a2 being Element
of A holds (ex C being Chain of A st a1 in C & a2 in C) iff (a1 < a2 iff not a2
<= a1)
by Th6,Th11;
theorem Th13:
for A being RelStr, T being Subset of A holds the InternalRel of
A well_orders T implies T is Chain of A
by ORDERS_1:7,Def7;
::
:: Upper and lower cones.
::
definition
let A;
let S;
func UpperCone(S) -> Subset of A equals
{a1 : for a2 st a2 in S holds a2 <
a1};
coherence
proof
set T = {a1 : for a2 st a2 in S holds a2 < a1};
T c= the carrier of A
proof
let x be object;
assume x in T;
then ex a1 st x = a1 & for a2 st a2 in S holds a2 < a1;
hence thesis;
end;
hence thesis;
end;
end;
definition
let A;
let S;
func LowerCone(S) -> Subset of A equals
{a1 : for a2 st a2 in S holds a1 <
a2};
coherence
proof
set T = {a1 : for a2 st a2 in S holds a1 < a2};
T c= the carrier of A
proof
let x be object;
assume x in T;
then ex a1 st x = a1 & for a2 st a2 in S holds a1 < a2;
hence thesis;
end;
hence thesis;
end;
end;
theorem Th14:
UpperCone({}(A)) = the carrier of A
proof
thus UpperCone({}(A)) c= the carrier of A;
let x be object;
assume x in the carrier of A;
then reconsider a = x as Element of A;
for a2 st a2 in {}(A) holds a2 < a;
hence thesis;
end;
theorem
UpperCone([#](A)) = {}
proof
thus UpperCone([#](A)) c= {}
proof
let x be object;
assume x in UpperCone([#](A));
then ex a st x = a & for a2 st a2 in [#](A) holds a2 < a;
hence thesis;
end;
thus thesis;
end;
theorem
LowerCone({}(A)) = the carrier of A
proof
thus LowerCone({}(A)) c= the carrier of A;
let x be object;
assume x in the carrier of A;
then reconsider a = x as Element of A;
for a2 st a2 in {}(A) holds a < a2;
hence thesis;
end;
theorem
LowerCone([#](A)) = {}
proof
thus LowerCone([#](A)) c= {}
proof
let x be object;
assume x in LowerCone([#](A));
then ex a st x = a & for a2 st a2 in [#](A) holds a < a2;
hence thesis;
end;
thus thesis;
end;
theorem Th18:
a in S implies not a in UpperCone(S)
proof
assume that
A1: a in S and
A2: a in UpperCone(S);
ex a1 st a1 = a & for a2 st a2 in S holds a2 < a1 by A2;
hence thesis by A1;
end;
theorem
not a in UpperCone{a}
proof
a in {a} by TARSKI:def 1;
hence thesis by Th18;
end;
theorem Th20:
a in S implies not a in LowerCone(S)
proof
assume that
A1: a in S and
A2: a in LowerCone(S);
ex a1 st a1 = a & for a2 st a2 in S holds a1 < a2 by A2;
hence thesis by A1;
end;
theorem Th21:
not a in LowerCone{a}
proof
a in {a} by TARSKI:def 1;
hence thesis by Th20;
end;
theorem
c < a iff a in UpperCone{c}
proof
thus c < a implies a in UpperCone{c}
proof
assume c < a;
then for b holds b in {c} implies b < a by TARSKI:def 1;
hence thesis;
end;
assume a in UpperCone{c};
then
A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a2 < a1;
c in {c} by TARSKI:def 1;
hence thesis by A1;
end;
theorem Th23:
a < c iff a in LowerCone{c}
proof
thus a < c implies a in LowerCone{c}
proof
assume a < c;
then for b holds b in {c} implies a < b by TARSKI:def 1;
hence thesis;
end;
assume a in LowerCone{c};
then
A1: ex a1 st a1 = a & for a2 st a2 in {c} holds a1 < a2;
c in {c} by TARSKI:def 1;
hence thesis by A1;
end;
::
:: Initial segments.
::
definition
let A;
let S;
let a;
func InitSegm(S,a) -> Subset of A equals
LowerCone{a} /\ S;
correctness;
end;
definition
let A;
let S;
mode Initial_Segm of S -> Subset of A means
:Def11:
ex a st a in S & it = InitSegm(S,a) if S <> {} otherwise it = {};
existence
proof
now
set x = the Element of S;
assume S <> {};
then reconsider x as Element of A by Lm1;
take T = InitSegm(S,x);
thus S <> {} implies ex a st a in S & T = InitSegm(S,a);
thus S = {} implies T = {};
end;
hence thesis;
end;
consistency;
end;
theorem Th24:
a in InitSegm(S,b) iff a < b & a in S
proof
a in InitSegm(S,b) iff a in LowerCone{b} & a in S by XBOOLE_0:def 4;
hence thesis by Th23;
end;
theorem
InitSegm({}(A),a) = {};
theorem Th26:
not a in InitSegm(S,a)
proof
assume not thesis;
then a in LowerCone{a} by XBOOLE_0:def 4;
then
A1: ex a1 st a = a1 & for a2 st a2 in {a} holds a1 < a2;
a in {a} by TARSKI:def 1;
hence thesis by A1;
end;
theorem
a1 < a2 implies InitSegm(S,a1) c= InitSegm(S,a2)
proof
assume
A1: a1 < a2;
let x be object;
assume
A2: x in InitSegm(S,a1);
then x in LowerCone{a1} by XBOOLE_0:def 4;
then consider a such that
A3: a = x and
A4: for b st b in {a1} holds a < b;
a1 in {a1} by TARSKI:def 1;
then a < a1 by A4;
then a < a2 by A1,Th5;
then for b holds b in {a2} implies a < b by TARSKI:def 1;
then
A5: x in LowerCone{a2} by A3;
x in S by A2,XBOOLE_0:def 4;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem Th28:
S c= T implies InitSegm(S,a) c= InitSegm(T,a)
proof
assume
A1: S c= T;
let x be object;
assume x in InitSegm(S,a);
then x in S & x in LowerCone{a} by XBOOLE_0:def 4;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem Th29:
for I being Initial_Segm of S holds I c= S
proof
let I be Initial_Segm of S;
per cases;
suppose
S = {};
hence thesis by Def11;
end;
suppose
S <> {};
then ex a st a in S & I = InitSegm(S,a) by Def11;
hence thesis by XBOOLE_1:17;
end;
end;
theorem Th30:
S <> {} iff not S is Initial_Segm of S
proof
thus S <> {} implies not S is Initial_Segm of S
proof
assume S <> {} & S is Initial_Segm of S;
then consider a such that
A1: a in S & S = InitSegm(S,a) by Def11;
a in LowerCone{a} by A1,XBOOLE_0:def 4;
hence thesis by Th21;
end;
thus thesis by Def11;
end;
theorem Th31:
S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S
proof
assume that
A1: S <> {} and
A2: S is Initial_Segm of T and
A3: T is Initial_Segm of S;
now
per cases;
suppose
S = {};
hence thesis by A1;
end;
suppose
T = {};
hence thesis by A1,A2,Def11;
end;
suppose
A4: S <> {} & T <> {};
then consider a2 such that
A5: a2 in T and
A6: S = InitSegm(T,a2) by A2,Def11;
consider a1 such that
A7: a1 in S and
A8: T = InitSegm(S,a1) by A3,A4,Def11;
a1 in LowerCone{a2} by A7,A6,XBOOLE_0:def 4;
then
A9: ex a st a = a1 & for b st b in {a2} holds a < b;
a2 in LowerCone{a1} by A8,A5,XBOOLE_0:def 4;
then
A10: ex a3 st a3 = a2 & for b st b in {a1} holds a3 < b;
a1 in {a1} by TARSKI:def 1;
then
A11: a2 < a1 by A10;
a2 in {a2} by TARSKI:def 1;
then a1 < a2 by A9;
hence thesis by A11,Th4;
end;
end;
hence thesis;
end;
theorem Th32:
a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T
proof
assume that
A1: a1 < a2 and
A2: a1 in S and
A3: a2 in T and
A4: T is Initial_Segm of S;
consider a such that
a in S and
A5: T = InitSegm(S,a) by A2,A4,Def11;
now
let b;
assume b in {a};
then
A6: b = a by TARSKI:def 1;
a2 in LowerCone{a} by A3,A5,XBOOLE_0:def 4;
then
A7: ex a3 st a3 = a2 & for c st c in {a} holds a3 < c;
a in {a} by TARSKI:def 1;
then a2 < a by A7;
hence a1 < b by A1,A6,Th5;
end;
then a1 in LowerCone{a};
hence thesis by A2,A5,XBOOLE_0:def 4;
end;
theorem Th33:
a in S & S is Initial_Segm of T implies InitSegm(S,a) = InitSegm (T,a)
proof
assume that
A1: a in S and
A2: S is Initial_Segm of T;
A3: S c= T by A2,Th29;
thus InitSegm(S,a) c= InitSegm(T,a)
proof
let x be object;
assume x in InitSegm(S,a);
then x in LowerCone{a} & x in S by XBOOLE_0:def 4;
hence thesis by A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in InitSegm(T,a);
then
A5: x in LowerCone{a} by XBOOLE_0:def 4;
then consider a1 such that
A6: x = a1 and
A7: for a2 st a2 in {a} holds a1 < a2;
A8: a1 in T by A4,A6,XBOOLE_0:def 4;
a in {a} by TARSKI:def 1;
then a1 < a by A7;
then x in S by A1,A2,A6,A8,Th32;
hence thesis by A5,XBOOLE_0:def 4;
end;
theorem
S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2 in S &
a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T
proof
assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1,a2 st a2 in S & a1 < a2 holds a1 in S and
A4: S <> T;
per cases;
case
T <> {};
set Y = T \ S;
not T c= S by A1,A4;
then Y <> {} by XBOOLE_1:37;
then consider x being object such that
A5: x in Y and
A6: for y being object st y in Y holds [x,y] in the InternalRel of A
by A2,WELLORD1:5
,XBOOLE_1:36;
reconsider x as Element of A by A5;
take x;
thus
A7: x in T by A5,XBOOLE_0:def 5;
S = LowerCone{x} /\ T
proof
thus S c= LowerCone{x} /\ T
proof
let y be object;
assume
A8: y in S;
then reconsider a = y as Element of A;
now
let a1;
assume that
A9: a1 in {x} and
A10: not a < a1;
A11: a1 = x by A9,TARSKI:def 1;
then
A12: a1 <> a by A5,A8,XBOOLE_0:def 5;
T is Chain of A by A2,Th13;
then a1 <= a by A1,A7,A8,A10,A11,Th12;
then a1 < a by A12;
then a1 in S by A3,A8;
hence contradiction by A5,A11,XBOOLE_0:def 5;
end;
then y in {a1 : for a2 st a2 in {x} holds a1 < a2};
hence thesis by A1,A8,XBOOLE_0:def 4;
end;
let y be object;
assume
A13: y in LowerCone{x} /\ T;
then y in LowerCone{x} by XBOOLE_0:def 4;
then consider a such that
A14: a = y and
A15: for a2 st a2 in {x} holds a < a2;
A16: now
assume y in Y;
then [x,y] in the InternalRel of A by A6;
then
A17: x <= a by A14;
x in {x} by TARSKI:def 1;
hence contradiction by A15,A17,Th6;
end;
y in T by A13,XBOOLE_0:def 4;
hence thesis by A16,XBOOLE_0:def 5;
end;
hence thesis;
end;
case
T = {};
hence thesis by A1;
end;
end;
theorem Th35:
S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2
in S & a1 in T & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T
proof
assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1,a2 st a2 in S & a1 in T & a1 < a2 holds a1 in S and
A4: S <> T;
per cases;
case
T <> {};
set Y = T \ S;
not T c= S by A1,A4;
then Y <> {} by XBOOLE_1:37;
then consider x being object such that
A5: x in Y and
A6: for y being object st y in Y holds [x,y] in the InternalRel of A
by A2,WELLORD1:5
,XBOOLE_1:36;
reconsider x as Element of A by A5;
take x;
thus
A7: x in T by A5,XBOOLE_0:def 5;
S = LowerCone{x} /\ T
proof
thus S c= LowerCone{x} /\ T
proof
let y be object;
assume
A8: y in S;
then reconsider a = y as Element of A;
now
let a1;
assume that
A9: a1 in {x} and
A10: not a < a1;
A11: a1 = x by A9,TARSKI:def 1;
then
A12: a1 <> a by A5,A8,XBOOLE_0:def 5;
T is Chain of A by A2,Th13;
then a1 <= a by A1,A7,A8,A10,A11,Th12;
then a1 < a by A12;
then a1 in S by A3,A7,A8,A11;
hence contradiction by A5,A11,XBOOLE_0:def 5;
end;
then y in {a1 : for a2 st a2 in {x} holds a1 < a2};
hence thesis by A1,A8,XBOOLE_0:def 4;
end;
let y be object;
assume
A13: y in LowerCone{x} /\ T;
then y in LowerCone{x} by XBOOLE_0:def 4;
then consider a such that
A14: a = y and
A15: for a2 st a2 in {x} holds a < a2;
A16: now
assume y in Y;
then [x,y] in the InternalRel of A by A6;
then
A17: x <= a by A14;
x in {x} by TARSKI:def 1;
hence contradiction by A15,A17,Th6;
end;
y in T by A13,XBOOLE_0:def 4;
hence thesis by A16,XBOOLE_0:def 5;
end;
hence thesis;
end;
case
T = {};
hence thesis by A1;
end;
end;
::
:: Chains of choice function of BOOL of partially ordered sets.
::
reserve f for Choice_Function of BOOL(the carrier of A);
definition
let A;
let f;
mode Chain of f -> Chain of A means
:Def12:
it <> {} & the InternalRel of A
well_orders it & for a st a in it holds f.UpperCone(InitSegm(it,a)) = a;
existence
proof
set AC = the carrier of A;
AC in BOOL AC & not {} in BOOL AC by ORDERS_1:1,2;
then reconsider aa = f.AC as Element of A by ORDERS_1:89;
reconsider X = {aa} as Chain of A by Th8;
take X;
thus X <> {};
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
the InternalRel of A is_reflexive_in the carrier of A & the
InternalRel of A is_transitive_in the carrier of A by Def2,Def3;
hence the InternalRel of A is_reflexive_in X & the InternalRel of A
is_transitive_in X & the InternalRel of A is_antisymmetric_in X by A1;
the InternalRel of A is_strongly_connected_in X by Def7;
hence the InternalRel of A is_connected_in X;
thus the InternalRel of A is_well_founded_in X
proof
reconsider x = aa as set;
let Y;
assume that
A2: Y c= X and
A3: Y <> {};
take x;
Y = X by A2,A3,ZFMISC_1:33;
hence x in Y by TARSKI:def 1;
thus (the InternalRel of A)-Seg(x) /\ Y c= {}
proof
let y be object;
assume
A4: y in (the InternalRel of A)-Seg(x) /\ Y;
then y in Y by XBOOLE_0:def 4;
then
A5: y = aa by A2,TARSKI:def 1;
y in (the InternalRel of A)-Seg(x) by A4,XBOOLE_0:def 4;
hence thesis by A5,WELLORD1:1;
end;
thus thesis;
end;
let a;
assume a in X;
then
A6: a = aa by TARSKI:def 1;
LowerCone{a} /\ X c= {}(A)
proof
let x be object;
assume
A7: x in LowerCone{a} /\ X;
then x in LowerCone{a} by XBOOLE_0:def 4;
then
A8: ex a1 st x = a1 & for a2 st a2 in {a} holds a1 < a2;
x in X by A7,XBOOLE_0:def 4;
hence thesis by A6,A8;
end;
then LowerCone{a} /\ X = {}(A);
hence thesis by A6,Th14;
end;
end;
reserve fC,fC1,fC2 for Chain of f;
theorem Th36:
{f.(the carrier of A)} is Chain of f
proof
set AC = the carrier of A;
AC in BOOL AC & not {} in BOOL AC by ORDERS_1:1,2;
then reconsider aa = f.AC as Element of A by ORDERS_1:89;
reconsider X = {aa} as Chain of A by Th8;
A1: the InternalRel of A is_well_founded_in X
proof
reconsider x = aa as set;
let Y;
assume that
A2: Y c= X and
A3: Y <> {};
take x;
Y = X by A2,A3,ZFMISC_1:33;
hence x in Y by TARSKI:def 1;
thus (the InternalRel of A)-Seg(x) /\ Y c= {}
proof
let y be object;
assume
A4: y in (the InternalRel of A)-Seg(x) /\ Y;
then y in Y by XBOOLE_0:def 4;
then
A5: y = aa by A2,TARSKI:def 1;
y in (the InternalRel of A)-Seg(x) by A4,XBOOLE_0:def 4;
hence thesis by A5,WELLORD1:1;
end;
thus thesis;
end;
A6: for a st a in X holds f.UpperCone(InitSegm(X,a)) = a
proof
let a;
assume a in X;
then
A7: a = aa by TARSKI:def 1;
LowerCone{a} /\ X c= {}(A)
proof
let x be object;
assume
A8: x in LowerCone{a} /\ X;
then x in LowerCone{a} by XBOOLE_0:def 4;
then
A9: ex a1 st x = a1 & for a2 st a2 in {a} holds a1 < a2;
x in X by A8,XBOOLE_0:def 4;
hence thesis by A7,A9;
end;
then LowerCone{a} /\ X = {}(A);
hence thesis by A7,Th14;
end;
the InternalRel of A is_strongly_connected_in X by Def7;
then
A10: the InternalRel of A is_connected_in X;
the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then
A11: the InternalRel of A is_antisymmetric_in X;
the InternalRel of A is_transitive_in the carrier of A by Def3;
then
A12: the InternalRel of A is_transitive_in X;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then the InternalRel of A is_reflexive_in X;
then the InternalRel of A well_orders X by A12,A11,A10,A1;
hence thesis by A6,Def12;
end;
theorem Th37:
f.(the carrier of A) in fC
proof
the InternalRel of A well_orders fC & fC <> {} by Def12;
then consider x being object such that
A1: x in fC and
A2: for y being object st y in fC holds [x,y] in the InternalRel of A
by WELLORD1:5;
reconsider x as Element of A by A1;
A3: now
set y = the Element of LowerCone{x} /\ fC;
assume
A4: LowerCone{x} /\ fC <> {}(A);
then reconsider a = y as Element of A by Lm1;
a in LowerCone{x} by A4,XBOOLE_0:def 4;
then
A5: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2;
y in fC by A4,XBOOLE_0:def 4;
then [x,y] in the InternalRel of A by A2;
then
A6: x <= a;
x in {x} by TARSKI:def 1;
hence contradiction by A6,A5,Th6;
end;
LowerCone{x} /\ fC = InitSegm(fC,x);
then f.UpperCone(LowerCone{x} /\ fC) = x by A1,Def12;
hence thesis by A1,A3,Th14;
end;
theorem Th38:
a in fC & b = f.(the carrier of A) implies b <= a
proof
assume that
A1: a in fC and
A2: b = f.(the carrier of A);
the InternalRel of A well_orders fC & fC <> {} by Def12;
then consider x being object such that
A3: x in fC and
A4: for y being object st y in fC holds [x,y] in the InternalRel of A
by WELLORD1:5;
reconsider x as Element of A by A3;
A5: now
set y = the Element of LowerCone{x} /\ fC;
assume
A6: LowerCone{x} /\ fC <> {}(A);
then reconsider a = y as Element of A by Lm1;
a in LowerCone{x} by A6,XBOOLE_0:def 4;
then
A7: ex a1 st a = a1 & for a2 st a2 in {x} holds a1 < a2;
y in fC by A6,XBOOLE_0:def 4;
then [x,y] in the InternalRel of A by A4;
then
A8: x <= a;
x in {x} by TARSKI:def 1;
hence contradiction by A8,A7,Th6;
end;
LowerCone{x} /\ fC = InitSegm(fC,x);
then f.UpperCone(LowerCone{x} /\ fC) = x by A3,Def12;
then
A9: f.(the carrier of A) = x by A5,Th14;
[x,a] in the InternalRel of A by A1,A4;
hence thesis by A2,A9;
end;
theorem
a = f.(the carrier of A) implies InitSegm(fC,a) = {}
proof
set x = the Element of LowerCone{a} /\ fC;
assume
A1: a = f.(the carrier of A);
then
A2: a in fC by Th37;
assume
A3: InitSegm(fC,a) <> {};
then reconsider b = x as Element of A by Lm1;
x in LowerCone{a} by A3,XBOOLE_0:def 4;
then
A4: ex a1 st a1 = b & for a2 st a2 in {a} holds a1 < a2;
a in {a} by TARSKI:def 1;
then
A5: b < a by A4;
A6: x in fC by A3,XBOOLE_0:def 4;
then a <= b by A1,Th38;
hence contradiction by A2,A6,A5,Th12;
end;
theorem
fC1 meets fC2
proof
f.(the carrier of A) in fC1 & f.(the carrier of A) in fC2 by Th37;
hence thesis by XBOOLE_0:3;
end;
theorem Th41:
fC1 <> fC2 implies (fC1 is Initial_Segm of fC2 iff not fC2 is
Initial_Segm of fC1)
proof
assume
A1: fC1 <> fC2;
set N = {a : a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a)};
A2: N c= fC1
proof
let x be object;
assume x in N;
then
ex a st a = x & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a);
hence thesis by XBOOLE_0:def 4;
end;
then reconsider N as Subset of A by XBOOLE_1:1;
A3: N c= fC2
proof
let x be object;
assume x in N;
then ex a st a = x & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a);
hence thesis by XBOOLE_0:def 4;
end;
A4: now
let a1,a2;
assume that
A5: a2 in N and
A6: a1 in fC1 and
A7: a1 < a2;
A8: ex a st a = a2 & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a) by A5;
A9: InitSegm(fC1,a1) = InitSegm(fC2,a1)
proof
thus InitSegm(fC1,a1) c= InitSegm(fC2,a1)
proof
let x be object;
assume
A10: x in InitSegm(fC1,a1);
then reconsider b = x as Element of A;
A11: b in fC1 by A10,Th24;
A12: b < a1 by A10,Th24;
then b < a2 by A7,Th5;
then b in InitSegm(fC1,a2) by A11,Th24;
then b in fC2 by A8,Th24;
hence thesis by A12,Th24;
end;
let x be object;
assume
A13: x in InitSegm(fC2,a1);
then reconsider b = x as Element of A;
A14: b in fC2 by A13,Th24;
A15: b < a1 by A13,Th24;
then b < a2 by A7,Th5;
then b in InitSegm(fC2,a2) by A14,Th24;
then b in fC1 by A8,Th24;
hence thesis by A15,Th24;
end;
a1 in InitSegm(fC2,a2) by A6,A7,A8,Th24;
then a1 in fC2 by XBOOLE_0:def 4;
then a1 in fC1 /\ fC2 by A6,XBOOLE_0:def 4;
hence a1 in N by A9;
end;
A16: now
let a1,a2;
assume that
A17: a2 in N and
A18: a1 in fC2 and
A19: a1 < a2;
A20: ex a st a = a2 & a in fC1 /\ fC2 & InitSegm(fC1,a) = InitSegm(fC2,a)
by A17;
A21: InitSegm(fC1,a1) = InitSegm(fC2,a1)
proof
thus InitSegm(fC1,a1) c= InitSegm(fC2,a1)
proof
let x be object;
assume
A22: x in InitSegm(fC1,a1);
then reconsider b = x as Element of A;
A23: b in fC1 by A22,Th24;
A24: b < a1 by A22,Th24;
then b < a2 by A19,Th5;
then b in InitSegm(fC1,a2) by A23,Th24;
then b in fC2 by A20,Th24;
hence thesis by A24,Th24;
end;
let x be object;
assume
A25: x in InitSegm(fC2,a1);
then reconsider b = x as Element of A;
A26: b in fC2 by A25,Th24;
A27: b < a1 by A25,Th24;
then b < a2 by A19,Th5;
then b in InitSegm(fC2,a2) by A26,Th24;
then b in fC1 by A20,Th24;
hence thesis by A27,Th24;
end;
a1 in InitSegm(fC1,a2) by A18,A19,A20,Th24;
then a1 in fC1 by XBOOLE_0:def 4;
then a1 in fC1 /\ fC2 by A18,XBOOLE_0:def 4;
hence a1 in N by A21;
end;
A28: the InternalRel of A well_orders fC1 & the InternalRel of A well_orders
fC2 by Def12;
now
per cases by A2,A4,A28,A3,A16,Th35;
suppose
A29: N is Initial_Segm of fC1 & N = fC2;
fC1 <> {} by Def12;
hence thesis by A29,Th31;
end;
suppose
A30: N is Initial_Segm of fC2 & N = fC1;
fC2 <> {} by Def12;
hence thesis by A30,Th31;
end;
suppose
N = fC1 & N = fC2;
hence thesis by A1;
end;
suppose
A31: N is Initial_Segm of fC1 & N is Initial_Segm of fC2;
fC2 <> {} by Def12;
then consider b such that
A32: b in fC2 and
A33: N = InitSegm(fC2,b) by A31,Def11;
fC1 <> {} by Def12;
then consider a such that
A34: a in fC1 and
A35: N = InitSegm(fC1,a) by A31,Def11;
A36: a = f.UpperCone(InitSegm(fC2,b)) by A34,A35,A33,Def12
.= b by A32,Def12;
then a in fC1 /\ fC2 by A34,A32,XBOOLE_0:def 4;
then a in N by A35,A33,A36;
hence thesis by A35,Th26;
end;
end;
hence thesis;
end;
theorem Th42:
fC1 c< fC2 iff fC1 is Initial_Segm of fC2
proof
thus fC1 c< fC2 implies fC1 is Initial_Segm of fC2
proof
assume
A1: fC1 c< fC2;
now
assume
A2: fC2 is Initial_Segm of fC1;
fC1 <> {} by Def12;
then ex a st a in fC1 & fC2 = InitSegm(fC1,a) by A2,Def11;
then fC2 c= fC1 by XBOOLE_1:17;
hence contradiction by A1,XBOOLE_0:def 8;
end;
hence thesis by A1,Th41;
end;
assume
A3: fC1 is Initial_Segm of fC2;
A4: fC2 <> {} by Def12;
then ex a st a in fC2 & fC1 = InitSegm(fC2,a) by A3,Def11;
then
A5: fC1 c= fC2 by XBOOLE_1:17;
fC1 <> fC2 by A3,A4,Th30;
hence thesis by A5;
end;
definition
let A;
let f;
func Chains f -> set means
:Def13:
x in it iff x is Chain of f;
existence
proof
defpred P[set] means $1 is Chain of f;
consider X such that
A1: for x holds x in X iff x in bool(the carrier of A) & P[x] from
XFAMILY:sch 1;
take X;
let x;
thus x in X implies x is Chain of f by A1;
assume x is Chain of f;
hence thesis by A1;
end;
uniqueness
proof
let D1,D2 be set;
assume
A2: for x holds x in D1 iff x is Chain of f;
assume
A3: for x holds x in D2 iff x is Chain of f;
thus D1 c= D2
proof
let x be object;
assume x in D1;
then x is Chain of f by A2;
hence thesis by A3;
end;
let x be object;
assume x in D2;
then x is Chain of f by A3;
hence thesis by A2;
end;
end;
registration
let A;
let f;
cluster Chains f -> non empty;
coherence
proof
set x = the Chain of f;
x in Chains f by Def13;
hence thesis;
end;
end;
Lm2: union(Chains(f)) is Subset of A
proof
now
let X;
assume X in Chains(f);
then X is Chain of f by Def13;
hence X c= the carrier of A;
end;
hence thesis by ZFMISC_1:76;
end;
Lm3: union(Chains(f)) is Chain of A
proof
reconsider C = union(Chains(f)) as Subset of A by Lm2;
the InternalRel of A is_strongly_connected_in C
proof
let x,y be object;
assume that
A1: x in C and
A2: y in C;
consider X such that
A3: x in X and
A4: X in Chains(f) by A1,TARSKI:def 4;
consider Y such that
A5: y in Y and
A6: Y in Chains(f) by A2,TARSKI:def 4;
reconsider X,Y as Chain of f by A4,A6,Def13;
A7: the InternalRel of A is_strongly_connected_in X by Def7;
A8: the InternalRel of A is_strongly_connected_in Y by Def7;
now
per cases;
suppose
X = Y;
hence thesis by A3,A5,A7;
end;
suppose
A9: X <> Y;
now
per cases by A9,Th41;
suppose
X is Initial_Segm of Y;
then X c< Y by Th42;
then X c= Y;
hence thesis by A3,A5,A8;
end;
suppose
Y is Initial_Segm of X;
then Y c< X by Th42;
then Y c= X;
hence thesis by A3,A5,A7;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
hence thesis by Def7;
end;
theorem Th43:
union(Chains(f)) <> {}
proof
{f.(the carrier of A)} is Chain of f by Th36;
then {f.(the carrier of A)} in Chains(f) by Def13;
hence thesis by ORDERS_1:6;
end;
theorem Th44:
fC <> union(Chains(f)) & S = union(Chains(f)) implies fC is Initial_Segm of S
proof
assume that
A1: fC <> union(Chains(f)) and
A2: S = union(Chains(f));
set x = the Element of S \ fC;
fC in Chains(f) by Def13;
then fC c= union(Chains(f)) by ZFMISC_1:74;
then not union(Chains(f)) c= fC by A1;
then
A3: S \ fC <> {} by A2,XBOOLE_1:37;
then
A4: not x in fC by XBOOLE_0:def 5;
x in S by A3,XBOOLE_0:def 5;
then consider X such that
A5: x in X and
A6: X in Chains(f) by A2,TARSKI:def 4;
reconsider X as Chain of f by A6,Def13;
not X c= fC by A3,A5,XBOOLE_0:def 5;
then not X c< fC;
then not X is Initial_Segm of fC by Th42;
then fC is Initial_Segm of X by A5,A4,Th41;
then consider a such that
A7: a in X and
A8: fC = InitSegm(X,a) by A5,Def11;
A9: X c= S by A2,A6,ZFMISC_1:74;
InitSegm(S,a) = InitSegm(X,a)
proof
thus InitSegm(S,a) c= InitSegm(X,a)
proof
let x be object;
assume
A10: x in InitSegm(S,a);
then
A11: x in LowerCone{a} by XBOOLE_0:def 4;
then consider b such that
A12: b = x and
A13: for a2 st a2 in {a} holds b < a2;
b in S by A10,A12,XBOOLE_0:def 4;
then consider Y such that
A14: b in Y and
A15: Y in Chains(f) by A2,TARSKI:def 4;
reconsider Y as Chain of f by A15,Def13;
a in {a} by TARSKI:def 1;
then
A16: b < a by A13;
now
per cases;
suppose
X = Y;
hence thesis by A11,A12,A14,XBOOLE_0:def 4;
end;
suppose
A17: X <> Y;
now
per cases by A17,Th41;
suppose
X is Initial_Segm of Y;
then x in X by A7,A12,A16,A14,Th32;
hence thesis by A11,XBOOLE_0:def 4;
end;
suppose
Y is Initial_Segm of X;
then Y c< X by Th42;
then Y c= X;
hence thesis by A11,A12,A14,XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
let x be object;
assume x in InitSegm(X,a);
then x in LowerCone{a} & x in X by XBOOLE_0:def 4;
hence thesis by A9,XBOOLE_0:def 4;
end;
hence thesis by A7,A8,A9,Def11;
end;
theorem Th45:
union(Chains(f)) is Chain of f
proof
reconsider C = union(Chains(f)) as Chain of A by Lm3;
A1: now
let a;
assume a in C;
then consider X such that
A2: a in X and
A3: X in Chains(f) by TARSKI:def 4;
reconsider X as Chain of f by A3,Def13;
now
InitSegm(C,a) = InitSegm(X,a) by A2,Th33,Th44;
hence f.UpperCone(InitSegm(C,a)) = a by A2,Def12;
end;
hence f.UpperCone(InitSegm(C,a)) = a;
end;
A4: the InternalRel of A well_orders C
proof
A5: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
the InternalRel of A is_reflexive_in the carrier of A & the
InternalRel of A is_transitive_in the carrier of A by Def2,Def3;
hence the InternalRel of A is_reflexive_in C & the InternalRel of A
is_transitive_in C & the InternalRel of A is_antisymmetric_in C by A5;
the InternalRel of A is_strongly_connected_in C by Def7;
hence the InternalRel of A is_connected_in C;
let Y;
set x = the Element of Y;
assume that
A6: Y c= C and
A7: Y <> {};
x in C by A6,A7;
then consider X such that
A8: x in X and
A9: X in Chains(f) by TARSKI:def 4;
reconsider X as Chain of f by A9,Def13;
A10: the InternalRel of A well_orders X by Def12;
X /\ Y <> {} by A7,A8,XBOOLE_0:def 4;
then consider a being object such that
A11: a in X /\ Y and
A12: for x being object st x in X /\ Y holds [a,x] in the InternalRel of A
by A10,WELLORD1:5
,XBOOLE_1:17;
take a;
thus a in Y by A11,XBOOLE_0:def 4;
reconsider aa = a as Element of A by A11;
thus (the InternalRel of A)-Seg(a) /\ Y c= {}
proof
let y be object;
assume
A13: y in (the InternalRel of A)-Seg(a) /\ Y;
then
A14: y in Y by XBOOLE_0:def 4;
then y in C by A6;
then reconsider b = y as Element of A;
A15: y in (the InternalRel of A)-Seg(a) by A13,XBOOLE_0:def 4;
then
A16: y <> a by WELLORD1:1;
[y,a] in the InternalRel of A by A15,WELLORD1:1;
then
A17: b <= aa;
now
per cases;
suppose
A18: X <> C;
a in X & b < aa by A11,A16,A17,XBOOLE_0:def 4;
hence y in X by A6,A14,A18,Th32,Th44;
end;
suppose
X = C;
hence y in X by A6,A14;
end;
end;
then y in X /\ Y by A14,XBOOLE_0:def 4;
then [a,y] in the InternalRel of A by A12;
then aa <= b;
hence thesis by A16,A17,Th2;
end;
thus thesis;
end;
C <> {} by Th43;
hence thesis by A4,A1,Def12;
end;
begin :: From original ORDERS_2
reserve R for Relation,
A for non empty Poset,
C for Chain of A,
S for Subset of A,
a,a1,a2,b,c1,c2 for Element of A;
::
:: Orders.
::
theorem Th46:
field((the InternalRel of A) |_2 S) = S
proof
set P = (the InternalRel of A) |_2 S;
thus field P c= S by WELLORD1:13;
thus S c= field P
proof
let x be object;
assume
A1: x in S;
then
A2: [x,x] in [:S,S:] by ZFMISC_1:87;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then [x,x] in the InternalRel of A by A1;
then [x,x] in P by A2,XBOOLE_0:def 4;
then x in dom P by XTUPLE_0:def 12;
hence thesis by XBOOLE_0:def 3;
end;
end;
theorem
(the InternalRel of A) |_2 S is being_linear-order implies S is Chain of A
proof
assume (the InternalRel of A) |_2 S is being_linear-order;
then
A1: (the InternalRel of A) |_2 S is connected;
field((the InternalRel of A) |_2 S) = S by Th46;
then
A2: (the InternalRel of A) |_2 S is_connected_in S by A1;
S is strongly_connected
proof
let x,y be object;
assume
A3: x in S & y in S;
then reconsider a = x, b = y as Element of A;
now
per cases;
suppose
x = y;
then a <= b;
hence thesis;
end;
suppose
x <> y;
then [x,y] in (the InternalRel of A) |_2 S or [y,x] in (the
InternalRel of A) |_2 S by A2,A3;
hence thesis by XBOOLE_0:def 4;
end;
end;
hence thesis;
end;
hence thesis;
end;
theorem
(the InternalRel of A) |_2 C is being_linear-order
proof
set P = (the InternalRel of A) |_2 C;
A1: P is_connected_in C
proof
let x,y be object;
assume
A2: x in C & y in C;
then
A3: [x,y] in [:C,C:] & [y,x] in [:C,C:] by ZFMISC_1:87;
the InternalRel of A is_strongly_connected_in C by Def7;
then
[x,y] in the InternalRel of A or [y,x] in the InternalRel of A by A2;
hence thesis by A3,XBOOLE_0:def 4;
end;
the InternalRel of A is being_partial-order;
then P is being_partial-order by ORDERS_1:26;
hence P is reflexive & P is transitive & P is antisymmetric;
C = field P by Th46;
hence thesis by A1;
end;
theorem
the InternalRel of A linearly_orders S implies S is Chain of A
by ORDERS_1:7,Def7;
theorem
the InternalRel of A linearly_orders C
proof
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
the InternalRel of A is_reflexive_in the carrier of A & the InternalRel
of A is_transitive_in the carrier of A by Def2,Def3;
hence the InternalRel of A is_reflexive_in C & the InternalRel of A
is_transitive_in C & the InternalRel of A is_antisymmetric_in C by A1;
the InternalRel of A is_strongly_connected_in C by Def7;
hence thesis;
end;
theorem
a is_minimal_in the InternalRel of A iff for b holds not b < a
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
thus a is_minimal_in the InternalRel of A implies for b holds not b < a
proof
assume
A2: a is_minimal_in the InternalRel of A;
let b;
a = b or not [b,a] in the InternalRel of A by A1,A2;
then a = b or not b <= a;
hence thesis;
end;
assume
A3: for b holds not b < a;
thus a in field(the InternalRel of A) by A1;
let y;
assume that
A4: y in field(the InternalRel of A) and
A5: y <> a and
A6: [y,a] in the InternalRel of A;
reconsider b = y as Element of A by A4,ORDERS_1:15;
b <= a by A6;
then b < a by A5;
hence thesis by A3;
end;
theorem
a is_maximal_in the InternalRel of A iff for b holds not a < b
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
thus a is_maximal_in the InternalRel of A implies for b holds not a < b
proof
assume
A2: a is_maximal_in the InternalRel of A;
let b;
a = b or not [a,b] in the InternalRel of A by A1,A2;
then a = b or not a <= b;
hence thesis;
end;
assume
A3: for b holds not a < b;
thus a in field(the InternalRel of A) by A1;
let y;
assume that
A4: y in field(the InternalRel of A) and
A5: y <> a and
A6: [a,y] in the InternalRel of A;
reconsider b = y as Element of A by A4,ORDERS_1:15;
a <= b by A6;
then a < b by A5;
hence thesis by A3;
end;
theorem
a is_superior_of the InternalRel of A iff for b st a <> b holds b < a
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
thus a is_superior_of the InternalRel of A implies for b st a <> b holds b <
a
proof
assume
A2: a is_superior_of the InternalRel of A;
let b;
assume
A3: a <> b;
then [b,a] in the InternalRel of A by A1,A2;
then b <= a;
hence thesis by A3;
end;
assume
A4: for b st a <> b holds b < a;
thus a in field(the InternalRel of A) by A1;
let y;
assume y in field(the InternalRel of A);
then reconsider b = y as Element of A by ORDERS_1:15;
assume y <> a;
then b < a by A4;
then b <= a;
hence thesis;
end;
theorem
a is_inferior_of the InternalRel of A iff for b st a <> b holds a < b
proof
A1: the carrier of A = field(the InternalRel of A) by ORDERS_1:15;
thus a is_inferior_of the InternalRel of A implies for b st a <> b holds a <
b
proof
assume
A2: a is_inferior_of the InternalRel of A;
let b;
assume
A3: a <> b;
then [a,b] in the InternalRel of A by A1,A2;
then a <= b;
hence thesis by A3;
end;
assume
A4: for b st a <> b holds a < b;
thus a in field(the InternalRel of A) by A1;
let y;
assume y in field(the InternalRel of A);
then reconsider b = y as Element of A by ORDERS_1:15;
assume y <> a;
then a < b by A4;
then a <= b;
hence thesis;
end;
Lm4: R well_orders X & Y c= X implies R well_orders Y
proof
assume that
A1: R well_orders X and
A2: Y c= X;
A3: R is_antisymmetric_in X & R is_connected_in X by A1;
A4: R is_well_founded_in X by A1;
R is_reflexive_in X & R is_transitive_in X by A1;
hence R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y &
R is_connected_in Y by A2,A3;
let Z be set;
assume that
A5: Z c= Y and
A6: Z <> {};
Z c= X by A2,A5;
hence thesis by A6,A4;
end;
::
:: Kuratowski - Zorn Lemma.
::
theorem Th55:
(for C ex a st for b st b in C holds b <= a) implies ex a st
for b holds not a < b
proof
set f = the Choice_Function of BOOL(the carrier of A);
reconsider F = union(Chains(f)) as Chain of f by Th45;
assume for C ex a st for b st b in C holds b <= a;
then consider a such that
A1: for b st b in F holds b <= a;
take a;
let b;
assume
A2: a < b;
now
let a1;
assume a1 in F;
then a1 <= a by A1;
hence a1 < b by A2,Th7;
end;
then b in {a1 : for a2 st a2 in F holds a2 < a1};
then not UpperCone(F) in {{}} by TARSKI:def 1;
then
A3: UpperCone(F) in BOOL(the carrier of A) by XBOOLE_0:def 5;
not {} in BOOL(the carrier of A) by ORDERS_1:1;
then
A4: f.UpperCone(F) in UpperCone(F) by A3,ORDERS_1:89;
then reconsider c = f.UpperCone(F) as Element of A;
reconsider Z = F \/ {c} as Subset of A;
A5: ex c11 being Element of A st c11 = c & for a2 st a2 in F holds a2 < c11
by A4;
A6: the InternalRel of A is_connected_in Z
proof
let x,y be object;
assume
A7: x in Z & y in Z;
then reconsider x1 = x, y1 = y as Element of A;
now
per cases by A7,XBOOLE_0:def 3;
suppose
x1 in F & y1 in F;
then x1 <= y1 or y1 <= x1 by Th11;
hence thesis;
end;
suppose
A8: x1 in F & y1 in {c};
then y1 = c by TARSKI:def 1;
then x1 < y1 by A5,A8;
then x1 <= y1;
hence thesis;
end;
suppose
A9: x1 in {c} & y1 in F;
then x1 = c by TARSKI:def 1;
then y1 < x1 by A5,A9;
then y1 <= x1;
hence thesis;
end;
suppose
A10: x1 in {c} & y1 in {c};
then x1 = c by TARSKI:def 1;
hence thesis by A10,TARSKI:def 1;
end;
end;
hence thesis;
end;
A11: now
let a1;
assume
A12: a1 in Z;
now
per cases;
suppose
A13: a1 = c;
InitSegm(Z,c) = F
proof
thus InitSegm(Z,c) c= F
proof
let x be object;
assume that
A14: x in InitSegm(Z,c) and
A15: not x in F;
x in Z by A14,XBOOLE_0:def 4;
then x in {c} by A15,XBOOLE_0:def 3;
then
A16: x = c by TARSKI:def 1;
x in LowerCone{c} by A14,XBOOLE_0:def 4;
hence contradiction by A16,Th21;
end;
let x be object;
assume
A17: x in F;
then reconsider y = x as Element of A;
y < c by A5,A17;
then
A18: x in LowerCone{c} by Th23;
x in Z by A17,XBOOLE_0:def 3;
hence thesis by A18,XBOOLE_0:def 4;
end;
hence f.UpperCone(InitSegm(Z,a1)) = a1 by A13;
end;
suppose
a1 <> c;
then not a1 in {c} by TARSKI:def 1;
then
A19: a1 in F by A12,XBOOLE_0:def 3;
A20: InitSegm(Z,a1) c= InitSegm(F,a1)
proof
let x be object;
assume
A21: x in InitSegm(Z,a1);
then
A22: x in LowerCone{a1} by XBOOLE_0:def 4;
now
assume
A23: not x in F;
x in Z by A21,XBOOLE_0:def 4;
then x in {c} by A23,XBOOLE_0:def 3;
then x = c by TARSKI:def 1;
then
A24: ex c1 st c1 = c & for c2 st c2 in {a1} holds c1 < c2 by A22;
A25: a1 < c by A5,A19;
a1 in {a1} by TARSKI:def 1;
then c < a1 by A24;
hence contradiction by A25,Th4;
end;
hence thesis by A22,XBOOLE_0:def 4;
end;
InitSegm(F,a1) c= InitSegm(Z,a1) by Th28,XBOOLE_1:7;
then InitSegm(Z,a1) = InitSegm(F,a1) by A20;
hence f.UpperCone(InitSegm(Z,a1)) = a1 by A19,Def12;
end;
end;
hence f.UpperCone(InitSegm(Z,a1)) = a1;
end;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then
A26: the InternalRel of A is_reflexive_in Z;
then the InternalRel of A is_strongly_connected_in Z by A6,ORDERS_1:7;
then
A27: Z is Chain of A by Def7;
A28: the InternalRel of A is_well_founded_in Z
proof
let Y;
assume that
A29: Y c= Z and
A30: Y <> {};
now
per cases;
case
A31: Y = {c};
take x = c;
thus x in Y by A31,TARSKI:def 1;
assume (the InternalRel of A)-Seg(x) meets Y;
then consider x9 being object such that
A32: x9 in (the InternalRel of A)-Seg(x) and
A33: x9 in Y by XBOOLE_0:3;
x9 = c by A31,A33,TARSKI:def 1;
hence contradiction by A32,WELLORD1:1;
end;
case
A34: Y <> {c};
set X = Y \ {c};
A35: now
assume X = {};
then Y c= {c} by XBOOLE_1:37;
hence contradiction by A30,A34,ZFMISC_1:33;
end;
A36: X c= F
proof
let x be object;
assume that
A37: x in X and
A38: not x in F;
x in Y by A37;
then x in {c} by A29,A38,XBOOLE_0:def 3;
hence thesis by A37,XBOOLE_0:def 5;
end;
the InternalRel of A well_orders F by Def12;
then the InternalRel of A well_orders X by A36,Lm4;
then the InternalRel of A is_well_founded_in X;
then consider x being object such that
A39: x in X and
A40: (the InternalRel of A)-Seg(x) misses X by A35;
take x9 = x;
thus x9 in Y by A39;
A41: (the InternalRel of A)-Seg(x) /\ X = {} by A40;
now
per cases;
suppose
A42: c in Y;
A43: now
x9 in F by A36,A39;
then reconsider x99 = x9 as Element of A;
assume
A44: c in (the InternalRel of A)-Seg(x9);
then [c,x9] in the InternalRel of A by WELLORD1:1;
then
A45: c <= x99;
A46: x99 < c by A5,A36,A39;
c <> x99 by A44,WELLORD1:1;
then c < x99 by A45;
hence contradiction by A46,Th4;
end;
A47: now
set x = the Element of (the InternalRel of A)-Seg(x9) /\ {c };
assume
A48: (the InternalRel of A)-Seg(x9) /\ {c} <> {};
then x in {c} by XBOOLE_0:def 4;
then x = c by TARSKI:def 1;
hence contradiction by A43,A48,XBOOLE_0:def 4;
end;
{c} c= Y by A42,ZFMISC_1:31;
then Y = X \/ {c} by XBOOLE_1:45;
then (the InternalRel of A)-Seg(x9) /\ Y = {} \/ {} by A41,A47,
XBOOLE_1:23
.= {};
hence (the InternalRel of A)-Seg(x9) misses Y;
end;
suppose
not c in Y;
then Y misses {c} by ZFMISC_1:50;
hence (the InternalRel of A)-Seg(x9) misses Y by A40,XBOOLE_1:83;
end;
end;
hence (the InternalRel of A)-Seg(x9) misses Y;
end;
end;
hence thesis;
end;
the InternalRel of A is_transitive_in the carrier of A by Def3;
then
A49: the InternalRel of A is_transitive_in Z;
the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then the InternalRel of A is_antisymmetric_in Z;
then the InternalRel of A well_orders Z by A26,A49,A6,A28;
then reconsider Z as Chain of f by A27,A11,Def12;
c in {c} by TARSKI:def 1;
then
A50: c in Z by XBOOLE_0:def 3;
Z in Chains(f) by Def13;
then c in F by A50,TARSKI:def 4;
hence thesis by A5;
end;
theorem
(for C ex a st for b st b in C holds a <= b) implies ex a st for b
holds not b < a
proof
set X = the carrier of A;
set R = (the InternalRel of A)~;
A1: dom R = dom the InternalRel of A by RELAT_2:12
.= X by PARTFUN1:def 2;
A2: for a,b being Element of A holds [a,b] in R iff b <= a
by RELAT_1:def 7;
reconsider R as Order of the carrier of A by A1,PARTFUN1:def 2;
set B = RelStr (# the carrier of A, R #);
assume
A3: for C ex a st for b st b in C holds a <= b;
for E being Chain of B ex e being Element of B st for f being Element of
B st f in E holds f <= e
proof
let E be Chain of B;
reconsider C = E as Subset of A;
the InternalRel of A is_strongly_connected_in C
proof
let x,y be object;
assume
A4: x in C & y in C;
then reconsider e = x, f = y as Element of B;
reconsider e1 = e, f1 = f as Element of A;
A5: e <= f or f <= e by A4,Th11;
now
per cases by A5;
suppose
[e,f] in R;
then f1 <= e1 by A2;
hence thesis;
end;
suppose
[f,e] in R;
then e1 <= f1 by A2;
hence thesis;
end;
end;
hence thesis;
end;
then reconsider C as Chain of A by Def7;
consider a such that
A6: for b st b in C holds a <= b by A3;
reconsider e = a as Element of B;
take e;
let f be Element of B;
reconsider b = f as Element of A;
assume f in E;
then a <= b by A6;
then [f,e] in R by A2;
hence thesis;
end;
then consider e being Element of B such that
A7: for f being Element of B holds not e < f by Th55;
reconsider d = e as Element of A;
take d;
let b;
reconsider f = b as Element of B;
assume
A8: b < d;
then b <= d;
then [e,f] in R by A2;
then e <= f;
then e < f by A8;
hence thesis by A7;
end;
:: from YELLOW14, 2009.07.26, A.T.
registration
cluster strict empty for RelStr;
existence
proof
take R = RelStr (#{},the Relation of {}#);
thus R is strict;
thus the carrier of R is empty;
end;
end;