:: Morphisms Into Chains, Part {I}
::  by Artur Korni{\l}owicz
::
:: Received February 6, 2003
:: Copyright (c) 2003-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 XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, ORDERS_2, WAYBEL_4,
      RELAT_1, RELAT_2, LATTICE3, LATTICES, FUNCT_1, YELLOW_1, LATTICE7,
      WAYBEL_0, SEQM_3, XXREAL_0, TARSKI, ARYTM_3, GROUP_4, ORDERS_1, WELLORD2,
      WELLORD1, YELLOW_0, EQREL_1, REWRITE1, WAYBEL_1, ORDINAL2, NUMBERS,
      CARD_1, NAT_1, WAYBEL35, FUNCT_7;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS,
      XCMPLX_0, NAT_1, RELAT_1, RELAT_2, FUNCT_1, RELSET_1, FUNCT_2, DOMAIN_1,
      FUNCT_7, STRUCT_0, WELLORD1, ORDERS_2, ORDERS_1, LATTICE3, YELLOW_0,
      YELLOW_1, ALG_1, WAYBEL_0, WAYBEL_1, WAYBEL_4, LATTICE7;
 constructors WELLORD1, NAT_1, REALSET1, ORDERS_3, WAYBEL_1, WAYBEL_4,
      LATTICE7, RELSET_1, NUMBERS, FUNCT_7;
 registrations SUBSET_1, ORDINAL1, RELSET_1, STRUCT_0, LATTICE3, YELLOW_0,
      WAYBEL_0, YELLOW_1, YELLOW_2, WAYBEL_4, ZFMISC_1, CARD_1;
 requirements SUBSET, BOOLE, NUMERALS;


begin

begin :: Main part

registration
  let L be RelStr;
  cluster auxiliary(i) for Relation of L;
end;

registration
  let L be transitive RelStr;
  cluster auxiliary(i) auxiliary(ii) for Relation of L;
end;

registration
  let L be with_suprema antisymmetric RelStr;
  cluster auxiliary(iii) for Relation of L;
end;

registration
  let L be non empty lower-bounded antisymmetric RelStr;
  cluster auxiliary(iv) for Relation of L;
end;

:: Definition 2.1, p. 203

definition
  let L be non empty RelStr, R be Relation of L;
  attr R is extra-order means
:: WAYBEL35:def 1

  R is auxiliary(i) auxiliary(ii) auxiliary(iv);
end;

registration
  let L be non empty RelStr;
  cluster extra-order -> auxiliary(i) auxiliary(ii) auxiliary(iv) for
Relation of
    L;
  cluster auxiliary(i) auxiliary(ii) auxiliary(iv) -> extra-order for
Relation of
    L;
end;

registration
  let L be non empty RelStr;
  cluster extra-order auxiliary(iii) -> auxiliary for Relation of L;
  cluster auxiliary -> extra-order for Relation of L;
end;

registration
  let L be lower-bounded antisymmetric transitive non empty RelStr;
  cluster extra-order for Relation of L;
end;

definition
  let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;
  func R-LowerMap -> Function of L, InclPoset LOWER L means
:: WAYBEL35:def 2

  for x being Element of L holds it.x = R-below x;
end;

registration
  let L be lower-bounded with_suprema Poset, R be auxiliary(ii) Relation of L;
  cluster R-LowerMap -> monotone;
end;

definition
  let L be 1-sorted, R be Relation of the carrier of L;
  mode strict_chain of R -> Subset of L means
:: WAYBEL35:def 3

    for x, y being set st x
    in it & y in it holds [x,y] in R or x = y or [y,x] in R;
end;

theorem :: WAYBEL35:1
  for L being 1-sorted, C being trivial Subset of L, R being
  Relation of the carrier of L holds C is strict_chain of R;

registration
  let L be non empty 1-sorted, R be Relation of the carrier of L;
  cluster 1-element for strict_chain of R;
end;

theorem :: WAYBEL35:2
  for L being antisymmetric RelStr, R being auxiliary(i) (Relation
of L), C being strict_chain of R, x, y being Element of L st x in C & y in C &
  x < y holds [x,y] in R;

theorem :: WAYBEL35:3
  for L being antisymmetric RelStr, R being auxiliary(i) (Relation of L)
  , x, y being Element of L st [x,y] in R & [y,x] in R holds x = y;

theorem :: WAYBEL35:4
  for L being non empty lower-bounded antisymmetric RelStr, x being
  Element of L, R being auxiliary(iv) Relation of L holds {Bottom L, x} is
  strict_chain of R;

theorem :: WAYBEL35:5
  for L being non empty lower-bounded antisymmetric RelStr, R being
auxiliary(iv) (Relation of L), C being strict_chain of R holds C \/ {Bottom L}
  is strict_chain of R;

