:: Kuratowski - Zorn Lemma
:: by Wojciech A. Trybulec and Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


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 )
proofend;
end;

registration
cluster reflexive  ->  total for RelStr ;
coherence
 for b1 being RelStr st b1 is reflexive holds
b1 is total
proofend;
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
proofend;
end;

registration
let A be total antisymmetric RelStr ;
cluster the InternalRel of A ->  antisymmetric ;
coherence
 the InternalRel of A is antisymmetric
proofend;
end;

registration
let A be total transitive RelStr ;
cluster the InternalRel of A ->  transitive ;
coherence
 the InternalRel of A is transitive
proofend;
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
proofend;
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
proofend;
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
proofend;
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 &amp; 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 &amp; 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
proofend;

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 &amp; a2 <= a1 holds
a1 = a2
proofend;

theorem Th3: :: ORDERS_2:3
for A being transitive RelStr
for a1, a2, a3 being Element of A st a1 <= a2 &amp; a2 <= a3 holds
a1 <= a3
proofend;

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 )
proofend;

theorem Th5: :: ORDERS_2:5
for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st a1 < a2 &amp; a2 < a3 holds
a1 < a3
proofend;

theorem Th6: :: ORDERS_2:6
for A being antisymmetric RelStr
for a1, a2 being Element of A st a1 <= a2 holds
not a2 < a1
proofend;

theorem Th7: :: ORDERS_2:7
for A being transitive antisymmetric RelStr
for a1, a2, a3 being Element of A st ( ( a1 < a2 &amp; a2 <= a3 ) or ( a1 <= a2 &amp; a2 < a3 ) ) holds
a1 < a3
proofend;

::
:: Chains.
::
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
proofend;
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
proofend;
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
proofend;

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 ) )
proofend;

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
proofend;

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 &amp; a2 in C ) )
proofend;

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 &amp; a2 in C ) iff ( a1 < a2 iff not a2 <= a1 ) )
proofend;

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
proofend;

::
:: Upper and lower cones.
::
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
proofend;
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
proofend;
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
proofend;

theorem :: ORDERS_2:15
for A being non empty Poset holds UpperCone ([#] A) = {}
proofend;

theorem :: ORDERS_2:16
for A being non empty Poset holds LowerCone ({} A) = the carrier of A
proofend;

theorem :: ORDERS_2:17
for A being non empty Poset holds LowerCone ([#] A) = {}
proofend;

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
proofend;

theorem :: ORDERS_2:19
for A being non empty Poset
for a being Element of A holds not a in UpperCone {a}
proofend;

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
proofend;

theorem Th21: :: ORDERS_2:21
for A being non empty Poset
for a being Element of A holds not a in LowerCone {a}
proofend;

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} )
proofend;

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} )
proofend;

::
:: Initial segments.
::
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 &amp; 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 &amp; b1 = InitSegm (S,a) ) ) &amp; ( not S <> {} implies ex b1 being Subset of A st b1 = {} ) )
proofend;
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 &amp; b3 = InitSegm (S,a) ) ) ) &amp; ( 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 &amp; a in S ) )
proofend;

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)
proofend;

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)
proofend;

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)
proofend;

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
proofend;

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 )
proofend;

theorem Th31: :: ORDERS_2:31
for A being non empty Poset
for S, T being Subset of A st S <> {} &amp; S is Initial_Segm of T holds
not T is Initial_Segm of S
proofend;

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 &amp; a1 in S &amp; a2 in T &amp; T is Initial_Segm of S holds
a1 in T
proofend;

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 &amp; S is Initial_Segm of T holds
InitSegm (S,a) = InitSegm (T,a)
proofend;

theorem :: ORDERS_2:34
for A being non empty Poset
for S, T being Subset of A st S c= T &amp; the InternalRel of A well_orders T &amp; ( for a1, a2 being Element of A st a2 in S &amp; a1 < a2 holds
a1 in S ) &amp; not S = T holds
S is Initial_Segm of T
proofend;

theorem Th35: :: ORDERS_2:35
for A being non empty Poset
for S, T being Subset of A st S c= T &amp; the InternalRel of A well_orders T &amp; ( for a1, a2 being Element of A st a2 in S &amp; a1 in T &amp; a1 < a2 holds
a1 in S ) &amp; not S = T holds
S is Initial_Segm of T
proofend;

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 <> {} &amp; the InternalRel of A well_orders it &amp; ( 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 <> {} &amp; the InternalRel of A well_orders b1 &amp; ( for a being Element of A st a in b1 holds
f . (UpperCone (InitSegm (b1,a))) = a ) )
proofend;
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 <> {} &amp; the InternalRel of A well_orders b3 &amp; ( 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
proofend;

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
proofend;

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 &amp; b = f . the carrier of A holds
b <= a
proofend;

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) = {}
proofend;

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
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff x is Chain of f ) ) &amp; ( for x being set holds
( x in b2 iff x is Chain of f ) ) holds
b1 = b2
proofend;
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
proofend;
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
proofend;

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
proofend;

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) <> {}
proofend;

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) &amp; S = union (Chains f) holds
fC is Initial_Segm of S
proofend;

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
proofend;

begin

::
:: Orders.
::
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
proofend;

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
proofend;

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
proofend;

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
proofend;

theorem :: ORDERS_2:50
for A being non empty Poset
for C being Chain of A holds the InternalRel of A linearly_orders C
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

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 )
proofend;

Lm4:  for X, Y being set
for R being Relation st R is_connected_in X &amp; Y c= X holds
R is_connected_in Y
proofend;

Lm5:  for X, Y being set
for R being Relation st R well_orders X &amp; Y c= X holds
R well_orders Y
proofend;

::
:: Kuratowski - Zorn Lemma.
::
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
proofend;

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
proofend;

:: from YELLOW14, 2009.07.26, A.T.
registration
cluster empty strict for RelStr ;
existence
 ex b1 being RelStr st
( b1 is strict &amp; b1 is empty )
proofend;
end;