:: WAYBEL35 semantic presentation
begin
Lm1: for x, y, X being set holds
( not y in {x} \/ X or y = x or y in X )
proof
let x, y, X be set ; ::_thesis: ( not y in {x} \/ X or y = x or y in X )
assume y in {x} \/ X ; ::_thesis: ( y = x or y in X )
then ( y in {x} or y in X ) by XBOOLE_0:def_3;
hence ( y = x or y in X ) by TARSKI:def_1; ::_thesis: verum
end;
begin
registration
let L be RelStr ;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being Relation of L st b1 is auxiliary(i)
proof
take IntRel L ; ::_thesis: IntRel L is auxiliary(i)
thus IntRel L is auxiliary(i) ; ::_thesis: verum
end;
end;
registration
let L be transitive RelStr ;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(i) auxiliary(ii) for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being Relation of L st
( b1 is auxiliary(i) & b1 is auxiliary(ii) )
proof
take IntRel L ; ::_thesis: ( IntRel L is auxiliary(i) & IntRel L is auxiliary(ii) )
thus ( IntRel L is auxiliary(i) & IntRel L is auxiliary(ii) ) ; ::_thesis: verum
end;
end;
registration
let L be antisymmetric with_suprema RelStr ;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iii) for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being Relation of L st b1 is auxiliary(iii)
proof
take IntRel L ; ::_thesis: IntRel L is auxiliary(iii)
thus IntRel L is auxiliary(iii) ; ::_thesis: verum
end;
end;
registration
let L be non empty antisymmetric lower-bounded RelStr ;
cluster Relation-like the carrier of L -defined the carrier of L -valued auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being Relation of L st b1 is auxiliary(iv)
proof
take IntRel L ; ::_thesis: IntRel L is auxiliary(iv)
thus IntRel L is auxiliary(iv) ; ::_thesis: verum
end;
end;
definition
let L be non empty RelStr ;
let R be Relation of L;
attrR is extra-order means :Def1: :: WAYBEL35:def 1
( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) );
end;
:: deftheorem Def1 defines extra-order WAYBEL35:def_1_:_
for L being non empty RelStr
for R being Relation of L holds
( R is extra-order iff ( R is auxiliary(i) & R is auxiliary(ii) & R is auxiliary(iv) ) );
registration
let L be non empty RelStr ;
cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) for Element of bool [: the carrier of L, the carrier of L:];
coherence
for b1 being Relation of L st b1 is extra-order holds
( b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) ) by Def1;
cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order for Element of bool [: the carrier of L, the carrier of L:];
coherence
for b1 being Relation of L st b1 is auxiliary(i) & b1 is auxiliary(ii) & b1 is auxiliary(iv) holds
b1 is extra-order by Def1;
end;
registration
let L be non empty RelStr ;
cluster auxiliary(iii) extra-order -> auxiliary for Element of bool [: the carrier of L, the carrier of L:];
coherence
for b1 being Relation of L st b1 is extra-order & b1 is auxiliary(iii) holds
b1 is auxiliary ;
cluster auxiliary -> extra-order for Element of bool [: the carrier of L, the carrier of L:];
coherence
for b1 being Relation of L st b1 is auxiliary holds
b1 is extra-order ;
end;
registration
let L be non empty transitive antisymmetric lower-bounded RelStr ;
cluster Relation-like the carrier of L -defined the carrier of L -valued extra-order for Element of bool [: the carrier of L, the carrier of L:];
existence
ex b1 being Relation of L st b1 is extra-order
proof
take IntRel L ; ::_thesis: IntRel L is extra-order
thus IntRel L is extra-order ; ::_thesis: verum
end;
end;
definition
let L be lower-bounded with_suprema Poset;
let R be auxiliary(ii) Relation of L;
funcR -LowerMap -> Function of L,(InclPoset (LOWER L)) means :Def2: :: WAYBEL35:def 2
for x being Element of L holds it . x = R -below x;
existence
ex b1 being Function of L,(InclPoset (LOWER L)) st
for x being Element of L holds b1 . x = R -below x
proof
deffunc H1( Element of L) -> Element of bool the carrier of L = R -below $1;
A1: for x being Element of L holds H1(x) is Element of (InclPoset (LOWER L))
proof
let x be Element of L; ::_thesis: H1(x) is Element of (InclPoset (LOWER L))
reconsider I = H1(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 H1(x) is Element of (InclPoset (LOWER L)) by YELLOW_1:1; ::_thesis: verum
end;
consider f being Function of L,(InclPoset (LOWER L)) such that
A2: for x being Element of L holds f . x = H1(x) from FUNCT_2:sch_9(A1);
take f ; ::_thesis: for x being Element of L holds f . x = R -below x
let x be Element of L; ::_thesis: f . x = R -below x
thus f . x = R -below x by A2; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function of L,(InclPoset (LOWER L)) st ( for x being Element of L holds b1 . x = R -below x ) & ( for x being Element of L holds b2 . x = R -below x ) holds
b1 = b2
proof
let M1, M2 be Function of L,(InclPoset (LOWER L)); ::_thesis: ( ( for x being Element of L holds M1 . x = R -below x ) & ( for x being Element of L holds M2 . x = R -below x ) implies M1 = M2 )
assume A3: for x being Element of L holds M1 . x = R -below x ; ::_thesis: ( ex x being Element of L st not M2 . x = R -below x or M1 = M2 )
assume A4: for x being Element of L holds M2 . x = R -below x ; ::_thesis: M1 = M2
for x being set st x in the carrier of L holds
M1 . x = M2 . x
proof
let x be set ; ::_thesis: ( x in the carrier of L implies M1 . x = M2 . x )
assume x in the carrier of L ; ::_thesis: M1 . x = M2 . x
then reconsider x9 = x as Element of L ;
thus M1 . x = R -below x9 by A3
.= M2 . x by A4 ; ::_thesis: verum
end;
hence M1 = M2 by FUNCT_2:12; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines -LowerMap WAYBEL35:def_2_:_
for L being lower-bounded with_suprema Poset
for R being auxiliary(ii) Relation of L
for b3 being Function of L,(InclPoset (LOWER L)) holds
( b3 = R -LowerMap iff for x being Element of L holds b3 . x = R -below x );
registration
let L be lower-bounded with_suprema Poset;
let R be auxiliary(ii) Relation of L;
clusterR -LowerMap -> monotone ;
coherence
R -LowerMap is monotone
proof
let x, y be Element of L; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or (R -LowerMap) . x <= (R -LowerMap) . y )
set s = R -LowerMap ;
A1: (R -LowerMap) . y = R -below y by Def2;
assume x <= y ; ::_thesis: (R -LowerMap) . x <= (R -LowerMap) . y
then A2: R -below x c= R -below y by WAYBEL_4:17;
(R -LowerMap) . x = R -below x by Def2;
hence (R -LowerMap) . x <= (R -LowerMap) . y by A2, A1, YELLOW_1:3; ::_thesis: verum
end;
end;
definition
let L be 1-sorted ;
let R be Relation of the carrier of L;
mode strict_chain of R -> Subset of L means :Def3: :: WAYBEL35:def 3
for x, y being set st x in it & y in it & not [x,y] in R & not x = y holds
[y,x] in R;
existence
ex b1 being Subset of L st
for x, y being set st x in b1 & y in b1 & not [x,y] in R & not x = y holds
[y,x] in R
proof
take {} L ; ::_thesis: for x, y being set st x in {} L & y in {} L & not [x,y] in R & not x = y holds
[y,x] in R
thus for x, y being set st x in {} L & y in {} L & not [x,y] in R & not x = y holds
[y,x] in R ; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines strict_chain WAYBEL35:def_3_:_
for L being 1-sorted
for R being Relation of the carrier of L
for b3 being Subset of L holds
( b3 is strict_chain of R iff for x, y being set st x in b3 & y in b3 & not [x,y] in R & not x = y holds
[y,x] in R );
theorem Th1: :: WAYBEL35:1
for L being 1-sorted
for C being trivial Subset of L
for R being Relation of the carrier of L holds C is strict_chain of R
proof
let L be 1-sorted ; ::_thesis: for C being trivial Subset of L
for R being Relation of the carrier of L holds C is strict_chain of R
let C be trivial Subset of L; ::_thesis: for R being Relation of the carrier of L holds C is strict_chain of R
let R be Relation of the carrier of L; ::_thesis: C is strict_chain of R
let x, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( x in C & y in C & not [x,y] in R & not x = y implies [y,x] in R )
thus ( x in C & y in C & not [x,y] in R & not x = y implies [y,x] in R ) by SUBSET_1:def_7; ::_thesis: verum
end;
registration
let L be non empty 1-sorted ;
let R be Relation of the carrier of L;
cluster1 -element for strict_chain of R;
existence
ex b1 being strict_chain of R st b1 is 1 -element
proof
set C = the 1 -element Subset of L;
reconsider C = the 1 -element Subset of L as strict_chain of R by Th1;
take C ; ::_thesis: C is 1 -element
thus C is 1 -element ; ::_thesis: verum
end;
end;
theorem Th2: :: WAYBEL35:2
for L being antisymmetric RelStr
for R being auxiliary(i) Relation of L
for C being strict_chain of R
for 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 ; ::_thesis: for R being auxiliary(i) Relation of L
for C being strict_chain of R
for x, y being Element of L st x in C & y in C & x < y holds
[x,y] in R
let R be auxiliary(i) Relation of L; ::_thesis: for C being strict_chain of R
for x, y being Element of L st x in C & y in C & x < y holds
[x,y] in R
let C be strict_chain of R; ::_thesis: for x, y being Element of L st x in C & y in C & x < y holds
[x,y] in R
let x, y be Element of L; ::_thesis: ( x in C & y in C & x < y implies [x,y] in R )
assume that
A1: x in C and
A2: y in C and
A3: x < y ; ::_thesis: [x,y] in R
( [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 [x,y] in R by A3, ORDERS_2:6; ::_thesis: verum
end;
theorem :: WAYBEL35:3
for L being antisymmetric RelStr
for R being auxiliary(i) Relation of L
for x, y being Element of L st [x,y] in R & [y,x] in R holds
x = y
proof
let L be antisymmetric RelStr ; ::_thesis: for R being auxiliary(i) Relation of L
for x, y being Element of L st [x,y] in R & [y,x] in R holds
x = y
let R be auxiliary(i) Relation of L; ::_thesis: for x, y being Element of L st [x,y] in R & [y,x] in R holds
x = y
let x, y be Element of L; ::_thesis: ( [x,y] in R & [y,x] in R implies x = y )
assume that
A1: [x,y] in R and
A2: [y,x] in R ; ::_thesis: x = y
A3: y <= x by A2, WAYBEL_4:def_3;
x <= y by A1, WAYBEL_4:def_3;
hence x = y by A3, ORDERS_2:2; ::_thesis: verum
end;
theorem :: WAYBEL35:4
for L being non empty antisymmetric lower-bounded RelStr
for x being Element of L
for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for x being Element of L
for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R
let x be Element of L; ::_thesis: for R being auxiliary(iv) Relation of L holds {(Bottom L),x} is strict_chain of R
let R be auxiliary(iv) Relation of L; ::_thesis: {(Bottom L),x} is strict_chain of R
let a, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( a in {(Bottom L),x} & y in {(Bottom L),x} & not [a,y] in R & not a = y implies [y,a] in R )
assume that
A1: a in {(Bottom L),x} and
A2: y in {(Bottom L),x} ; ::_thesis: ( [a,y] in R or a = y or [y,a] in R )
A3: ( y = Bottom L or y = x ) by A2, TARSKI:def_2;
( a = Bottom L or a = x ) by A1, TARSKI:def_2;
hence ( [a,y] in R or a = y or [y,a] in R ) by A3, WAYBEL_4:def_6; ::_thesis: verum
end;
theorem Th5: :: WAYBEL35:5
for L being non empty antisymmetric lower-bounded RelStr
for R being auxiliary(iv) Relation of L
for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for R being auxiliary(iv) Relation of L
for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R
let R be auxiliary(iv) Relation of L; ::_thesis: for C being strict_chain of R holds C \/ {(Bottom L)} is strict_chain of R
let C be strict_chain of R; ::_thesis: C \/ {(Bottom L)} is strict_chain of R
set A = C \/ {(Bottom L)};
let x, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( x in C \/ {(Bottom L)} & y in C \/ {(Bottom L)} & not [x,y] in R & not x = y implies [y,x] in R )
assume that
A1: x in C \/ {(Bottom L)} and
A2: y in C \/ {(Bottom L)} ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
reconsider x = x, y = y as Element of L by A1, A2;
percases ( ( x in C & y in C ) or ( x in C & y = Bottom L ) or ( x = Bottom L & y in C ) or ( x = Bottom L & y = Bottom L ) ) by A1, A2, Lm1;
suppose ( x in C & y in C ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
hence ( [x,y] in R or x = y or [y,x] in R ) by Def3; ::_thesis: verum
end;
suppose ( x in C & y = Bottom L ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
hence ( [x,y] in R or x = y or [y,x] in R ) by WAYBEL_4:def_6; ::_thesis: verum
end;
suppose ( x = Bottom L & y in C ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
hence ( [x,y] in R or x = y or [y,x] in R ) by WAYBEL_4:def_6; ::_thesis: verum
end;
suppose ( x = Bottom L & y = Bottom L ) ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
hence ( [x,y] in R or x = y or [y,x] in R ) ; ::_thesis: verum
end;
end;
end;
definition
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C be strict_chain of R;
attrC is maximal means :Def4: :: WAYBEL35:def 4
for D being strict_chain of R st C c= D holds
C = D;
end;
:: deftheorem Def4 defines maximal WAYBEL35:def_4_:_
for L being 1-sorted
for R being Relation of the carrier of L
for C being strict_chain of R holds
( C is maximal iff for D being strict_chain of R st C c= D holds
C = D );
definition
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C be set ;
defpred S1[ set ] means ( $1 is strict_chain of R & C c= $1 );
func Strict_Chains (R,C) -> set means :Def5: :: WAYBEL35:def 5
for x being set holds
( x in it iff ( x is strict_chain of R & C c= x ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x is strict_chain of R & C c= x ) )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff ( x is strict_chain of R & C c= x ) )
thus for x being set holds
( x in X iff ( x is strict_chain of R & C c= x ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x is strict_chain of R & C c= x ) ) ) & ( for x being set holds
( x in b2 iff ( x is strict_chain of R & C c= x ) ) ) holds
b1 = b2
proof
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Strict_Chains WAYBEL35:def_5_:_
for L being 1-sorted
for R being Relation of the carrier of L
for C being set
for b4 being set holds
( b4 = Strict_Chains (R,C) iff for x being set holds
( x in b4 iff ( x is strict_chain of R & C c= x ) ) );
registration
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C be strict_chain of R;
cluster Strict_Chains (R,C) -> non empty ;
coherence
not Strict_Chains (R,C) is empty by Def5;
end;
notation
let R be Relation;
let X be set ;
synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R;
end;
theorem :: WAYBEL35:6
for L being 1-sorted
for R being Relation of the carrier of L
for 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 ; ::_thesis: for R being Relation of the carrier of L
for 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 ) )
let R be Relation of the carrier of L; ::_thesis: for 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 ) )
let C be strict_chain of R; ::_thesis: ( 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 ) )
set X = Strict_Chains (R,C);
A1: field (RelIncl (Strict_Chains (R,C))) = Strict_Chains (R,C) by WELLORD2:def_1;
thus A2: Strict_Chains (R,C) is_inductive_wrt RelIncl (Strict_Chains (R,C)) ::_thesis: ex D being set st
( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )
proof
let Y be set ; :: according to ORDERS_1:def_9 ::_thesis: ( not Y c= Strict_Chains (R,C) or not (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order or ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) ) )
assume that
A3: Y c= Strict_Chains (R,C) and
A4: (RelIncl (Strict_Chains (R,C))) |_2 Y is being_linear-order ; ::_thesis: ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )
percases ( Y is empty or not Y is empty ) ;
supposeA5: Y is empty ; ::_thesis: ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )
take C ; ::_thesis: ( C in Strict_Chains (R,C) & ( for b1 being set holds
( not b1 in Y or [b1,C] in RelIncl (Strict_Chains (R,C)) ) ) )
thus ( C in Strict_Chains (R,C) & ( for b1 being set holds
( not b1 in Y or [b1,C] in RelIncl (Strict_Chains (R,C)) ) ) ) by A5, Def5; ::_thesis: verum
end;
supposeA6: not Y is empty ; ::_thesis: ex b1 being set st
( b1 in Strict_Chains (R,C) & ( for b2 being set holds
( not b2 in Y or [b2,b1] in RelIncl (Strict_Chains (R,C)) ) ) )
take Z = union Y; ::_thesis: ( Z in Strict_Chains (R,C) & ( for b1 being set holds
( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) ) ) )
Z c= the carrier of L
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in Z or z in the carrier of L )
assume z in Z ; ::_thesis: z in the carrier of L
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 z in the carrier of L by A7; ::_thesis: verum
end;
then reconsider S = Z as Subset of L ;
A9: S is strict_chain of R
proof
(RelIncl (Strict_Chains (R,C))) |_2 Y is connected by A4, ORDERS_1:def_5;
then A10: (RelIncl (Strict_Chains (R,C))) |_2 Y is_connected_in field ((RelIncl (Strict_Chains (R,C))) |_2 Y) by RELAT_2:def_14;
A11: (RelIncl (Strict_Chains (R,C))) |_2 Y = RelIncl Y by A3, WELLORD2:7;
let x, y be set ; :: according to WAYBEL35:def_3 ::_thesis: ( x in S & y in S & not [x,y] in R & not x = y implies [y,x] in R )
A12: field (RelIncl Y) = Y by WELLORD2:def_1;
assume x in S ; ::_thesis: ( not y in S or [x,y] in R or x = y or [y,x] in R )
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 ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
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;
percases ( A <> B or A = B ) ;
suppose A <> B ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
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 ( [x,y] in R or x = y or [y,x] in R ) by A13, A16, A15, A18, Def3; ::_thesis: verum
end;
suppose A = B ; ::_thesis: ( [x,y] in R or x = y or [y,x] in R )
hence ( [x,y] in R or x = y or [y,x] in R ) by A13, A16, A15, Def3; ::_thesis: verum
end;
end;
end;
C c= Z
proof
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in C or c in Z )
assume A19: c in C ; ::_thesis: c in Z
consider y being set such that
A20: y in Y by A6, XBOOLE_0:def_1;
C c= y by A3, A20, Def5;
hence c in Z by A19, A20, TARSKI:def_4; ::_thesis: verum
end;
hence A21: Z in Strict_Chains (R,C) by A9, Def5; ::_thesis: for b1 being set holds
( not b1 in Y or [b1,Z] in RelIncl (Strict_Chains (R,C)) )
let y be set ; ::_thesis: ( not y in Y or [y,Z] in RelIncl (Strict_Chains (R,C)) )
assume A22: y in Y ; ::_thesis: [y,Z] in RelIncl (Strict_Chains (R,C))
then y c= Z by ZFMISC_1:74;
hence [y,Z] in RelIncl (Strict_Chains (R,C)) by A3, A21, A22, WELLORD2:def_1; ::_thesis: verum
end;
end;
end;
A23: RelIncl (Strict_Chains (R,C)) is_transitive_in Strict_Chains (R,C) by WELLORD2:20;
A24: RelIncl (Strict_Chains (R,C)) is_antisymmetric_in Strict_Chains (R,C) by WELLORD2:21;
RelIncl (Strict_Chains (R,C)) is_reflexive_in Strict_Chains (R,C) by WELLORD2:19;
then RelIncl (Strict_Chains (R,C)) partially_orders Strict_Chains (R,C) by A23, A24, ORDERS_1:def_7;
then consider D being set such that
A25: D is_maximal_in RelIncl (Strict_Chains (R,C)) by A1, A2, ORDERS_1:63;
take D ; ::_thesis: ( D is_maximal_in RelIncl (Strict_Chains (R,C)) & C c= D )
thus D is_maximal_in RelIncl (Strict_Chains (R,C)) by A25; ::_thesis: C c= D
D in field (RelIncl (Strict_Chains (R,C))) by A25, ORDERS_1:def_11;
hence C c= D by A1, Def5; ::_thesis: verum
end;
theorem Th7: :: WAYBEL35:7
for L being non empty transitive RelStr
for C being non empty Subset of L
for 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 ; ::_thesis: for C being non empty Subset of L
for 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)) )
let C be non empty Subset of L; ::_thesis: for 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)) )
let X be Subset of C; ::_thesis: ( ex_sup_of X,L & "\/" (X,L) in C implies ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) )
assume that
A1: ex_sup_of X,L and
A2: "\/" (X,L) in C ; ::_thesis: ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) )
the carrier of (subrelstr C) = C by YELLOW_0:def_15;
hence ( ex_sup_of X, subrelstr C & "\/" (X,L) = "\/" (X,(subrelstr C)) ) by A1, A2, YELLOW_0:64; ::_thesis: verum
end;
Lm2: for L being non empty Poset
for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R
for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds
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; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R
for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds
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 ) ) )
let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R
for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds
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 ) ) )
let C be non empty strict_chain of R; ::_thesis: for X being Subset of C st ex_sup_of X,L & C is maximal & not "\/" (X,L) in C holds
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 ) ) )
let X be Subset of C; ::_thesis: ( ex_sup_of X,L & C is maximal & not "\/" (X,L) in C implies 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 ) ) ) )
assume that
A1: ex_sup_of X,L and
A2: C is maximal ; ::_thesis: ( "\/" (X,L) in C or 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 ) ) ) )
set s = "\/" (X,L);
A3: C c= C \/ {("\/" (X,L))} by XBOOLE_1:7;
assume A4: not "\/" (X,L) in C ; ::_thesis: 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 ) ) )
then not C \/ {("\/" (X,L))} c= C by ZFMISC_1:39;
then A5: C \/ {("\/" (X,L))} is not strict_chain of R by A3, A2, Def4;
ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
proof
A6: for a being Element of L st a in C & not [a,("\/" (X,L))] in R & not [("\/" (X,L)),a] in R holds
ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
proof
let a be Element of L; ::_thesis: ( a in C & not [a,("\/" (X,L))] in R & not [("\/" (X,L)),a] in R implies ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) )
assume that
A7: a in C and
A8: not [a,("\/" (X,L))] in R and
A9: not [("\/" (X,L)),a] in R ; ::_thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
take a ; ::_thesis: ( a in C & "\/" (X,L) < a & not [("\/" (X,L)),a] in R )
thus a in C by A7; ::_thesis: ( "\/" (X,L) < a & not [("\/" (X,L)),a] in R )
a is_>=_than X
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= a )
assume A10: x in X ; ::_thesis: x <= a
percases ( [a,x] in R or [x,a] in R or a = x ) by A7, A10, Def3;
supposeA11: [a,x] in R ; ::_thesis: x <= a
A12: a <= a ;
x <= "\/" (X,L) by A1, A10, YELLOW_4:1;
hence x <= a by A12, A8, A11, WAYBEL_4:def_4; ::_thesis: verum
end;
suppose ( [x,a] in R or a = x ) ; ::_thesis: x <= a
hence x <= a by WAYBEL_4:def_3; ::_thesis: verum
end;
end;
end;
then "\/" (X,L) <= a by A1, YELLOW_0:def_9;
hence "\/" (X,L) < a by A4, A7, ORDERS_2:def_6; ::_thesis: not [("\/" (X,L)),a] in R
thus not [("\/" (X,L)),a] in R by A9; ::_thesis: verum
end;
consider a, b being set such that
A13: a in C \/ {("\/" (X,L))} and
A14: b in C \/ {("\/" (X,L))} and
A15: not [a,b] in R and
A16: a <> b and
A17: not [b,a] in R by A5, Def3;
reconsider a = a, b = b as Element of L by A13, A14;
percases ( ( a in C & b in C ) or ( a in C & b = "\/" (X,L) ) or ( a = "\/" (X,L) & b in C ) or ( a = "\/" (X,L) & b = "\/" (X,L) ) ) by A13, A14, Lm1;
suppose ( a in C & b in C ) ; ::_thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A16, A17, Def3; ::_thesis: verum
end;
suppose ( a in C & b = "\/" (X,L) ) ; ::_thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A17, A6; ::_thesis: verum
end;
suppose ( a = "\/" (X,L) & b in C ) ; ::_thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A15, A17, A6; ::_thesis: verum
end;
suppose ( a = "\/" (X,L) & b = "\/" (X,L) ) ; ::_thesis: ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R )
hence ex cs being Element of L st
( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A16; ::_thesis: verum
end;
end;
end;
then consider cs being Element of L such that
A18: cs in C and
A19: "\/" (X,L) < cs and
A20: not [("\/" (X,L)),cs] in R ;
take cs ; ::_thesis: ( 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 ) ) )
thus ( cs in C & "\/" (X,L) < cs & not [("\/" (X,L)),cs] in R ) by A18, A19, A20; ::_thesis: 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 ) )
reconsider cs1 = cs as Element of (subrelstr C) by A18, YELLOW_0:def_15;
take cs1 ; ::_thesis: ( cs = cs1 & X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds
cs1 <= a ) )
thus cs = cs1 ; ::_thesis: ( X is_<=_than cs1 & ( for a being Element of (subrelstr C) st X is_<=_than a holds
cs1 <= a ) )
A21: "\/" (X,L) <= cs by A19, ORDERS_2:def_6;
thus X is_<=_than cs1 ::_thesis: for a being Element of (subrelstr C) st X is_<=_than a holds
cs1 <= a
proof
let b be Element of (subrelstr C); :: according to LATTICE3:def_9 ::_thesis: ( not b in X or b <= cs1 )
reconsider b0 = b as Element of L by YELLOW_0:58;
assume b in X ; ::_thesis: b <= cs1
then b0 <= "\/" (X,L) by A1, YELLOW_4:1;
then b0 <= cs by A21, ORDERS_2:3;
hence b <= cs1 by YELLOW_0:60; ::_thesis: verum
end;
let a be Element of (subrelstr C); ::_thesis: ( X is_<=_than a implies cs1 <= a )
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 ; ::_thesis: cs1 <= a
then X is_<=_than a0 by A22, YELLOW_0:62;
then A23: "\/" (X,L) <= 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, WAYBEL_4:def_4;
hence cs1 <= a by YELLOW_0:60; ::_thesis: verum
end;
theorem Th8: :: WAYBEL35:8
for L being non empty Poset
for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R
for 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; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R
for X being Subset of C st ex_sup_of X,L & C is maximal holds
ex_sup_of X, subrelstr C
let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R
for X being Subset of C st ex_sup_of X,L & C is maximal holds
ex_sup_of X, subrelstr C
let C be non empty strict_chain of R; ::_thesis: for X being Subset of C st ex_sup_of X,L & C is maximal holds
ex_sup_of X, subrelstr C
let X be Subset of C; ::_thesis: ( ex_sup_of X,L & C is maximal implies ex_sup_of X, subrelstr C )
assume that
A1: ex_sup_of X,L and
A2: C is maximal ; ::_thesis: ex_sup_of X, subrelstr C
set s = "\/" (X,L);
percases ( "\/" (X,L) in C or not "\/" (X,L) in C ) ;
suppose "\/" (X,L) in C ; ::_thesis: ex_sup_of X, subrelstr C
hence ex_sup_of X, subrelstr C by A1, Th7; ::_thesis: verum
end;
suppose not "\/" (X,L) in C ; ::_thesis: ex_sup_of X, subrelstr C
then 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 ) ) ) by A1, A2, Lm2;
hence ex_sup_of X, subrelstr C by YELLOW_0:15; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL35:9
for L being non empty Poset
for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R
for 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; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R
for 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) ) )
let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R
for 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) ) )
let C be non empty strict_chain of R; ::_thesis: for 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) ) )
let X be Subset of C; ::_thesis: ( ex_inf_of (uparrow ("\/" (X,L))) /\ C,L & ex_sup_of X,L & C is maximal implies ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) )
set s = "\/" (X,L);
set x = "\/" (X,(subrelstr C));
set U = uparrow ("\/" (X,L));
assume that
A1: ex_inf_of (uparrow ("\/" (X,L))) /\ C,L and
A2: ex_sup_of X,L and
A3: C is maximal ; ::_thesis: ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) )
A4: "\/" (X,L) <= "\/" (X,L) ;
reconsider x1 = "\/" (X,(subrelstr C)) as Element of L by YELLOW_0:58;
A5: the carrier of (subrelstr C) = C by YELLOW_0:def_15;
percases ( "\/" (X,L) in C or not "\/" (X,L) in C ) ;
supposeA6: "\/" (X,L) in C ; ::_thesis: ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) )
then A7: "\/" (X,L) = "\/" (X,(subrelstr C)) by A2, A5, YELLOW_0:64;
A8: (uparrow ("\/" (X,L))) /\ C is_>=_than x1
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in (uparrow ("\/" (X,L))) /\ C or x1 <= b )
assume b in (uparrow ("\/" (X,L))) /\ C ; ::_thesis: x1 <= b
then b in uparrow ("\/" (X,L)) by XBOOLE_0:def_4;
hence x1 <= b by A7, WAYBEL_0:18; ::_thesis: verum
end;
for a being Element of L st (uparrow ("\/" (X,L))) /\ C is_>=_than a holds
a <= x1
proof
"\/" (X,L) in uparrow ("\/" (X,L)) by A4, WAYBEL_0:18;
then A9: x1 in (uparrow ("\/" (X,L))) /\ C by A6, A7, XBOOLE_0:def_4;
let a be Element of L; ::_thesis: ( (uparrow ("\/" (X,L))) /\ C is_>=_than a implies a <= x1 )
assume (uparrow ("\/" (X,L))) /\ C is_>=_than a ; ::_thesis: a <= x1
hence a <= x1 by A9, LATTICE3:def_8; ::_thesis: verum
end;
hence ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by A1, A6, A8, YELLOW_0:def_10; ::_thesis: verum
end;
suppose not "\/" (X,L) in C ; ::_thesis: ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) )
then consider cs being Element of L such that
A10: cs in C and
A11: "\/" (X,L) < cs and
A12: not [("\/" (X,L)),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: "\/" (X,L) <= cs by A11, ORDERS_2:def_6;
A15: for a being Element of L st (uparrow ("\/" (X,L))) /\ C is_>=_than a holds
a <= cs
proof
cs in uparrow ("\/" (X,L)) by A14, WAYBEL_0:18;
then A16: cs in (uparrow ("\/" (X,L))) /\ C by A10, XBOOLE_0:def_4;
let a be Element of L; ::_thesis: ( (uparrow ("\/" (X,L))) /\ C is_>=_than a implies a <= cs )
assume (uparrow ("\/" (X,L))) /\ C is_>=_than a ; ::_thesis: a <= cs
hence a <= cs by A16, LATTICE3:def_8; ::_thesis: verum
end;
A17: cs <= cs ;
A18: (uparrow ("\/" (X,L))) /\ C is_>=_than cs
proof
let b be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not b in (uparrow ("\/" (X,L))) /\ C or cs <= b )
assume A19: b in (uparrow ("\/" (X,L))) /\ C ; ::_thesis: cs <= b
then b in uparrow ("\/" (X,L)) by XBOOLE_0:def_4;
then A20: "\/" (X,L) <= 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, WAYBEL_4:def_4; ::_thesis: verum
end;
ex_sup_of X, subrelstr C by A2, A3, Th8;
then cs = "\/" (X,(subrelstr C)) by A13, YELLOW_0:def_9;
hence ( "\/" (X,(subrelstr C)) = "/\" (((uparrow ("\/" (X,L))) /\ C),L) & ( not "\/" (X,L) in C implies "\/" (X,L) < "/\" (((uparrow ("\/" (X,L))) /\ C),L) ) ) by A15, A1, A11, A18, YELLOW_0:def_10; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL35:10
for L being non empty complete Poset
for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R st C is maximal holds
subrelstr C is complete
proof
let L be non empty complete Poset; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being non empty strict_chain of R st C is maximal holds
subrelstr C is complete
let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being non empty strict_chain of R st C is maximal holds
subrelstr C is complete
let C be non empty strict_chain of R; ::_thesis: ( C is maximal implies subrelstr C is complete )
assume A1: C is maximal ; ::_thesis: subrelstr C is complete
for X being Subset of (subrelstr C) holds ex_sup_of X, subrelstr C
proof
let X be Subset of (subrelstr C); ::_thesis: ex_sup_of X, subrelstr C
X is Subset of C by YELLOW_0:def_15;
hence ex_sup_of X, subrelstr C by A1, Th8, YELLOW_0:17; ::_thesis: verum
end;
hence subrelstr C is complete by YELLOW_0:53; ::_thesis: verum
end;
theorem :: WAYBEL35:11
for L being non empty antisymmetric lower-bounded RelStr
for R being auxiliary(iv) Relation of L
for C being strict_chain of R st C is maximal holds
Bottom L in C
proof
let L be non empty antisymmetric lower-bounded RelStr ; ::_thesis: for R being auxiliary(iv) Relation of L
for C being strict_chain of R st C is maximal holds
Bottom L in C
let R be auxiliary(iv) Relation of L; ::_thesis: for C being strict_chain of R st C is maximal holds
Bottom L in C
let C be strict_chain of R; ::_thesis: ( C is maximal implies Bottom L in C )
assume A1: for D being strict_chain of R st C c= D holds
C = D ; :: according to WAYBEL35:def_4 ::_thesis: Bottom L in C
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 ; ::_thesis: contradiction
then not Bottom L in {(Bottom L)} by A2, XBOOLE_0:def_3;
hence contradiction by TARSKI:def_1; ::_thesis: verum
end;
theorem :: WAYBEL35:12
for L being non empty upper-bounded Poset
for R being auxiliary(ii) Relation of L
for C being strict_chain of R
for 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; ::_thesis: for R being auxiliary(ii) Relation of L
for C being strict_chain of R
for 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 )
let R be auxiliary(ii) Relation of L; ::_thesis: for C being strict_chain of R
for 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 )
let C be strict_chain of R; ::_thesis: for 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 )
let m be Element of L; ::_thesis: ( C is maximal & m is_maximum_of C & [m,(Top L)] in R implies ( [(Top L),(Top L)] in R & m = Top L ) )
assume that
A1: C is maximal and
A2: m is_maximum_of C and
A3: [m,(Top L)] in R ; ::_thesis: ( [(Top L),(Top L)] in R & m = Top L )
A4: C c= C \/ {(Top L)} by XBOOLE_1:7;
now__::_thesis:_not_m_<>_Top_L
A5: m <= Top L by YELLOW_0:45;
assume A6: m <> Top L ; ::_thesis: contradiction
A7: {(Top L)} c= C \/ {(Top L)} by XBOOLE_1:7;
A8: ex_sup_of C,L by A2, WAYBEL_1:def_7;
A9: sup C = m by A2, WAYBEL_1:def_7;
C \/ {(Top L)} is strict_chain of R
proof
let a, b be set ; :: according to WAYBEL35:def_3 ::_thesis: ( a in C \/ {(Top L)} & b in C \/ {(Top L)} & not [a,b] in R & not a = b implies [b,a] in R )
assume that
A10: a in C \/ {(Top L)} and
A11: b in C \/ {(Top L)} ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
A12: Top L <= Top L ;
percases ( ( a in C & b in C ) or ( a = Top L & b in C ) or ( a in C & b = Top L ) or ( a = Top L & b = Top L ) ) by A10, A11, Lm1;
suppose ( a in C & b in C ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) by Def3; ::_thesis: verum
end;
supposethat A13: a = Top L and
A14: b in C ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
reconsider b = b as Element of L by A14;
b <= sup C by A8, A14, YELLOW_4:1;
hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A9, A12, A13, WAYBEL_4:def_4; ::_thesis: verum
end;
supposethat A15: a in C and
A16: b = Top L ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
reconsider a = a as Element of L by A15;
a <= sup C by A8, A15, YELLOW_4:1;
hence ( [a,b] in R or a = b or [b,a] in R ) by A3, A9, A12, A16, WAYBEL_4:def_4; ::_thesis: verum
end;
suppose ( a = Top L & b = Top L ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) ; ::_thesis: verum
end;
end;
end;
then A17: C \/ {(Top L)} = C by A1, A4, Def4;
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; ::_thesis: verum
end;
hence ( [(Top L),(Top L)] in R & m = Top L ) by A3; ::_thesis: verum
end;
definition
let L be RelStr ;
let C be set ;
let R be Relation of the carrier of L;
predR satisfies_SIC_on C means :Def6: :: WAYBEL35:def 6
for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y );
end;
:: deftheorem Def6 defines satisfies_SIC_on WAYBEL35:def_6_:_
for L being RelStr
for C being set
for R being Relation of the carrier of L holds
( R satisfies_SIC_on C iff for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) );
definition
let L be RelStr ;
let R be Relation of the carrier of L;
let C be strict_chain of R;
attrC is satisfying_SIC means :Def7: :: WAYBEL35:def 7
R satisfies_SIC_on C;
end;
:: deftheorem Def7 defines satisfying_SIC WAYBEL35:def_7_:_
for L being RelStr
for R being Relation of the carrier of L
for C being strict_chain of R holds
( C is satisfying_SIC iff R satisfies_SIC_on C );
theorem Th13: :: WAYBEL35:13
for L being RelStr
for C being set
for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds
for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
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 ; ::_thesis: for C being set
for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds
for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )
let C be set ; ::_thesis: for R being auxiliary(i) Relation of L st R satisfies_SIC_on C holds
for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )
let R be auxiliary(i) Relation of L; ::_thesis: ( R satisfies_SIC_on C implies for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y ) )
assume A1: R satisfies_SIC_on C ; ::_thesis: for x, z being Element of L st x in C & z in C & [x,z] in R & x <> z holds
ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )
let x, z be Element of L; ::_thesis: ( 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 ) )
assume that
A2: x in C and
A3: z in C and
A4: [x,z] in R and
A5: x <> z ; ::_thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x < y )
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, Def6;
take y ; ::_thesis: ( y in C & [x,y] in R & [y,z] in R & x < y )
thus ( y in C & [x,y] in R & [y,z] in R ) by A6, A7, A8; ::_thesis: x < y
x <= y by A7, WAYBEL_4:def_3;
hence x < y by A9, ORDERS_2:def_6; ::_thesis: verum
end;
registration
let L be RelStr ;
let R be Relation of the carrier of L;
cluster trivial -> satisfying_SIC for strict_chain of R;
coherence
for b1 being strict_chain of R st b1 is trivial holds
b1 is satisfying_SIC
proof
let C be strict_chain of R; ::_thesis: ( C is trivial implies C is satisfying_SIC )
assume A1: C is trivial ; ::_thesis: C is satisfying_SIC
let x, z be Element of L; :: according to WAYBEL35:def_6,WAYBEL35:def_7 ::_thesis: ( 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 ) )
assume that
A2: x in C and
A3: z in C and
[x,z] in R and
A4: x <> z ; ::_thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
thus ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) by A2, A3, A4, A1, SUBSET_1:def_7; ::_thesis: verum
end;
end;
registration
let L be non empty RelStr ;
let R be Relation of the carrier of L;
cluster1 -element for strict_chain of R;
existence
ex b1 being strict_chain of R st b1 is 1 -element
proof
set C = the 1 -element Subset of L;
reconsider C = the 1 -element Subset of L as strict_chain of R by Th1;
take C ; ::_thesis: C is 1 -element
thus C is 1 -element ; ::_thesis: verum
end;
end;
theorem :: WAYBEL35:14
for L being lower-bounded with_suprema Poset
for R being auxiliary(i) auxiliary(ii) Relation of L
for 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; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for C being strict_chain of R st C is maximal & R is satisfying_SI holds
R satisfies_SIC_on C
let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for C being strict_chain of R st C is maximal & R is satisfying_SI holds
R satisfies_SIC_on C
let C be strict_chain of R; ::_thesis: ( C is maximal & R is satisfying_SI implies R satisfies_SIC_on C )
assume that
A1: C is maximal and
A2: R is satisfying_SI ; ::_thesis: R satisfies_SIC_on C
let x, z be Element of L; :: according to WAYBEL35:def_6 ::_thesis: ( 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 ) )
assume that
A3: x in C and
A4: z in C and
A5: [x,z] in R and
A6: x <> z ; ::_thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
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: for y being Element of L holds
( not y in C or not [x,y] in R or not [y,z] in R or not x <> y ) ; ::_thesis: contradiction
A12: x <= y by A7, WAYBEL_4:def_3;
A13: C \/ {y} is strict_chain of R
proof
let a, b be set ; :: according to WAYBEL35:def_3 ::_thesis: ( a in C \/ {y} & b in C \/ {y} & not [a,b] in R & not a = b implies [b,a] in R )
assume that
A14: a in C \/ {y} and
A15: b in C \/ {y} ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
percases ( ( a in C & b in C ) or ( a in C & b = y ) or ( a = y & b in C ) or ( a = y & b = y ) ) by A14, A15, Lm1;
suppose ( a in C & b in C ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) by Def3; ::_thesis: verum
end;
supposethat A16: a in C and
A17: b = y ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
now__::_thesis:_(_[a,b]_in_R_or_a_=_b_or_[b,a]_in_R_)
reconsider a = a as Element of L by A16;
A18: a <= a ;
percases ( x = a or a = z or ( not [x,a] in R & a <> x ) or ( not [a,z] in R & a <> z ) ) by A11, A16;
suppose x = a ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) by A7, A17; ::_thesis: verum
end;
suppose a = z ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A17; ::_thesis: verum
end;
suppose ( not [x,a] in R & a <> x ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
then [a,x] in R by A3, A16, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A12, A17, A18, WAYBEL_4:def_4; ::_thesis: verum
end;
suppose ( not [a,z] in R & a <> z ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
then [z,a] in R by A4, A16, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A10, A17, A18, WAYBEL_4:def_4; ::_thesis: verum
end;
end;
end;
hence ( [a,b] in R or a = b or [b,a] in R ) ; ::_thesis: verum
end;
supposethat A19: a = y and
A20: b in C ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
now__::_thesis:_(_[a,b]_in_R_or_a_=_b_or_[b,a]_in_R_)
reconsider b = b as Element of L by A20;
A21: b <= b ;
percases ( x = b or b = z or ( not [x,b] in R & b <> x ) or ( not [b,z] in R & b <> z ) ) by A11, A20;
suppose x = b ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) by A7, A19; ::_thesis: verum
end;
suppose b = z ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A19; ::_thesis: verum
end;
suppose ( not [x,b] in R & b <> x ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
then [b,x] in R by A3, A20, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A12, A19, A21, WAYBEL_4:def_4; ::_thesis: verum
end;
suppose ( not [b,z] in R & b <> z ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
then [z,b] in R by A4, A20, Def3;
hence ( [a,b] in R or a = b or [b,a] in R ) by A10, A19, A21, WAYBEL_4:def_4; ::_thesis: verum
end;
end;
end;
hence ( [a,b] in R or a = b or [b,a] in R ) ; ::_thesis: verum
end;
suppose ( a = y & b = y ) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) ; ::_thesis: verum
end;
end;
end;
C c= C \/ {y} by XBOOLE_1:7;
then C \/ {y} = C by A13, A1, Def4;
then y in C by ZFMISC_1:39;
hence contradiction by A11, A7, A8, A9; ::_thesis: verum
end;
definition
let R be Relation;
let C, y be set ;
func SetBelow (R,C,y) -> set equals :: WAYBEL35:def 8
(R " {y}) /\ C;
coherence
(R " {y}) /\ C is set ;
end;
:: deftheorem defines SetBelow WAYBEL35:def_8_:_
for R being Relation
for C, y being set holds SetBelow (R,C,y) = (R " {y}) /\ C;
theorem Th15: :: WAYBEL35:15
for R being Relation
for 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; ::_thesis: for C, x, y being set holds
( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) )
let C, x, y be set ; ::_thesis: ( x in SetBelow (R,C,y) iff ( [x,y] in R & x in C ) )
hereby ::_thesis: ( [x,y] in R & x in C implies x in SetBelow (R,C,y) )
assume A1: x in SetBelow (R,C,y) ; ::_thesis: ( [x,y] in R & x in C )
then x in R " {y} by XBOOLE_0:def_4;
then ex a being set st
( [x,a] in R & a in {y} ) by RELAT_1:def_14;
hence [x,y] in R by TARSKI:def_1; ::_thesis: x in C
thus x in C by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
assume that
A2: [x,y] in R and
A3: x in C ; ::_thesis: x in SetBelow (R,C,y)
y in {y} by TARSKI:def_1;
then x in R " {y} by A2, RELAT_1:def_14;
hence x in SetBelow (R,C,y) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
definition
let L be 1-sorted ;
let R be Relation of the carrier of L;
let C, y be set ;
:: original: SetBelow
redefine func SetBelow (R,C,y) -> Subset of L;
coherence
SetBelow (R,C,y) is Subset of L
proof
(R " {y}) /\ C c= the carrier of L ;
hence SetBelow (R,C,y) is Subset of L ; ::_thesis: verum
end;
end;
theorem Th16: :: WAYBEL35:16
for L being RelStr
for R being auxiliary(i) Relation of L
for C being set
for y being Element of L holds SetBelow (R,C,y) is_<=_than y
proof
let L be RelStr ; ::_thesis: for R being auxiliary(i) Relation of L
for C being set
for y being Element of L holds SetBelow (R,C,y) is_<=_than y
let R be auxiliary(i) Relation of L; ::_thesis: for C being set
for y being Element of L holds SetBelow (R,C,y) is_<=_than y
let C be set ; ::_thesis: for y being Element of L holds SetBelow (R,C,y) is_<=_than y
let y be Element of L; ::_thesis: SetBelow (R,C,y) is_<=_than y
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in SetBelow (R,C,y) or b <= y )
assume b in SetBelow (R,C,y) ; ::_thesis: b <= y
then [b,y] in R by Th15;
hence b <= y by WAYBEL_4:def_3; ::_thesis: verum
end;
theorem Th17: :: WAYBEL35:17
for L being reflexive transitive RelStr
for R being auxiliary(ii) Relation of L
for C being Subset of L
for 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 ; ::_thesis: for R being auxiliary(ii) Relation of L
for C being Subset of L
for x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y)
let R be auxiliary(ii) Relation of L; ::_thesis: for C being Subset of L
for x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y)
let C be Subset of L; ::_thesis: for x, y being Element of L st x <= y holds
SetBelow (R,C,x) c= SetBelow (R,C,y)
let x, y be Element of L; ::_thesis: ( x <= y implies SetBelow (R,C,x) c= SetBelow (R,C,y) )
assume A1: x <= y ; ::_thesis: SetBelow (R,C,x) c= SetBelow (R,C,y)
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in SetBelow (R,C,x) or a in SetBelow (R,C,y) )
assume A2: a in SetBelow (R,C,x) ; ::_thesis: a in SetBelow (R,C,y)
then reconsider L = L as non empty reflexive RelStr ;
reconsider a = 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 a in SetBelow (R,C,y) by A3, Th15; ::_thesis: verum
end;
theorem Th18: :: WAYBEL35:18
for L being RelStr
for R being auxiliary(i) Relation of L
for C being set
for 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 ; ::_thesis: for R being auxiliary(i) Relation of L
for C being set
for 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))
let R be auxiliary(i) Relation of L; ::_thesis: for C being set
for 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))
let C be set ; ::_thesis: for 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))
let x be Element of L; ::_thesis: ( x in C & [x,x] in R & ex_sup_of SetBelow (R,C,x),L implies x = sup (SetBelow (R,C,x)) )
assume that
A1: x in C and
A2: [x,x] in R and
A3: ex_sup_of SetBelow (R,C,x),L ; ::_thesis: x = sup (SetBelow (R,C,x))
A4: for a being Element of L st SetBelow (R,C,x) is_<=_than a holds
x <= a
proof
let a be Element of L; ::_thesis: ( SetBelow (R,C,x) is_<=_than a implies x <= a )
assume A5: SetBelow (R,C,x) is_<=_than a ; ::_thesis: x <= a
x in SetBelow (R,C,x) by A1, A2, Th15;
hence x <= a by A5, LATTICE3:def_9; ::_thesis: verum
end;
SetBelow (R,C,x) is_<=_than x by Th16;
hence x = sup (SetBelow (R,C,x)) by A4, A3, YELLOW_0:def_9; ::_thesis: verum
end;
definition
let L be RelStr ;
let C be Subset of L;
attrC is sup-closed means :Def9: :: WAYBEL35:def 9
for X being Subset of C st ex_sup_of X,L holds
"\/" (X,L) = "\/" (X,(subrelstr C));
end;
:: deftheorem Def9 defines sup-closed WAYBEL35:def_9_:_
for L being RelStr
for C being Subset of L holds
( C is sup-closed iff for X being Subset of C st ex_sup_of X,L holds
"\/" (X,L) = "\/" (X,(subrelstr C)) );
theorem Th19: :: WAYBEL35:19
for L being non empty complete Poset
for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )
proof
let L be non empty complete Poset; ::_thesis: for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )
let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R
for p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )
let C be satisfying_SIC strict_chain of R; ::_thesis: for p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )
let p, q be Element of L; ::_thesis: ( p in C & q in C & p < q implies ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) )
assume that
A1: p in C and
A2: q in C and
A3: p < q ; ::_thesis: ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )
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 S1[ 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 Element of NAT
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Element of D ex y being Element of D st S1[n,x,y]
let x be Element of D; ::_thesis: ex y being Element of D st S1[n,x,y]
x in D ;
then reconsider t = x as Element of L ;
A14: x in C by Th15;
A15: [x,w] in R by Th15;
percases ( x <> w or x = w ) ;
suppose x <> w ; ::_thesis: ex y being Element of D st S1[n,x,y]
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 ; ::_thesis: S1[n,x,y]
take b ; ::_thesis: ( y = b & y in C & [x,y] in R & b <= w )
thus ( y = b & y in C & [x,y] in R & b <= w ) by A16, A17, A18, WAYBEL_4:def_3; ::_thesis: verum
end;
supposeA19: x = w ; ::_thesis: ex y being Element of D st S1[n,x,y]
take x ; ::_thesis: S1[n,x,x]
take t ; ::_thesis: ( x = t & x in C & [x,x] in R & t <= w )
thus ( x = t & x in C & [x,x] in R & t <= w ) by A19, Th15; ::_thesis: verum
end;
end;
end;
consider f being Function of NAT,D such that
A20: f . 0 = g and
A21: for n being Element of NAT holds S1[n,f . n,f . (n + 1)] from RECDEF_1:sch_2(A13);
reconsider f = f as Function of NAT, the carrier of L by FUNCT_2:7;
take y = sup (rng f); ::_thesis: ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )
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; ::_thesis: ( [y,q] in R & y = sup (SetBelow (R,C,y)) )
rng f is_<=_than w
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in rng f or x <= w )
assume x in rng f ; ::_thesis: x <= w
then consider n being set such that
A24: n in dom f and
A25: f . n = x by FUNCT_1:def_3;
reconsider n = 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 . (n + 1) by A25, WAYBEL_4:def_3;
hence x <= w by A26, ORDERS_2:3; ::_thesis: verum
end;
then y <= w by A22, YELLOW_0:def_9;
hence [y,q] in R by A7, A12, WAYBEL_4:def_4; ::_thesis: y = sup (SetBelow (R,C,y))
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; ::_thesis: ( SetBelow (R,C,y) is_<=_than x implies y <= x )
assume A29: SetBelow (R,C,y) is_<=_than x ; ::_thesis: y <= x
rng f is_<=_than x
proof
defpred S2[ Nat] means f . $1 in C;
let m be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not m in rng f or m <= x )
assume m in rng f ; ::_thesis: m <= x
then consider n being set such that
A30: n in dom f and
A31: f . n = m by FUNCT_1:def_3;
reconsider n = n as Element of NAT by A30;
A32: f . n <= f . n ;
A33: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; ::_thesis: ( S2[k] implies S2[k + 1] )
k is Element of NAT by ORDINAL1:def_12;
then 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 ( S2[k] implies S2[k + 1] ) ; ::_thesis: verum
end;
A34: S2[ 0 ] by A9, A20;
for n being Nat holds S2[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 . (n + 1) <= 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, LATTICE3:def_9; ::_thesis: verum
end;
hence y <= x by A22, YELLOW_0:def_9; ::_thesis: verum
end;
SetBelow (R,C,y) is_<=_than y by Th16;
hence y = sup (SetBelow (R,C,y)) by A28, A27, YELLOW_0:def_9; ::_thesis: verum
end;
theorem :: WAYBEL35:20
for L being non empty lower-bounded Poset
for R being extra-order Relation of L
for 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 non empty lower-bounded Poset; ::_thesis: for R being extra-order Relation of L
for 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))
let R be extra-order Relation of L; ::_thesis: for 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))
let C be non empty strict_chain of R; ::_thesis: ( 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 implies for c being Element of L st c in C holds
c = sup (SetBelow (R,C,c)) )
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 ; ::_thesis: ( not R satisfies_SIC_on C or for c being Element of L st c in C holds
c = sup (SetBelow (R,C,c)) )
assume A3: R satisfies_SIC_on C ; ::_thesis: for c being Element of L st c in C holds
c = sup (SetBelow (R,C,c))
let c be Element of L; ::_thesis: ( c in C implies c = sup (SetBelow (R,C,c)) )
assume A4: c in C ; ::_thesis: c = sup (SetBelow (R,C,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 sup (SetBelow (R,C,c)) = "\/" ((SetBelow (R,C,c)),(subrelstr C)) by A1, A5, Def9;
then sup (SetBelow (R,C,c)) in the carrier of (subrelstr C) ;
then A6: sup (SetBelow (R,C,c)) in C by YELLOW_0:def_15;
percases ( c = sup (SetBelow (R,C,c)) or c <> sup (SetBelow (R,C,c)) ) ;
suppose c = sup (SetBelow (R,C,c)) ; ::_thesis: c = sup (SetBelow (R,C,c))
hence c = sup (SetBelow (R,C,c)) ; ::_thesis: verum
end;
supposeA7: c <> sup (SetBelow (R,C,c)) ; ::_thesis: c = sup (SetBelow (R,C,c))
A8: now__::_thesis:_(_c_<_sup_(SetBelow_(R,C,c))_implies_c_=_sup_(SetBelow_(R,C,c))_)
assume A9: c < sup (SetBelow (R,C,c)) ; ::_thesis: c = sup (SetBelow (R,C,c))
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; ::_thesis: ( SetBelow (R,C,c) is_<=_than a implies c <= a )
assume SetBelow (R,C,c) is_<=_than a ; ::_thesis: c <= a
then A11: sup (SetBelow (R,C,c)) <= a by A5, YELLOW_0:def_9;
c <= sup (SetBelow (R,C,c)) by A9, ORDERS_2:def_6;
hence c <= a by A11, ORDERS_2:3; ::_thesis: verum
end;
SetBelow (R,C,c) is_<=_than c by Th16;
hence c = sup (SetBelow (R,C,c)) by A10, A5, YELLOW_0:def_9; ::_thesis: verum
end;
( [c,(sup (SetBelow (R,C,c)))] in R or [(sup (SetBelow (R,C,c))),c] in R ) by A7, A4, A6, Def3;
then ( c <= sup (SetBelow (R,C,c)) or [(sup (SetBelow (R,C,c))),c] in R ) by WAYBEL_4:def_3;
then consider y being Element of L such that
A12: y in C and
[(sup (SetBelow (R,C,c))),y] in R and
A13: [y,c] in R and
A14: sup (SetBelow (R,C,c)) < y by A8, A3, A4, A6, A7, Th13, ORDERS_2:def_6;
y in SetBelow (R,C,c) by A12, A13, Th15;
hence c = sup (SetBelow (R,C,c)) by A5, A14, ORDERS_2:6, YELLOW_4:1; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL35:21
for L being non empty reflexive antisymmetric RelStr
for R being auxiliary(i) Relation of L
for 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 ; ::_thesis: for R being auxiliary(i) Relation of L
for 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
let R be auxiliary(i) Relation of L; ::_thesis: for 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
let C be strict_chain of R; ::_thesis: ( ( 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)) ) ) implies R satisfies_SIC_on C )
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)) ) ; ::_thesis: R satisfies_SIC_on C
let x, z be Element of L; :: according to WAYBEL35:def_6 ::_thesis: ( 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 ) )
assume that
A2: x in C and
A3: z in C and
A4: [x,z] in R and
A5: x <> z ; ::_thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
A6: z = sup (SetBelow (R,C,z)) by A1, A3;
percases ( for y being Element of L holds
( not y in SetBelow (R,C,z) or not x < y ) or ex y being Element of L st
( y in SetBelow (R,C,z) & x < y ) ) ;
supposeA7: for y being Element of L holds
( not y in SetBelow (R,C,z) or not x < y ) ; ::_thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
reconsider x = x as Element of L ;
A8: SetBelow (R,C,z) is_<=_than x
proof
let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in SetBelow (R,C,z) or b <= x )
assume A9: b in SetBelow (R,C,z) ; ::_thesis: b <= x
then A10: not x < b by A7;
percases ( x <> b or x = b ) ;
supposeA11: x <> b ; ::_thesis: b <= x
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; ::_thesis: verum
end;
suppose x = b ; ::_thesis: b <= x
hence b <= x ; ::_thesis: verum
end;
end;
end;
A13: for a being Element of L st SetBelow (R,C,z) is_<=_than a holds
x <= a
proof
A14: x in SetBelow (R,C,z) by A2, A4, Th15;
let a be Element of L; ::_thesis: ( SetBelow (R,C,z) is_<=_than a implies x <= a )
assume SetBelow (R,C,z) is_<=_than a ; ::_thesis: x <= a
hence x <= a by A14, LATTICE3:def_9; ::_thesis: verum
end;
ex_sup_of SetBelow (R,C,z),L by A1, A3;
hence ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y ) by A13, A5, A6, A8, YELLOW_0:def_9; ::_thesis: verum
end;
suppose ex y being Element of L st
( y in SetBelow (R,C,z) & x < y ) ; ::_thesis: ex y being Element of L st
( y in C & [x,y] in R & [y,z] in R & x <> y )
then consider y being Element of L such that
A15: y in SetBelow (R,C,z) and
A16: x < y ;
take y ; ::_thesis: ( y in C & [x,y] in R & [y,z] in R & x <> y )
thus y in C by A15, Th15; ::_thesis: ( [x,y] in R & [y,z] in R & x <> y )
hence [x,y] in R by A2, A16, Th2; ::_thesis: ( [y,z] in R & x <> y )
thus [y,z] in R by A15, Th15; ::_thesis: x <> y
thus x <> y by A16; ::_thesis: verum
end;
end;
end;
definition
let L be non empty RelStr ;
let R be Relation of the carrier of L;
let C be set ;
defpred S1[ set ] means $1 = sup (SetBelow (R,C,$1));
func SupBelow (R,C) -> set means :Def10: :: WAYBEL35:def 10
for y being set holds
( y in it iff y = sup (SetBelow (R,C,y)) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff y = sup (SetBelow (R,C,y)) )
proof
consider X being set such that
A1: for x being set holds
( x in X iff ( x in the carrier of L & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for y being set holds
( y in X iff y = sup (SetBelow (R,C,y)) )
thus for y being set holds
( y in X iff y = sup (SetBelow (R,C,y)) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff y = sup (SetBelow (R,C,y)) ) ) & ( for y being set holds
( y in b2 iff y = sup (SetBelow (R,C,y)) ) ) holds
b1 = b2
proof
thus for X1, X2 being set st ( for x being set holds
( x in X1 iff S1[x] ) ) & ( for x being set holds
( x in X2 iff S1[x] ) ) holds
X1 = X2 from XBOOLE_0:sch_3(); ::_thesis: verum
end;
end;
:: deftheorem Def10 defines SupBelow WAYBEL35:def_10_:_
for L being non empty RelStr
for R being Relation of the carrier of L
for C being set
for b4 being set holds
( b4 = SupBelow (R,C) iff for y being set holds
( y in b4 iff y = sup (SetBelow (R,C,y)) ) );
definition
let L be non empty RelStr ;
let R be Relation of the carrier of L;
let C be set ;
:: original: SupBelow
redefine func SupBelow (R,C) -> Subset of L;
coherence
SupBelow (R,C) is Subset of L
proof
SupBelow (R,C) c= the carrier of L
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SupBelow (R,C) or x in the carrier of L )
assume x in SupBelow (R,C) ; ::_thesis: x in the carrier of L
then x = sup (SetBelow (R,C,x)) by Def10;
hence x in the carrier of L ; ::_thesis: verum
end;
hence SupBelow (R,C) is Subset of L ; ::_thesis: verum
end;
end;
theorem Th22: :: WAYBEL35:22
for L being non empty reflexive transitive RelStr
for R being auxiliary(i) auxiliary(ii) Relation of L
for 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 ; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for 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
let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for 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
let C be strict_chain of R; ::_thesis: ( ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) implies SupBelow (R,C) is strict_chain of R )
assume A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ; ::_thesis: SupBelow (R,C) is strict_chain of R
thus SupBelow (R,C) is strict_chain of R ::_thesis: verum
proof
let a, b be set ; :: according to WAYBEL35:def_3 ::_thesis: ( a in SupBelow (R,C) & b in SupBelow (R,C) & not [a,b] in R & not a = b implies [b,a] in R )
assume A2: a in SupBelow (R,C) ; ::_thesis: ( not b in SupBelow (R,C) or [a,b] in R or a = b or [b,a] in R )
then A3: a = sup (SetBelow (R,C,a)) by Def10;
reconsider a = 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) ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
then A7: b = sup (SetBelow (R,C,b)) by Def10;
reconsider b = b as Element of L by A6;
A8: b <= b ;
A9: ex_sup_of SetBelow (R,C,b),L by A1;
percases ( a = b or a <> b ) ;
suppose a = b ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
hence ( [a,b] in R or a = b or [b,a] in R ) ; ::_thesis: verum
end;
supposeA10: a <> b ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
( ( 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 ) ; ::_thesis: a = b
SetBelow (R,C,a) = SetBelow (R,C,b)
proof
thus SetBelow (R,C,a) c= SetBelow (R,C,b) :: according to XBOOLE_0:def_10 ::_thesis: SetBelow (R,C,b) c= SetBelow (R,C,a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetBelow (R,C,a) or x in SetBelow (R,C,b) )
assume A12: x in SetBelow (R,C,a) ; ::_thesis: x in SetBelow (R,C,b)
then reconsider x = 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 x in SetBelow (R,C,b) by A13, Th15; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SetBelow (R,C,b) or x in SetBelow (R,C,a) )
assume A14: x in SetBelow (R,C,b) ; ::_thesis: x in SetBelow (R,C,a)
then reconsider x = 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 x in SetBelow (R,C,a) by A15, Th15; ::_thesis: verum
end;
hence a = b by A2, A7, Def10; ::_thesis: verum
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 ( [a,b] in R or a = b or [b,a] in R ) ::_thesis: verum
proof
percases ( ( [x,a] in R & not [x,b] in R ) or ( not [x,a] in R & [x,b] in R ) ) by A17;
supposethat A19: [x,a] in R and
A20: not [x,b] in R ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
SetBelow (R,C,b) is_<=_than x
proof
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in SetBelow (R,C,b) or y <= x )
assume A21: y in SetBelow (R,C,b) ; ::_thesis: y <= x
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, WAYBEL_4:def_4; ::_thesis: verum
end;
then b <= x by A7, A9, YELLOW_0:def_9;
hence ( [a,b] in R or a = b or [b,a] in R ) by A4, A19, WAYBEL_4:def_4; ::_thesis: verum
end;
supposethat A23: not [x,a] in R and
A24: [x,b] in R ; ::_thesis: ( [a,b] in R or a = b or [b,a] in R )
SetBelow (R,C,a) is_<=_than x
proof
let y be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not y in SetBelow (R,C,a) or y <= x )
assume A25: y in SetBelow (R,C,a) ; ::_thesis: y <= x
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, WAYBEL_4:def_4; ::_thesis: verum
end;
then a <= x by A3, A5, YELLOW_0:def_9;
hence ( [a,b] in R or a = b or [b,a] in R ) by A8, A24, WAYBEL_4:def_4; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
theorem :: WAYBEL35:23
for L being non empty Poset
for R being auxiliary(i) auxiliary(ii) Relation of L
for 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; ::_thesis: for R being auxiliary(i) auxiliary(ii) Relation of L
for 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
let R be auxiliary(i) auxiliary(ii) Relation of L; ::_thesis: for 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
let C be Subset of L; ::_thesis: ( ( for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ) implies SupBelow (R,C) is sup-closed )
assume A1: for c being Element of L holds ex_sup_of SetBelow (R,C,c),L ; ::_thesis: SupBelow (R,C) is sup-closed
let X be Subset of (SupBelow (R,C)); :: according to WAYBEL35:def_9 ::_thesis: ( ex_sup_of X,L implies "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) )
set s = "\/" (X,L);
assume A2: ex_sup_of X,L ; ::_thesis: "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C))))
A3: ex_sup_of SetBelow (R,C,("\/" (X,L))),L by A1;
X is_<=_than sup (SetBelow (R,C,("\/" (X,L))))
proof
let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in X or x <= sup (SetBelow (R,C,("\/" (X,L)))) )
A4: ex_sup_of SetBelow (R,C,x),L by A1;
assume A5: x in X ; ::_thesis: x <= sup (SetBelow (R,C,("\/" (X,L))))
then A6: x = sup (SetBelow (R,C,x)) by Def10;
SetBelow (R,C,x) c= SetBelow (R,C,("\/" (X,L))) by A2, A5, Th17, YELLOW_4:1;
hence x <= sup (SetBelow (R,C,("\/" (X,L)))) by A3, A6, A4, YELLOW_0:34; ::_thesis: verum
end;
then A7: "\/" (X,L) <= sup (SetBelow (R,C,("\/" (X,L)))) 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,("\/" (X,L))) is_<=_than "\/" (X,L) by Th16;
then sup (SetBelow (R,C,("\/" (X,L)))) <= "\/" (X,L) by A3, YELLOW_0:def_9;
then "\/" (X,L) = sup (SetBelow (R,C,("\/" (X,L)))) by A7, ORDERS_2:2;
then "\/" (X,L) in SupBelow (R,C) by Def10;
hence "\/" (X,L) = "\/" (X,(subrelstr (SupBelow (R,C)))) by A8, A2, YELLOW_0:64; ::_thesis: verum
end;
theorem Th24: :: WAYBEL35:24
for L being non empty complete Poset
for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for 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 non empty complete Poset; ::_thesis: for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for 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)
let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R
for 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)
let C be satisfying_SIC strict_chain of R; ::_thesis: for 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)
let d be Element of L; ::_thesis: ( d in SupBelow (R,C) implies d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L) )
deffunc H1( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,$1] in R ) } ;
set p = "\/" (H1(d),L);
A1: ex_sup_of SetBelow (R,C,d),L by YELLOW_0:17;
A2: H1(d) is_<=_than d
proof
let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in H1(d) or a <= d )
assume a in H1(d) ; ::_thesis: a <= 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; ::_thesis: verum
end;
assume d in SupBelow (R,C) ; ::_thesis: d = "\/" ( { b where b is Element of L : ( b in SupBelow (R,C) & [b,d] in R ) } ,L)
then A3: d = sup (SetBelow (R,C,d)) by Def10;
assume A4: "\/" (H1(d),L) <> d ; ::_thesis: contradiction
ex_sup_of H1(d),L by YELLOW_0:17;
then "\/" (H1(d),L) <= d by A2, YELLOW_0:def_9;
then A5: "\/" (H1(d),L) < d by A4, ORDERS_2:def_6;
now__::_thesis:_ex_a_being_Element_of_L_st_
(_a_in_C_&_[a,d]_in_R_&_not_a_<=_"\/"_(H1(d),L)_)
percases ( not SetBelow (R,C,d) is_<=_than "\/" (H1(d),L) or ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not "\/" (H1(d),L) <= a ) ) by A3, A1, A4, YELLOW_0:def_9;
suppose not SetBelow (R,C,d) is_<=_than "\/" (H1(d),L) ; ::_thesis: ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) )
then consider a being Element of L such that
A6: a in SetBelow (R,C,d) and
A7: not a <= "\/" (H1(d),L) by LATTICE3:def_9;
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 <= "\/" (H1(d),L) ) by A8, A7; ::_thesis: verum
end;
suppose ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not "\/" (H1(d),L) <= a ) ; ::_thesis: ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) )
then consider a being Element of L such that
A9: SetBelow (R,C,d) is_<=_than a and
A10: not "\/" (H1(d),L) <= a ;
d <= a by A3, A1, A9, YELLOW_0:def_9;
then "\/" (H1(d),L) < a by A5, ORDERS_2:7;
hence ex a being Element of L st
( a in C & [a,d] in R & not a <= "\/" (H1(d),L) ) by A10, ORDERS_2:def_6; ::_thesis: verum
end;
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 <= "\/" (H1(d),L) ;
percases ( [cc,cc] in R or not [cc,cc] in R ) ;
suppose [cc,cc] in R ; ::_thesis: contradiction
then cc = sup (SetBelow (R,C,cc)) by A11, Th18, YELLOW_0:17;
then cc in SupBelow (R,C) by Def10;
then cc in H1(d) by A12;
hence contradiction by A13, YELLOW_0:17, YELLOW_4:1; ::_thesis: verum
end;
supposeA14: not [cc,cc] in R ; ::_thesis: contradiction
ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R )
proof
percases ( not SetBelow (R,C,d) is_<=_than cc or ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not cc <= a ) ) by A3, A1, A12, A14, YELLOW_0:def_9;
suppose not SetBelow (R,C,d) is_<=_than cc ; ::_thesis: ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R )
then consider cs being Element of L such that
A15: cs in SetBelow (R,C,d) and
A16: not cs <= cc by LATTICE3:def_9;
take cs ; ::_thesis: ( cs in C & cc < cs & [cs,d] in R )
A17: not [cs,cc] in R by A16, WAYBEL_4:def_3;
thus cs in C by A15, Th15; ::_thesis: ( cc < cs & [cs,d] in R )
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; ::_thesis: [cs,d] in R
thus [cs,d] in R by A15, Th15; ::_thesis: verum
end;
supposeA18: ex a being Element of L st
( SetBelow (R,C,d) is_<=_than a & not cc <= a ) ; ::_thesis: ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R )
cc in SetBelow (R,C,d) by A11, A12, Th15;
hence ex cs being Element of L st
( cs in C & cc < cs & [cs,d] in R ) by A18, LATTICE3:def_9; ::_thesis: verum
end;
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 H1(d) by A25;
then y <= "\/" (H1(d),L) by YELLOW_0:17, YELLOW_4:1;
then cc < "\/" (H1(d),L) by A22, ORDERS_2:7;
hence contradiction by A13, ORDERS_2:def_6; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL35:25
for L being non empty complete Poset
for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C)
proof
let L be non empty complete Poset; ::_thesis: for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C)
let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow (R,C)
let C be satisfying_SIC strict_chain of R; ::_thesis: R satisfies_SIC_on SupBelow (R,C)
let c, d be Element of L; :: according to WAYBEL35:def_6 ::_thesis: ( c in SupBelow (R,C) & d in SupBelow (R,C) & [c,d] in R & c <> d implies ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) )
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 ; ::_thesis: ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y )
A5: c <= d by A3, WAYBEL_4:def_3;
deffunc H1( Element of L) -> set = { b where b is Element of L : ( b in SupBelow (R,C) & [b,$1] in R ) } ;
A6: d = "\/" (H1(d),L) by A2, Th24;
A7: ex_sup_of H1(d),L by YELLOW_0:17;
percases ( not H1(d) is_<=_than c or ex g being Element of L st
( H1(d) is_<=_than g & not c <= g ) ) by A4, A6, A7, YELLOW_0:def_9;
suppose not H1(d) is_<=_than c ; ::_thesis: ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y )
then consider g being Element of L such that
A8: g in H1(d) and
A9: not g <= c by LATTICE3:def_9;
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 = y as Element of L ;
take y ; ::_thesis: ( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y )
thus y in SupBelow (R,C) by A11; ::_thesis: ( [c,y] in R & [y,d] in R & c <> y )
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; ::_thesis: ( [y,d] in R & c <> y )
thus [y,d] in R by A12; ::_thesis: c <> y
thus c <> y by A9, A10; ::_thesis: verum
end;
suppose ex g being Element of L st
( H1(d) is_<=_than g & not c <= g ) ; ::_thesis: ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y )
then consider g being Element of L such that
A13: H1(d) is_<=_than g and
A14: not c <= g ;
d <= g by A6, A7, A13, YELLOW_0:def_9;
hence ex y being Element of L st
( y in SupBelow (R,C) & [c,y] in R & [y,d] in R & c <> y ) by A5, A14, ORDERS_2:3; ::_thesis: verum
end;
end;
end;
theorem :: WAYBEL35:26
for L being non empty complete Poset
for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for a, b being Element of L st a in C & b in C & a < b holds
ex d being Element of L st
( d in SupBelow (R,C) & a < d & [d,b] in R )
proof
let L be non empty complete Poset; ::_thesis: for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for a, b being Element of L st a in C & b in C & a < b holds
ex d being Element of L st
( d in SupBelow (R,C) & a < d & [d,b] in R )
let R be extra-order Relation of L; ::_thesis: for C being satisfying_SIC strict_chain of R
for a, b being Element of L st a in C & b in C & a < b holds
ex d being Element of L st
( d in SupBelow (R,C) & a < d & [d,b] in R )
let C be satisfying_SIC strict_chain of R; ::_thesis: for a, b being Element of L st a in C & b in C & a < b holds
ex d being Element of L st
( d in SupBelow (R,C) & a < d & [d,b] in R )
let a, b be Element of L; ::_thesis: ( a in C & b in C & a < b implies ex d being Element of L st
( d in SupBelow (R,C) & a < d & [d,b] in R ) )
assume that
A1: a in C and
A2: b in C and
A3: a < b ; ::_thesis: ex d being Element of L st
( d in SupBelow (R,C) & a < d & [d,b] in R )
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 ; ::_thesis: ( d in SupBelow (R,C) & a < d & [d,b] in R )
thus ( d in SupBelow (R,C) & a < d & [d,b] in R ) by A4, A5, A6, Def10; ::_thesis: verum
end;