definition
  let L be 1-sorted, R be (Relation of the carrier of L), C be strict_chain of
  R;
  attr C is maximal means
:: WAYBEL35:def 4

  for D being strict_chain of R st C c= D holds C = D;
end;

definition
  let L be 1-sorted, R be (Relation of the carrier of L), C be set;
  func Strict_Chains (R,C) -> set means
:: WAYBEL35:def 5

  for x being set holds x in it iff x is strict_chain of R & C c= x;
end;

registration
  let L be 1-sorted, R be (Relation of the carrier of L), C be strict_chain of
  R;
  cluster Strict_Chains (R,C) -> non empty;
end;

notation
  let R be Relation, X be set;
  synonym X is_inductive_wrt R for X has_upper_Zorn_property_wrt R;
end;

:: Lemma 2.2, p. 203

theorem :: WAYBEL35:6
  for L being 1-sorted, R being (Relation of the carrier of L), C being
  strict_chain of R holds Strict_Chains (R,C) is_inductive_wrt RelIncl
Strict_Chains (R,C) & ex D being set st D is_maximal_in RelIncl Strict_Chains (
  R,C) & C c= D;

:: Lemma 2.3 (ii), p. 203
:: It is a trivial consequence of YELLOW_0:65
:: Maybe to cancel

theorem :: WAYBEL35:7
  for L being non empty transitive RelStr, C being non empty
  Subset of L, X being Subset of C st ex_sup_of X,L & "\/"(X,L) in C holds
  ex_sup_of X,subrelstr C & "\/"(X,L) = "\/"(X,subrelstr C);

:: Lemma 2.3, p. 203

theorem :: WAYBEL35:8
  for L being non empty Poset, R being auxiliary(i) auxiliary(ii)
  (Relation of L), C being non empty strict_chain of R, X being Subset of C st
  ex_sup_of X,L & C is maximal holds ex_sup_of X,subrelstr C;

:: Lemma 2.3 (i), (iii), p. 203

theorem :: WAYBEL35:9
  for L being non empty Poset, R being auxiliary(i) auxiliary(ii) (
  Relation of L), C being non empty strict_chain of R, X being Subset of C st
ex_inf_of (uparrow "\/"(X,L)) /\ C,L & ex_sup_of X,L & C is maximal holds "\/"(
X,subrelstr C) = "/\"((uparrow "\/"(X,L)) /\ C,L) & (not "\/"(X,L) in C implies
  "\/"(X,L) < "/\"((uparrow "\/"(X,L)) /\ C,L));

:: Proposition 2.4, p. 204

theorem :: WAYBEL35:10
  for L being complete non empty Poset, R being auxiliary(i)
  auxiliary(ii) (Relation of L), C being non empty strict_chain of R st C is
  maximal holds subrelstr C is complete;

:: Proposition 2.5 (i), p. 204

theorem :: WAYBEL35:11
  for L being non empty lower-bounded antisymmetric RelStr, R being
auxiliary(iv) (Relation of L), C being strict_chain of R st C is maximal holds
  Bottom L in C;

:: Proposition 2.5 (ii), p. 204

theorem :: WAYBEL35:12
  for L being non empty upper-bounded Poset, R being auxiliary(ii) (
Relation of L), C being strict_chain of R, m being Element of L st C is maximal
  & m is_maximum_of C & [m,Top L] in R holds [Top L,Top L] in R & m = Top L;

:: Definition (SI_C) p. 204

definition
  let L be RelStr, C be set, R be Relation of the carrier of L;
  pred R satisfies_SIC_on C means
:: WAYBEL35:def 6

  for x, z being Element of L holds x
in C & z in C & [x,z] in R & x <> z implies ex y being Element of L st y in C &
  [x,y] in R & [y,z] in R & x <> y;
end;

definition
  let L be RelStr, R be (Relation of the carrier of L), C be strict_chain of R;
  attr C is satisfying_SIC means
:: WAYBEL35:def 7

  R satisfies_SIC_on C;
end;

theorem :: WAYBEL35:13
  for L being RelStr, C being set, R being auxiliary(i) (Relation
of L) st R satisfies_SIC_on C holds for x, z being Element of L holds x in C &
z in C & [x,z] in R & x <> z implies ex y being Element of L st y in C & [x,y]
  in R & [y,z] in R & x < y;

registration
  let L be RelStr, R be Relation of the carrier of L;
  cluster trivial -> satisfying_SIC for strict_chain of R;
end;

registration
  let L be non empty RelStr, R be Relation of the carrier of L;
  cluster 1-element for strict_chain of R;
end;

:: Proposition 2.5 (iii), p. 204

theorem :: WAYBEL35:14
  for L being lower-bounded with_suprema Poset, R being auxiliary(i)
