:: Morphisms Into Chains, Part {I}
:: by Artur Korni{\l}owicz
::
:: Received February 6, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ORDERS_2, WAYBEL_4,
RELAT_1, RELAT_2, LATTICE3, LATTICES, FUNCT_1, YELLOW_1, LATTICE7,
WAYBEL_0, SEQM_3, XXREAL_0, TARSKI, ARYTM_3, GROUP_4, ORDERS_1, WELLORD2,
WELLORD1, YELLOW_0, EQREL_1, REWRITE1, WAYBEL_1, ORDINAL2, NUMBERS,
CARD_1, NAT_1, WAYBEL35, FUNCT_7;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
XCMPLX_0, NAT_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1,
FUNCT_7, STRUCT_0, WELLORD1, ORDERS_2, ORDERS_1, LATTICE3, YELLOW_0,
YELLOW_1, ALG_1, WAYBEL_0, WAYBEL_1, WAYBEL_4, LATTICE7;
constructors WELLORD1, NAT_1, REALSET1, ORDERS_3, WAYBEL_1, WAYBEL_4,
LATTICE7, RELSET_1, NUMBERS, FUNCT_7;
registrations SUBSET_1, ORDINAL1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0,
WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_4, ZFMISC_1, CARD_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, XBOOLE_0, ORDERS_1, LATTICE3, WAYBEL_1;
equalities XBOOLE_0;
expansions XBOOLE_0, ORDERS_1, LATTICE3, WAYBEL_1;
theorems WAYBEL_4, FUNCT_2, YELLOW_1, TARSKI, ORDERS_2, YELLOW_0, YELLOW_4,
WAYBEL_0, XBOOLE_0, LATTICE7, XBOOLE_1, RELAT_1, WELLORD2, ORDERS_1,
RELAT_2, ZFMISC_1, FUNCT_1, SUBSET_1;
schemes FUNCT_2, RECDEF_1, NAT_1, XFAMILY;
begin :: Preliminaries
Lm1: for x,y,X being set st y in {x} \/ X holds y = x or y in X
proof
let x,y,X be set;
assume y in {x} \/ X;
then y in {x} or y in X by XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
begin :: Main part
registration
let L be RelStr;
cluster auxiliary(i) for Relation of L;
existence
proof
take IntRel L;
thus thesis;
end;
end;
registration
let L be transitive RelStr;
cluster auxiliary(i) auxiliary(ii) for Relation of L;
existence
proof
take IntRel L;
thus thesis;
end;
end;
registration
let L be with_suprema antisymmetric RelStr;
cluster auxiliary(iii) for Relation of L;
existence
proof
take IntRel L;
thus thesis;
end;
end;
registration
let L be non empty lower-bounded antisymmetric RelStr;
cluster auxiliary(iv) for Relation of L;
existence
proof
take IntRel L;
thus thesis;
end;
end;
:: Definition 2.1, p. 203
definition
let L be non empty RelStr, R be Relation of L;
attr R is extra-order means
R is auxiliary(i) auxiliary(ii) auxiliary(iv);
end;
registration
let L be non empty RelStr;
cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) for
Relation of
L;
coherence;
cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order for
Relation of
L;
coherence;
end;
registration
let L be non empty RelStr;
cluster extra-order auxiliary(iii) -> auxiliary for Relation of L;
coherence;
cluster auxiliary -> extra-order for Relation of L;
coherence;
end;
registration
let L be lower-bounded antisymmetric transitive non empty RelStr;
cluster extra-order for Relation of L;
existence
proof
take IntRel L;
thus thesis;
end;
end;
definition
let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;
func R-LowerMap -> Function of L, InclPoset LOWER L means
:Def2:
for x being Element of L holds it.x = R-below x;
existence
proof
deffunc F(Element of L) = R-below $1;
A1: for x being Element of L holds F(x) is Element of InclPoset LOWER L
proof
let x be Element of L;
reconsider I = F(x) as lower Subset of L;
LOWER L = {X where X is Subset of L: X is lower} by LATTICE7:def 7;
then I in LOWER L;
hence thesis by YELLOW_1:1;
end;
consider f being Function of L, InclPoset LOWER L such that
A2: for x being Element of L holds f.x = F(x) from FUNCT_2:sch 9(A1);
take f;
let x be Element of L;
thus thesis by A2;
end;
uniqueness
proof
let M1, M2 be Function of L, InclPoset LOWER L;
assume
A3: for x be Element of L holds M1.x = R-below x;
assume
A4: for x be Element of L holds M2.x = R-below x;
for x be object st x in the carrier of L holds M1.x = M2.x
proof
let x be object;
assume x in the carrier of L;
then reconsider x9 = x as Element of L;
thus M1.x = R-below x9 by A3
.= M2.x by A4;
end;
hence thesis by FUNCT_2:12;
end;
end;
registration
let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;
cluster R-LowerMap -> monotone;
coherence
proof
let x, y be Element of L;
set s = R-LowerMap;
A1: s.y = R-below y by Def2;
assume x <= y;
then
A2: R-below x c= R-below y by WAYBEL_4:17;
s.x = R-below x by Def2;
hence thesis by A2,A1,YELLOW_1:3;
end;
end;
definition
let L be 1-sorted, R be Relation of the carrier of L;
mode strict_chain of R -> Subset of L means
:Def3:
for x, y being set st x
in it & y in it holds [x,y] in R or x = y or [y,x] in R;
existence
proof
take {}L;
thus thesis;
end;
end;
theorem Th1:
for L being 1-sorted, C being trivial Subset of L, R being
Relation of the carrier of L holds C is strict_chain of R
proof
let L be 1-sorted, C be trivial Subset of L, R be Relation of the carrier of
L;
let x, y be set;
thus thesis by SUBSET_1:def 7;
end;
registration
let L be non empty 1-sorted, R be Relation of the carrier of L;
cluster 1-element for strict_chain of R;
existence
proof
set C = the 1-element Subset of L;
reconsider C as strict_chain of R by Th1;
take C;
thus thesis;
end;
end;
theorem Th2:
for L being antisymmetric RelStr, R being auxiliary(i) (Relation
of L), C being strict_chain of R, x, y being Element of L st x in C & y in C &
x < y holds [x,y] in R
proof
let L be antisymmetric RelStr, R be auxiliary(i) (Relation of L), C be
strict_chain of R, x, y be Element of L;
assume that
A1: x in C and
A2: y in C and
A3: x < y;
[x,y] in R or [y,x] in R by A1,A2,A3,Def3;
then [x,y] in R or y <= x by WAYBEL_4:def 3;
hence thesis by A3,ORDERS_2:6;
end;
theorem
for L being antisymmetric RelStr, R being auxiliary(i) (Relation of L)
, x, y being Element of L st [x,y] in R & [y,x] in R holds x = y
proof
let L be antisymmetric RelStr, R be auxiliary(i) (Relation of L), x, y be
Element of L;
assume that
A1: [x,y] in R and
A2: [y,x] in R;
A3: y <= x by A2,WAYBEL_4:def 3;
x <= y by A1,WAYBEL_4:def 3;
hence thesis by A3,ORDERS_2:2;
end;
theorem
for L being non empty lower-bounded antisymmetric RelStr, x being
Element of L, R being auxiliary(iv) Relation of L holds {Bottom L, x} is
strict_chain of R
proof
let L be non empty lower-bounded antisymmetric RelStr, x be Element of L, R
be auxiliary(iv) Relation of L;
let a, y be set;
assume that
A1: a in {Bottom L, x} and
A2: y in {Bottom L, x};
A3: y = Bottom L or y = x by A2,TARSKI:def 2;
a = Bottom L or a = x by A1,TARSKI:def 2;
hence thesis by A3,WAYBEL_4:def 6;
end;
theorem Th5:
for L being non empty lower-bounded antisymmetric RelStr, R being
auxiliary(iv) (Relation of L), C being strict_chain of R holds C \/ {Bottom L}
is strict_chain of R
proof
let L be non empty lower-bounded antisymmetric RelStr, R be auxiliary(iv) (
Relation of L), C be strict_chain of R;
set A = C \/ {Bottom L};
let x, y be set;
assume that
A1: x in A and
A2: y in A;
reconsider x, y as Element of L by A1,A2;
per cases by A1,A2,Lm1;
suppose
x in C & y in C;
hence thesis by Def3;
end;
suppose
x in C & y = Bottom L;
hence thesis by WAYBEL_4:def 6;
end;
suppose
x = Bottom L & y in C;
hence thesis by WAYBEL_4:def 6;
end;
suppose
x = Bottom L & y = Bottom L;
hence thesis;
end;
end;
definition
let L be 1-sorted, R be (Relation of the carrier of L), C be strict_chain of
R;
attr C is maximal means
for D being strict_chain of R st C c= D holds C = D;
end;
definition
let L be 1-sorted, R be (Relation of the carrier of L), C be set;
defpred P[set] means $1 is strict_chain of R & C c= $1;
func Strict_Chains (R,C) -> set means
:Def5:
for x being set holds x in it iff x is strict_chain of R & C c= x;
existence
proof
consider X being set such that
A1: for x being set holds x in X iff x in bool the carrier of L & P[x]
from XFAMILY:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (
for x being set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;
end;
end;
registration
let L be 1-sorted, R be (Relation of the carrier of L), C be strict_chain of
R;
cluster Strict_Chains (R,C) -> non empty;
coherence by Def5;
end;
notation
let R be Relation, X be set;
synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R;
end;
:: Lemma 2.2, p. 203
theorem
for L being 1-sorted, R being (Relation of the carrier of L), C being
strict_chain of R holds Strict_Chains (R,C) is_inductive_wrt RelIncl
Strict_Chains (R,C) & ex D being set st D is_maximal_in RelIncl Strict_Chains (
R,C) & C c= D
proof
let L be 1-sorted, R be (Relation of the carrier of L), C be strict_chain of
R;
set X = Strict_Chains (R,C);
A1: field RelIncl X = X by WELLORD2:def 1;
thus
A2: X is_inductive_wrt RelIncl X
proof
let Y be set such that
A3: Y c= X and
A4: RelIncl X |_2 Y is being_linear-order;
per cases;
suppose
A5: Y is empty;
take C;
thus thesis by A5,Def5;
end;
suppose
A6: Y is non empty;
take Z = union Y;
Z c= the carrier of L
proof
let z be object;
assume z in Z;
then consider A being set such that
A7: z in A and
A8: A in Y by TARSKI:def 4;
A is strict_chain of R by A3,A8,Def5;
hence thesis by A7;
end;
then reconsider S = Z as Subset of L;
A9: S is strict_chain of R
proof
RelIncl X |_2 Y is connected by A4;
then
A10: RelIncl X |_2 Y is_connected_in field (RelIncl X |_2 Y) by
RELAT_2:def 14;
A11: (RelIncl X |_2 Y) = RelIncl Y by A3,WELLORD2:7;
let x, y be set;
A12: field RelIncl Y = Y by WELLORD2:def 1;
assume x in S;
then consider A being set such that
A13: x in A and
A14: A in Y by TARSKI:def 4;
A15: A is strict_chain of R by A3,A14,Def5;
assume y in S;
then consider B being set such that
A16: y in B and
A17: B in Y by TARSKI:def 4;
A18: B is strict_chain of R by A3,A17,Def5;
per cases;
suppose
A <> B;
then [A,B] in RelIncl Y or [B,A] in RelIncl Y by A14,A17,A10,A11,A12,
RELAT_2:def 6;
then A c= B or B c= A by A14,A17,WELLORD2:def 1;
hence thesis by A13,A16,A15,A18,Def3;
end;
suppose
A = B;
hence thesis by A13,A16,A15,Def3;
end;
end;
C c= Z
proof
let c be object;
assume
A19: c in C;
consider y being object such that
A20: y in Y by A6;
reconsider y as set by TARSKI:1;
C c= y by A3,A20,Def5;
hence thesis by A19,A20,TARSKI:def 4;
end;
hence
A21: Z in X by A9,Def5;
let y be set;
assume
A22: y in Y;
then y c= Z by ZFMISC_1:74;
hence thesis by A3,A21,A22,WELLORD2:def 1;
end;
end;
A23: RelIncl X is_transitive_in X by WELLORD2:20;
A24: RelIncl X is_antisymmetric_in X by WELLORD2:21;
RelIncl X is_reflexive_in X by WELLORD2:19;
then RelIncl X partially_orders X by A23,A24;
then consider D being set such that
A25: D is_maximal_in RelIncl X by A1,A2,ORDERS_1:63;
take D;
thus D is_maximal_in RelIncl X by A25;
D in field RelIncl X by A25;
hence thesis by A1,Def5;
end;
:: Lemma 2.3 (ii), p. 203
:: It is a trivial consequence of YELLOW_0:65
:: Maybe to cancel
theorem Th7:
for L being non empty transitive RelStr, C being non empty
Subset of L, X being Subset of C st ex_sup_of X,L & "\/"(X,L) in C holds
ex_sup_of X,subrelstr C & "\/"(X,L) = "\/"(X,subrelstr C)
proof
let L be non empty transitive RelStr, C be non empty Subset of L, X be
Subset of C such that
A1: ex_sup_of X,L and
A2: "\/"(X,L) in C;
the carrier of subrelstr C = C by YELLOW_0:def 15;
hence thesis by A1,A2,YELLOW_0:64;
end;
Lm2: for L being non empty Poset, R being auxiliary(i) auxiliary(ii) (Relation
of L), C being non empty strict_chain of R, X being Subset of C st ex_sup_of X,
L & C is maximal & not "\/"(X,L) in C ex cs being Element of L st cs in C &
"\/"(X,L) < cs & not ["\/"(X,L),cs] in R & ex cs1 being Element of subrelstr C
st cs = cs1 & X is_<=_than cs1 & for a being Element of subrelstr C st X
is_<=_than a holds cs1 <= a
proof
let L be non empty Poset, R be auxiliary(i) auxiliary(ii) (Relation of L), C
be non empty strict_chain of R, X be Subset of C such that
A1: ex_sup_of X,L and
A2: C is maximal;
set s = "\/"(X,L);
A3: C c= C \/ {s} by XBOOLE_1:7;
assume
A4: not s in C;
then not C \/ {s} c= C by ZFMISC_1:39;
then
A5: not C \/ {s} is strict_chain of R by A3,A2;
ex cs being Element of L st cs in C & s < cs & not [s,cs] in R
proof
A6: for a being Element of L st a in C & not [a,s] in R & not [s,a] in R
ex cs being Element of L st cs in C & s < cs & not [s,cs] in R
proof
let a be Element of L;
assume that
A7: a in C and
A8: not [a,s] in R and
A9: not [s,a] in R;
take a;
thus a in C by A7;
a is_>=_than X
proof
let x be Element of L;
assume
A10: x in X;
per cases by A7,A10,Def3;
suppose
A11: [a,x] in R;
A12: a <= a;
x <= s by A1,A10,YELLOW_4:1;
hence x <= a by A12,A8,A11,WAYBEL_4:def 4;
end;
suppose
[x,a] in R or a = x;
hence x <= a by WAYBEL_4:def 3;
end;
end;
then s <= a by A1,YELLOW_0:def 9;
hence s < a by A4,A7,ORDERS_2:def 6;
thus thesis by A9;
end;
consider a, b being set such that
A13: a in C \/ {s} and
A14: b in C \/ {s} and
A15: not [a,b] in R and
A16: a <> b and
A17: not [b,a] in R by A5,Def3;
reconsider a, b as Element of L by A13,A14;
per cases by A13,A14,Lm1;
suppose
a in C & b in C;
hence thesis by A15,A16,A17,Def3;
end;
suppose
a in C & b = s;
hence thesis by A15,A17,A6;
end;
suppose
a = s & b in C;
hence thesis by A15,A17,A6;
end;
suppose
a = s & b = s;
hence thesis by A16;
end;
end;
then consider cs being Element of L such that
A18: cs in C and
A19: s < cs and
A20: not [s,cs] in R;
take cs;
thus cs in C & s < cs & not [s,cs] in R by A18,A19,A20;
reconsider cs1 = cs as Element of subrelstr C by A18,YELLOW_0:def 15;
take cs1;
thus cs = cs1;
A21: s <= cs by A19,ORDERS_2:def 6;
thus X is_<=_than cs1
proof
let b be Element of subrelstr C;
reconsider b0 = b as Element of L by YELLOW_0:58;
assume b in X;
then b0 <= s by A1,YELLOW_4:1;
then b0 <= cs by A21,ORDERS_2:3;
hence b <= cs1 by YELLOW_0:60;
end;
let a be Element of subrelstr C;
reconsider a0 = a as Element of L by YELLOW_0:58;
A22: the carrier of subrelstr C = C by YELLOW_0:def 15;
assume X is_<=_than a;
then X is_<=_than a0 by A22,YELLOW_0:62;
then
A23: s <= a0 by A1,YELLOW_0:def 9;
A24: cs <= cs;
[cs1,a] in R or a = cs1 or [a,cs1] in R by A22,Def3;
then cs <= a0 by A20,A23,A24,WAYBEL_4:def 3,def 4;
hence thesis by YELLOW_0:60;
end;
:: Lemma 2.3, p. 203
theorem Th8:
for L being non empty Poset, R being auxiliary(i) auxiliary(ii)
(Relation of L), C being non empty strict_chain of R, X being Subset of C st
ex_sup_of X,L & C is maximal holds ex_sup_of X,subrelstr C
proof
let L be non empty Poset, R be auxiliary(i) auxiliary(ii) (Relation of L), C
be non empty strict_chain of R, X be Subset of C;
assume that
A1: ex_sup_of X,L and
A2: C is maximal;
set s = "\/"(X,L);
per cases;
suppose
s in C;
hence thesis by A1,Th7;
end;
suppose
not s in C;
then ex cs being Element of L st cs in C & s < cs & not [s,cs] in R & ex
cs1 being Element of subrelstr C st cs = cs1 & X is_<=_than cs1 & for a being
Element of subrelstr C st X is_<=_than a holds cs1 <= a by A1,A2,Lm2;
hence thesis by YELLOW_0:15;
end;
end;
:: Lemma 2.3 (i), (iii), p. 203
theorem
for L being non empty Poset, R being auxiliary(i) auxiliary(ii) (
Relation of L), C being non empty strict_chain of R, X being Subset of C st
ex_inf_of (uparrow "\/"(X,L)) /\ C,L & ex_sup_of X,L & C is maximal holds "\/"(
X,subrelstr C) = "/\"((uparrow "\/"(X,L)) /\ C,L) & (not "\/"(X,L) in C implies
"\/"(X,L) < "/\"((uparrow "\/"(X,L)) /\ C,L))
proof
let L be non empty Poset, R be auxiliary(i) auxiliary(ii) (Relation of L), C
be non empty strict_chain of R, X be Subset of C;
set s = "\/"(X,L), x = "\/"(X,subrelstr C), U = uparrow s;
assume that
A1: ex_inf_of U /\ C,L and
A2: ex_sup_of X,L and
A3: C is maximal;
A4: s <= s;
reconsider x1 = x as Element of L by YELLOW_0:58;
A5: the carrier of subrelstr C = C by YELLOW_0:def 15;
per cases;
suppose
A6: s in C;
then
A7: s = x by A2,A5,YELLOW_0:64;
A8: U /\ C is_>=_than x1
proof
let b be Element of L;
assume b in U /\ C;
then b in U by XBOOLE_0:def 4;
hence x1 <= b by A7,WAYBEL_0:18;
end;
for a being Element of L st U /\ C is_>=_than a holds a <= x1
proof
s in U by A4,WAYBEL_0:18;
then
A9: x1 in U /\ C by A6,A7,XBOOLE_0:def 4;
let a be Element of L;
assume U /\ C is_>=_than a;
hence thesis by A9;
end;
hence thesis by A1,A6,A8,YELLOW_0:def 10;
end;
suppose
not s in C;
then consider cs being Element of L such that
A10: cs in C and
A11: s < cs and
A12: not [s,cs] in R and
A13: ex cs1 being Element of subrelstr C st cs = cs1 & X is_<=_than
cs1 & for a being Element of subrelstr C st X is_<=_than a holds cs1 <= a by A2
,A3,Lm2;
A14: s <= cs by A11,ORDERS_2:def 6;
A15: for a being Element of L st U /\ C is_>=_than a holds a <= cs
proof
cs in U by A14,WAYBEL_0:18;
then
A16: cs in U /\ C by A10,XBOOLE_0:def 4;
let a be Element of L;
assume U /\ C is_>=_than a;
hence thesis by A16;
end;
A17: cs <= cs;
A18: U /\ C is_>=_than cs
proof
let b be Element of L;
assume
A19: b in U /\ C;
then b in U by XBOOLE_0:def 4;
then
A20: s <= b by WAYBEL_0:18;
b in C by A19,XBOOLE_0:def 4;
then [b,cs] in R or b = cs or [cs,b] in R by A10,Def3;
hence cs <= b by A12,A17,A20,WAYBEL_4:def 3,def 4;
end;
ex_sup_of X,subrelstr C by A2,A3,Th8;
then cs = x by A13,YELLOW_0:def 9;
hence thesis by A15,A1,A11,A18,YELLOW_0:def 10;
end;
end;
:: Proposition 2.4, p. 204
theorem
for L being complete non empty Poset, R being auxiliary(i)
auxiliary(ii) (Relation of L), C being non empty strict_chain of R st C is
maximal holds subrelstr C is complete
proof
let L be complete non empty Poset, R be auxiliary(i) auxiliary(ii) (Relation
of L), C be non empty strict_chain of R;
assume
A1: C is maximal;
for X being Subset of subrelstr C holds ex_sup_of X,subrelstr C
proof
let X be Subset of subrelstr C;
X is Subset of C by YELLOW_0:def 15;
hence thesis by A1,Th8,YELLOW_0:17;
end;
hence thesis by YELLOW_0:53;
end;
:: Proposition 2.5 (i), p. 204
theorem
for L being non empty lower-bounded antisymmetric RelStr, R being
auxiliary(iv) (Relation of L), C being strict_chain of R st C is maximal holds
Bottom L in C
proof
let L be non empty lower-bounded antisymmetric RelStr, R be auxiliary(iv) (
Relation of L), C be strict_chain of R such that
A1: for D being strict_chain of R st C c= D holds C = D;
C \/ {Bottom L} is strict_chain of R by Th5;
then
A2: C \/ {Bottom L} = C by A1,XBOOLE_1:7;
assume not Bottom L in C;
then not Bottom L in {Bottom L} by A2,XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
:: Proposition 2.5 (ii), p. 204
theorem
for L being non empty upper-bounded Poset, R being auxiliary(ii) (
Relation of L), C being strict_chain of R, m being Element of L st C is maximal
& m is_maximum_of C & [m,Top L] in R holds [Top L,Top L] in R & m = Top L
proof
let L be non empty upper-bounded Poset, R be auxiliary(ii) (Relation of L),
C be strict_chain of R, m be Element of L such that
A1: C is maximal and
A2: m is_maximum_of C and
A3: [m,Top L] in R;
A4: C c= C \/ {Top L} by XBOOLE_1:7;
now
A5: m <= Top L by YELLOW_0:45;
assume
A6: m <> Top L;
A7: {Top L} c= C \/ {Top L} by XBOOLE_1:7;
A8: ex_sup_of C,L by A2;
A9: sup C = m by A2;
C \/ {Top L} is strict_chain of R
proof
let a, b be set;
assume that
A10: a in C \/ {Top L} and
A11: b in C \/ {Top L};
A12: Top L <= Top L;
per cases by A10,A11,Lm1;
suppose
a in C & b in C;
hence thesis by Def3;
end;
suppose that
A13: a = Top L and
A14: b in C;
reconsider b as Element of L by A14;
b <= sup C by A8,A14,YELLOW_4:1;
hence thesis by A3,A9,A12,A13,WAYBEL_4:def 4;
end;
suppose that
A15: a in C and
A16: b = Top L;
reconsider a as Element of L by A15;
a <= sup C by A8,A15,YELLOW_4:1;
hence thesis by A3,A9,A12,A16,WAYBEL_4:def 4;
end;
suppose
a = Top L & b = Top L;
hence thesis;
end;
end;
then
A17: C \/ {Top L} = C by A1,A4;
Top L in {Top L} by TARSKI:def 1;
then Top L <= sup C by A7,A8,A17,YELLOW_4:1;
hence contradiction by A6,A5,A9,ORDERS_2:2;
end;
hence thesis by A3;
end;
:: Definition (SI_C) p. 204
definition
let L be RelStr, C be set, R be Relation of the carrier of L;
pred R satisfies_SIC_on C means
for x, z being Element of L holds x
in C & z in C & [x,z] in R & x <> z implies ex y being Element of L st y in C &
[x,y] in R & [y,z] in R & x <> y;
end;
definition
let L be RelStr, R be (Relation of the carrier of L), C be strict_chain of R;
attr C is satisfying_SIC means
:Def7:
R satisfies_SIC_on C;
end;
theorem Th13:
for L being RelStr, C being set, R being auxiliary(i) (Relation
of L) st R satisfies_SIC_on C holds for x, z being Element of L holds x in C &
z in C & [x,z] in R & x <> z implies ex y being Element of L st y in C & [x,y]
in R & [y,z] in R & x < y
proof
let L be RelStr, C be set, R be auxiliary(i) Relation of L such that
A1: R satisfies_SIC_on C;
let x, z be Element of L;
assume that
A2: x in C and
A3: z in C and
A4: [x,z] in R and
A5: x <> z;
consider y being Element of L such that
A6: y in C and
A7: [x,y] in R and
A8: [y,z] in R and
A9: x <> y by A2,A3,A4,A5,A1;
take y;
thus y in C & [x,y] in R & [y,z] in R by A6,A7,A8;
x <= y by A7,WAYBEL_4:def 3;
hence thesis by A9,ORDERS_2:def 6;
end;
registration
let L be RelStr, R be Relation of the carrier of L;
cluster trivial -> satisfying_SIC for strict_chain of R;
coherence
proof
let C be strict_chain of R;
assume
A1: C is trivial;
let x, z be Element of L;
assume that
A2: x in C and
A3: z in C and
[x,z] in R and
A4: x <> z;
thus thesis by A2,A3,A4,A1,SUBSET_1:def 7;
end;
end;
registration
let L be non empty RelStr, R be Relation of the carrier of L;
cluster 1-element for strict_chain of R;
existence
proof
set C = the 1-element Subset of L;
reconsider C as strict_chain of R by Th1;
take C;
thus thesis;
end;
end;
:: Proposition 2.5 (iii), p. 204
theorem
for L being lower-bounded with_suprema Poset, R being auxiliary(i)
auxiliary(ii) (Relation of L), C being strict_chain of R st C is maximal & R is
satisfying_SI holds R satisfies_SIC_on C
proof
let L be lower-bounded with_suprema Poset, R be auxiliary(i) auxiliary(ii) (
Relation of L), C be strict_chain of R such that
A1: C is maximal and
A2: R is satisfying_SI;
let x, z be Element of L;
assume that
A3: x in C and
A4: z in C and
A5: [x,z] in R and
A6: x <> z;
consider y being Element of L such that
A7: [x,y] in R and
A8: [y,z] in R and
A9: x <> y by A2,A5,A6,WAYBEL_4:def 20;
A10: y <= z by A8,WAYBEL_4:def 3;
assume
A11: not thesis;
A12: x <= y by A7,WAYBEL_4:def 3;
A13: C \/ {y} is strict_chain of R
proof
let a, b be set such that
A14: a in C \/ {y} and
A15: b in C \/ {y};
per cases by A14,A15,Lm1;
suppose
a in C & b in C;
hence thesis by Def3;
end;
suppose that
A16: a in C and
A17: b = y;
now
reconsider a as Element of L by A16;
A18: a <= a;
per cases by A11,A16;
suppose
x = a;
hence thesis by A7,A17;
end;
suppose
a = z;
hence thesis by A8,A17;
end;
suppose
not [x,a] in R & a <> x;
then [a,x] in R by A3,A16,Def3;
hence thesis by A12,A17,A18,WAYBEL_4:def 4;
end;
suppose
not [a,z] in R & a <> z;
then [z,a] in R by A4,A16,Def3;
hence thesis by A10,A17,A18,WAYBEL_4:def 4;
end;
end;
hence thesis;
end;
suppose that
A19: a = y and
A20: b in C;
now
reconsider b as Element of L by A20;
A21: b <= b;
per cases by A11,A20;
suppose
x = b;
hence thesis by A7,A19;
end;
suppose
b = z;
hence thesis by A8,A19;
end;
suppose
not [x,b] in R & b <> x;
then [b,x] in R by A3,A20,Def3;
hence thesis by A12,A19,A21,WAYBEL_4:def 4;
end;
suppose
not [b,z] in R & b <> z;
then [z,b] in R by A4,A20,Def3;
hence thesis by A10,A19,A21,WAYBEL_4:def 4;
end;
end;
hence thesis;
end;
suppose
a = y & b = y;
hence thesis;
end;
end;
C c= C \/ {y} by XBOOLE_1:7;
then C \/ {y} = C by A13,A1;
then y in C by ZFMISC_1:39;
hence thesis by A11,A7,A8,A9;
end;
definition
let R be Relation, C be set, y be object;
func SetBelow (R,C,y) -> set equals
( R"{y} ) /\ C;
coherence;
end;
theorem Th15:
for R being Relation, C, x, y being set holds x in SetBelow (R,C
,y) iff [x,y] in R & x in C
proof
let R be Relation, C, x, y be set;
hereby
assume
A1: x in SetBelow (R,C,y);
then x in R"{y} by XBOOLE_0:def 4;
then ex a being object st [x,a] in R & a in {y} by RELAT_1:def 14;
hence [x,y] in R by TARSKI:def 1;
thus x in C by A1,XBOOLE_0:def 4;
end;
assume that
A2: [x,y] in R and
A3: x in C;
y in {y} by TARSKI:def 1;
then x in R"{y} by A2,RELAT_1:def 14;
hence thesis by A3,XBOOLE_0:def 4;
end;
definition
let L be 1-sorted, R be (Relation of the carrier of L),
C be set, y be object;
redefine func SetBelow (R,C,y) -> Subset of L; :: redefines SetBelow (WAYBEL35, definition)
coherence
proof
( R"{y} ) /\ C c= the carrier of L;
hence thesis;
end;
end;
theorem Th16:
for L being RelStr, R being auxiliary(i) (Relation of L), C
being set, y being Element of L holds SetBelow (R,C,y) is_<=_than y
proof
let L be RelStr, R be auxiliary(i) (Relation of L), C be set, y be Element
of L;
let b be Element of L;
assume b in SetBelow (R,C,y);
then [b,y] in R by Th15;
hence thesis by WAYBEL_4:def 3;
end;
theorem Th17:
for L being reflexive transitive RelStr, R being auxiliary(ii) (
Relation of L), C being Subset of L, x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y)
proof
let L be reflexive transitive RelStr, R be auxiliary(ii) (Relation of L), C
be Subset of L, x, y be Element of L such that
A1: x <= y;
let a be object;
assume
A2: a in SetBelow (R,C,x);
then reconsider L as non empty reflexive RelStr;
reconsider a as Element of L by A2;
A3: a in C by A2,Th15;
A4: a <= a;
[a,x] in R by A2,Th15;
then [a,y] in R by A4,A1,WAYBEL_4:def 4;
hence thesis by A3,Th15;
end;
theorem Th18:
for L being RelStr, R being auxiliary(i) (Relation of L), C
being set, x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,
C,x),L holds x = sup SetBelow (R,C,x)
proof
let L be RelStr, R be auxiliary(i) (Relation of L), C be set, x be Element
of L;
assume that
A1: x in C and
A2: [x,x] in R and
A3: ex_sup_of SetBelow (R,C,x),L;
A4: for a being Element of L st SetBelow (R,C,x) is_<=_than a holds x <= a
by A1,A2,Th15;
SetBelow (R,C,x) is_<=_than x by Th16;
hence thesis by A4,A3,YELLOW_0:def 9;
end;
definition
let L be RelStr, C be Subset of L;
attr C is sup-closed means
for X being Subset of C st ex_sup_of X,L
holds "\/"(X,L) = "\/"(X,subrelstr C);
end;
:: Lemma 2.6, p. 205
theorem Th19:
for L being complete non empty Poset, R being extra-order (
Relation of L), C being satisfying_SIC strict_chain of R, p, q being Element of
L st p in C & q in C & p < q ex y being Element of L st p < y & [y,q] in R & y
= sup SetBelow (R,C,y)
proof
let L be complete non empty Poset, R be extra-order (Relation of L), C be
satisfying_SIC strict_chain of R, p, q be Element of L such that
A1: p in C and
A2: q in C and
A3: p < q;
A4: R satisfies_SIC_on C by Def7;
not q <= p by A3,ORDERS_2:6;
then not [q,p] in R by WAYBEL_4:def 3;
then [p,q] in R by A1,A2,A3,Def3;
then consider w being Element of L such that
A5: w in C and
A6: [p,w] in R and
A7: [w,q] in R and
A8: p < w by A1,A2,A3,A4,Th13;
consider x1 being Element of L such that
A9: x1 in C and
[p,x1] in R and
A10: [x1,w] in R and
A11: p < x1 by A1,A4,A5,A6,A8,Th13;
defpred P[set,set,set] means ex b being Element of L st $3 = b &
$3 in C & [$2,$3] in R & b <= w;
A12: q <= q;
reconsider D = SetBelow(R,C,w) as non empty set by A9,A10,Th15;
reconsider g = x1 as Element of D by A9,A10,Th15;
A13: for n being Nat, x being Element of D ex y being Element of
D st P[n,x,y]
proof
let n be Nat;
let x be Element of D;
x in D;
then reconsider t = x as Element of L;
A14: x in C by Th15;
A15: [x,w] in R by Th15;
per cases;
suppose
x <> w;
then consider b being Element of L such that
A16: b in C and
A17: [x,b] in R and
A18: [b,w] in R and
t < b by A4,A5,A14,A15,Th13;
reconsider y = b as Element of D by A16,A18,Th15;
take y, b;
thus thesis by A16,A17,A18,WAYBEL_4:def 3;
end;
suppose
A19: x = w;
take x, t;
thus thesis by A19,Th15;
end;
end;
consider f being sequence of D such that
A20: f.0 = g and
A21: for n being Nat holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A13);
reconsider f as sequence of the carrier of L by FUNCT_2:7;
take y = sup rng f;
A22: ex_sup_of rng f,L by YELLOW_0:17;
A23: dom f = NAT by FUNCT_2:def 1;
then x1 <= y by A20,A22,FUNCT_1:3,YELLOW_4:1;
hence p < y by A11,ORDERS_2:7;
rng f is_<=_than w
proof
let x be Element of L;
assume x in rng f;
then consider n being object such that
A24: n in dom f and
A25: f.n = x by FUNCT_1:def 3;
reconsider n as Element of NAT by A24;
A26: ex b being Element of L st f.(n+1) = b & f.(n+1) in C &
[f.n,f.(n+1)] in R & b <= w by A21;
then x <= f.In(n+1,NAT) by A25,WAYBEL_4:def 3;
hence x <= w by A26,ORDERS_2:3;
end;
then y <= w by A22,YELLOW_0:def 9;
hence [y,q] in R by A7,A12,WAYBEL_4:def 4;
A27: ex_sup_of SetBelow (R,C,y),L by YELLOW_0:17;
A28: for x being Element of L st SetBelow (R,C,y) is_<=_than x holds y <= x
proof
let x be Element of L such that
A29: SetBelow (R,C,y) is_<=_than x;
rng f is_<=_than x
proof
defpred P[Nat] means f.$1 in C;
let m be Element of L;
assume m in rng f;
then consider n being object such that
A30: n in dom f and
A31: f.n = m by FUNCT_1:def 3;
reconsider n as Element of NAT by A30;
A32: f.n <= f.n;
A33: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
ex b being Element of L st f.(k+1) = b & f.(k+1) in
C & [f.k,f.(k+1)] in R & b <= w by A21;
hence thesis;
end;
A34: P[0] by A9,A20;
for n being Nat holds P[n] from NAT_1:sch 2(A34,A33);
then
A35: f.n in C;
A36: ex b being Element of L st f.(n+1) = b & f.(n+1) in C
& [f.n,f.(n+1)] in R & b <= w by A21;
f.In(n+1,NAT) <= y by A22,A23,FUNCT_1:3,YELLOW_4:1;
then [m,y] in R by A31,A36,A32,WAYBEL_4:def 4;
then m in SetBelow (R,C,y) by A31,A35,Th15;
hence m <= x by A29;
end;
hence thesis by A22,YELLOW_0:def 9;
end;
SetBelow (R,C,y) is_<=_than y by Th16;
hence thesis by A28,A27,YELLOW_0:def 9;
end;
:: Lemma 2.7, p. 205, 1 => 2
theorem
for L being lower-bounded non empty Poset, R being extra-order (
Relation of L), C being non empty strict_chain of R st C is sup-closed & (for c
being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L) & R
satisfies_SIC_on C holds for c being Element of L st c in C holds c = sup
SetBelow (R,C,c)
proof
let L be lower-bounded non empty Poset, R be extra-order (Relation of L), C
be non empty strict_chain of R;
assume that
A1: C is sup-closed and
A2: for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c), L;
assume
A3: R satisfies_SIC_on C;
let c be Element of L such that
A4: c in C;
A5: ex_sup_of SetBelow (R,C,c),L by A2,A4;
set d = sup SetBelow (R,C,c);
SetBelow (R,C,c) c= C by XBOOLE_1:17;
then d = "\/"(SetBelow (R,C,c),subrelstr C) by A1,A5;
then d in the carrier of subrelstr C;
then
A6: d in C by YELLOW_0:def 15;
per cases;
suppose
c = d;
hence thesis;
end;
suppose
A7: c <> d;
A8: now
assume
A9: c < d;
A10: for a being Element of L st SetBelow (R,C,c) is_<=_than a holds c <= a
proof
let a be Element of L;
assume SetBelow (R,C,c) is_<=_than a;
then
A11: d <= a by A5,YELLOW_0:def 9;
c <= d by A9,ORDERS_2:def 6;
hence thesis by A11,ORDERS_2:3;
end;
SetBelow (R,C,c) is_<=_than c by Th16;
hence thesis by A10,A5,YELLOW_0:def 9;
end;
[c,d] in R or [d,c] in R by A7,A4,A6,Def3;
then c <= d or [d,c] in R by WAYBEL_4:def 3;
then consider y being Element of L such that
A12: y in C and
[d,y] in R and
A13: [y,c] in R and
A14: d < y by A8,A3,A4,A6,A7,Th13,ORDERS_2:def 6;
y in SetBelow (R,C,c) by A12,A13,Th15;
hence thesis by A5,A14,ORDERS_2:6,YELLOW_4:1;
end;
end;
:: Lemma 2.7, p. 205, 2 => 1
theorem
for L being non empty reflexive antisymmetric RelStr, R being
auxiliary(i) (Relation of L), C being strict_chain of R st (for c being Element
of L st c in C holds ex_sup_of SetBelow (R,C,c),L & c = sup SetBelow (R,C,c))
holds R satisfies_SIC_on C
proof
let L be non empty reflexive antisymmetric RelStr, R be auxiliary(i) (
Relation of L), C be strict_chain of R;
assume
A1: for c being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),
L & c = sup SetBelow (R,C,c);
let x, z be Element of L;
assume that
A2: x in C and
A3: z in C and
A4: [x,z] in R and
A5: x <> z;
A6: z = sup SetBelow (R,C,z) by A1,A3;
per cases;
suppose
A7: not ex y being Element of L st y in SetBelow (R,C,z) & x < y;
reconsider x as Element of L;
A8: SetBelow (R,C,z) is_<=_than x
proof
let b be Element of L;
assume
A9: b in SetBelow (R,C,z);
then
A10: not x < b by A7;
per cases;
suppose
A11: x <> b;
b in C by A9,Th15;
then
A12: [x,b] in R or x = b or [b,x] in R by A2,Def3;
not x <= b by A11,A10,ORDERS_2:def 6;
hence b <= x by A12,WAYBEL_4:def 3;
end;
suppose
x = b;
hence b <= x;
end;
end;
A13: for a being Element of L st SetBelow (R,C,z) is_<=_than a holds x <= a
by A2,A4,Th15;
ex_sup_of SetBelow (R,C,z),L by A1,A3;
hence thesis by A13,A5,A6,A8,YELLOW_0:def 9;
end;
suppose
ex y being Element of L st y in SetBelow (R,C,z) & x < y;
then consider y being Element of L such that
A14: y in SetBelow (R,C,z) and
A15: x < y;
take y;
thus y in C by A14,Th15;
hence [x,y] in R by A2,A15,Th2;
thus [y,z] in R by A14,Th15;
thus thesis by A15;
end;
end;
definition
let L be non empty RelStr, R be (Relation of the carrier of L), C be set;
defpred P[set] means $1 = sup SetBelow (R,C,$1);
func SupBelow (R,C) -> set means
:Def10:
for y being set holds y in it iff y = sup SetBelow (R,C,y);
existence
proof
consider X being set such that
A1: for x being set holds x in X iff x in the carrier of L & P[x] from
XFAMILY:sch 1;
take X;
thus thesis by A1;
end;
uniqueness
proof
thus for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (
for x being set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;
end;
end;
definition
let L be non empty RelStr, R be (Relation of the carrier of L), C be set;
redefine func SupBelow (R,C) -> Subset of L; :: redefines SupBelow (WAYBEL35, definition)
coherence
proof
SupBelow (R,C) c= the carrier of L
proof
let x be object;
assume x in SupBelow (R,C);
then x = sup SetBelow (R,C,x) by Def10;
hence thesis;
end;
hence thesis;
end;
end;
:: Lemma 2.8, (i) a), p. 205
theorem Th22:
for L being non empty reflexive transitive RelStr, R being
auxiliary(i) auxiliary(ii) (Relation of L), C being strict_chain of R st (for c
being Element of L holds ex_sup_of SetBelow (R,C,c),L) holds SupBelow (R,C) is
strict_chain of R
proof
let L be non empty reflexive transitive RelStr, R be auxiliary(i)
auxiliary(ii) (Relation of L), C be strict_chain of R;
assume
A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L;
thus SupBelow (R,C) is strict_chain of R
proof
let a, b be set;
assume
A2: a in SupBelow (R,C);
then
A3: a = sup SetBelow (R,C,a) by Def10;
reconsider a as Element of L by A2;
A4: a <= a;
A5: ex_sup_of SetBelow (R,C,a),L by A1;
assume
A6: b in SupBelow (R,C);
then
A7: b = sup SetBelow (R,C,b) by Def10;
reconsider b as Element of L by A6;
A8: b <= b;
A9: ex_sup_of SetBelow (R,C,b),L by A1;
per cases;
suppose
a = b;
hence thesis;
end;
suppose
A10: a <> b;
(for x being Element of L st x in C holds [x,a] in R iff [x,b] in R
) implies a = b
proof
assume
A11: for x being Element of L st x in C holds [x,a] in R iff [x,b] in R;
SetBelow (R,C,a) = SetBelow (R,C,b)
proof
thus SetBelow (R,C,a) c= SetBelow (R,C,b)
proof
let x be object;
assume
A12: x in SetBelow (R,C,a);
then reconsider x as Element of L;
A13: x in C by A12,Th15;
[x,a] in R by A12,Th15;
then [x,b] in R by A13,A11;
hence thesis by A13,Th15;
end;
let x be object;
assume
A14: x in SetBelow (R,C,b);
then reconsider x as Element of L;
A15: x in C by A14,Th15;
[x,b] in R by A14,Th15;
then [x,a] in R by A15,A11;
hence thesis by A15,Th15;
end;
hence thesis by A2,A7,Def10;
end;
then consider x being Element of L such that
A16: x in C and
A17: [x,a] in R & not [x,b] in R or not [x,a] in R & [x,b] in R by A10;
A18: x <= x;
thus thesis
proof
per cases by A17;
suppose that
A19: [x,a] in R and
A20: not [x,b] in R;
SetBelow (R,C,b) is_<=_than x
proof
let y be Element of L;
assume
A21: y in SetBelow (R,C,b);
then [y,b] in R by Th15;
then
A22: y <= b by WAYBEL_4:def 3;
y in C by A21,Th15;
then [y,x] in R or x = y or [x,y] in R by A16,Def3;
hence y <= x by A18,A20,A22,WAYBEL_4:def 3,def 4;
end;
then b <= x by A7,A9,YELLOW_0:def 9;
hence thesis by A4,A19,WAYBEL_4:def 4;
end;
suppose that
A23: not [x,a] in R and
A24: [x,b] in R;
SetBelow (R,C,a) is_<=_than x
proof
let y be Element of L;
assume
A25: y in SetBelow (R,C,a);
then [y,a] in R by Th15;
then
A26: y <= a by WAYBEL_4:def 3;
y in C by A25,Th15;
then [y,x] in R or x = y or [x,y] in R by A16,Def3;
hence y <= x by A18,A23,A26,WAYBEL_4:def 3,def 4;
end;
then a <= x by A3,A5,YELLOW_0:def 9;
hence thesis by A8,A24,WAYBEL_4:def 4;
end;
end;
end;
end;
end;
:: Lemma 2.8, (i) b), p. 205
theorem
for L being non empty Poset, R being auxiliary(i) auxiliary(ii) (
Relation of L), C being Subset of L st (for c being Element of L holds
ex_sup_of SetBelow (R,C,c),L) holds SupBelow (R,C) is sup-closed
proof
let L be non empty Poset, R be auxiliary(i) auxiliary(ii) (Relation of L), C
be Subset of L;
assume
A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L;
let X be Subset of SupBelow (R,C);
set s = "\/"(X,L);
assume
A2: ex_sup_of X,L;
A3: ex_sup_of SetBelow (R,C,s),L by A1;
X is_<=_than sup SetBelow (R,C,s)
proof
let x be Element of L;
A4: ex_sup_of SetBelow (R,C,x),L by A1;
assume
A5: x in X;
then
A6: x = sup SetBelow (R,C,x) by Def10;
SetBelow (R,C,x) c= SetBelow (R,C,s) by A2,A5,Th17,YELLOW_4:1;
hence x <= sup SetBelow (R,C,s) by A3,A6,A4,YELLOW_0:34;
end;
then
A7: s <= sup SetBelow (R,C,s) by A2,YELLOW_0:def 9;
A8: the carrier of subrelstr SupBelow (R,C) = SupBelow (R,C) by YELLOW_0:def 15
;
SetBelow (R,C,s) is_<=_than s by Th16;
then sup SetBelow (R,C,s) <= s by A3,YELLOW_0:def 9;
then s = sup SetBelow (R,C,s) by A7,ORDERS_2:2;
then s in SupBelow (R,C) by Def10;
hence thesis by A8,A2,YELLOW_0:64;
end;
theorem Th24:
for L being complete non empty Poset, R being extra-order (
Relation of L), C being satisfying_SIC strict_chain of R, d being Element of L
st d in SupBelow (R,C) holds d = "\/"({b where b is Element of L: b in SupBelow
(R,C) & [b,d] in R},L)
proof
let L be complete non empty Poset, R be extra-order (Relation of L), C be
satisfying_SIC strict_chain of R, d be Element of L;
deffunc F(Element of L) = {b where b is Element of L: b in SupBelow(R,C) & [
b,$1] in R};
set p = "\/"(F(d),L);
A1: ex_sup_of SetBelow (R,C,d),L by YELLOW_0:17;
A2: F(d) is_<=_than d
proof
let a be Element of L;
assume a in F(d);
then ex b being Element of L st a = b & b in SupBelow(R,C) & [b,d] in R;
hence a <= d by WAYBEL_4:def 3;
end;
assume d in SupBelow (R,C);
then
A3: d = sup SetBelow(R,C,d) by Def10;
assume
A4: p <> d;
ex_sup_of F(d),L by YELLOW_0:17;
then p <= d by A2,YELLOW_0:def 9;
then
A5: p < d by A4,ORDERS_2:def 6;
now
per cases by A3,A1,A4,YELLOW_0:def 9;
suppose
not SetBelow(R,C,d) is_<=_than p;
then consider a being Element of L such that
A6: a in SetBelow(R,C,d) and
A7: not a <= p;
A8: [a,d] in R by A6,Th15;
a in C by A6,Th15;
hence ex a being Element of L st a in C & [a,d] in R & not a <= p by A8
,A7;
end;
suppose
ex a being Element of L st SetBelow(R,C,d) is_<=_than a & not p <= a;
then consider a being Element of L such that
A9: SetBelow(R,C,d) is_<=_than a and
A10: not p <= a;
d <= a by A3,A1,A9,YELLOW_0:def 9;
then p < a by A5,ORDERS_2:7;
hence ex a being Element of L st a in C & [a,d] in R & not a <= p by A10,
ORDERS_2:def 6;
end;
end;
then consider cc being Element of L such that
A11: cc in C and
A12: [cc,d] in R and
A13: not cc <= p;
per cases;
suppose
[cc,cc] in R;
then cc = sup SetBelow (R,C,cc) by A11,Th18,YELLOW_0:17;
then cc in SupBelow (R,C) by Def10;
then cc in F(d) by A12;
hence contradiction by A13,YELLOW_0:17,YELLOW_4:1;
end;
suppose
A14: not [cc,cc] in R;
ex cs being Element of L st cs in C & cc < cs & [cs,d] in R
proof
per cases by A3,A1,A12,A14,YELLOW_0:def 9;
suppose
not SetBelow(R,C,d) is_<=_than cc;
then consider cs being Element of L such that
A15: cs in SetBelow(R,C,d) and
A16: not cs <= cc;
take cs;
A17: not [cs,cc] in R by A16,WAYBEL_4:def 3;
thus cs in C by A15,Th15;
then [cc,cs] in R by A17,A11,A16,Def3;
then cc <= cs by WAYBEL_4:def 3;
hence cc < cs by A16,ORDERS_2:def 6;
thus thesis by A15,Th15;
end;
suppose
A18: ex a being Element of L st SetBelow(R,C,d) is_<=_than a & not cc <= a;
cc in SetBelow(R,C,d) by A11,A12,Th15;
hence thesis by A18;
end;
end;
then consider cs being Element of L such that
A19: cs in C and
A20: cc < cs and
A21: [cs,d] in R;
consider y being Element of L such that
A22: cc < y and
A23: [y,cs] in R and
A24: y = sup SetBelow (R,C,y) by A11,A19,A20,Th19;
A25: y in SupBelow (R,C) by A24,Def10;
A26: d <= d;
y <= cs by A23,WAYBEL_4:def 3;
then [y,d] in R by A21,A26,WAYBEL_4:def 4;
then y in F(d) by A25;
then y <= p by YELLOW_0:17,YELLOW_4:1;
then cc < p by A22,ORDERS_2:7;
hence contradiction by A13,ORDERS_2:def 6;
end;
end;
:: Lemma 2.8, (ii), p. 205
theorem
for L being complete non empty Poset, R being extra-order (Relation of
L), C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow
(R,C)
proof
let L be complete non empty Poset, R be extra-order (Relation of L), C be
satisfying_SIC strict_chain of R;
let c, d be Element of L;
assume that
A1: c in SupBelow (R,C) and
A2: d in SupBelow (R,C) and
A3: [c,d] in R and
A4: c <> d;
A5: c <= d by A3,WAYBEL_4:def 3;
deffunc F(Element of L) = {b where b is Element of L: b in SupBelow(R,C) & [
b,$1] in R};
A6: d = "\/"(F(d),L) by A2,Th24;
A7: ex_sup_of F(d),L by YELLOW_0:17;
per cases by A4,A6,A7,YELLOW_0:def 9;
suppose
not F(d) is_<=_than c;
then consider g being Element of L such that
A8: g in F(d) and
A9: not g <= c;
consider y being Element of L such that
A10: g = y and
A11: y in SupBelow(R,C) and
A12: [y,d] in R by A8;
reconsider y as Element of L;
take y;
thus y in SupBelow(R,C) by A11;
for c being Element of L holds ex_sup_of SetBelow (R,C,c),L by YELLOW_0:17;
then SupBelow (R,C) is strict_chain of R by Th22;
then [c,y] in R or c = y or [y,c] in R by A1,A11,Def3;
hence [c,y] in R by A9,A10,WAYBEL_4:def 3;
thus [y,d] in R by A12;
thus thesis by A9,A10;
end;
suppose
ex g being Element of L st F(d) is_<=_than g & not c <= g;
then consider g being Element of L such that
A13: F(d) is_<=_than g and
A14: not c <= g;
d <= g by A6,A7,A13,YELLOW_0:def 9;
hence thesis by A5,A14,ORDERS_2:3;
end;
end;
:: Lemma 2.8, (iii), p. 205
theorem
for L being complete non empty Poset, R being extra-order (Relation of
L), C being satisfying_SIC strict_chain of R, a, b being Element of L st a in C
& b in C & a < b ex d being Element of L st d in SupBelow (R,C) & a < d & [d,b]
in R
proof
let L be complete non empty Poset, R be extra-order (Relation of L), C be
satisfying_SIC strict_chain of R, a, b be Element of L;
assume that
A1: a in C and
A2: b in C and
A3: a < b;
consider d being Element of L such that
A4: a < d and
A5: [d,b] in R and
A6: d = sup SetBelow (R,C,d) by A1,A2,A3,Th19;
take d;
thus thesis by A4,A5,A6,Def10;
end;