:: The Well Ordering Relations
::  by Grzegorz Bancerek
::
:: Received April 4, 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 RELAT_1, RELAT_2, XBOOLE_0, SUBSET_1, TARSKI, FUNCT_1, ZFMISC_1,
      WELLORD1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELAT_2, FUNCT_1;
 constructors TARSKI, SUBSET_1, FUNCT_1, RELAT_2, XTUPLE_0;
 registrations FUNCT_1, RELAT_1;
 requirements SUBSET, BOOLE;


begin

reserve a,b,c,d,x,y,z for object, X,Y,Z for set;
reserve R,S,T for Relation;

definition
  let R; let a be object;
  func R-Seg(a) -> set equals
:: WELLORD1:def 1
  Coim(R,a) \ {a};
end;

theorem :: WELLORD1:1
  x in R-Seg a iff x <> a & [x,a] in R;

theorem :: WELLORD1:2
  x in field R or R-Seg(x) = {};

definition
  let R;
  attr R is well_founded means
:: WELLORD1:def 2

  for Y st Y c= field R & Y <> {} ex a st a in Y & R-Seg a misses Y;
  let X;
  pred R is_well_founded_in X means
:: WELLORD1:def 3

  for Y st Y c= X & Y <> {} ex a st a in Y & R-Seg a misses Y;
end;

theorem :: WELLORD1:3
  R is well_founded iff R is_well_founded_in field R;

definition
  let R;
  attr R is well-ordering means
:: WELLORD1:def 4

  R is reflexive & R is transitive & R is
  antisymmetric & R is connected & R is well_founded;
  let X;
  pred R well_orders X means
:: WELLORD1:def 5

  R is_reflexive_in X & R is_transitive_in X
  & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X;
end;

registration
  cluster well-ordering ->
          reflexive transitive antisymmetric connected well_founded
  for Relation;
  cluster reflexive transitive antisymmetric connected well_founded
          -> well-ordering for Relation;
end;

theorem :: WELLORD1:4
  R well_orders field R iff R is well-ordering;

theorem :: WELLORD1:5
  R well_orders X implies for Y st Y c= X & Y <> {} ex a st a in Y & for
  b st b in Y holds [a,b] in R;

theorem :: WELLORD1:6
  R is well-ordering implies for Y st Y c= field R & Y <> {} ex a
  st a in Y & for b st b in Y holds [a,b] in R;

theorem :: WELLORD1:7
  for R st R is well-ordering & field R <> {} ex a st a in field R & for
  b st b in field R holds [a,b] in R;

theorem :: WELLORD1:8
  for R st R is well-ordering for a st a in field R holds (for b st b in
field R holds [b,a] in R) or ex b st b in field R & [a,b] in R & for c st c in
  field R & [a,c] in R holds c = a or [b,c] in R;

reserve F,G for Function;

theorem :: WELLORD1:9
  R-Seg(a) c= field R;

definition
  let R,Y;
  func R |_2 Y -> Relation equals
:: WELLORD1:def 6
  R /\ [:Y,Y:];
end;

theorem :: WELLORD1:10
  R |_2 X = X|`R|X;

theorem :: WELLORD1:11
  R |_2 X = X|`(R|X);

theorem :: WELLORD1:12
  x in field(R |_2 X) implies x in field R & x in X;

theorem :: WELLORD1:13
  field(R |_2 X) c= field R & field(R |_2 X) c= X;

theorem :: WELLORD1:14
  (R |_2 X)-Seg(a) c= R-Seg(a);

theorem :: WELLORD1:15
  R is reflexive implies R |_2 X is reflexive;

theorem :: WELLORD1:16
  R is connected implies R |_2 Y is connected;

theorem :: WELLORD1:17
  R is transitive implies R |_2 Y is transitive;

theorem :: WELLORD1:18
  R is antisymmetric implies R |_2 Y is antisymmetric;

theorem :: WELLORD1:19
  (R |_2 X) |_2 Y = R |_2 (X /\ Y);

theorem :: WELLORD1:20
  (R |_2 X) |_2 Y = (R |_2 Y) |_2 X;

theorem :: WELLORD1:21
  (R |_2 Y) |_2 Y = R |_2 Y;

theorem :: WELLORD1:22
  Z c= Y implies (R |_2 Y) |_2 Z = R |_2 Z;

theorem :: WELLORD1:23
  R |_2 field R = R;

theorem :: WELLORD1:24
  R is well_founded implies R |_2 X is well_founded;

theorem :: WELLORD1:25
  R is well-ordering implies R |_2 Y is well-ordering;

theorem :: WELLORD1:26
  R is well-ordering implies R-Seg(a),R-Seg(b) are_c=-comparable;

theorem :: WELLORD1:27
  R is well-ordering & b in R-Seg(a) implies (R |_2 (R-Seg(a)))
  -Seg(b) = R-Seg(b);

theorem :: WELLORD1:28
  R is well-ordering & Y c= field R implies (Y = field R or (ex a
st a in field R & Y = R-Seg(a) ) iff for a st a in Y for b st [b,a] in R holds
  b in Y );

theorem :: WELLORD1:29
  R is well-ordering & a in field R & b in field R implies ( [a,b]
  in R iff R-Seg(a) c= R-Seg(b) );

