:: ORDERS_2 semantic presentation
begin
definition
attrc1 is strict ;
struct RelStr -> 1-sorted ;
aggrRelStr(# carrier, InternalRel #) -> RelStr ;
sel InternalRel c1 -> Relation of the carrier of c1;
end;
registration
let X be non empty set ;
let R be Relation of X;
cluster RelStr(# X,R #) -> non empty ;
coherence
not RelStr(# X,R #) is empty ;
end;
definition
let A be RelStr ;
attrA is total means :Def1: :: ORDERS_2:def 1
the InternalRel of A is total ;
attrA is reflexive means :Def2: :: ORDERS_2:def 2
the InternalRel of A is_reflexive_in the carrier of A;
attrA is transitive means :Def3: :: ORDERS_2:def 3
the InternalRel of A is_transitive_in the carrier of A;
attrA is antisymmetric means :Def4: :: ORDERS_2:def 4
the InternalRel of A is_antisymmetric_in the carrier of A;
end;
:: deftheorem Def1 defines total ORDERS_2:def_1_:_
for A being RelStr holds
( A is total iff the InternalRel of A is total );
:: deftheorem Def2 defines reflexive ORDERS_2:def_2_:_
for A being RelStr holds
( A is reflexive iff the InternalRel of A is_reflexive_in the carrier of A );
:: deftheorem Def3 defines transitive ORDERS_2:def_3_:_
for A being RelStr holds
( A is transitive iff the InternalRel of A is_transitive_in the carrier of A );
:: deftheorem Def4 defines antisymmetric ORDERS_2:def_4_:_
for A being RelStr holds
( A is antisymmetric iff the InternalRel of A is_antisymmetric_in the carrier of A );
registration
cluster1 -element strict total reflexive transitive antisymmetric for RelStr ;
existence
ex b1 being RelStr st
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is strict & b1 is total & b1 is 1 -element )
proof
set R = the Order of {{}};
take L = RelStr(# {{}}, the Order of {{}} #); ::_thesis: ( L is reflexive & L is transitive & L is antisymmetric & L is strict & L is total & L is 1 -element )
A1: field the Order of {{}} = the carrier of L by ORDERS_1:12;
hence the InternalRel of L is_reflexive_in the carrier of L by RELAT_2:def_9; :: according to ORDERS_2:def_2 ::_thesis: ( L is transitive & L is antisymmetric & L is strict & L is total & L is 1 -element )
thus the InternalRel of L is_transitive_in the carrier of L by A1, RELAT_2:def_16; :: according to ORDERS_2:def_3 ::_thesis: ( L is antisymmetric & L is strict & L is total & L is 1 -element )
thus the InternalRel of L is_antisymmetric_in the carrier of L by A1, RELAT_2:def_12; :: according to ORDERS_2:def_4 ::_thesis: ( L is strict & L is total & L is 1 -element )
thus L is strict ; ::_thesis: ( L is total & L is 1 -element )
thus the InternalRel of L is total ; :: according to ORDERS_2:def_1 ::_thesis: L is 1 -element
thus the carrier of L is 1 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;
registration
cluster reflexive -> total for RelStr ;
coherence
for b1 being RelStr st b1 is reflexive holds
b1 is total
proof
let L be RelStr ; ::_thesis: ( L is reflexive implies L is total )
assume L is reflexive ; ::_thesis: L is total
then the InternalRel of L is_reflexive_in the carrier of L by Def2;
then dom the InternalRel of L = the carrier of L by ORDERS_1:13;
hence the InternalRel of L is total by PARTFUN1:def_2; :: according to ORDERS_2:def_1 ::_thesis: verum
end;
end;
definition
mode Poset is reflexive transitive antisymmetric RelStr ;
end;
registration
let A be total RelStr ;
cluster the InternalRel of A -> total ;
coherence
the InternalRel of A is total by Def1;
end;
registration
let A be reflexive RelStr ;
cluster the InternalRel of A -> reflexive ;
coherence
the InternalRel of A is reflexive
proof
set R = the InternalRel of A;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then A1: field the InternalRel of A = the carrier of A by ORDERS_1:13;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
hence the InternalRel of A is reflexive by A1, RELAT_2:def_9; ::_thesis: verum
end;
end;
registration
let A be total antisymmetric RelStr ;
cluster the InternalRel of A -> antisymmetric ;
coherence
the InternalRel of A is antisymmetric
proof
set R = the InternalRel of A;
( field the InternalRel of A = the carrier of A & the InternalRel of A is_antisymmetric_in the carrier of A ) by Def4, ORDERS_1:12;
hence the InternalRel of A is antisymmetric by RELAT_2:def_12; ::_thesis: verum
end;
end;
registration
let A be total transitive RelStr ;
cluster the InternalRel of A -> transitive ;
coherence
the InternalRel of A is transitive
proof
set R = the InternalRel of A;
( field the InternalRel of A = the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def3, ORDERS_1:12;
hence the InternalRel of A is transitive by RELAT_2:def_16; ::_thesis: verum
end;
end;
registration
let X be set ;
let O be reflexive total Relation of X;
cluster RelStr(# X,O #) -> reflexive ;
coherence
RelStr(# X,O #) is reflexive
proof
set A = RelStr(# X,O #);
field O = X by ORDERS_1:12;
hence the InternalRel of RelStr(# X,O #) is_reflexive_in the carrier of RelStr(# X,O #) by RELAT_2:def_9; :: according to ORDERS_2:def_2 ::_thesis: verum
end;
end;
registration
let X be set ;
let O be transitive total Relation of X;
cluster RelStr(# X,O #) -> transitive ;
coherence
RelStr(# X,O #) is transitive
proof
set A = RelStr(# X,O #);
field O = X by ORDERS_1:12;
hence the InternalRel of RelStr(# X,O #) is_transitive_in the carrier of RelStr(# X,O #) by RELAT_2:def_16; :: according to ORDERS_2:def_3 ::_thesis: verum
end;
end;
registration
let X be set ;
let O be antisymmetric total Relation of X;
cluster RelStr(# X,O #) -> antisymmetric ;
coherence
RelStr(# X,O #) is antisymmetric
proof
set A = RelStr(# X,O #);
field O = X by ORDERS_1:12;
hence the InternalRel of RelStr(# X,O #) is_antisymmetric_in the carrier of RelStr(# X,O #) by RELAT_2:def_12; :: according to ORDERS_2:def_4 ::_thesis: verum
end;
end;
Lm1: for x being set
for A being non empty Poset
for S being Subset of A st x in S holds
x is Element of A
;
definition
let A be RelStr ;
let a1, a2 be Element of A;
preda1 <= a2 means :Def5: :: ORDERS_2:def 5
[a1,a2] in the InternalRel of A;
end;
:: deftheorem Def5 defines <= ORDERS_2:def_5_:_
for A being RelStr
for a1, a2 being Element of A holds
( a1 <= a2 iff [a1,a2] in the InternalRel of A );
notation
let A be RelStr ;
let a1, a2 be Element of A;
synonym a2 >= a1 for a1 <= a2;
end;
definition
let A be RelStr ;
let a1, a2 be Element of A;
preda1 < a2 means :Def6: :: ORDERS_2:def 6
( a1 <= a2 & a1 <> a2 );
irreflexivity
for a1 being Element of A holds
( not a1 <= a1 or not a1 <> a1 ) ;
end;
:: deftheorem Def6 defines < ORDERS_2:def_6_:_
for A being RelStr
for a1, a2 being Element of A holds
( a1 < a2 iff ( a1 <= a2 & a1 <> a2 ) );
notation
let A be RelStr ;
let a1, a2 be Element of A;
synonym a2 > a1 for a1 < a2;
end;
theorem Th1: :: ORDERS_2:1
for A being non empty reflexive RelStr
for a being Element of A holds a <= a
proof
let A be non empty reflexive RelStr ; ::_thesis: for a being Element of A holds a <= a
let a be Element of A; ::_thesis: a <= a
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then [a,a] in the InternalRel of A by RELAT_2:def_1;
hence a <= a by Def5; ::_thesis: verum
end;
definition
let A be non empty reflexive RelStr ;
let a1, a2 be Element of A;
:: original: <=
redefine preda1 <= a2;
reflexivity
for a1 being Element of A holds (A,b1,b1) by Th1;
end;
theorem Th2: :: ORDERS_2:2
for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 & a2 <= a1 holds
a1 = a2
proof
let A be antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A st a1 <= a2 & a2 <= a1 holds
a1 = a2
let a1, a2 be Element of A; ::_thesis: ( a1 <= a2 & a2 <= a1 implies a1 = a2 )
assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a1] in the InternalRel of A ; :: according to ORDERS_2:def_5 ::_thesis: a1 = a2
A3: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
a1 in the carrier of A by A1, ZFMISC_1:87;
hence a1 = a2 by A1, A2, A3, RELAT_2:def_4; ::_thesis: verum
end;
theorem Th3: :: ORDERS_2:3
for A being transitive RelStr
for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds
a1 <= a3
proof
let A be transitive RelStr ; ::_thesis: for a1, a2, a3 being Element of A st a1 <= a2 & a2 <= a3 holds
a1 <= a3
let a1, a2, a3 be Element of A; ::_thesis: ( a1 <= a2 & a2 <= a3 implies a1 <= a3 )
assume that
A1: [a1,a2] in the InternalRel of A and
A2: [a2,a3] in the InternalRel of A ; :: according to ORDERS_2:def_5 ::_thesis: a1 <= a3
A3: the InternalRel of A is_transitive_in the carrier of A by Def3;
a1 in the carrier of A by A1, ZFMISC_1:87;
hence [a1,a3] in the InternalRel of A by A1, A2, A3, RELAT_2:def_8; :: according to ORDERS_2:def_5 ::_thesis: verum
end;
theorem Th4: :: ORDERS_2:4
for A being antisymmetric RelStr
for a1, a2 being Element of A holds
( not a1 < a2 or not a2 < a1 )
proof
let A be antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A holds
( not a1 < a2 or not a2 < a1 )
let a1, a2 be Element of A; ::_thesis: ( not a1 < a2 or not a2 < a1 )
assume that
A1: a1 < a2 and
A2: a2 < a1 ; ::_thesis: contradiction
( a1 <= a2 & a2 <= a1 ) by A1, A2, Def6;
hence contradiction by A1, Th2; ::_thesis: verum
end;
theorem Th5: :: ORDERS_2:5
for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds
a1 < a3
proof
let A be transitive antisymmetric RelStr ; ::_thesis: for a1, a2, a3 being Element of A st a1 < a2 & a2 < a3 holds
a1 < a3
let a1, a2, a3 be Element of A; ::_thesis: ( a1 < a2 & a2 < a3 implies a1 < a3 )
assume A1: ( a1 < a2 & a2 < a3 ) ; ::_thesis: a1 < a3
then ( a1 <= a2 & a2 <= a3 ) by Def6;
hence a1 <= a3 by Th3; :: according to ORDERS_2:def_6 ::_thesis: a1 <> a3
thus a1 <> a3 by A1, Th4; ::_thesis: verum
end;
theorem Th6: :: ORDERS_2:6
for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1
proof
let A be antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1
let a1, a2 be Element of A; ::_thesis: ( a1 <= a2 implies not a2 < a1 )
assume that
A1: a1 <= a2 and
A2: a2 < a1 ; ::_thesis: contradiction
a2 <= a1 by A2, Def6;
hence contradiction by A1, A2, Th2; ::_thesis: verum
end;
theorem Th7: :: ORDERS_2:7
for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) holds
a1 < a3
proof
let A be transitive antisymmetric RelStr ; ::_thesis: for a1, a2, a3 being Element of A st ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) holds
a1 < a3
let a1, a2, a3 be Element of A; ::_thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
A1: now__::_thesis:_(_a1_<_a2_&_a2_<=_a3_&_(_(_a1_<_a2_&_a2_<=_a3_)_or_(_a1_<=_a2_&_a2_<_a3_)_)_implies_a1_<_a3_)
assume that
A2: a1 < a2 and
A3: a2 <= a3 ; ::_thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
a1 <= a2 by A2, Def6;
then ( a1 <= a3 & a1 <> a3 ) by A2, A3, Th2, Th3;
hence ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 ) by Def6; ::_thesis: verum
end;
A4: now__::_thesis:_(_a1_<=_a2_&_a2_<_a3_&_(_(_a1_<_a2_&_a2_<=_a3_)_or_(_a1_<=_a2_&_a2_<_a3_)_)_implies_a1_<_a3_)
assume that
A5: a1 <= a2 and
A6: a2 < a3 ; ::_thesis: ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 )
a2 <= a3 by A6, Def6;
then ( a1 <= a3 & a1 <> a3 ) by A5, A6, Th2, Th3;
hence ( ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) implies a1 < a3 ) by Def6; ::_thesis: verum
end;
assume ( ( a1 < a2 & a2 <= a3 ) or ( a1 <= a2 & a2 < a3 ) ) ; ::_thesis: a1 < a3
hence a1 < a3 by A1, A4; ::_thesis: verum
end;
definition
let A be RelStr ;
let IT be Subset of A;
attrIT is strongly_connected means :Def7: :: ORDERS_2:def 7
the InternalRel of A is_strongly_connected_in IT;
end;
:: deftheorem Def7 defines strongly_connected ORDERS_2:def_7_:_
for A being RelStr
for IT being Subset of A holds
( IT is strongly_connected iff the InternalRel of A is_strongly_connected_in IT );
registration
let A be RelStr ;
cluster empty -> strongly_connected for Element of bool the carrier of A;
coherence
for b1 being Subset of A st b1 is empty holds
b1 is strongly_connected
proof
let S be Subset of A; ::_thesis: ( S is empty implies S is strongly_connected )
assume S is empty ; ::_thesis: S is strongly_connected
then A1: S = {} A ;
let x1, x2 be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: ( not x1 in S or not x2 in S or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
thus ( not x1 in S or not x2 in S or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A ) by A1; ::_thesis: verum
end;
end;
registration
let A be RelStr ;
cluster strongly_connected for Element of bool the carrier of A;
existence
ex b1 being Subset of A st b1 is strongly_connected
proof
take {} A ; ::_thesis: {} A is strongly_connected
thus {} A is strongly_connected ; ::_thesis: verum
end;
end;
definition
let A be RelStr ;
mode Chain of A is strongly_connected Subset of A;
end;
theorem Th8: :: ORDERS_2:8
for A being non empty reflexive RelStr
for a being Element of A holds {a} is Chain of A
proof
let A be non empty reflexive RelStr ; ::_thesis: for a being Element of A holds {a} is Chain of A
let a be Element of A; ::_thesis: {a} is Chain of A
A1: the InternalRel of A is_reflexive_in the carrier of A by Def2;
{a} is strongly_connected
proof
let x1, x2 be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: ( not x1 in {a} or not x2 in {a} or [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
assume ( x1 in {a} & x2 in {a} ) ; ::_thesis: ( [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A )
then ( x1 = a & x2 = a ) by TARSKI:def_1;
hence ( [x1,x2] in the InternalRel of A or [x2,x1] in the InternalRel of A ) by A1, RELAT_2:def_1; ::_thesis: verum
end;
hence {a} is Chain of A ; ::_thesis: verum
end;
theorem Th9: :: ORDERS_2:9
for A being non empty reflexive RelStr
for a1, a2 being Element of A holds
( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
proof
let A be non empty reflexive RelStr ; ::_thesis: for a1, a2 being Element of A holds
( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
let a1, a2 be Element of A; ::_thesis: ( {a1,a2} is Chain of A iff ( a1 <= a2 or a2 <= a1 ) )
A1: a2 <= a2 ;
thus ( not {a1,a2} is Chain of A or a1 <= a2 or a2 <= a1 ) ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Chain of A )
proof
assume {a1,a2} is Chain of A ; ::_thesis: ( a1 <= a2 or a2 <= a1 )
then A2: the InternalRel of A is_strongly_connected_in {a1,a2} by Def7;
( a1 in {a1,a2} & a2 in {a1,a2} ) by TARSKI:def_2;
then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A2, RELAT_2:def_7;
hence ( a1 <= a2 or a2 <= a1 ) by Def5; ::_thesis: verum
end;
assume A3: ( a1 <= a2 or a2 <= a1 ) ; ::_thesis: {a1,a2} is Chain of A
A4: a1 <= a1 ;
{a1,a2} is strongly_connected
proof
let x be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: for b1 being set holds
( not x in {a1,a2} or not b1 in {a1,a2} or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in {a1,a2} or not y in {a1,a2} or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A5: ( x in {a1,a2} & y in {a1,a2} ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( ( x = a1 & y = a1 ) or ( x = a1 & y = a2 ) or ( x = a2 & y = a1 ) or ( x = a2 & y = a2 ) ) by A5, TARSKI:def_2;
suppose ( x = a1 & y = a1 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A4, Def5; ::_thesis: verum
end;
suppose ( x = a1 & y = a2 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, Def5; ::_thesis: verum
end;
suppose ( x = a2 & y = a1 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, Def5; ::_thesis: verum
end;
suppose ( x = a2 & y = a2 ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A1, Def5; ::_thesis: verum
end;
end;
end;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
hence {a1,a2} is Chain of A ; ::_thesis: verum
end;
theorem :: ORDERS_2:10
for A being RelStr
for C being Chain of A
for S being Subset of A st S c= C holds
S is Chain of A
proof
let A be RelStr ; ::_thesis: for C being Chain of A
for S being Subset of A st S c= C holds
S is Chain of A
let C be Chain of A; ::_thesis: for S being Subset of A st S c= C holds
S is Chain of A
let S be Subset of A; ::_thesis: ( S c= C implies S is Chain of A )
assume A1: S c= C ; ::_thesis: S is Chain of A
the InternalRel of A is_strongly_connected_in C by Def7;
then the InternalRel of A is_strongly_connected_in S by A1, ORDERS_1:11;
hence S is Chain of A by Def7; ::_thesis: verum
end;
theorem Th11: :: ORDERS_2:11
for A being reflexive RelStr
for a1, a2 being Element of A holds
( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
proof
let A be reflexive RelStr ; ::_thesis: for a1, a2 being Element of A holds
( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
let a1, a2 be Element of A; ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) iff ex C being Chain of A st
( a1 in C & a2 in C ) )
thus ( for C being Chain of A holds
( not a1 in C or not a2 in C ) or a1 <= a2 or a2 <= a1 ) ::_thesis: ( ( a1 <= a2 or a2 <= a1 ) implies ex C being Chain of A st
( a1 in C & a2 in C ) )
proof
given C being Chain of A such that A1: ( a1 in C & a2 in C ) ; ::_thesis: ( a1 <= a2 or a2 <= a1 )
the InternalRel of A is_strongly_connected_in C by Def7;
then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by A1, RELAT_2:def_7;
hence ( a1 <= a2 or a2 <= a1 ) by Def5; ::_thesis: verum
end;
assume A2: ( a1 <= a2 or a2 <= a1 ) ; ::_thesis: ex C being Chain of A st
( a1 in C & a2 in C )
then ( [a1,a2] in the InternalRel of A or [a2,a1] in the InternalRel of A ) by Def5;
then reconsider B = A as non empty reflexive RelStr ;
reconsider b1 = a1, b2 = a2 as Element of B ;
reconsider Y = {b1,b2} as Chain of A by A2, Th9;
take Y ; ::_thesis: ( a1 in Y & a2 in Y )
thus ( a1 in Y & a2 in Y ) by TARSKI:def_2; ::_thesis: verum
end;
theorem Th12: :: ORDERS_2:12
for A being reflexive antisymmetric RelStr
for a1, a2 being Element of A holds
( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
proof
let A be reflexive antisymmetric RelStr ; ::_thesis: for a1, a2 being Element of A holds
( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
let a1, a2 be Element of A; ::_thesis: ( ex C being Chain of A st
( a1 in C & a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
thus ( ex C being Chain of A st
( a1 in C & a2 in C ) implies ( a1 < a2 iff not a2 <= a1 ) ) ::_thesis: not ( ( a1 < a2 implies not a2 <= a1 ) & ( not a2 <= a1 implies a1 < a2 ) & ( for C being Chain of A holds
( not a1 in C or not a2 in C ) ) )
proof
given C being Chain of A such that A1: ( a1 in C & a2 in C ) ; ::_thesis: ( a1 < a2 iff not a2 <= a1 )
thus ( a1 < a2 implies not a2 <= a1 ) by Th6; ::_thesis: ( not a2 <= a1 implies a1 < a2 )
assume that
A2: not a2 <= a1 and
A3: not a1 < a2 ; ::_thesis: contradiction
( not a1 <= a2 or a1 = a2 ) by A3, Def6;
hence contradiction by A1, A2, Th11; ::_thesis: verum
end;
assume ( a1 < a2 iff not a2 <= a1 ) ; ::_thesis: ex C being Chain of A st
( a1 in C & a2 in C )
then ( a1 <= a2 or a2 <= a1 ) by Def6;
hence ex C being Chain of A st
( a1 in C & a2 in C ) by Th11; ::_thesis: verum
end;
theorem Th13: :: ORDERS_2:13
for A being RelStr
for T being Subset of A st the InternalRel of A well_orders T holds
T is Chain of A
proof
let A be RelStr ; ::_thesis: for T being Subset of A st the InternalRel of A well_orders T holds
T is Chain of A
let T be Subset of A; ::_thesis: ( the InternalRel of A well_orders T implies T is Chain of A )
assume the InternalRel of A well_orders T ; ::_thesis: T is Chain of A
then ( the InternalRel of A is_connected_in T & the InternalRel of A is_reflexive_in T ) by WELLORD1:def_5;
then the InternalRel of A is_strongly_connected_in T by ORDERS_1:7;
hence T is Chain of A by Def7; ::_thesis: verum
end;
definition
let A be non empty Poset;
let S be Subset of A;
func UpperCone S -> Subset of A equals :: ORDERS_2:def 8
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ;
coherence
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } is Subset of A
proof
set T = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ;
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } c= the carrier of A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } or x in the carrier of A )
assume x in { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ; ::_thesis: x in the carrier of A
then ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in S holds
a2 < a1 ) ) ;
hence x in the carrier of A ; ::_thesis: verum
end;
hence { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } is Subset of A ; ::_thesis: verum
end;
end;
:: deftheorem defines UpperCone ORDERS_2:def_8_:_
for A being non empty Poset
for S being Subset of A holds UpperCone S = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a2 < a1 } ;
definition
let A be non empty Poset;
let S be Subset of A;
func LowerCone S -> Subset of A equals :: ORDERS_2:def 9
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } ;
coherence
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } is Subset of A
proof
set T = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } ;
{ a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } c= the carrier of A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } or x in the carrier of A )
assume x in { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } ; ::_thesis: x in the carrier of A
then ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in S holds
a1 < a2 ) ) ;
hence x in the carrier of A ; ::_thesis: verum
end;
hence { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } is Subset of A ; ::_thesis: verum
end;
end;
:: deftheorem defines LowerCone ORDERS_2:def_9_:_
for A being non empty Poset
for S being Subset of A holds LowerCone S = { a1 where a1 is Element of A : for a2 being Element of A st a2 in S holds
a1 < a2 } ;
theorem Th14: :: ORDERS_2:14
for A being non empty Poset holds UpperCone ({} A) = the carrier of A
proof
let A be non empty Poset; ::_thesis: UpperCone ({} A) = the carrier of A
thus UpperCone ({} A) c= the carrier of A ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of A c= UpperCone ({} A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A or x in UpperCone ({} A) )
assume x in the carrier of A ; ::_thesis: x in UpperCone ({} A)
then reconsider a = x as Element of A ;
for a2 being Element of A st a2 in {} A holds
a2 < a ;
hence x in UpperCone ({} A) ; ::_thesis: verum
end;
theorem :: ORDERS_2:15
for A being non empty Poset holds UpperCone ([#] A) = {}
proof
let A be non empty Poset; ::_thesis: UpperCone ([#] A) = {}
thus UpperCone ([#] A) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= UpperCone ([#] A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UpperCone ([#] A) or x in {} )
assume x in UpperCone ([#] A) ; ::_thesis: x in {}
then ex a being Element of A st
( x = a & ( for a2 being Element of A st a2 in [#] A holds
a2 < a ) ) ;
hence x in {} ; ::_thesis: verum
end;
thus {} c= UpperCone ([#] A) by XBOOLE_1:2; ::_thesis: verum
end;
theorem :: ORDERS_2:16
for A being non empty Poset holds LowerCone ({} A) = the carrier of A
proof
let A be non empty Poset; ::_thesis: LowerCone ({} A) = the carrier of A
thus LowerCone ({} A) c= the carrier of A ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of A c= LowerCone ({} A)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of A or x in LowerCone ({} A) )
assume x in the carrier of A ; ::_thesis: x in LowerCone ({} A)
then reconsider a = x as Element of A ;
for a2 being Element of A st a2 in {} A holds
a < a2 ;
hence x in LowerCone ({} A) ; ::_thesis: verum
end;
theorem :: ORDERS_2:17
for A being non empty Poset holds LowerCone ([#] A) = {}
proof
let A be non empty Poset; ::_thesis: LowerCone ([#] A) = {}
thus LowerCone ([#] A) c= {} :: according to XBOOLE_0:def_10 ::_thesis: {} c= LowerCone ([#] A)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in LowerCone ([#] A) or x in {} )
assume x in LowerCone ([#] A) ; ::_thesis: x in {}
then ex a being Element of A st
( x = a & ( for a2 being Element of A st a2 in [#] A holds
a < a2 ) ) ;
hence x in {} ; ::_thesis: verum
end;
thus {} c= LowerCone ([#] A) by XBOOLE_1:2; ::_thesis: verum
end;
theorem Th18: :: ORDERS_2:18
for A being non empty Poset
for a being Element of A
for S being Subset of A st a in S holds
not a in UpperCone S
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S being Subset of A st a in S holds
not a in UpperCone S
let a be Element of A; ::_thesis: for S being Subset of A st a in S holds
not a in UpperCone S
let S be Subset of A; ::_thesis: ( a in S implies not a in UpperCone S )
assume that
A1: a in S and
A2: a in UpperCone S ; ::_thesis: contradiction
ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in S holds
a2 < a1 ) ) by A2;
hence contradiction by A1; ::_thesis: verum
end;
theorem :: ORDERS_2:19
for A being non empty Poset
for a being Element of A holds not a in UpperCone {a}
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds not a in UpperCone {a}
let a be Element of A; ::_thesis: not a in UpperCone {a}
a in {a} by TARSKI:def_1;
hence not a in UpperCone {a} by Th18; ::_thesis: verum
end;
theorem Th20: :: ORDERS_2:20
for A being non empty Poset
for a being Element of A
for S being Subset of A st a in S holds
not a in LowerCone S
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S being Subset of A st a in S holds
not a in LowerCone S
let a be Element of A; ::_thesis: for S being Subset of A st a in S holds
not a in LowerCone S
let S be Subset of A; ::_thesis: ( a in S implies not a in LowerCone S )
assume that
A1: a in S and
A2: a in LowerCone S ; ::_thesis: contradiction
ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in S holds
a1 < a2 ) ) by A2;
hence contradiction by A1; ::_thesis: verum
end;
theorem Th21: :: ORDERS_2:21
for A being non empty Poset
for a being Element of A holds not a in LowerCone {a}
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds not a in LowerCone {a}
let a be Element of A; ::_thesis: not a in LowerCone {a}
a in {a} by TARSKI:def_1;
hence not a in LowerCone {a} by Th20; ::_thesis: verum
end;
theorem :: ORDERS_2:22
for A being non empty Poset
for c, a being Element of A holds
( c < a iff a in UpperCone {c} )
proof
let A be non empty Poset; ::_thesis: for c, a being Element of A holds
( c < a iff a in UpperCone {c} )
let c, a be Element of A; ::_thesis: ( c < a iff a in UpperCone {c} )
thus ( c < a implies a in UpperCone {c} ) ::_thesis: ( a in UpperCone {c} implies c < a )
proof
assume c < a ; ::_thesis: a in UpperCone {c}
then for b being Element of A st b in {c} holds
b < a by TARSKI:def_1;
hence a in UpperCone {c} ; ::_thesis: verum
end;
assume a in UpperCone {c} ; ::_thesis: c < a
then A1: ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in {c} holds
a2 < a1 ) ) ;
c in {c} by TARSKI:def_1;
hence c < a by A1; ::_thesis: verum
end;
theorem Th23: :: ORDERS_2:23
for A being non empty Poset
for a, c being Element of A holds
( a < c iff a in LowerCone {c} )
proof
let A be non empty Poset; ::_thesis: for a, c being Element of A holds
( a < c iff a in LowerCone {c} )
let a, c be Element of A; ::_thesis: ( a < c iff a in LowerCone {c} )
thus ( a < c implies a in LowerCone {c} ) ::_thesis: ( a in LowerCone {c} implies a < c )
proof
assume a < c ; ::_thesis: a in LowerCone {c}
then for b being Element of A st b in {c} holds
a < b by TARSKI:def_1;
hence a in LowerCone {c} ; ::_thesis: verum
end;
assume a in LowerCone {c} ; ::_thesis: a < c
then A1: ex a1 being Element of A st
( a1 = a & ( for a2 being Element of A st a2 in {c} holds
a1 < a2 ) ) ;
c in {c} by TARSKI:def_1;
hence a < c by A1; ::_thesis: verum
end;
definition
let A be non empty Poset;
let S be Subset of A;
let a be Element of A;
func InitSegm (S,a) -> Subset of A equals :: ORDERS_2:def 10
(LowerCone {a}) /\ S;
correctness
coherence
(LowerCone {a}) /\ S is Subset of A;
;
end;
:: deftheorem defines InitSegm ORDERS_2:def_10_:_
for A being non empty Poset
for S being Subset of A
for a being Element of A holds InitSegm (S,a) = (LowerCone {a}) /\ S;
definition
let A be non empty Poset;
let S be Subset of A;
mode Initial_Segm of S -> Subset of A means :Def11: :: ORDERS_2:def 11
ex a being Element of A st
( a in S & it = InitSegm (S,a) ) if S <> {}
otherwise it = {} ;
existence
( ( S <> {} implies ex b1 being Subset of A ex a being Element of A st
( a in S & b1 = InitSegm (S,a) ) ) & ( not S <> {} implies ex b1 being Subset of A st b1 = {} ) )
proof
now__::_thesis:_(_S_<>_{}_implies_ex_T_being_Subset_of_A_st_
(_(_S_<>_{}_implies_ex_a_being_Element_of_A_st_
(_a_in_S_&_T_=_InitSegm_(S,a)_)_)_&_(_S_=_{}_implies_T_=_{}_)_)_)
set x = the Element of S;
assume S <> {} ; ::_thesis: ex T being Subset of A st
( ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) & ( S = {} implies T = {} ) )
then reconsider x = the Element of S as Element of A by Lm1;
take T = InitSegm (S,x); ::_thesis: ( ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) & ( S = {} implies T = {} ) )
thus ( S <> {} implies ex a being Element of A st
( a in S & T = InitSegm (S,a) ) ) ; ::_thesis: ( S = {} implies T = {} )
thus ( S = {} implies T = {} ) ; ::_thesis: verum
end;
hence ( ( S <> {} implies ex b1 being Subset of A ex a being Element of A st
( a in S & b1 = InitSegm (S,a) ) ) & ( not S <> {} implies ex b1 being Subset of A st b1 = {} ) ) ; ::_thesis: verum
end;
consistency
for b1 being Subset of A holds verum ;
end;
:: deftheorem Def11 defines Initial_Segm ORDERS_2:def_11_:_
for A being non empty Poset
for S, b3 being Subset of A holds
( ( S <> {} implies ( b3 is Initial_Segm of S iff ex a being Element of A st
( a in S & b3 = InitSegm (S,a) ) ) ) & ( not S <> {} implies ( b3 is Initial_Segm of S iff b3 = {} ) ) );
theorem Th24: :: ORDERS_2:24
for A being non empty Poset
for a, b being Element of A
for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
proof
let A be non empty Poset; ::_thesis: for a, b being Element of A
for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
let a, b be Element of A; ::_thesis: for S being Subset of A holds
( a in InitSegm (S,b) iff ( a < b & a in S ) )
let S be Subset of A; ::_thesis: ( a in InitSegm (S,b) iff ( a < b & a in S ) )
( a in InitSegm (S,b) iff ( a in LowerCone {b} & a in S ) ) by XBOOLE_0:def_4;
hence ( a in InitSegm (S,b) iff ( a < b & a in S ) ) by Th23; ::_thesis: verum
end;
theorem :: ORDERS_2:25
for A being non empty Poset
for a being Element of A holds InitSegm (({} A),a) = {} ;
theorem Th26: :: ORDERS_2:26
for A being non empty Poset
for a being Element of A
for S being Subset of A holds not a in InitSegm (S,a)
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S being Subset of A holds not a in InitSegm (S,a)
let a be Element of A; ::_thesis: for S being Subset of A holds not a in InitSegm (S,a)
let S be Subset of A; ::_thesis: not a in InitSegm (S,a)
assume a in InitSegm (S,a) ; ::_thesis: contradiction
then a in LowerCone {a} by XBOOLE_0:def_4;
then A1: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
a in {a} by TARSKI:def_1;
hence contradiction by A1; ::_thesis: verum
end;
theorem :: ORDERS_2:27
for A being non empty Poset
for a1, a2 being Element of A
for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
proof
let A be non empty Poset; ::_thesis: for a1, a2 being Element of A
for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
let a1, a2 be Element of A; ::_thesis: for S being Subset of A st a1 < a2 holds
InitSegm (S,a1) c= InitSegm (S,a2)
let S be Subset of A; ::_thesis: ( a1 < a2 implies InitSegm (S,a1) c= InitSegm (S,a2) )
assume A1: a1 < a2 ; ::_thesis: InitSegm (S,a1) c= InitSegm (S,a2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a1) or x in InitSegm (S,a2) )
assume A2: x in InitSegm (S,a1) ; ::_thesis: x in InitSegm (S,a2)
then x in LowerCone {a1} by XBOOLE_0:def_4;
then consider a being Element of A such that
A3: a = x and
A4: for b being Element of A st b in {a1} holds
a < b ;
a1 in {a1} by TARSKI:def_1;
then a < a1 by A4;
then a < a2 by A1, Th5;
then for b being Element of A st b in {a2} holds
a < b by TARSKI:def_1;
then A5: x in LowerCone {a2} by A3;
x in S by A2, XBOOLE_0:def_4;
hence x in InitSegm (S,a2) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th28: :: ORDERS_2:28
for A being non empty Poset
for a being Element of A
for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
let a be Element of A; ::_thesis: for S, T being Subset of A st S c= T holds
InitSegm (S,a) c= InitSegm (T,a)
let S, T be Subset of A; ::_thesis: ( S c= T implies InitSegm (S,a) c= InitSegm (T,a) )
assume A1: S c= T ; ::_thesis: InitSegm (S,a) c= InitSegm (T,a)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a) or x in InitSegm (T,a) )
assume x in InitSegm (S,a) ; ::_thesis: x in InitSegm (T,a)
then ( x in S & x in LowerCone {a} ) by XBOOLE_0:def_4;
hence x in InitSegm (T,a) by A1, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th29: :: ORDERS_2:29
for A being non empty Poset
for S being Subset of A
for I being Initial_Segm of S holds I c= S
proof
let A be non empty Poset; ::_thesis: for S being Subset of A
for I being Initial_Segm of S holds I c= S
let S be Subset of A; ::_thesis: for I being Initial_Segm of S holds I c= S
let I be Initial_Segm of S; ::_thesis: I c= S
percases ( S = {} or S <> {} ) ;
suppose S = {} ; ::_thesis: I c= S
hence I c= S by Def11; ::_thesis: verum
end;
suppose S <> {} ; ::_thesis: I c= S
then ex a being Element of A st
( a in S & I = InitSegm (S,a) ) by Def11;
hence I c= S by XBOOLE_1:17; ::_thesis: verum
end;
end;
end;
theorem Th30: :: ORDERS_2:30
for A being non empty Poset
for S being Subset of A holds
( S <> {} iff not S is Initial_Segm of S )
proof
let A be non empty Poset; ::_thesis: for S being Subset of A holds
( S <> {} iff not S is Initial_Segm of S )
let S be Subset of A; ::_thesis: ( S <> {} iff not S is Initial_Segm of S )
thus ( S <> {} implies not S is Initial_Segm of S ) ::_thesis: ( S is not Initial_Segm of S implies S <> {} )
proof
assume ( S <> {} & S is Initial_Segm of S ) ; ::_thesis: contradiction
then consider a being Element of A such that
A1: ( a in S & S = InitSegm (S,a) ) by Def11;
a in LowerCone {a} by A1, XBOOLE_0:def_4;
hence contradiction by Th21; ::_thesis: verum
end;
thus ( S is not Initial_Segm of S implies S <> {} ) by Def11; ::_thesis: verum
end;
theorem Th31: :: ORDERS_2:31
for A being non empty Poset
for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds
not T is Initial_Segm of S
proof
let A be non empty Poset; ::_thesis: for S, T being Subset of A st S <> {} & S is Initial_Segm of T holds
not T is Initial_Segm of S
let S, T be Subset of A; ::_thesis: ( S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S )
assume that
A1: S <> {} and
A2: S is Initial_Segm of T and
A3: T is Initial_Segm of S ; ::_thesis: contradiction
now__::_thesis:_contradiction
percases ( S = {} or T = {} or ( S <> {} & T <> {} ) ) ;
suppose S = {} ; ::_thesis: contradiction
hence contradiction by A1; ::_thesis: verum
end;
suppose T = {} ; ::_thesis: contradiction
hence contradiction by A1, A2, Def11; ::_thesis: verum
end;
supposeA4: ( S <> {} & T <> {} ) ; ::_thesis: contradiction
then consider a2 being Element of A such that
A5: a2 in T and
A6: S = InitSegm (T,a2) by A2, Def11;
consider a1 being Element of A such that
A7: a1 in S and
A8: T = InitSegm (S,a1) by A3, A4, Def11;
a1 in LowerCone {a2} by A7, A6, XBOOLE_0:def_4;
then A9: ex a being Element of A st
( a = a1 & ( for b being Element of A st b in {a2} holds
a < b ) ) ;
a2 in LowerCone {a1} by A8, A5, XBOOLE_0:def_4;
then A10: ex a3 being Element of A st
( a3 = a2 & ( for b being Element of A st b in {a1} holds
a3 < b ) ) ;
a1 in {a1} by TARSKI:def_1;
then A11: a2 < a1 by A10;
a2 in {a2} by TARSKI:def_1;
then a1 < a2 by A9;
hence contradiction by A11, Th4; ::_thesis: verum
end;
end;
end;
hence contradiction ; ::_thesis: verum
end;
theorem Th32: :: ORDERS_2:32
for A being non empty Poset
for a1, a2 being Element of A
for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
proof
let A be non empty Poset; ::_thesis: for a1, a2 being Element of A
for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let a1, a2 be Element of A; ::_thesis: for S, T being Subset of A st a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S holds
a1 in T
let S, T be Subset of A; ::_thesis: ( a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T )
assume that
A1: a1 < a2 and
A2: a1 in S and
A3: a2 in T and
A4: T is Initial_Segm of S ; ::_thesis: a1 in T
consider a being Element of A such that
a in S and
A5: T = InitSegm (S,a) by A2, A4, Def11;
now__::_thesis:_for_b_being_Element_of_A_st_b_in_{a}_holds_
a1_<_b
let b be Element of A; ::_thesis: ( b in {a} implies a1 < b )
assume b in {a} ; ::_thesis: a1 < b
then A6: b = a by TARSKI:def_1;
a2 in LowerCone {a} by A3, A5, XBOOLE_0:def_4;
then A7: ex a3 being Element of A st
( a3 = a2 & ( for c being Element of A st c in {a} holds
a3 < c ) ) ;
a in {a} by TARSKI:def_1;
then a2 < a by A7;
hence a1 < b by A1, A6, Th5; ::_thesis: verum
end;
then a1 in LowerCone {a} ;
hence a1 in T by A2, A5, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th33: :: ORDERS_2:33
for A being non empty Poset
for a being Element of A
for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
let a be Element of A; ::_thesis: for S, T being Subset of A st a in S & S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
let S, T be Subset of A; ::_thesis: ( a in S & S is Initial_Segm of T implies InitSegm (S,a) = InitSegm (T,a) )
assume that
A1: a in S and
A2: S is Initial_Segm of T ; ::_thesis: InitSegm (S,a) = InitSegm (T,a)
A3: S c= T by A2, Th29;
thus InitSegm (S,a) c= InitSegm (T,a) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (T,a) c= InitSegm (S,a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a) or x in InitSegm (T,a) )
assume x in InitSegm (S,a) ; ::_thesis: x in InitSegm (T,a)
then ( x in LowerCone {a} & x in S ) by XBOOLE_0:def_4;
hence x in InitSegm (T,a) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (T,a) or x in InitSegm (S,a) )
assume A4: x in InitSegm (T,a) ; ::_thesis: x in InitSegm (S,a)
then A5: x in LowerCone {a} by XBOOLE_0:def_4;
then consider a1 being Element of A such that
A6: x = a1 and
A7: for a2 being Element of A st a2 in {a} holds
a1 < a2 ;
A8: a1 in T by A4, A6, XBOOLE_0:def_4;
a in {a} by TARSKI:def_1;
then a1 < a by A7;
then x in S by A1, A2, A6, A8, Th32;
hence x in InitSegm (S,a) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem :: ORDERS_2:34
for A being non empty Poset
for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
proof
let A be non empty Poset; ::_thesis: for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
let S, T be Subset of A; ::_thesis: ( S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S ) & not S = T implies S is Initial_Segm of T )
assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1, a2 being Element of A st a2 in S & a1 < a2 holds
a1 in S and
A4: S <> T ; ::_thesis: S is Initial_Segm of T
percases ( T <> {} or T = {} ) ;
:: according to ORDERS_2:def_11
case T <> {} ; ::_thesis: ex a being Element of A st
( a in T & S = InitSegm (T,a) )
set Y = T \ S;
not T c= S by A1, A4, XBOOLE_0:def_10;
then T \ S <> {} by XBOOLE_1:37;
then consider x being set such that
A5: x in T \ S and
A6: for y being set st y in T \ S holds
[x,y] in the InternalRel of A by A2, WELLORD1:5, XBOOLE_1:36;
reconsider x = x as Element of A by A5;
take x ; ::_thesis: ( x in T & S = InitSegm (T,x) )
thus A7: x in T by A5, XBOOLE_0:def_5; ::_thesis: S = InitSegm (T,x)
S = (LowerCone {x}) /\ T
proof
thus S c= (LowerCone {x}) /\ T :: according to XBOOLE_0:def_10 ::_thesis: (LowerCone {x}) /\ T c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in S or y in (LowerCone {x}) /\ T )
assume A8: y in S ; ::_thesis: y in (LowerCone {x}) /\ T
then reconsider a = y as Element of A ;
now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_{x}_holds_
a_<_a1
let a1 be Element of A; ::_thesis: ( a1 in {x} implies a < a1 )
assume that
A9: a1 in {x} and
A10: not a < a1 ; ::_thesis: contradiction
A11: a1 = x by A9, TARSKI:def_1;
then A12: a1 <> a by A5, A8, XBOOLE_0:def_5;
T is Chain of A by A2, Th13;
then a1 <= a by A1, A7, A8, A10, A11, Th12;
then a1 < a by A12, Def6;
then a1 in S by A3, A8;
hence contradiction by A5, A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then y in { a1 where a1 is Element of A : for a2 being Element of A st a2 in {x} holds
a1 < a2 } ;
hence y in (LowerCone {x}) /\ T by A1, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (LowerCone {x}) /\ T or y in S )
assume A13: y in (LowerCone {x}) /\ T ; ::_thesis: y in S
then y in LowerCone {x} by XBOOLE_0:def_4;
then consider a being Element of A such that
A14: a = y and
A15: for a2 being Element of A st a2 in {x} holds
a < a2 ;
A16: now__::_thesis:_not_y_in_T_\_S
assume y in T \ S ; ::_thesis: contradiction
then [x,y] in the InternalRel of A by A6;
then A17: x <= a by A14, Def5;
x in {x} by TARSKI:def_1;
hence contradiction by A15, A17, Th6; ::_thesis: verum
end;
y in T by A13, XBOOLE_0:def_4;
hence y in S by A16, XBOOLE_0:def_5; ::_thesis: verum
end;
hence S = InitSegm (T,x) ; ::_thesis: verum
end;
case T = {} ; ::_thesis: S = {}
hence S = {} by A1; ::_thesis: verum
end;
end;
end;
theorem Th35: :: ORDERS_2:35
for A being non empty Poset
for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
proof
let A be non empty Poset; ::_thesis: for S, T being Subset of A st S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T holds
S is Initial_Segm of T
let S, T be Subset of A; ::_thesis: ( S c= T & the InternalRel of A well_orders T & ( for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S ) & not S = T implies S is Initial_Segm of T )
assume that
A1: S c= T and
A2: the InternalRel of A well_orders T and
A3: for a1, a2 being Element of A st a2 in S & a1 in T & a1 < a2 holds
a1 in S and
A4: S <> T ; ::_thesis: S is Initial_Segm of T
percases ( T <> {} or T = {} ) ;
:: according to ORDERS_2:def_11
case T <> {} ; ::_thesis: ex a being Element of A st
( a in T & S = InitSegm (T,a) )
set Y = T \ S;
not T c= S by A1, A4, XBOOLE_0:def_10;
then T \ S <> {} by XBOOLE_1:37;
then consider x being set such that
A5: x in T \ S and
A6: for y being set st y in T \ S holds
[x,y] in the InternalRel of A by A2, WELLORD1:5, XBOOLE_1:36;
reconsider x = x as Element of A by A5;
take x ; ::_thesis: ( x in T & S = InitSegm (T,x) )
thus A7: x in T by A5, XBOOLE_0:def_5; ::_thesis: S = InitSegm (T,x)
S = (LowerCone {x}) /\ T
proof
thus S c= (LowerCone {x}) /\ T :: according to XBOOLE_0:def_10 ::_thesis: (LowerCone {x}) /\ T c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in S or y in (LowerCone {x}) /\ T )
assume A8: y in S ; ::_thesis: y in (LowerCone {x}) /\ T
then reconsider a = y as Element of A ;
now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_{x}_holds_
a_<_a1
let a1 be Element of A; ::_thesis: ( a1 in {x} implies a < a1 )
assume that
A9: a1 in {x} and
A10: not a < a1 ; ::_thesis: contradiction
A11: a1 = x by A9, TARSKI:def_1;
then A12: a1 <> a by A5, A8, XBOOLE_0:def_5;
T is Chain of A by A2, Th13;
then a1 <= a by A1, A7, A8, A10, A11, Th12;
then a1 < a by A12, Def6;
then a1 in S by A3, A7, A8, A11;
hence contradiction by A5, A11, XBOOLE_0:def_5; ::_thesis: verum
end;
then y in { a1 where a1 is Element of A : for a2 being Element of A st a2 in {x} holds
a1 < a2 } ;
hence y in (LowerCone {x}) /\ T by A1, A8, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (LowerCone {x}) /\ T or y in S )
assume A13: y in (LowerCone {x}) /\ T ; ::_thesis: y in S
then y in LowerCone {x} by XBOOLE_0:def_4;
then consider a being Element of A such that
A14: a = y and
A15: for a2 being Element of A st a2 in {x} holds
a < a2 ;
A16: now__::_thesis:_not_y_in_T_\_S
assume y in T \ S ; ::_thesis: contradiction
then [x,y] in the InternalRel of A by A6;
then A17: x <= a by A14, Def5;
x in {x} by TARSKI:def_1;
hence contradiction by A15, A17, Th6; ::_thesis: verum
end;
y in T by A13, XBOOLE_0:def_4;
hence y in S by A16, XBOOLE_0:def_5; ::_thesis: verum
end;
hence S = InitSegm (T,x) ; ::_thesis: verum
end;
case T = {} ; ::_thesis: S = {}
hence S = {} by A1; ::_thesis: verum
end;
end;
end;
definition
let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
mode Chain of f -> Chain of A means :Def12: :: ORDERS_2:def 12
( it <> {} & the InternalRel of A well_orders it & ( for a being Element of A st a in it holds
f . (UpperCone (InitSegm (it,a))) = a ) );
existence
ex b1 being Chain of A st
( b1 <> {} & the InternalRel of A well_orders b1 & ( for a being Element of A st a in b1 holds
f . (UpperCone (InitSegm (b1,a))) = a ) )
proof
set AC = the carrier of A;
( the carrier of A in BOOL the carrier of A & not {} in BOOL the carrier of A ) by ORDERS_1:1, ORDERS_1:2;
then reconsider aa = f . the carrier of A as Element of A by ORDERS_1:def_1;
reconsider X = {aa} as Chain of A by Th8;
take X ; ::_thesis: ( X <> {} & the InternalRel of A well_orders X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
thus X <> {} ; ::_thesis: ( the InternalRel of A well_orders X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
hence ( the InternalRel of A is_reflexive_in X & the InternalRel of A is_transitive_in X & the InternalRel of A is_antisymmetric_in X ) by A1, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to WELLORD1:def_5 ::_thesis: ( the InternalRel of A is_connected_in X & the InternalRel of A is_well_founded_in X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
the InternalRel of A is_strongly_connected_in X by Def7;
hence the InternalRel of A is_connected_in X by ORDERS_1:7; ::_thesis: ( the InternalRel of A is_well_founded_in X & ( for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a ) )
thus the InternalRel of A is_well_founded_in X ::_thesis: for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a
proof
reconsider x = aa as set ;
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= X or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
assume that
A2: Y c= X and
A3: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
take x ; ::_thesis: ( x in Y & the InternalRel of A -Seg x misses Y )
Y = X by A2, A3, ZFMISC_1:33;
hence x in Y by TARSKI:def_1; ::_thesis: the InternalRel of A -Seg x misses Y
thus ( the InternalRel of A -Seg x) /\ Y c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= ( the InternalRel of A -Seg x) /\ Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ( the InternalRel of A -Seg x) /\ Y or y in {} )
assume A4: y in ( the InternalRel of A -Seg x) /\ Y ; ::_thesis: y in {}
then y in Y by XBOOLE_0:def_4;
then A5: y = aa by A2, TARSKI:def_1;
y in the InternalRel of A -Seg x by A4, XBOOLE_0:def_4;
hence y in {} by A5, WELLORD1:1; ::_thesis: verum
end;
thus {} c= ( the InternalRel of A -Seg x) /\ Y by XBOOLE_1:2; ::_thesis: verum
end;
let a be Element of A; ::_thesis: ( a in X implies f . (UpperCone (InitSegm (X,a))) = a )
assume a in X ; ::_thesis: f . (UpperCone (InitSegm (X,a))) = a
then A6: a = aa by TARSKI:def_1;
(LowerCone {a}) /\ X c= {} A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LowerCone {a}) /\ X or x in {} A )
assume A7: x in (LowerCone {a}) /\ X ; ::_thesis: x in {} A
then x in LowerCone {a} by XBOOLE_0:def_4;
then A8: ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
x in X by A7, XBOOLE_0:def_4;
hence x in {} A by A6, A8; ::_thesis: verum
end;
then (LowerCone {a}) /\ X = {} A ;
hence f . (UpperCone (InitSegm (X,a))) = a by A6, Th14; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines Chain ORDERS_2:def_12_:_
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for b3 being Chain of A holds
( b3 is Chain of f iff ( b3 <> {} & the InternalRel of A well_orders b3 & ( for a being Element of A st a in b3 holds
f . (UpperCone (InitSegm (b3,a))) = a ) ) );
theorem Th36: :: ORDERS_2:36
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds {(f . the carrier of A)} is Chain of f
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds {(f . the carrier of A)} is Chain of f
let f be Choice_Function of BOOL the carrier of A; ::_thesis: {(f . the carrier of A)} is Chain of f
set AC = the carrier of A;
( the carrier of A in BOOL the carrier of A & not {} in BOOL the carrier of A ) by ORDERS_1:1, ORDERS_1:2;
then reconsider aa = f . the carrier of A as Element of A by ORDERS_1:def_1;
reconsider X = {aa} as Chain of A by Th8;
A1: the InternalRel of A is_well_founded_in X
proof
reconsider x = aa as set ;
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= X or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
assume that
A2: Y c= X and
A3: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
take x ; ::_thesis: ( x in Y & the InternalRel of A -Seg x misses Y )
Y = X by A2, A3, ZFMISC_1:33;
hence x in Y by TARSKI:def_1; ::_thesis: the InternalRel of A -Seg x misses Y
thus ( the InternalRel of A -Seg x) /\ Y c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= ( the InternalRel of A -Seg x) /\ Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ( the InternalRel of A -Seg x) /\ Y or y in {} )
assume A4: y in ( the InternalRel of A -Seg x) /\ Y ; ::_thesis: y in {}
then y in Y by XBOOLE_0:def_4;
then A5: y = aa by A2, TARSKI:def_1;
y in the InternalRel of A -Seg x by A4, XBOOLE_0:def_4;
hence y in {} by A5, WELLORD1:1; ::_thesis: verum
end;
thus {} c= ( the InternalRel of A -Seg x) /\ Y by XBOOLE_1:2; ::_thesis: verum
end;
A6: for a being Element of A st a in X holds
f . (UpperCone (InitSegm (X,a))) = a
proof
let a be Element of A; ::_thesis: ( a in X implies f . (UpperCone (InitSegm (X,a))) = a )
assume a in X ; ::_thesis: f . (UpperCone (InitSegm (X,a))) = a
then A7: a = aa by TARSKI:def_1;
(LowerCone {a}) /\ X c= {} A
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (LowerCone {a}) /\ X or x in {} A )
assume A8: x in (LowerCone {a}) /\ X ; ::_thesis: x in {} A
then x in LowerCone {a} by XBOOLE_0:def_4;
then A9: ex a1 being Element of A st
( x = a1 & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
x in X by A8, XBOOLE_0:def_4;
hence x in {} A by A7, A9; ::_thesis: verum
end;
then (LowerCone {a}) /\ X = {} A ;
hence f . (UpperCone (InitSegm (X,a))) = a by A7, Th14; ::_thesis: verum
end;
the InternalRel of A is_strongly_connected_in X by Def7;
then A10: the InternalRel of A is_connected_in X by ORDERS_1:7;
the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then A11: the InternalRel of A is_antisymmetric_in X by ORDERS_1:9;
the InternalRel of A is_transitive_in the carrier of A by Def3;
then A12: the InternalRel of A is_transitive_in X by ORDERS_1:10;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then the InternalRel of A is_reflexive_in X by ORDERS_1:8;
then the InternalRel of A well_orders X by A12, A11, A10, A1, WELLORD1:def_5;
hence {(f . the carrier of A)} is Chain of f by A6, Def12; ::_thesis: verum
end;
theorem Th37: :: ORDERS_2:37
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f holds f . the carrier of A in fC
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f holds f . the carrier of A in fC
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f holds f . the carrier of A in fC
let fC be Chain of f; ::_thesis: f . the carrier of A in fC
( the InternalRel of A well_orders fC & fC <> {} ) by Def12;
then consider x being set such that
A1: x in fC and
A2: for y being set st y in fC holds
[x,y] in the InternalRel of A by WELLORD1:5;
reconsider x = x as Element of A by A1;
A3: now__::_thesis:_not_(LowerCone_{x})_/\_fC_<>_{}_A
set y = the Element of (LowerCone {x}) /\ fC;
assume A4: (LowerCone {x}) /\ fC <> {} A ; ::_thesis: contradiction
then reconsider a = the Element of (LowerCone {x}) /\ fC as Element of A by Lm1;
a in LowerCone {x} by A4, XBOOLE_0:def_4;
then A5: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {x} holds
a1 < a2 ) ) ;
the Element of (LowerCone {x}) /\ fC in fC by A4, XBOOLE_0:def_4;
then [x, the Element of (LowerCone {x}) /\ fC] in the InternalRel of A by A2;
then A6: x <= a by Def5;
x in {x} by TARSKI:def_1;
hence contradiction by A6, A5, Th6; ::_thesis: verum
end;
(LowerCone {x}) /\ fC = InitSegm (fC,x) ;
then f . (UpperCone ((LowerCone {x}) /\ fC)) = x by A1, Def12;
hence f . the carrier of A in fC by A1, A3, Th14; ::_thesis: verum
end;
theorem Th38: :: ORDERS_2:38
for A being non empty Poset
for a, b being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
proof
let A be non empty Poset; ::_thesis: for a, b being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let a, b be Element of A; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f st a in fC & b = f . the carrier of A holds
b <= a
let fC be Chain of f; ::_thesis: ( a in fC & b = f . the carrier of A implies b <= a )
assume that
A1: a in fC and
A2: b = f . the carrier of A ; ::_thesis: b <= a
( the InternalRel of A well_orders fC & fC <> {} ) by Def12;
then consider x being set such that
A3: x in fC and
A4: for y being set st y in fC holds
[x,y] in the InternalRel of A by WELLORD1:5;
reconsider x = x as Element of A by A3;
A5: now__::_thesis:_not_(LowerCone_{x})_/\_fC_<>_{}_A
set y = the Element of (LowerCone {x}) /\ fC;
assume A6: (LowerCone {x}) /\ fC <> {} A ; ::_thesis: contradiction
then reconsider a = the Element of (LowerCone {x}) /\ fC as Element of A by Lm1;
a in LowerCone {x} by A6, XBOOLE_0:def_4;
then A7: ex a1 being Element of A st
( a = a1 & ( for a2 being Element of A st a2 in {x} holds
a1 < a2 ) ) ;
the Element of (LowerCone {x}) /\ fC in fC by A6, XBOOLE_0:def_4;
then [x, the Element of (LowerCone {x}) /\ fC] in the InternalRel of A by A4;
then A8: x <= a by Def5;
x in {x} by TARSKI:def_1;
hence contradiction by A8, A7, Th6; ::_thesis: verum
end;
(LowerCone {x}) /\ fC = InitSegm (fC,x) ;
then f . (UpperCone ((LowerCone {x}) /\ fC)) = x by A3, Def12;
then A9: f . the carrier of A = x by A5, Th14;
[x,a] in the InternalRel of A by A1, A4;
hence b <= a by A2, A9, Def5; ::_thesis: verum
end;
theorem :: ORDERS_2:39
for A being non empty Poset
for a being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
proof
let A be non empty Poset; ::_thesis: for a being Element of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let a be Element of A; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f st a = f . the carrier of A holds
InitSegm (fC,a) = {}
let fC be Chain of f; ::_thesis: ( a = f . the carrier of A implies InitSegm (fC,a) = {} )
set x = the Element of (LowerCone {a}) /\ fC;
assume A1: a = f . the carrier of A ; ::_thesis: InitSegm (fC,a) = {}
then A2: a in fC by Th37;
assume A3: InitSegm (fC,a) <> {} ; ::_thesis: contradiction
then reconsider b = the Element of (LowerCone {a}) /\ fC as Element of A by Lm1;
the Element of (LowerCone {a}) /\ fC in LowerCone {a} by A3, XBOOLE_0:def_4;
then A4: ex a1 being Element of A st
( a1 = b & ( for a2 being Element of A st a2 in {a} holds
a1 < a2 ) ) ;
a in {a} by TARSKI:def_1;
then A5: b < a by A4;
A6: the Element of (LowerCone {a}) /\ fC in fC by A3, XBOOLE_0:def_4;
then a <= b by A1, Th38;
hence contradiction by A2, A6, A5, Th12; ::_thesis: verum
end;
theorem :: ORDERS_2:40
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds fC1 meets fC2
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds fC1 meets fC2
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC1, fC2 being Chain of f holds fC1 meets fC2
let fC1, fC2 be Chain of f; ::_thesis: fC1 meets fC2
( f . the carrier of A in fC1 & f . the carrier of A in fC2 ) by Th37;
hence fC1 meets fC2 by XBOOLE_0:3; ::_thesis: verum
end;
theorem Th41: :: ORDERS_2:41
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC1, fC2 being Chain of f st fC1 <> fC2 holds
( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
let fC1, fC2 be Chain of f; ::_thesis: ( fC1 <> fC2 implies ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) )
assume A1: fC1 <> fC2 ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
set N = { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) } ;
A2: { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) } c= fC1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) } or x in fC1 )
assume x in { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) } ; ::_thesis: x in fC1
then ex a being Element of A st
( a = x & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) ;
hence x in fC1 by XBOOLE_0:def_4; ::_thesis: verum
end;
then reconsider N = { a where a is Element of A : ( a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) } as Subset of A by XBOOLE_1:1;
A3: N c= fC2
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in N or x in fC2 )
assume x in N ; ::_thesis: x in fC2
then ex a being Element of A st
( a = x & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) ;
hence x in fC2 by XBOOLE_0:def_4; ::_thesis: verum
end;
A4: now__::_thesis:_for_a1,_a2_being_Element_of_A_st_a2_in_N_&_a1_in_fC1_&_a1_<_a2_holds_
a1_in_N
let a1, a2 be Element of A; ::_thesis: ( a2 in N & a1 in fC1 & a1 < a2 implies a1 in N )
assume that
A5: a2 in N and
A6: a1 in fC1 and
A7: a1 < a2 ; ::_thesis: a1 in N
A8: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) by A5;
A9: InitSegm (fC1,a1) = InitSegm (fC2,a1)
proof
thus InitSegm (fC1,a1) c= InitSegm (fC2,a1) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (fC2,a1) c= InitSegm (fC1,a1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC1,a1) or x in InitSegm (fC2,a1) )
assume A10: x in InitSegm (fC1,a1) ; ::_thesis: x in InitSegm (fC2,a1)
then reconsider b = x as Element of A ;
A11: b in fC1 by A10, Th24;
A12: b < a1 by A10, Th24;
then b < a2 by A7, Th5;
then b in InitSegm (fC1,a2) by A11, Th24;
then b in fC2 by A8, Th24;
hence x in InitSegm (fC2,a1) by A12, Th24; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC2,a1) or x in InitSegm (fC1,a1) )
assume A13: x in InitSegm (fC2,a1) ; ::_thesis: x in InitSegm (fC1,a1)
then reconsider b = x as Element of A ;
A14: b in fC2 by A13, Th24;
A15: b < a1 by A13, Th24;
then b < a2 by A7, Th5;
then b in InitSegm (fC2,a2) by A14, Th24;
then b in fC1 by A8, Th24;
hence x in InitSegm (fC1,a1) by A15, Th24; ::_thesis: verum
end;
a1 in InitSegm (fC2,a2) by A6, A7, A8, Th24;
then a1 in fC2 by XBOOLE_0:def_4;
then a1 in fC1 /\ fC2 by A6, XBOOLE_0:def_4;
hence a1 in N by A9; ::_thesis: verum
end;
A16: now__::_thesis:_for_a1,_a2_being_Element_of_A_st_a2_in_N_&_a1_in_fC2_&_a1_<_a2_holds_
a1_in_N
let a1, a2 be Element of A; ::_thesis: ( a2 in N & a1 in fC2 & a1 < a2 implies a1 in N )
assume that
A17: a2 in N and
A18: a1 in fC2 and
A19: a1 < a2 ; ::_thesis: a1 in N
A20: ex a being Element of A st
( a = a2 & a in fC1 /\ fC2 & InitSegm (fC1,a) = InitSegm (fC2,a) ) by A17;
A21: InitSegm (fC1,a1) = InitSegm (fC2,a1)
proof
thus InitSegm (fC1,a1) c= InitSegm (fC2,a1) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (fC2,a1) c= InitSegm (fC1,a1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC1,a1) or x in InitSegm (fC2,a1) )
assume A22: x in InitSegm (fC1,a1) ; ::_thesis: x in InitSegm (fC2,a1)
then reconsider b = x as Element of A ;
A23: b in fC1 by A22, Th24;
A24: b < a1 by A22, Th24;
then b < a2 by A19, Th5;
then b in InitSegm (fC1,a2) by A23, Th24;
then b in fC2 by A20, Th24;
hence x in InitSegm (fC2,a1) by A24, Th24; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (fC2,a1) or x in InitSegm (fC1,a1) )
assume A25: x in InitSegm (fC2,a1) ; ::_thesis: x in InitSegm (fC1,a1)
then reconsider b = x as Element of A ;
A26: b in fC2 by A25, Th24;
A27: b < a1 by A25, Th24;
then b < a2 by A19, Th5;
then b in InitSegm (fC2,a2) by A26, Th24;
then b in fC1 by A20, Th24;
hence x in InitSegm (fC1,a1) by A27, Th24; ::_thesis: verum
end;
a1 in InitSegm (fC1,a2) by A18, A19, A20, Th24;
then a1 in fC1 by XBOOLE_0:def_4;
then a1 in fC1 /\ fC2 by A18, XBOOLE_0:def_4;
hence a1 in N by A21; ::_thesis: verum
end;
A28: ( the InternalRel of A well_orders fC1 & the InternalRel of A well_orders fC2 ) by Def12;
now__::_thesis:_(_fC1_is_Initial_Segm_of_fC2_iff_fC2_is_not_Initial_Segm_of_fC1_)
percases ( ( N is Initial_Segm of fC1 & N = fC2 ) or ( N is Initial_Segm of fC2 & N = fC1 ) or ( N = fC1 & N = fC2 ) or ( N is Initial_Segm of fC1 & N is Initial_Segm of fC2 ) ) by A2, A4, A28, A3, A16, Th35;
supposeA29: ( N is Initial_Segm of fC1 & N = fC2 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
fC1 <> {} by Def12;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A29, Th31; ::_thesis: verum
end;
supposeA30: ( N is Initial_Segm of fC2 & N = fC1 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
fC2 <> {} by Def12;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A30, Th31; ::_thesis: verum
end;
suppose ( N = fC1 & N = fC2 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A1; ::_thesis: verum
end;
supposeA31: ( N is Initial_Segm of fC1 & N is Initial_Segm of fC2 ) ; ::_thesis: ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 )
fC2 <> {} by Def12;
then consider b being Element of A such that
A32: b in fC2 and
A33: N = InitSegm (fC2,b) by A31, Def11;
fC1 <> {} by Def12;
then consider a being Element of A such that
A34: a in fC1 and
A35: N = InitSegm (fC1,a) by A31, Def11;
A36: a = f . (UpperCone (InitSegm (fC2,b))) by A34, A35, A33, Def12
.= b by A32, Def12 ;
then a in fC1 /\ fC2 by A34, A32, XBOOLE_0:def_4;
then a in N by A35, A33, A36;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) by A35, Th26; ::_thesis: verum
end;
end;
end;
hence ( fC1 is Initial_Segm of fC2 iff fC2 is not Initial_Segm of fC1 ) ; ::_thesis: verum
end;
theorem Th42: :: ORDERS_2:42
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC1, fC2 being Chain of f holds
( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
let fC1, fC2 be Chain of f; ::_thesis: ( fC1 c< fC2 iff fC1 is Initial_Segm of fC2 )
thus ( fC1 c< fC2 implies fC1 is Initial_Segm of fC2 ) ::_thesis: ( fC1 is Initial_Segm of fC2 implies fC1 c< fC2 )
proof
assume A1: fC1 c< fC2 ; ::_thesis: fC1 is Initial_Segm of fC2
now__::_thesis:_fC2_is_not_Initial_Segm_of_fC1
assume A2: fC2 is Initial_Segm of fC1 ; ::_thesis: contradiction
fC1 <> {} by Def12;
then ex a being Element of A st
( a in fC1 & fC2 = InitSegm (fC1,a) ) by A2, Def11;
then fC2 c= fC1 by XBOOLE_1:17;
hence contradiction by A1, XBOOLE_0:def_8; ::_thesis: verum
end;
hence fC1 is Initial_Segm of fC2 by A1, Th41; ::_thesis: verum
end;
assume A3: fC1 is Initial_Segm of fC2 ; ::_thesis: fC1 c< fC2
A4: fC2 <> {} by Def12;
then ex a being Element of A st
( a in fC2 & fC1 = InitSegm (fC2,a) ) by A3, Def11;
then A5: fC1 c= fC2 by XBOOLE_1:17;
fC1 <> fC2 by A3, A4, Th30;
hence fC1 c< fC2 by A5, XBOOLE_0:def_8; ::_thesis: verum
end;
definition
let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
func Chains f -> set means :Def13: :: ORDERS_2:def 13
for x being set holds
( x in it iff x is Chain of f );
existence
ex b1 being set st
for x being set holds
( x in b1 iff x is Chain of f )
proof
defpred S1[ set ] means $1 is Chain of f;
consider X being set such that
A1: for x being set holds
( x in X iff ( x in bool the carrier of A & S1[x] ) ) from XBOOLE_0:sch_1();
take X ; ::_thesis: for x being set holds
( x in X iff x is Chain of f )
let x be set ; ::_thesis: ( x in X iff x is Chain of f )
thus ( x in X implies x is Chain of f ) by A1; ::_thesis: ( x is Chain of f implies x in X )
assume x is Chain of f ; ::_thesis: x in X
hence x in X by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Chain of f ) ) & ( for x being set holds
( x in b2 iff x is Chain of f ) ) holds
b1 = b2
proof
let D1, D2 be set ; ::_thesis: ( ( for x being set holds
( x in D1 iff x is Chain of f ) ) & ( for x being set holds
( x in D2 iff x is Chain of f ) ) implies D1 = D2 )
assume A2: for x being set holds
( x in D1 iff x is Chain of f ) ; ::_thesis: ( ex x being set st
( ( x in D2 implies x is Chain of f ) implies ( x is Chain of f & not x in D2 ) ) or D1 = D2 )
assume A3: for x being set holds
( x in D2 iff x is Chain of f ) ; ::_thesis: D1 = D2
thus D1 c= D2 :: according to XBOOLE_0:def_10 ::_thesis: D2 c= D1
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D1 or x in D2 )
assume x in D1 ; ::_thesis: x in D2
then x is Chain of f by A2;
hence x in D2 by A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in D2 or x in D1 )
assume x in D2 ; ::_thesis: x in D1
then x is Chain of f by A3;
hence x in D1 by A2; ::_thesis: verum
end;
end;
:: deftheorem Def13 defines Chains ORDERS_2:def_13_:_
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A
for b3 being set holds
( b3 = Chains f iff for x being set holds
( x in b3 iff x is Chain of f ) );
registration
let A be non empty Poset;
let f be Choice_Function of BOOL the carrier of A;
cluster Chains f -> non empty ;
coherence
not Chains f is empty
proof
set x = the Chain of f;
the Chain of f in Chains f by Def13;
hence not Chains f is empty ; ::_thesis: verum
end;
end;
Lm2: for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Subset of A
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Subset of A
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) is Subset of A
now__::_thesis:_for_X_being_set_st_X_in_Chains_f_holds_
X_c=_the_carrier_of_A
let X be set ; ::_thesis: ( X in Chains f implies X c= the carrier of A )
assume X in Chains f ; ::_thesis: X c= the carrier of A
then X is Chain of f by Def13;
hence X c= the carrier of A ; ::_thesis: verum
end;
hence union (Chains f) is Subset of A by ZFMISC_1:76; ::_thesis: verum
end;
Lm3: for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of A
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of A
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) is Chain of A
reconsider C = union (Chains f) as Subset of A by Lm2;
the InternalRel of A is_strongly_connected_in C
proof
let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds
( not x in C or not b1 in C or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in C or not y in C or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume that
A1: x in C and
A2: y in C ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
consider X being set such that
A3: x in X and
A4: X in Chains f by A1, TARSKI:def_4;
consider Y being set such that
A5: y in Y and
A6: Y in Chains f by A2, TARSKI:def_4;
reconsider X = X, Y = Y as Chain of f by A4, A6, Def13;
A7: the InternalRel of A is_strongly_connected_in X by Def7;
A8: the InternalRel of A is_strongly_connected_in Y by Def7;
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( X = Y or X <> Y ) ;
suppose X = Y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A7, RELAT_2:def_7; ::_thesis: verum
end;
supposeA9: X <> Y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( X is Initial_Segm of Y or Y is Initial_Segm of X ) by A9, Th41;
suppose X is Initial_Segm of Y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then X c< Y by Th42;
then X c= Y by XBOOLE_0:def_8;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A8, RELAT_2:def_7; ::_thesis: verum
end;
suppose Y is Initial_Segm of X ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then Y c< X by Th42;
then Y c= X by XBOOLE_0:def_8;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A3, A5, A7, RELAT_2:def_7; ::_thesis: verum
end;
end;
end;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
end;
end;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
hence union (Chains f) is Chain of A by Def7; ::_thesis: verum
end;
theorem Th43: :: ORDERS_2:43
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) <> {}
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) <> {}
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) <> {}
{(f . the carrier of A)} is Chain of f by Th36;
then {(f . the carrier of A)} in Chains f by Def13;
hence union (Chains f) <> {} by ORDERS_1:6; ::_thesis: verum
end;
theorem Th44: :: ORDERS_2:44
for A being non empty Poset
for S being Subset of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
proof
let A be non empty Poset; ::_thesis: for S being Subset of A
for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let S be Subset of A; ::_thesis: for f being Choice_Function of BOOL the carrier of A
for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let f be Choice_Function of BOOL the carrier of A; ::_thesis: for fC being Chain of f st fC <> union (Chains f) & S = union (Chains f) holds
fC is Initial_Segm of S
let fC be Chain of f; ::_thesis: ( fC <> union (Chains f) & S = union (Chains f) implies fC is Initial_Segm of S )
assume that
A1: fC <> union (Chains f) and
A2: S = union (Chains f) ; ::_thesis: fC is Initial_Segm of S
set x = the Element of S \ fC;
fC in Chains f by Def13;
then fC c= union (Chains f) by ZFMISC_1:74;
then not union (Chains f) c= fC by A1, XBOOLE_0:def_10;
then A3: S \ fC <> {} by A2, XBOOLE_1:37;
then A4: not the Element of S \ fC in fC by XBOOLE_0:def_5;
the Element of S \ fC in S by A3, XBOOLE_0:def_5;
then consider X being set such that
A5: the Element of S \ fC in X and
A6: X in Chains f by A2, TARSKI:def_4;
reconsider X = X as Chain of f by A6, Def13;
not X c= fC by A3, A5, XBOOLE_0:def_5;
then not X c< fC by XBOOLE_0:def_8;
then X is not Initial_Segm of fC by Th42;
then fC is Initial_Segm of X by A5, A4, Th41;
then consider a being Element of A such that
A7: a in X and
A8: fC = InitSegm (X,a) by A5, Def11;
A9: X c= S by A2, A6, ZFMISC_1:74;
InitSegm (S,a) = InitSegm (X,a)
proof
thus InitSegm (S,a) c= InitSegm (X,a) :: according to XBOOLE_0:def_10 ::_thesis: InitSegm (X,a) c= InitSegm (S,a)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (S,a) or x in InitSegm (X,a) )
assume A10: x in InitSegm (S,a) ; ::_thesis: x in InitSegm (X,a)
then A11: x in LowerCone {a} by XBOOLE_0:def_4;
then consider b being Element of A such that
A12: b = x and
A13: for a2 being Element of A st a2 in {a} holds
b < a2 ;
b in S by A10, A12, XBOOLE_0:def_4;
then consider Y being set such that
A14: b in Y and
A15: Y in Chains f by A2, TARSKI:def_4;
reconsider Y = Y as Chain of f by A15, Def13;
a in {a} by TARSKI:def_1;
then A16: b < a by A13;
now__::_thesis:_x_in_InitSegm_(X,a)
percases ( X = Y or X <> Y ) ;
suppose X = Y ; ::_thesis: x in InitSegm (X,a)
hence x in InitSegm (X,a) by A11, A12, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA17: X <> Y ; ::_thesis: x in InitSegm (X,a)
now__::_thesis:_x_in_InitSegm_(X,a)
percases ( X is Initial_Segm of Y or Y is Initial_Segm of X ) by A17, Th41;
suppose X is Initial_Segm of Y ; ::_thesis: x in InitSegm (X,a)
then x in X by A7, A12, A16, A14, Th32;
hence x in InitSegm (X,a) by A11, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose Y is Initial_Segm of X ; ::_thesis: x in InitSegm (X,a)
then Y c< X by Th42;
then Y c= X by XBOOLE_0:def_8;
hence x in InitSegm (X,a) by A11, A12, A14, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence x in InitSegm (X,a) ; ::_thesis: verum
end;
end;
end;
hence x in InitSegm (X,a) ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (X,a) or x in InitSegm (S,a) )
assume x in InitSegm (X,a) ; ::_thesis: x in InitSegm (S,a)
then ( x in LowerCone {a} & x in X ) by XBOOLE_0:def_4;
hence x in InitSegm (S,a) by A9, XBOOLE_0:def_4; ::_thesis: verum
end;
hence fC is Initial_Segm of S by A7, A8, A9, Def11; ::_thesis: verum
end;
theorem Th45: :: ORDERS_2:45
for A being non empty Poset
for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of f
proof
let A be non empty Poset; ::_thesis: for f being Choice_Function of BOOL the carrier of A holds union (Chains f) is Chain of f
let f be Choice_Function of BOOL the carrier of A; ::_thesis: union (Chains f) is Chain of f
reconsider C = union (Chains f) as Chain of A by Lm3;
A1: now__::_thesis:_for_a_being_Element_of_A_st_a_in_C_holds_
f_._(UpperCone_(InitSegm_(C,a)))_=_a
let a be Element of A; ::_thesis: ( a in C implies f . (UpperCone (InitSegm (C,a))) = a )
assume a in C ; ::_thesis: f . (UpperCone (InitSegm (C,a))) = a
then consider X being set such that
A2: a in X and
A3: X in Chains f by TARSKI:def_4;
reconsider X = X as Chain of f by A3, Def13;
now__::_thesis:_f_._(UpperCone_(InitSegm_(C,a)))_=_a
InitSegm (C,a) = InitSegm (X,a) by A2, Th33, Th44;
hence f . (UpperCone (InitSegm (C,a))) = a by A2, Def12; ::_thesis: verum
end;
hence f . (UpperCone (InitSegm (C,a))) = a ; ::_thesis: verum
end;
A4: the InternalRel of A well_orders C
proof
A5: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
hence ( the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C ) by A5, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to WELLORD1:def_5 ::_thesis: ( the InternalRel of A is_connected_in C & the InternalRel of A is_well_founded_in C )
the InternalRel of A is_strongly_connected_in C by Def7;
hence the InternalRel of A is_connected_in C by ORDERS_1:7; ::_thesis: the InternalRel of A is_well_founded_in C
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= C or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
set x = the Element of Y;
assume that
A6: Y c= C and
A7: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
the Element of Y in C by A6, A7, TARSKI:def_3;
then consider X being set such that
A8: the Element of Y in X and
A9: X in Chains f by TARSKI:def_4;
reconsider X = X as Chain of f by A9, Def13;
A10: the InternalRel of A well_orders X by Def12;
X /\ Y <> {} by A7, A8, XBOOLE_0:def_4;
then consider a being set such that
A11: a in X /\ Y and
A12: for x being set st x in X /\ Y holds
[a,x] in the InternalRel of A by A10, WELLORD1:5, XBOOLE_1:17;
take a ; ::_thesis: ( a in Y & the InternalRel of A -Seg a misses Y )
thus a in Y by A11, XBOOLE_0:def_4; ::_thesis: the InternalRel of A -Seg a misses Y
reconsider aa = a as Element of A by A11;
thus ( the InternalRel of A -Seg a) /\ Y c= {} :: according to XBOOLE_0:def_7,XBOOLE_0:def_10 ::_thesis: {} c= ( the InternalRel of A -Seg a) /\ Y
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in ( the InternalRel of A -Seg a) /\ Y or y in {} )
assume A13: y in ( the InternalRel of A -Seg a) /\ Y ; ::_thesis: y in {}
then A14: y in Y by XBOOLE_0:def_4;
then y in C by A6;
then reconsider b = y as Element of A ;
A15: y in the InternalRel of A -Seg a by A13, XBOOLE_0:def_4;
then A16: y <> a by WELLORD1:1;
[y,a] in the InternalRel of A by A15, WELLORD1:1;
then A17: b <= aa by Def5;
now__::_thesis:_y_in_X
percases ( X <> C or X = C ) ;
supposeA18: X <> C ; ::_thesis: y in X
( a in X & b < aa ) by A11, A16, A17, Def6, XBOOLE_0:def_4;
hence y in X by A6, A14, A18, Th32, Th44; ::_thesis: verum
end;
suppose X = C ; ::_thesis: y in X
hence y in X by A6, A14; ::_thesis: verum
end;
end;
end;
then y in X /\ Y by A14, XBOOLE_0:def_4;
then [a,y] in the InternalRel of A by A12;
then aa <= b by Def5;
hence y in {} by A16, A17, Th2; ::_thesis: verum
end;
thus {} c= ( the InternalRel of A -Seg a) /\ Y by XBOOLE_1:2; ::_thesis: verum
end;
C <> {} by Th43;
hence union (Chains f) is Chain of f by A4, A1, Def12; ::_thesis: verum
end;
begin
theorem Th46: :: ORDERS_2:46
for A being non empty Poset
for S being Subset of A holds field ( the InternalRel of A |_2 S) = S
proof
let A be non empty Poset; ::_thesis: for S being Subset of A holds field ( the InternalRel of A |_2 S) = S
let S be Subset of A; ::_thesis: field ( the InternalRel of A |_2 S) = S
set P = the InternalRel of A |_2 S;
thus field ( the InternalRel of A |_2 S) c= S by WELLORD1:13; :: according to XBOOLE_0:def_10 ::_thesis: S c= field ( the InternalRel of A |_2 S)
thus S c= field ( the InternalRel of A |_2 S) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in S or x in field ( the InternalRel of A |_2 S) )
assume A1: x in S ; ::_thesis: x in field ( the InternalRel of A |_2 S)
then A2: [x,x] in [:S,S:] by ZFMISC_1:87;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then [x,x] in the InternalRel of A by A1, RELAT_2:def_1;
then [x,x] in the InternalRel of A |_2 S by A2, XBOOLE_0:def_4;
then x in dom ( the InternalRel of A |_2 S) by XTUPLE_0:def_12;
hence x in field ( the InternalRel of A |_2 S) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
theorem :: ORDERS_2:47
for A being non empty Poset
for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds
S is Chain of A
proof
let A be non empty Poset; ::_thesis: for S being Subset of A st the InternalRel of A |_2 S is being_linear-order holds
S is Chain of A
let S be Subset of A; ::_thesis: ( the InternalRel of A |_2 S is being_linear-order implies S is Chain of A )
assume the InternalRel of A |_2 S is being_linear-order ; ::_thesis: S is Chain of A
then A1: the InternalRel of A |_2 S is connected by ORDERS_1:def_5;
field ( the InternalRel of A |_2 S) = S by Th46;
then A2: the InternalRel of A |_2 S is_connected_in S by A1, RELAT_2:def_14;
S is strongly_connected
proof
let x be set ; :: according to RELAT_2:def_7,ORDERS_2:def_7 ::_thesis: for b1 being set holds
( not x in S or not b1 in S or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in S or not y in S or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A3: ( x in S & y in S ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider a = x, b = y as Element of A ;
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( x = y or x <> y ) ;
suppose x = y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then a <= b ;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then ( [x,y] in the InternalRel of A |_2 S or [y,x] in the InternalRel of A |_2 S ) by A2, A3, RELAT_2:def_6;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
hence S is Chain of A ; ::_thesis: verum
end;
theorem :: ORDERS_2:48
for A being non empty Poset
for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order
proof
let A be non empty Poset; ::_thesis: for C being Chain of A holds the InternalRel of A |_2 C is being_linear-order
let C be Chain of A; ::_thesis: the InternalRel of A |_2 C is being_linear-order
set P = the InternalRel of A |_2 C;
A1: the InternalRel of A |_2 C is_connected_in C
proof
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in C or not b1 in C or x = b1 or [x,b1] in the InternalRel of A |_2 C or [b1,x] in the InternalRel of A |_2 C )
let y be set ; ::_thesis: ( not x in C or not y in C or x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C )
assume A2: ( x in C & y in C ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C )
then A3: ( [x,y] in [:C,C:] & [y,x] in [:C,C:] ) by ZFMISC_1:87;
the InternalRel of A is_strongly_connected_in C by Def7;
then ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A2, RELAT_2:def_7;
hence ( x = y or [x,y] in the InternalRel of A |_2 C or [y,x] in the InternalRel of A |_2 C ) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;
the InternalRel of A is being_partial-order by ORDERS_1:def_4;
then the InternalRel of A |_2 C is being_partial-order by ORDERS_1:26;
hence ( the InternalRel of A |_2 C is reflexive & the InternalRel of A |_2 C is transitive & the InternalRel of A |_2 C is antisymmetric ) by ORDERS_1:def_4; :: according to ORDERS_1:def_5 ::_thesis: the InternalRel of A |_2 C is connected
C = field ( the InternalRel of A |_2 C) by Th46;
hence the InternalRel of A |_2 C is connected by A1, RELAT_2:def_14; ::_thesis: verum
end;
theorem :: ORDERS_2:49
for A being non empty Poset
for S being Subset of A st the InternalRel of A linearly_orders S holds
S is Chain of A
proof
let A be non empty Poset; ::_thesis: for S being Subset of A st the InternalRel of A linearly_orders S holds
S is Chain of A
let S be Subset of A; ::_thesis: ( the InternalRel of A linearly_orders S implies S is Chain of A )
assume the InternalRel of A linearly_orders S ; ::_thesis: S is Chain of A
then ( the InternalRel of A is_reflexive_in S & the InternalRel of A is_connected_in S ) by ORDERS_1:def_8;
then the InternalRel of A is_strongly_connected_in S by ORDERS_1:7;
hence S is Chain of A by Def7; ::_thesis: verum
end;
theorem :: ORDERS_2:50
for A being non empty Poset
for C being Chain of A holds the InternalRel of A linearly_orders C
proof
let A be non empty Poset; ::_thesis: for C being Chain of A holds the InternalRel of A linearly_orders C
let C be Chain of A; ::_thesis: the InternalRel of A linearly_orders C
A1: the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
( the InternalRel of A is_reflexive_in the carrier of A & the InternalRel of A is_transitive_in the carrier of A ) by Def2, Def3;
hence ( the InternalRel of A is_reflexive_in C & the InternalRel of A is_transitive_in C & the InternalRel of A is_antisymmetric_in C ) by A1, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to ORDERS_1:def_8 ::_thesis: the InternalRel of A is_connected_in C
the InternalRel of A is_strongly_connected_in C by Def7;
hence the InternalRel of A is_connected_in C by ORDERS_1:7; ::_thesis: verum
end;
theorem :: ORDERS_2:51
for A being non empty Poset
for a being Element of A holds
( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
let a be Element of A; ::_thesis: ( a is_minimal_in the InternalRel of A iff for b being Element of A holds not b < a )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus ( a is_minimal_in the InternalRel of A implies for b being Element of A holds not b < a ) ::_thesis: ( ( for b being Element of A holds not b < a ) implies a is_minimal_in the InternalRel of A )
proof
assume A2: a is_minimal_in the InternalRel of A ; ::_thesis: for b being Element of A holds not b < a
let b be Element of A; ::_thesis: not b < a
( a = b or not [b,a] in the InternalRel of A ) by A1, A2, ORDERS_1:def_12;
then ( a = b or not b <= a ) by Def5;
hence not b < a by Def6; ::_thesis: verum
end;
assume A3: for b being Element of A holds not b < a ; ::_thesis: a is_minimal_in the InternalRel of A
thus a in field the InternalRel of A by A1; :: according to ORDERS_1:def_12 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or not [b1,a] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or not [y,a] in the InternalRel of A )
assume that
A4: y in field the InternalRel of A and
A5: y <> a and
A6: [y,a] in the InternalRel of A ; ::_thesis: contradiction
reconsider b = y as Element of A by A4, ORDERS_1:15;
b <= a by A6, Def5;
then b < a by A5, Def6;
hence contradiction by A3; ::_thesis: verum
end;
theorem :: ORDERS_2:52
for A being non empty Poset
for a being Element of A holds
( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
let a be Element of A; ::_thesis: ( a is_maximal_in the InternalRel of A iff for b being Element of A holds not a < b )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus ( a is_maximal_in the InternalRel of A implies for b being Element of A holds not a < b ) ::_thesis: ( ( for b being Element of A holds not a < b ) implies a is_maximal_in the InternalRel of A )
proof
assume A2: a is_maximal_in the InternalRel of A ; ::_thesis: for b being Element of A holds not a < b
let b be Element of A; ::_thesis: not a < b
( a = b or not [a,b] in the InternalRel of A ) by A1, A2, ORDERS_1:def_11;
then ( a = b or not a <= b ) by Def5;
hence not a < b by Def6; ::_thesis: verum
end;
assume A3: for b being Element of A holds not a < b ; ::_thesis: a is_maximal_in the InternalRel of A
thus a in field the InternalRel of A by A1; :: according to ORDERS_1:def_11 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or not [a,b1] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or not [a,y] in the InternalRel of A )
assume that
A4: y in field the InternalRel of A and
A5: y <> a and
A6: [a,y] in the InternalRel of A ; ::_thesis: contradiction
reconsider b = y as Element of A by A4, ORDERS_1:15;
a <= b by A6, Def5;
then a < b by A5, Def6;
hence contradiction by A3; ::_thesis: verum
end;
theorem :: ORDERS_2:53
for A being non empty Poset
for a being Element of A holds
( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds
b < a )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds
b < a )
let a be Element of A; ::_thesis: ( a is_superior_of the InternalRel of A iff for b being Element of A st a <> b holds
b < a )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus ( a is_superior_of the InternalRel of A implies for b being Element of A st a <> b holds
b < a ) ::_thesis: ( ( for b being Element of A st a <> b holds
b < a ) implies a is_superior_of the InternalRel of A )
proof
assume A2: a is_superior_of the InternalRel of A ; ::_thesis: for b being Element of A st a <> b holds
b < a
let b be Element of A; ::_thesis: ( a <> b implies b < a )
assume A3: a <> b ; ::_thesis: b < a
then [b,a] in the InternalRel of A by A1, A2, ORDERS_1:def_13;
then b <= a by Def5;
hence b < a by A3, Def6; ::_thesis: verum
end;
assume A4: for b being Element of A st a <> b holds
b < a ; ::_thesis: a is_superior_of the InternalRel of A
thus a in field the InternalRel of A by A1; :: according to ORDERS_1:def_13 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or [b1,a] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or [y,a] in the InternalRel of A )
assume y in field the InternalRel of A ; ::_thesis: ( y = a or [y,a] in the InternalRel of A )
then reconsider b = y as Element of A by ORDERS_1:15;
assume y <> a ; ::_thesis: [y,a] in the InternalRel of A
then b < a by A4;
then b <= a by Def6;
hence [y,a] in the InternalRel of A by Def5; ::_thesis: verum
end;
theorem :: ORDERS_2:54
for A being non empty Poset
for a being Element of A holds
( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds
a < b )
proof
let A be non empty Poset; ::_thesis: for a being Element of A holds
( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds
a < b )
let a be Element of A; ::_thesis: ( a is_inferior_of the InternalRel of A iff for b being Element of A st a <> b holds
a < b )
A1: the carrier of A = field the InternalRel of A by ORDERS_1:15;
thus ( a is_inferior_of the InternalRel of A implies for b being Element of A st a <> b holds
a < b ) ::_thesis: ( ( for b being Element of A st a <> b holds
a < b ) implies a is_inferior_of the InternalRel of A )
proof
assume A2: a is_inferior_of the InternalRel of A ; ::_thesis: for b being Element of A st a <> b holds
a < b
let b be Element of A; ::_thesis: ( a <> b implies a < b )
assume A3: a <> b ; ::_thesis: a < b
then [a,b] in the InternalRel of A by A1, A2, ORDERS_1:def_14;
then a <= b by Def5;
hence a < b by A3, Def6; ::_thesis: verum
end;
assume A4: for b being Element of A st a <> b holds
a < b ; ::_thesis: a is_inferior_of the InternalRel of A
thus a in field the InternalRel of A by A1; :: according to ORDERS_1:def_14 ::_thesis: for b1 being set holds
( not b1 in field the InternalRel of A or b1 = a or [a,b1] in the InternalRel of A )
let y be set ; ::_thesis: ( not y in field the InternalRel of A or y = a or [a,y] in the InternalRel of A )
assume y in field the InternalRel of A ; ::_thesis: ( y = a or [a,y] in the InternalRel of A )
then reconsider b = y as Element of A by ORDERS_1:15;
assume y <> a ; ::_thesis: [a,y] in the InternalRel of A
then a < b by A4;
then a <= b by Def6;
hence [a,y] in the InternalRel of A by Def5; ::_thesis: verum
end;
Lm4: for X, Y being set
for R being Relation st R is_connected_in X & Y c= X holds
R is_connected_in Y
proof
let X, Y be set ; ::_thesis: for R being Relation st R is_connected_in X & Y c= X holds
R is_connected_in Y
let R be Relation; ::_thesis: ( R is_connected_in X & Y c= X implies R is_connected_in Y )
assume A1: ( R is_connected_in X & Y c= X ) ; ::_thesis: R is_connected_in Y
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in Y or not b1 in Y or x = b1 or [x,b1] in R or [b1,x] in R )
let y be set ; ::_thesis: ( not x in Y or not y in Y or x = y or [x,y] in R or [y,x] in R )
assume ( x in Y & y in Y ) ; ::_thesis: ( x = y or [x,y] in R or [y,x] in R )
hence ( x = y or [x,y] in R or [y,x] in R ) by A1, RELAT_2:def_6; ::_thesis: verum
end;
Lm5: for X, Y being set
for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
proof
let X, Y be set ; ::_thesis: for R being Relation st R well_orders X & Y c= X holds
R well_orders Y
let R be Relation; ::_thesis: ( R well_orders X & Y c= X implies R well_orders Y )
assume that
A1: R well_orders X and
A2: Y c= X ; ::_thesis: R well_orders Y
A3: ( R is_antisymmetric_in X & R is_connected_in X ) by A1, WELLORD1:def_5;
A4: R is_well_founded_in X by A1, WELLORD1:def_5;
( R is_reflexive_in X & R is_transitive_in X ) by A1, WELLORD1:def_5;
hence ( R is_reflexive_in Y & R is_transitive_in Y & R is_antisymmetric_in Y & R is_connected_in Y ) by A2, A3, Lm4, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10; :: according to WELLORD1:def_5 ::_thesis: R is_well_founded_in Y
let Z be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Z c= Y or Z = {} or ex b1 being set st
( b1 in Z & R -Seg b1 misses Z ) )
assume that
A5: Z c= Y and
A6: Z <> {} ; ::_thesis: ex b1 being set st
( b1 in Z & R -Seg b1 misses Z )
Z c= X by A2, A5, XBOOLE_1:1;
hence ex b1 being set st
( b1 in Z & R -Seg b1 misses Z ) by A6, A4, WELLORD1:def_3; ::_thesis: verum
end;
theorem Th55: :: ORDERS_2:55
for A being non empty Poset st ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ) holds
ex a being Element of A st
for b being Element of A holds not a < b
proof
let A be non empty Poset; ::_thesis: ( ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ) implies ex a being Element of A st
for b being Element of A holds not a < b )
set f = the Choice_Function of BOOL the carrier of A;
reconsider F = union (Chains the Choice_Function of BOOL the carrier of A) as Chain of the Choice_Function of BOOL the carrier of A by Th45;
assume for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
b <= a ; ::_thesis: ex a being Element of A st
for b being Element of A holds not a < b
then consider a being Element of A such that
A1: for b being Element of A st b in F holds
b <= a ;
take a ; ::_thesis: for b being Element of A holds not a < b
let b be Element of A; ::_thesis: not a < b
assume A2: a < b ; ::_thesis: contradiction
now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_F_holds_
a1_<_b
let a1 be Element of A; ::_thesis: ( a1 in F implies a1 < b )
assume a1 in F ; ::_thesis: a1 < b
then a1 <= a by A1;
hence a1 < b by A2, Th7; ::_thesis: verum
end;
then b in { a1 where a1 is Element of A : for a2 being Element of A st a2 in F holds
a2 < a1 } ;
then not UpperCone F in {{}} by TARSKI:def_1;
then A3: UpperCone F in BOOL the carrier of A by XBOOLE_0:def_5;
not {} in BOOL the carrier of A by ORDERS_1:1;
then A4: the Choice_Function of BOOL the carrier of A . (UpperCone F) in UpperCone F by A3, ORDERS_1:def_1;
then reconsider c = the Choice_Function of BOOL the carrier of A . (UpperCone F) as Element of A ;
reconsider Z = F \/ {c} as Subset of A ;
A5: ex c11 being Element of A st
( c11 = c & ( for a2 being Element of A st a2 in F holds
a2 < c11 ) ) by A4;
A6: the InternalRel of A is_connected_in Z
proof
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in Z or not b1 in Z or x = b1 or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in Z or not y in Z or x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A7: ( x in Z & y in Z ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider x1 = x, y1 = y as Element of A ;
now__::_thesis:_(_x_=_y_or_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( ( x1 in F & y1 in F ) or ( x1 in F & y1 in {c} ) or ( x1 in {c} & y1 in F ) or ( x1 in {c} & y1 in {c} ) ) by A7, XBOOLE_0:def_3;
suppose ( x1 in F & y1 in F ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then ( x1 <= y1 or y1 <= x1 ) by Th11;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
supposeA8: ( x1 in F & y1 in {c} ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then y1 = c by TARSKI:def_1;
then x1 < y1 by A5, A8;
then x1 <= y1 by Def6;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
supposeA9: ( x1 in {c} & y1 in F ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then x1 = c by TARSKI:def_1;
then y1 < x1 by A5, A9;
then y1 <= x1 by Def6;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
supposeA10: ( x1 in {c} & y1 in {c} ) ; ::_thesis: ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then x1 = c by TARSKI:def_1;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by A10, TARSKI:def_1; ::_thesis: verum
end;
end;
end;
hence ( x = y or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
A11: now__::_thesis:_for_a1_being_Element_of_A_st_a1_in_Z_holds_
the_Choice_Function_of_BOOL_the_carrier_of_A_._(UpperCone_(InitSegm_(Z,a1)))_=_a1
let a1 be Element of A; ::_thesis: ( a1 in Z implies the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 )
assume A12: a1 in Z ; ::_thesis: the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1
now__::_thesis:_the_Choice_Function_of_BOOL_the_carrier_of_A_._(UpperCone_(InitSegm_(Z,a1)))_=_a1
percases ( a1 = c or a1 <> c ) ;
supposeA13: a1 = c ; ::_thesis: the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1
InitSegm (Z,c) = F
proof
thus InitSegm (Z,c) c= F :: according to XBOOLE_0:def_10 ::_thesis: F c= InitSegm (Z,c)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (Z,c) or x in F )
assume that
A14: x in InitSegm (Z,c) and
A15: not x in F ; ::_thesis: contradiction
x in Z by A14, XBOOLE_0:def_4;
then x in {c} by A15, XBOOLE_0:def_3;
then A16: x = c by TARSKI:def_1;
x in LowerCone {c} by A14, XBOOLE_0:def_4;
hence contradiction by A16, Th21; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in F or x in InitSegm (Z,c) )
assume A17: x in F ; ::_thesis: x in InitSegm (Z,c)
then reconsider y = x as Element of A ;
y < c by A5, A17;
then A18: x in LowerCone {c} by Th23;
x in Z by A17, XBOOLE_0:def_3;
hence x in InitSegm (Z,c) by A18, XBOOLE_0:def_4; ::_thesis: verum
end;
hence the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 by A13; ::_thesis: verum
end;
suppose a1 <> c ; ::_thesis: the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1
then not a1 in {c} by TARSKI:def_1;
then A19: a1 in F by A12, XBOOLE_0:def_3;
A20: InitSegm (Z,a1) c= InitSegm (F,a1)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in InitSegm (Z,a1) or x in InitSegm (F,a1) )
assume A21: x in InitSegm (Z,a1) ; ::_thesis: x in InitSegm (F,a1)
then A22: x in LowerCone {a1} by XBOOLE_0:def_4;
now__::_thesis:_x_in_F
assume A23: not x in F ; ::_thesis: contradiction
x in Z by A21, XBOOLE_0:def_4;
then x in {c} by A23, XBOOLE_0:def_3;
then x = c by TARSKI:def_1;
then A24: ex c1 being Element of A st
( c1 = c & ( for c2 being Element of A st c2 in {a1} holds
c1 < c2 ) ) by A22;
A25: a1 < c by A5, A19;
a1 in {a1} by TARSKI:def_1;
then c < a1 by A24;
hence contradiction by A25, Th4; ::_thesis: verum
end;
hence x in InitSegm (F,a1) by A22, XBOOLE_0:def_4; ::_thesis: verum
end;
InitSegm (F,a1) c= InitSegm (Z,a1) by Th28, XBOOLE_1:7;
then InitSegm (Z,a1) = InitSegm (F,a1) by A20, XBOOLE_0:def_10;
hence the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 by A19, Def12; ::_thesis: verum
end;
end;
end;
hence the Choice_Function of BOOL the carrier of A . (UpperCone (InitSegm (Z,a1))) = a1 ; ::_thesis: verum
end;
the InternalRel of A is_reflexive_in the carrier of A by Def2;
then A26: the InternalRel of A is_reflexive_in Z by ORDERS_1:8;
then the InternalRel of A is_strongly_connected_in Z by A6, ORDERS_1:7;
then A27: Z is Chain of A by Def7;
A28: the InternalRel of A is_well_founded_in Z
proof
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= Z or Y = {} or ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) )
assume that
A29: Y c= Z and
A30: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y )
now__::_thesis:_(_(_Y_=_{c}_&_ex_x_being_Element_of_A_st_
(_x_in_Y_&_not_the_InternalRel_of_A_-Seg_x_meets_Y_)_)_or_(_Y_<>_{c}_&_ex_x9_being_set_st_
(_x9_in_Y_&_the_InternalRel_of_A_-Seg_x9_misses_Y_)_)_)
percases ( Y = {c} or Y <> {c} ) ;
caseA31: Y = {c} ; ::_thesis: ex x being Element of A st
( x in Y & not the InternalRel of A -Seg x meets Y )
take x = c; ::_thesis: ( x in Y & not the InternalRel of A -Seg x meets Y )
thus x in Y by A31, TARSKI:def_1; ::_thesis: not the InternalRel of A -Seg x meets Y
assume the InternalRel of A -Seg x meets Y ; ::_thesis: contradiction
then consider x9 being set such that
A32: x9 in the InternalRel of A -Seg x and
A33: x9 in Y by XBOOLE_0:3;
x9 = c by A31, A33, TARSKI:def_1;
hence contradiction by A32, WELLORD1:1; ::_thesis: verum
end;
caseA34: Y <> {c} ; ::_thesis: ex x9 being set st
( x9 in Y & the InternalRel of A -Seg x9 misses Y )
set X = Y \ {c};
A35: now__::_thesis:_not_Y_\_{c}_=_{}
assume Y \ {c} = {} ; ::_thesis: contradiction
then Y c= {c} by XBOOLE_1:37;
hence contradiction by A30, A34, ZFMISC_1:33; ::_thesis: verum
end;
A36: Y \ {c} c= F
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y \ {c} or x in F )
assume that
A37: x in Y \ {c} and
A38: not x in F ; ::_thesis: contradiction
x in Y by A37;
then x in {c} by A29, A38, XBOOLE_0:def_3;
hence contradiction by A37, XBOOLE_0:def_5; ::_thesis: verum
end;
the InternalRel of A well_orders F by Def12;
then the InternalRel of A well_orders Y \ {c} by A36, Lm5;
then the InternalRel of A is_well_founded_in Y \ {c} by WELLORD1:def_5;
then consider x being set such that
A39: x in Y \ {c} and
A40: the InternalRel of A -Seg x misses Y \ {c} by A35, WELLORD1:def_3;
take x9 = x; ::_thesis: ( x9 in Y & the InternalRel of A -Seg x9 misses Y )
thus x9 in Y by A39; ::_thesis: the InternalRel of A -Seg x9 misses Y
A41: ( the InternalRel of A -Seg x) /\ (Y \ {c}) = {} by A40, XBOOLE_0:def_7;
now__::_thesis:_the_InternalRel_of_A_-Seg_x9_misses_Y
percases ( c in Y or not c in Y ) ;
supposeA42: c in Y ; ::_thesis: the InternalRel of A -Seg x9 misses Y
A43: now__::_thesis:_not_c_in_the_InternalRel_of_A_-Seg_x9
x9 in F by A36, A39;
then reconsider x99 = x9 as Element of A ;
assume A44: c in the InternalRel of A -Seg x9 ; ::_thesis: contradiction
then [c,x9] in the InternalRel of A by WELLORD1:1;
then A45: c <= x99 by Def5;
A46: x99 < c by A5, A36, A39;
c <> x99 by A44, WELLORD1:1;
then c < x99 by A45, Def6;
hence contradiction by A46, Th4; ::_thesis: verum
end;
A47: now__::_thesis:_not_(_the_InternalRel_of_A_-Seg_x9)_/\_{c}_<>_{}
set x = the Element of ( the InternalRel of A -Seg x9) /\ {c};
assume A48: ( the InternalRel of A -Seg x9) /\ {c} <> {} ; ::_thesis: contradiction
then the Element of ( the InternalRel of A -Seg x9) /\ {c} in {c} by XBOOLE_0:def_4;
then the Element of ( the InternalRel of A -Seg x9) /\ {c} = c by TARSKI:def_1;
hence contradiction by A43, A48, XBOOLE_0:def_4; ::_thesis: verum
end;
{c} c= Y by A42, ZFMISC_1:31;
then Y = (Y \ {c}) \/ {c} by XBOOLE_1:45;
then ( the InternalRel of A -Seg x9) /\ Y = {} \/ {} by A41, A47, XBOOLE_1:23
.= {} ;
hence the InternalRel of A -Seg x9 misses Y by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose not c in Y ; ::_thesis: the InternalRel of A -Seg x9 misses Y
then Y misses {c} by ZFMISC_1:50;
hence the InternalRel of A -Seg x9 misses Y by A40, XBOOLE_1:83; ::_thesis: verum
end;
end;
end;
hence the InternalRel of A -Seg x9 misses Y ; ::_thesis: verum
end;
end;
end;
hence ex b1 being set st
( b1 in Y & the InternalRel of A -Seg b1 misses Y ) ; ::_thesis: verum
end;
the InternalRel of A is_transitive_in the carrier of A by Def3;
then A49: the InternalRel of A is_transitive_in Z by ORDERS_1:10;
the InternalRel of A is_antisymmetric_in the carrier of A by Def4;
then the InternalRel of A is_antisymmetric_in Z by ORDERS_1:9;
then the InternalRel of A well_orders Z by A26, A49, A6, A28, WELLORD1:def_5;
then reconsider Z = Z as Chain of the Choice_Function of BOOL the carrier of A by A27, A11, Def12;
c in {c} by TARSKI:def_1;
then A50: c in Z by XBOOLE_0:def_3;
Z in Chains the Choice_Function of BOOL the carrier of A by Def13;
then c in F by A50, TARSKI:def_4;
hence contradiction by A5; ::_thesis: verum
end;
theorem :: ORDERS_2:56
for A being non empty Poset st ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ) holds
ex a being Element of A st
for b being Element of A holds not b < a
proof
let A be non empty Poset; ::_thesis: ( ( for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ) implies ex a being Element of A st
for b being Element of A holds not b < a )
set X = the carrier of A;
set R = the InternalRel of A ~ ;
A1: dom ( the InternalRel of A ~) = dom the InternalRel of A by RELAT_2:12
.= the carrier of A by PARTFUN1:def_2 ;
A2: for a, b being Element of A holds
( [a,b] in the InternalRel of A ~ iff b <= a )
proof
let a, b be Element of A; ::_thesis: ( [a,b] in the InternalRel of A ~ iff b <= a )
( [a,b] in the InternalRel of A ~ iff [b,a] in the InternalRel of A ) by RELAT_1:def_7;
hence ( [a,b] in the InternalRel of A ~ iff b <= a ) by Def5; ::_thesis: verum
end;
reconsider R = the InternalRel of A ~ as Order of the carrier of A by A1, PARTFUN1:def_2;
set B = RelStr(# the carrier of A,R #);
assume A3: for C being Chain of A ex a being Element of A st
for b being Element of A st b in C holds
a <= b ; ::_thesis: ex a being Element of A st
for b being Element of A holds not b < a
for E being Chain of RelStr(# the carrier of A,R #) ex e being Element of RelStr(# the carrier of A,R #) st
for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
proof
let E be Chain of RelStr(# the carrier of A,R #); ::_thesis: ex e being Element of RelStr(# the carrier of A,R #) st
for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
reconsider C = E as Subset of A ;
the InternalRel of A is_strongly_connected_in C
proof
let x be set ; :: according to RELAT_2:def_7 ::_thesis: for b1 being set holds
( not x in C or not b1 in C or [x,b1] in the InternalRel of A or [b1,x] in the InternalRel of A )
let y be set ; ::_thesis: ( not x in C or not y in C or [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
assume A4: ( x in C & y in C ) ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then reconsider e = x, f = y as Element of RelStr(# the carrier of A,R #) ;
reconsider e1 = e, f1 = f as Element of A ;
A5: ( e <= f or f <= e ) by A4, Th11;
now__::_thesis:_(_[x,y]_in_the_InternalRel_of_A_or_[y,x]_in_the_InternalRel_of_A_)
percases ( [e,f] in R or [f,e] in R ) by A5, Def5;
suppose [e,f] in R ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then f1 <= e1 by A2;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
suppose [f,e] in R ; ::_thesis: ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A )
then e1 <= f1 by A2;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) by Def5; ::_thesis: verum
end;
end;
end;
hence ( [x,y] in the InternalRel of A or [y,x] in the InternalRel of A ) ; ::_thesis: verum
end;
then reconsider C = C as Chain of A by Def7;
consider a being Element of A such that
A6: for b being Element of A st b in C holds
a <= b by A3;
reconsider e = a as Element of RelStr(# the carrier of A,R #) ;
take e ; ::_thesis: for f being Element of RelStr(# the carrier of A,R #) st f in E holds
f <= e
let f be Element of RelStr(# the carrier of A,R #); ::_thesis: ( f in E implies f <= e )
reconsider b = f as Element of A ;
assume f in E ; ::_thesis: f <= e
then a <= b by A6;
then [f,e] in R by A2;
hence f <= e by Def5; ::_thesis: verum
end;
then consider e being Element of RelStr(# the carrier of A,R #) such that
A7: for f being Element of RelStr(# the carrier of A,R #) holds not e < f by Th55;
reconsider d = e as Element of A ;
take d ; ::_thesis: for b being Element of A holds not b < d
let b be Element of A; ::_thesis: not b < d
reconsider f = b as Element of RelStr(# the carrier of A,R #) ;
assume A8: b < d ; ::_thesis: contradiction
then b <= d by Def6;
then [e,f] in R by A2;
then e <= f by Def5;
then e < f by A8, Def6;
hence contradiction by A7; ::_thesis: verum
end;
registration
cluster empty strict for RelStr ;
existence
ex b1 being RelStr st
( b1 is strict & b1 is empty )
proof
take R = RelStr(# {}, the Relation of {} #); ::_thesis: ( R is strict & R is empty )
thus R is strict ; ::_thesis: R is empty
thus the carrier of R is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;