:: Kuratowski - Zorn Lemma
::  by Wojciech A. Trybulec and Grzegorz Bancerek
::
:: Received September 19, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies STRUCT_0, RELAT_1, XBOOLE_0, PARTFUN1, RELAT_2, ORDERS_1,
      SUBSET_1, XXREAL_0, ARYTM_3, TREES_2, TARSKI, WELLORD1, FUNCT_1,
      ZFMISC_1, ORDERS_2, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1,
      RELSET_1, PARTFUN1, CARD_1, WELLORD1, DOMAIN_1, STRUCT_0, ORDERS_1;
 constructors RELAT_2, WELLORD1, PARTFUN1, DOMAIN_1, ORDERS_1, PRE_TOPC,
      RELSET_1, SETFAM_1;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PARTFUN1, CARD_1,
      RELAT_2;
 requirements BOOLE, SUBSET;


begin :: Original ORDERS_1

reserve X,Y,x,y for set;

definition
  struct(1-sorted) RelStr (# carrier -> set, InternalRel -> Relation of the
    carrier #);
end;

registration
  let X be non empty set;
  let R be Relation of X;
  cluster RelStr(#X,R#) -> non empty;
end;

definition
  let A be RelStr;
  attr A is total means
:: ORDERS_2:def 1

  the InternalRel of A is total;
  attr A is reflexive means
:: ORDERS_2:def 2

  the InternalRel of A is_reflexive_in the carrier of A;
  attr A is transitive means
:: ORDERS_2:def 3

  the InternalRel of A is_transitive_in the carrier of A;
  attr A is antisymmetric means
:: ORDERS_2:def 4

  the InternalRel of A is_antisymmetric_in the carrier of A;
end;

registration
  cluster reflexive transitive antisymmetric strict total 1-element for RelStr;
end;

registration
  cluster reflexive -> total for RelStr;
end;

definition
  mode Poset is reflexive transitive antisymmetric RelStr;
end;

registration
  let A be total RelStr;
  cluster the InternalRel of A -> total;
end;

registration
  let A be reflexive RelStr;
  cluster the InternalRel of A -> reflexive;
end;

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

registration
  let A be transitive RelStr;
  cluster the InternalRel of A -> transitive;
end;

registration
  let X be set;
  let O be total reflexive Relation of X;
  cluster RelStr(#X,O#) -> reflexive;
end;

registration
  let X be set;
  let O be total transitive Relation of X;
  cluster RelStr(#X,O#) -> transitive;
end;

registration
  let X be set;
  let O be total antisymmetric Relation of X;
  cluster RelStr(#X,O#) -> antisymmetric;
end;

reserve A for non empty Poset;
reserve a,a1,a2,a3,b,c for Element of A;
reserve S,T for Subset of A;

definition
  let A be RelStr;
  let a1,a2 be Element of A;

  pred a1 <= a2 means
:: ORDERS_2:def 5

  [a1,a2] in the InternalRel of A;
end;

notation
  let A be RelStr;
  let a1,a2 be Element of A;
  synonym a2 >= a1 for a1 <= a2;
end;

definition
  let A be RelStr;
  let a1,a2 be Element of A;
  pred a1 < a2 means
:: ORDERS_2:def 6

  a1 <= a2 & a1 <> a2;
  irreflexivity;
end;

notation
  let A be RelStr;
  let a1,a2 be Element of A;
  synonym a2 > a1 for a1 < a2;
end;

theorem :: ORDERS_2:1
  for A being reflexive non empty RelStr, a being Element of A holds a <= a;

definition
  let A be reflexive non empty RelStr;
  let a1,a2 be Element of A;
  redefine pred a1 <= a2;
  reflexivity;
end;

theorem :: ORDERS_2:2
  for A being antisymmetric RelStr, a1,a2 being Element of A st a1
  <= a2 & a2 <= a1 holds a1 = a2;

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

theorem :: ORDERS_2:4
  for A being antisymmetric RelStr, a1,a2 being Element of A holds
  not(a1 < a2 & a2 < a1);

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

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

theorem :: ORDERS_2:7
  for A being transitive antisymmetric RelStr for a1,a2,a3 being
  Element of A holds a1 < a2 & a2 <= a3 or a1 <= a2 & a2 < a3 implies a1 < a3;

::
::  Chains.
::

definition
  let A be RelStr;
  let IT be Subset of A;
  attr IT is strongly_connected means
:: ORDERS_2:def 7

  the InternalRel of A is_strongly_connected_in IT;
end;

registration
  let A be RelStr;
  cluster empty -> strongly_connected for Subset of A;
end;

registration
  let A be RelStr;
  cluster strongly_connected for Subset of A;
end;

definition
  let A be RelStr;
  mode Chain of A is strongly_connected Subset of A;
end;

theorem :: ORDERS_2:8
  for A being non empty reflexive RelStr for a being Element of A
  holds {a} is Chain of A;

theorem :: ORDERS_2:9
  for A being non empty reflexive RelStr, a1,a2 being Element of A
  holds {a1,a2} is Chain of A iff a1 <= a2 or a2 <= a1;

theorem :: ORDERS_2:10
  for A being RelStr, C being Chain of A, S being Subset of A holds S c=
  C implies S is Chain of A;

theorem :: ORDERS_2:11
  for A being reflexive RelStr, a1,a2 being Element of A holds (ex
  C being Chain of A st a1 in C & a2 in C) iff a1 <= a2 or a2 <= a1;

theorem :: ORDERS_2:12
  for A being reflexive antisymmetric RelStr, a1,a2 being Element
of A holds (ex C being Chain of A st a1 in C & a2 in C) iff (a1 < a2 iff not a2
  <= a1);

theorem :: ORDERS_2:13
  for A being RelStr, T being Subset of A holds the InternalRel of
  A well_orders T implies T is Chain of A;

::
::  Upper and lower cones.
::

definition
  let A;
  let S;
  func UpperCone(S) -> Subset of A equals
:: ORDERS_2:def 8
  {a1 : for a2 st a2 in S holds a2 <
  a1};
end;

definition
  let A;
  let S;
  func LowerCone(S) -> Subset of A equals
:: ORDERS_2:def 9
  {a1 : for a2 st a2 in S holds a1 <
  a2};
end;

theorem :: ORDERS_2:14
  UpperCone({}(A)) = the carrier of A;

theorem :: ORDERS_2:15
  UpperCone([#](A)) = {};

theorem :: ORDERS_2:16
  LowerCone({}(A)) = the carrier of A;

theorem :: ORDERS_2:17
  LowerCone([#](A)) = {};

theorem :: ORDERS_2:18
  a in S implies not a in UpperCone(S);

theorem :: ORDERS_2:19
  not a in UpperCone{a};

theorem :: ORDERS_2:20
  a in S implies not a in LowerCone(S);

theorem :: ORDERS_2:21
  not a in LowerCone{a};

theorem :: ORDERS_2:22
  c < a iff a in UpperCone{c};

theorem :: ORDERS_2:23
  a < c iff a in LowerCone{c};

::
::  Initial segments.
::

definition
  let A;
  let S;
  let a;
  func InitSegm(S,a) -> Subset of A equals
:: ORDERS_2:def 10
  LowerCone{a} /\ S;
end;

definition
  let A;
  let S;
  mode Initial_Segm of S -> Subset of A means
:: ORDERS_2:def 11

    ex a st a in S & it = InitSegm(S,a) if S <> {} otherwise it = {};
end;

theorem :: ORDERS_2:24
  a in InitSegm(S,b) iff a < b & a in S;

theorem :: ORDERS_2:25
  InitSegm({}(A),a) = {};

theorem :: ORDERS_2:26
  not a in InitSegm(S,a);

theorem :: ORDERS_2:27
  a1 < a2 implies InitSegm(S,a1) c= InitSegm(S,a2);

theorem :: ORDERS_2:28
  S c= T implies InitSegm(S,a) c= InitSegm(T,a);

theorem :: ORDERS_2:29
  for I being Initial_Segm of S holds I c= S;

theorem :: ORDERS_2:30
  S <> {} iff not S is Initial_Segm of S;

theorem :: ORDERS_2:31
  S <> {} & S is Initial_Segm of T implies not T is Initial_Segm of S;

theorem :: ORDERS_2:32
  a1 < a2 & a1 in S & a2 in T & T is Initial_Segm of S implies a1 in T;

theorem :: ORDERS_2:33
  a in S & S is Initial_Segm of T implies InitSegm(S,a) = InitSegm (T,a);

theorem :: ORDERS_2:34
  S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2 in S &
  a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T;

theorem :: ORDERS_2:35
  S c= T & the InternalRel of A well_orders T & (for a1,a2 st a2
in S & a1 in T & a1 < a2 holds a1 in S) implies S = T or S is Initial_Segm of T
;

::
::  Chains of choice function of BOOL of partially ordered sets.
::

reserve f for Choice_Function of BOOL(the carrier of A);

definition
  let A;
  let f;
  mode Chain of f -> Chain of A means
:: ORDERS_2:def 12

    it <> {} & the InternalRel of A
    well_orders it & for a st a in it holds f.UpperCone(InitSegm(it,a)) = a;
end;

reserve fC,fC1,fC2 for Chain of f;

theorem :: ORDERS_2:36
  {f.(the carrier of A)} is Chain of f;

theorem :: ORDERS_2:37
  f.(the carrier of A) in fC;

theorem :: ORDERS_2:38
  a in fC & b = f.(the carrier of A) implies b <= a;

theorem :: ORDERS_2:39
  a = f.(the carrier of A) implies InitSegm(fC,a) = {};

theorem :: ORDERS_2:40
  fC1 meets fC2;

theorem :: ORDERS_2:41
  fC1 <> fC2 implies (fC1 is Initial_Segm of fC2 iff not fC2 is
  Initial_Segm of fC1);

theorem :: ORDERS_2:42
  fC1 c< fC2 iff fC1 is Initial_Segm of fC2;

definition
  let A;
  let f;
  func Chains f -> set means
:: ORDERS_2:def 13

  x in it iff x is Chain of f;
end;

registration
  let A;
  let f;
  cluster Chains f -> non empty;
end;

theorem :: ORDERS_2:43
  union(Chains(f)) <> {};

theorem :: ORDERS_2:44
  fC <> union(Chains(f)) & S = union(Chains(f)) implies fC is Initial_Segm of S
;

theorem :: ORDERS_2:45
  union(Chains(f)) is Chain of f;

begin :: From original ORDERS_2

reserve R for Relation,
  A for non empty Poset,
  C for Chain of A,
  S for Subset of A,
  a,a1,a2,b,c1,c2 for Element of A;

::
::  Orders.
::

theorem :: ORDERS_2:46
  field((the InternalRel of A) |_2 S) = S;

theorem :: ORDERS_2:47
  (the InternalRel of A) |_2 S is being_linear-order implies S is Chain of A;

theorem :: ORDERS_2:48
  (the InternalRel of A) |_2 C is being_linear-order;

theorem :: ORDERS_2:49
  the InternalRel of A linearly_orders S implies S is Chain of A;

theorem :: ORDERS_2:50
  the InternalRel of A linearly_orders C;

theorem :: ORDERS_2:51
  a is_minimal_in the InternalRel of A iff for b holds not b < a;

theorem :: ORDERS_2:52
  a is_maximal_in the InternalRel of A iff for b holds not a < b;

theorem :: ORDERS_2:53
  a is_superior_of the InternalRel of A iff for b st a <> b holds b < a;

theorem :: ORDERS_2:54
  a is_inferior_of the InternalRel of A iff for b st a <> b holds a < b;

::
::  Kuratowski - Zorn Lemma.
::

theorem :: ORDERS_2:55
  (for C ex a st for b st b in C holds b <= a) implies ex a st
  for b holds not a < b;

theorem :: ORDERS_2:56
  (for C ex a st for b st b in C holds a <= b) implies ex a st for b
  holds not b < a;

:: from YELLOW14, 2009.07.26, A.T.

registration
  cluster strict empty for RelStr;
end;