theorem :: WELLORD1:30
  R is well-ordering & a in field R & b in field R implies ( R-Seg
  (a) c= R-Seg(b) iff a = b or a in R-Seg(b) );

theorem :: WELLORD1:31
  R is well-ordering & X c= field R implies field(R |_2 X) = X;

theorem :: WELLORD1:32
  R is well-ordering implies field(R |_2 R-Seg(a)) = R-Seg(a);

theorem :: WELLORD1:33
  R is well-ordering implies for Z st for a st a in field R & R
  -Seg(a) c= Z holds a in Z holds field R c= Z;

theorem :: WELLORD1:34
  R is well-ordering & a in field R & b in field R & (for c st c
  in R-Seg(a) holds [c,b] in R & c <> b) implies [a,b] in R;

theorem :: WELLORD1:35
  R is well-ordering & dom F = field R & rng F c= field R & (for a
,b st [a,b] in R & a <> b holds [F.a,F.b] in R & F.a <> F.b) implies for a st a
  in field R holds [a,F.a] in R;

definition
  let R,S,F;
  pred F is_isomorphism_of R,S means
:: WELLORD1:def 7

  dom F = field R & rng F = field S
& F is one-to-one & for a,b holds [a,b] in R iff a in field R & b in field R &
  [F.a,F.b] in S;
end;

theorem :: WELLORD1:36
  F is_isomorphism_of R,S implies for a,b st [a,b] in R & a <> b
  holds [F.a,F.b] in S & F.a <> F.b;

definition
  let R,S;
  pred R,S are_isomorphic means
:: WELLORD1:def 8

  ex F st F is_isomorphism_of R,S;
end;

theorem :: WELLORD1:37
  id(field R) is_isomorphism_of R,R;

theorem :: WELLORD1:38
  R,R are_isomorphic;

theorem :: WELLORD1:39
  F is_isomorphism_of R,S implies F" is_isomorphism_of S,R;

theorem :: WELLORD1:40
  R,S are_isomorphic implies S,R are_isomorphic;

theorem :: WELLORD1:41
  F is_isomorphism_of R,S & G is_isomorphism_of S,T implies G*F
  is_isomorphism_of R,T;

theorem :: WELLORD1:42
  R,S are_isomorphic & S,T are_isomorphic implies R,T are_isomorphic;

theorem :: WELLORD1:43
  F is_isomorphism_of R,S implies ( R is reflexive implies S is
  reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected
implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) &
  ( R is well_founded implies S is well_founded );

theorem :: WELLORD1:44
  R is well-ordering & F is_isomorphism_of R,S implies S is well-ordering;

theorem :: WELLORD1:45
  R is well-ordering implies for F,G st F is_isomorphism_of R,S &
  G is_isomorphism_of R,S holds F = G;

definition
  let R,S;
  assume that
 R is well-ordering and
 R,S are_isomorphic;
  func canonical_isomorphism_of(R,S) -> Function means
:: WELLORD1:def 9

  it is_isomorphism_of R,S;
end;

theorem :: WELLORD1:46
  R is well-ordering implies for a st a in field R holds
  not R,R |_2 (R-Seg(a)) are_isomorphic;

theorem :: WELLORD1:47
  R is well-ordering & a in field R & b in field R & a <> b
  implies not R |_2 (R-Seg(a)),R |_2 (R-Seg(b)) are_isomorphic;

theorem :: WELLORD1:48
  R is well-ordering & Z c= field R & F is_isomorphism_of R,S
  implies F|Z is_isomorphism_of R |_2 Z,S |_2 (F.:Z) & R |_2 Z,S |_2 (F.:Z)
  are_isomorphic;

theorem :: WELLORD1:49
  F is_isomorphism_of R,S implies for a st a in field R ex b st b
  in field S & F.:(R-Seg(a)) = S-Seg(b);

theorem :: WELLORD1:50
  R is well-ordering & F is_isomorphism_of R,S implies for a st a
  in field R ex b st b in field S & R |_2 (R-Seg(a)),S |_2 (S-Seg(b))
  are_isomorphic;

theorem :: WELLORD1:51
  R is well-ordering & S is well-ordering & a in field R & b in
field S & c in field S & R,S |_2 (S-Seg(b)) are_isomorphic & R |_2 (R-Seg(a)),S
  |_2 (S-Seg(c)) are_isomorphic implies S-Seg(c) c= S-Seg(b) & [c,b] in S;

theorem :: WELLORD1:52
  R is well-ordering & S is well-ordering implies R,S
  are_isomorphic or (ex a st a in field R & R |_2 (R-Seg(a)),S are_isomorphic )
  or ex a st a in field S & R,S |_2 (S-Seg(a)) are_isomorphic;

theorem :: WELLORD1:53
  Y c= field R & R is well-ordering implies R,R |_2 Y are_isomorphic or
  ex a st a in field R & R |_2 (R-Seg(a)),R |_2 Y are_isomorphic;

:: from AMISTD_3, 2010.01.10, A.T.

theorem :: WELLORD1:54
  R,S are_isomorphic & R is well-ordering implies S is well-ordering;