auxiliary(ii) (Relation of L), C being strict_chain of R st C is maximal & R is
  satisfying_SI holds R satisfies_SIC_on C;

definition
  let R be Relation, C be set, y be object;
  func SetBelow (R,C,y) -> set equals
:: WAYBEL35:def 8
  ( R"{y} ) /\ C;
end;

theorem :: WAYBEL35:15
  for R being Relation, C, x, y being set holds x in SetBelow (R,C
  ,y) iff [x,y] in R & x in C;

definition
  let L be 1-sorted, R be (Relation of the carrier of L),
      C be set, y be object;
  redefine func SetBelow (R,C,y) -> Subset of L;
end;

theorem :: WAYBEL35:16
  for L being RelStr, R being auxiliary(i) (Relation of L), C
  being set, y being Element of L holds SetBelow (R,C,y) is_<=_than y;

theorem :: WAYBEL35:17
  for L being reflexive transitive RelStr, R being auxiliary(ii) (
  Relation of L), C being Subset of L, x, y being Element of L st x <= y holds
  SetBelow (R,C,x) c= SetBelow (R,C,y);

theorem :: WAYBEL35:18
  for L being RelStr, R being auxiliary(i) (Relation of L), C
being set, x being Element of L st x in C & [x,x] in R & ex_sup_of SetBelow (R,
  C,x),L holds x = sup SetBelow (R,C,x);

definition
  let L be RelStr, C be Subset of L;
  attr C is sup-closed means
:: WAYBEL35:def 9

  for X being Subset of C st ex_sup_of X,L
  holds "\/"(X,L) = "\/"(X,subrelstr C);
end;

:: Lemma 2.6, p. 205

theorem :: WAYBEL35:19
  for L being complete non empty Poset, R being extra-order (
Relation of L), C being satisfying_SIC strict_chain of R, p, q being Element of
L st p in C & q in C & p < q ex y being Element of L st p < y & [y,q] in R & y
  = sup SetBelow (R,C,y);

:: Lemma 2.7, p. 205,  1 => 2

theorem :: WAYBEL35:20
  for L being lower-bounded non empty Poset, R being extra-order (
Relation of L), C being non empty strict_chain of R st C is sup-closed & (for c
  being Element of L st c in C holds ex_sup_of SetBelow (R,C,c),L) & R
  satisfies_SIC_on C holds for c being Element of L st c in C holds c = sup
  SetBelow (R,C,c);

:: Lemma 2.7, p. 205, 2 => 1

theorem :: WAYBEL35:21
  for L being non empty reflexive antisymmetric RelStr, R being
auxiliary(i) (Relation of L), C being strict_chain of R st (for c being Element
  of L st c in C holds ex_sup_of SetBelow (R,C,c),L & c = sup SetBelow (R,C,c))
  holds R satisfies_SIC_on C;

definition
  let L be non empty RelStr, R be (Relation of the carrier of L), C be set;
  func SupBelow (R,C) -> set means
:: WAYBEL35:def 10

  for y being set holds y in it iff y = sup SetBelow (R,C,y);
end;

definition
  let L be non empty RelStr, R be (Relation of the carrier of L), C be set;
  redefine func SupBelow (R,C) -> Subset of L;
end;

:: Lemma 2.8, (i) a), p. 205

theorem :: WAYBEL35:22
  for L being non empty reflexive transitive RelStr, R being
auxiliary(i) auxiliary(ii) (Relation of L), C being strict_chain of R st (for c
being Element of L holds ex_sup_of SetBelow (R,C,c),L) holds SupBelow (R,C) is
  strict_chain of R;

:: Lemma 2.8, (i) b), p. 205

theorem :: WAYBEL35:23
  for L being non empty Poset, R being auxiliary(i) auxiliary(ii) (
  Relation of L), C being Subset of L st (for c being Element of L holds
  ex_sup_of SetBelow (R,C,c),L) holds SupBelow (R,C) is sup-closed;

theorem :: WAYBEL35:24
  for L being complete non empty Poset, R being extra-order (
Relation of L), C being satisfying_SIC strict_chain of R, d being Element of L
st d in SupBelow (R,C) holds d = "\/"({b where b is Element of L: b in SupBelow
  (R,C) & [b,d] in R},L);

:: Lemma 2.8, (ii), p. 205

theorem :: WAYBEL35:25
  for L being complete non empty Poset, R being extra-order (Relation of
L), C being satisfying_SIC strict_chain of R holds R satisfies_SIC_on SupBelow
  (R,C);

:: Lemma 2.8, (iii), p. 205

theorem :: WAYBEL35:26
  for L being complete non empty Poset, R being extra-order (Relation of
L), C being satisfying_SIC strict_chain of R, a, b being Element of L st a in C
& b in C & a < b ex d being Element of L st d in SupBelow (R,C) & a < d & [d,b]
  in R;