The Mizar article:

On Same Equivalents of Well-foundedness

by
Piotr Rudnicki, and
Andrzej Trybulec

Received February 25, 1997

Copyright (c) 1997 Association of Mizar Users

MML identifier: WELLFND1
[ MML identifier index ]


environ

 vocabulary PARTFUN1, FRAENKEL, FUNCT_1, RELAT_1, BOOLE, TARSKI, CARD_1,
      CARD_5, ORDINAL2, ORDERS_1, WELLORD1, WAYBEL_0, SETFAM_1, CAT_1, FUNCT_4,
      CARD_2, FINSET_1, ORDINAL1, REALSET1, FUNCOP_1, NEWTON, NORMSP_1,
      WELLFND1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NUMBERS, NAT_1, RELAT_1,
      FUNCT_1, SETFAM_1, STRUCT_0, RELSET_1, PARTFUN1, FUNCT_2, FUNCT_4,
      FUNCOP_1, ORDINAL1, WELLORD1, ORDINAL2, FINSET_1, CARD_1, CARD_2,
      ORDERS_1, FRAENKEL, REALSET1, CQC_LANG, NORMSP_1, CARD_5, RFUNCT_3,
      WAYBEL_0;
 constructors NAT_1, WELLORD1, DOMAIN_1, CARD_2, REALSET1, FUNCT_4, CQC_LANG,
      NORMSP_1, CARD_5, RFUNCT_3, WAYBEL_0, FRAENKEL, MEMBERED;
 clusters SUBSET_1, STRUCT_0, RELSET_1, ORDERS_1, FRAENKEL, REALSET1, NORMSP_1,
      CARD_5, ALTCAT_1, WAYBEL_0, FUNCOP_1, CQC_LANG, PARTFUN1, CARD_1,
      MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE;
 definitions TARSKI, RELAT_1, FUNCT_1, WELLORD1, WAYBEL_0, FRAENKEL, XBOOLE_0;
 theorems TARSKI, ENUMSET1, ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1, ORDINAL1,
      WELLORD1, GRFUNC_1, PARTFUN1, FUNCT_2, ORDINAL2, FUNCOP_1, CARD_1,
      ORDERS_1, FUNCT_4, FRAENKEL, CQC_LANG, NORMSP_1, CARD_4, CARD_5, SPPOL_1,
      AMI_5, WAYBEL_0, SETFAM_1, XBOOLE_0, XBOOLE_1;
 schemes NAT_1, SUBSET_1, RECDEF_1, FUNCT_2, DOMAIN_1, FUNCT_7;

begin :: Preliminaries

:: General preliminaries :::::::::::::::::::::::::::::::::::::::::::::

definition let A, B be set;
  cluster PFuncs(A,B) -> functional;
  coherence
   proof
    let x be set;
    assume x in PFuncs(A,B);
     then ex f being Function st x = f & dom f c= A & rng f c= B
      by PARTFUN1:def 5;
    hence x is Function;
   end;
end;

definition
 let R be 1-sorted, X be set,
     p be PartFunc of the carrier of R, X;
 redefine func dom p -> Subset of R;
 coherence
  proof dom p c= the carrier of R; hence thesis; end;
end;

theorem Th1:
 for X being set, f, g being Function
  st f c= g & X c= dom f holds f|X = g|X
proof let X be set, f, g be Function; assume
A1: f c= g & X c= dom f;
  hence f|X = g|(dom f)|X by GRFUNC_1:64
           .= g|(X/\ dom f) by RELAT_1:100
           .= g|X by A1,XBOOLE_1:28;
end;

theorem Th2:
 for X being functional set
  st for f, g being Function st f in X & g in X holds f tolerates g
   holds union X is Function
proof let X be functional set; assume
A1: for f, g being Function st f in X & g in X holds f tolerates g;
A2: union X is Relation-like
    proof let x be set; assume x in union X;
         then consider ux being set such that
    A3: x in ux & ux in X by TARSKI:def 4;
           ux is Function by A3,FRAENKEL:def 1;
         hence thesis by A3,RELAT_1:def 1;
    end;
      union X is Function-like
    proof let x,y1,y2 be set; assume
    A4: [x,y1] in union X & [x,y2] in union X & y1<>y2;
         then consider fx being set such that
    A5: [x, y1] in fx & fx in X by TARSKI:def 4;
         consider gx being set such that
    A6: [x, y2] in gx & gx in X by A4,TARSKI:def 4;
         reconsider fx, gx as Function by A5,A6,FRAENKEL:def 1;
           fx tolerates gx by A1,A5,A6;
         then consider h being Function such that
    A7: fx c= h & gx c= h by PARTFUN1:131;
         thus contradiction by A4,A5,A6,A7,FUNCT_1:def 1;
    end;
 hence union X is Function by A2;
end;

scheme PFSeparation {X, Y() -> set, P[set]}:
 ex PFS being Subset of PFuncs(X(), Y()) st
  for pfs being PartFunc of X(), Y() holds pfs in PFS iff P[pfs]
proof defpred p[set] means P[$1];
     consider fs being Subset of PFuncs (X(), Y()) such that
A1: for f being set holds f in fs iff f in PFuncs(X(), Y()) & p[f]
                                            from Subset_Ex;
 take fs;
 let pfs be PartFunc of X(), Y();
       pfs in PFuncs(X(), Y()) by PARTFUN1:119;
 hence thesis by A1;
end;

:: Cardinals ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

definition
 let X be set;
 cluster nextcard X -> non empty;
 coherence by CARD_1:def 6;
end;

definition
 cluster regular Aleph;
 existence by CARD_5:42;
end;

theorem Th3:
 for M being regular Aleph, X being set
  st X c= M & Card X in M holds sup X in M
proof let M be regular Aleph;
     cf M = M by CARD_5:def 4;
 hence thesis by CARD_5:38;
end;

:: Relational structures ::::::::::::::::::::::::::::::::::::::::::::::

theorem Th4:
 for R being RelStr, x being set
  holds (the InternalRel of R)-Seg x c= the carrier of R
proof let R be RelStr, x be set;
  set r = the InternalRel of R, c = the carrier of R;
    r-Seg x c= field r & field r c= c \/ c by RELSET_1:19,WELLORD1:13;
 hence r-Seg x c= c by XBOOLE_1:1;
end;

definition
 let R be RelStr, X be Subset of R;
 redefine
 attr X is lower means :Def1:
  for x, y being set
   st x in X & [y, x] in the InternalRel of R holds y in X;
 compatibility proof
  hereby assume
  A1: X is lower;
   let x, y be set such that
  A2: x in X and
  A3: [y, x] in the InternalRel of R;
         x in the carrier of R & y in the carrier of R
                                               by A3,ZFMISC_1:106;
       then reconsider x' = x, y' = y as Element of R;
         y' <= x' by A3,ORDERS_1:def 9;
   hence y in X by A1,A2,WAYBEL_0:def 19;
  end;
  assume
A4: for x, y being set
      st x in X & [y, x] in the InternalRel of R holds y in X;
  let x,y be Element of R such that
A5: x in X;
  assume y <= x; then [y,x] in the InternalRel of R by ORDERS_1:def 9;
  hence thesis by A4,A5;
 end;
end;

theorem Th5:
 for R being RelStr, X being Subset of R, x being set
  st X is lower & x in X holds (the InternalRel of R)-Seg x c= X
proof let R be RelStr, X be Subset of R, x be set such that
A1: X is lower & x in X;
 let z be set; assume z in (the InternalRel of R)-Seg x;
     then [z,x] in (the InternalRel of R) by WELLORD1:def 1;
 hence z in X by A1,Def1;
end;

theorem Th6:
 for R being RelStr, X being lower Subset of R,
     Y being Subset of R, x being set
  st Y = X \/ {x} & (the InternalRel of R)-Seg x c= X
   holds Y is lower
proof let R be RelStr, X be lower Subset of R, Y be Subset of R,
          x be set;
  set r = the InternalRel of R;
 assume
A1: Y = X \/ {x} & r-Seg x c= X;
 let z, y be set; assume
A2: z in Y & [y, z] in r;
 per cases by A1,A2,XBOOLE_0:def 2;
 suppose z in X; then y in X by A2,Def1;
  hence y in Y by A1,XBOOLE_0:def 2;
 suppose z in {x} & y = z;
  hence thesis by A2;
 suppose
 A3: z in {x} & y <> z; then z = x by TARSKI:def 1;
      then y in r-Seg x by A2,A3,WELLORD1:def 1;
  hence thesis by A1,XBOOLE_0:def 2;
end;

begin :: Well-founded relational structures

definition
 let R be RelStr;
 attr R is well_founded means :Def2:
 the InternalRel of R is_well_founded_in the carrier of R;
end;

definition
 cluster non empty well_founded RelStr;
 existence proof
     reconsider er = {} as Relation of {{}} by RELSET_1:25;
  take R = RelStr(#{{}}, er#);
  thus R is non empty;
  let Y be set;
  assume Y c= the carrier of R & Y <> {};
then A1: Y = {{}} by ZFMISC_1:39;
  take e = {};
  thus e in Y by A1,TARSKI:def 1;
  assume (the InternalRel of R)-Seg e /\ Y <> {};
   then consider x being set such that
A2: x in (the InternalRel of R)-Seg e /\ Y by XBOOLE_0:def 1;
       x in (the InternalRel of R)-Seg e & x in Y by A2,XBOOLE_0:def 3;
  hence contradiction by WELLORD1:def 1;
 end;
end;

definition
 let R be RelStr, X be Subset of R;
 attr X is well_founded means :Def3:
 the InternalRel of R is_well_founded_in X;
end;

definition
 let R be RelStr;
 cluster well_founded Subset of R;
 existence proof {} c= the carrier of R by XBOOLE_1:2;
  then reconsider e = {} as Subset of R;
  take e; let Y be set; assume Y c= e & Y <> {};
  hence thesis by XBOOLE_1:3;
 end;
end;

definition
 let R be RelStr;
 func well_founded-Part R -> Subset of R means :Def4:
  it = union {S where S is Subset of R : S is well_founded lower};
 existence proof
   set IT = {S where S is Subset of R : S is well_founded lower};
     IT c= bool the carrier of R
   proof let x be set; assume x in IT;
        then ex S being Subset of R st x = S & S is well_founded lower;
    hence x in bool the carrier of R;
   end;
   then reconsider IT as Subset-Family of R by SETFAM_1:def 7;
     union IT is Subset of R;
  hence thesis;
 end;
 uniqueness;
end;

definition
 let R be RelStr;
 cluster well_founded-Part R -> lower well_founded;
 coherence proof
   set wfp = well_founded-Part R,
       r = the InternalRel of R,
       IT = {S where S is Subset of R : S is well_founded lower};
A1: wfp = union IT by Def4;
  hereby let x, y be set; assume
  A2: x in wfp & [y, x] in r;
       then consider Y being set such that
  A3: x in Y & Y in IT by A1,TARSKI:def 4;
       consider S being Subset of R such that
  A4: Y = S & S is well_founded lower by A3;
         y in S by A2,A3,A4,Def1;
   hence y in wfp by A1,A3,A4,TARSKI:def 4;
  end;
  let Y be set; assume
A5: Y c= wfp & Y <> {};
     then consider y being set such that
A6: y in Y by XBOOLE_0:def 1;
     consider YY being set such that
A7: y in YY & YY in IT by A1,A5,A6,TARSKI:def 4;
     consider S being Subset of R such that
A8: YY = S & S is well_founded lower by A7;
A9: r is_well_founded_in S by A8,Def3;
   set YS = Y /\ S;
       YS c= S & YS <> {} by A6,A7,A8,XBOOLE_0:def 3,XBOOLE_1:17;
     then consider a being set such that
A10: a in YS & r-Seg a misses YS by A9,WELLORD1:def 3;
A11: a in Y & a in S by A10,XBOOLE_0:def 3;
     then r-Seg a c= S by A8,Th5;
then A12:   r-Seg a /\ Y = r-Seg a /\ S /\ Y by XBOOLE_1:28
                 .= r-Seg a /\ YS by XBOOLE_1:16;
       r-Seg a /\ YS = {} by A10,XBOOLE_0:def 7;
     then r-Seg a misses Y by A12,XBOOLE_0:def 7;
  hence thesis by A11;
 end;
end;

theorem Th7:
 for R being non empty RelStr, x be Element of R
  holds {x} is well_founded Subset of R
proof
 let R be non empty RelStr, x be Element of R;
  set r = the InternalRel of R;
  reconsider sx = {x} as Subset of R;
    sx is well_founded
  proof let Y be set; assume
  A1:  Y c= sx & Y <> {};
   take x;
          Y = sx by A1,ZFMISC_1:39;
   hence x in Y by TARSKI:def 1;
   assume not thesis; then consider a being set such that
   A2: a in r-Seg x /\ Y by XBOOLE_0:4;
          a in r-Seg x & a in Y by A2,XBOOLE_0:def 3;
        then a <> x & a = x by A1,TARSKI:def 1,WELLORD1:def 1;
   hence contradiction;
  end;
 hence thesis;
end;

theorem Th8:
 for R being RelStr, X, Y being well_founded Subset of R
  st X is lower holds X \/ Y is well_founded Subset of R
proof let R be RelStr, X, Y be well_founded Subset of R;
  set r = the InternalRel of R;
  assume
A1: X is lower;
A2: r is_well_founded_in X by Def3;
A3: r is_well_founded_in Y by Def3;
  reconsider XY = X \/ Y as Subset of R;
    XY is well_founded
  proof let Z be set such that
  A4: Z c= XY & Z <> {};
    set XZ = X /\ Z;
  A5: XZ c= X by XBOOLE_1:17;
   per cases;
    suppose XZ = {}; then X misses Z by XBOOLE_0:def 7;
    then Z c= Y by A4,XBOOLE_1:73;
     hence thesis by A3,A4,WELLORD1:def 3;
    suppose XZ <> {}; then consider a being set such that
    A6: a in XZ & r-Seg a misses XZ by A2,A5,WELLORD1:def 3;
     take a;
     thus a in Z by A6,XBOOLE_0:def 3;
     assume r-Seg a /\ Z <> {}; then consider b being set such that
    A7: b in r-Seg a /\ Z by XBOOLE_0:def 1;
    A8: b in r-Seg a & b in Z by A7,XBOOLE_0:def 3;
    then A9: b <> a & [b,a] in r by WELLORD1:def 1;
           a in X by A6,XBOOLE_0:def 3;
         then b in X by A1,A9,Def1;
         then b in XZ by A8,XBOOLE_0:def 3;
     hence contradiction by A6,A8,XBOOLE_0:3;
  end;
 hence thesis;
end;

theorem Th9:
 for R being RelStr
  holds R is well_founded iff well_founded-Part R = the carrier of R
proof let R be RelStr;
  set r = the InternalRel of R, c = the carrier of R,
      wfp = well_founded-Part R;
     c c= c;
   then reconsider cs = c as Subset of R;
   set IT = {S where S is Subset of R : S is well_founded lower};
A1: wfp = union IT by Def4;
 hereby assume
 A2: R is well_founded;
 A3: cs is lower proof let x, y be set; thus thesis by ZFMISC_1:106;
                  end;
        r is_well_founded_in cs by A2,Def2;
      then cs is well_founded by Def3; then cs in IT by A3;
      then cs c= wfp by A1,ZFMISC_1:92;
  hence wfp = c by XBOOLE_0:def 10;
 end;
 assume
A4: wfp = c;
 let Y be set; assume
A5: Y c= c & Y <> {};
     then consider y being set such that
A6: y in Y by XBOOLE_0:def 1;
     consider YY being set such that
A7: y in YY & YY in IT by A1,A4,A5,A6,TARSKI:def 4;
     consider S being Subset of R such that
A8: YY = S & S is well_founded lower by A7;
A9: r is_well_founded_in S by A8,Def3;
   set YS = Y /\ S;
       YS c= S & YS <> {} by A6,A7,A8,XBOOLE_0:def 3,XBOOLE_1:17;
     then consider a being set such that
A10: a in YS & r-Seg a misses YS by A9,WELLORD1:def 3;
A11:   r-Seg a /\ YS = {} by A10,XBOOLE_0:def 7;
A12: a in Y & a in S by A10,XBOOLE_0:def 3;
     then r-Seg a c= S by A8,Th5;
     then r-Seg a /\ Y = r-Seg a /\ S /\ Y by XBOOLE_1:28
                .= r-Seg a /\ YS by XBOOLE_1:16;
     then r-Seg a misses Y by A11,XBOOLE_0:def 7;
 hence thesis by A12;
end;

theorem Th10:
 for R being non empty RelStr,
     x being Element of R
  st (the InternalRel of R)-Seg x c= well_founded-Part R
   holds x in well_founded-Part R
proof let R be non empty RelStr, x be Element of R;
   set wfp = well_founded-Part R,
       IT = {S where S is Subset of R : S is well_founded lower},
       xwfp = wfp \/ {x};
A1: wfp = union IT by Def4;
       x in {x} by TARSKI:def 1;
then A2: x in xwfp by XBOOLE_0:def 2;
     reconsider xwfp as Subset of R;
 assume (the InternalRel of R)-Seg x c= wfp;
then A3: xwfp is lower by Th6;
       {x} is well_founded Subset of R by Th7;
     then xwfp is well_founded by Th8; then xwfp in IT by A3;
 hence x in wfp by A1,A2,TARSKI:def 4;
end;

:: Well-founded induction :::::::::::::::::::::::::::::::::::::::::::::

scheme WFMin {R() -> non empty RelStr,
              x() -> Element of R(),
              P[set]}:
 ex x being Element of R() st P[x] &
   not ex y being Element of R()
        st x <> y & P[y] & [y,x] in the InternalRel of R()
provided
A1: P[x()] and
A2: R() is well_founded
proof defpred p[set] means P[$1];
   set c = the carrier of R(),
       r = the InternalRel of R(),
       Z = {x where x is Element of c: p[x]};
A3: Z is Subset of c from SubsetD;
       x() in Z by A1;
     then reconsider Z as non empty Subset of c by A3;
       r is_well_founded_in c by A2,Def2;
     then consider a being set such that
A4: a in Z & r-Seg a misses Z by WELLORD1:def 3;
     reconsider a as Element of R() by A4;
 take a;
       ex a' being Element of c st a' = a & P[a'] by A4;
 hence P[a];
 given y being Element of R() such that
A5: a <> y & P[y] & [y,a] in r;
       y in Z & y in r-Seg a by A5,WELLORD1:def 1;
 hence contradiction by A4,XBOOLE_0:3;
end;

theorem Th11: :: WF iff WFInduction
for R being non empty RelStr holds
 R is well_founded iff
 for S being set
  st for x being Element of R
      st (the InternalRel of R)-Seg x c= S holds x in S
   holds the carrier of R c= S
proof let R be non empty RelStr;
  set c = the carrier of R,
      r = the InternalRel of R;
 hereby assume
 A1: R is well_founded;
  let S be set such that
 A2: for x being Element of c st r-Seg x c= S holds x in S;
  assume not c c= S;
      then consider x being set such that
 A3: x in c & not x in S by TARSKI:def 3;
      reconsider x as Element of R by A3;
      defpred P[set] means $1 in c & not $1 in S;
 A4: P[x] by A3;
      consider x0 being Element of R such that
 A5: P[x0] and
 A6: not ex y being Element of R
         st x0 <> y & P[y] & [y,x0] in r from WFMin(A4, A1);
      now assume not r-Seg x0 c= S;
         then consider z being set such that
    A7: z in r-Seg x0 & not z in S by TARSKI:def 3;
    A8: x0 <> z & [z, x0] in r by A7,WELLORD1:def 1;
         then z in c by ZFMISC_1:106;
         then reconsider z as Element of R;
           z = z;
     hence contradiction by A6,A7,A8;
    end;
  hence contradiction by A2,A5;
 end;
 assume
A9: for S being set
      st for x being Element of c st r-Seg x c= S holds x in S
       holds c c= S;
 assume not R is well_founded;
     then not r is_well_founded_in c by Def2;
     then consider Y being set such that
A10: Y c= c & Y <> {} and
A11: not ex a being set st a in Y & r-Seg a misses Y by WELLORD1:def 3;
       now let x be Element of c such that
     A12: r-Seg x c= c\Y;
      assume not x in c\Y;
          then x in Y by XBOOLE_0:def 4;
          then r-Seg x meets Y by A11;
          then consider z being set such that
     A13: z in r-Seg x & z in Y by XBOOLE_0:3;
       thus contradiction by A12,A13,XBOOLE_0:def 4;
     end;
     then c c= c\Y by A9; then Y c= c\Y by A10,XBOOLE_1:1;
 hence contradiction by A10,XBOOLE_1:38;
end;

scheme WFInduction {R() -> non empty RelStr, P[set]}:
 for x being Element of R() holds P[x]
provided
A1: for x being Element of R()
      st for y being Element of R()
          st y <> x & [y,x] in the InternalRel of R() holds P[y]
       holds P[x]
    and
A2: R() is well_founded
proof
   set c = the carrier of R(),
       r = the InternalRel of R(),
       Z = {x where x is Element of c: P[x]};
       now let x be Element of c such that
     A3: r-Seg x c= Z;
          reconsider x' = x as Element of R();
            now let y' be Element of R(); assume
                 y' <> x' & [y',x'] in r;
               then y' in r-Seg x' by WELLORD1:def 1; then y' in Z by A3;
               then consider y being Element of c such that
          A4: y = y' & P[y];
           thus P[y'] by A4;
          end; then P[x'] by A1;
      hence x in Z;
     end;
then A5: c c= Z by A2,Th11;
 let x be Element of R();
       x in c; then x in Z by A5;
     then consider x' being Element of c such that
A6: x = x' & P[x'];
 thus thesis by A6;
end;

:: Well-foundedness and recursive definitions :::::::::::::::::::::::::

definition
 let R be non empty RelStr, V be non empty set,
     H be Function of
       [:the carrier of R, PFuncs(the carrier of R, V):], V,
     F be Function;
 pred F is_recursively_expressed_by H means :Def5:
  for x being Element of R
   holds F.x = H.[x, F|(the InternalRel of R)-Seg x];
end;

theorem :: Well foundedness and existence
  for R being non empty RelStr holds
 R is well_founded iff
 for V being non empty set,
     H being Function of
       [:the carrier of R, PFuncs(the carrier of R, V):], V
  ex F being Function of the carrier of R, V
   st F is_recursively_expressed_by H
proof let R be non empty RelStr;
   set c = the carrier of R,
       r = the InternalRel of R;

 defpred PDR[ ] means
         for V being non empty set,
             H being Function of [:c, PFuncs(c, V):], V
          ex F being Function of c, V
           st F is_recursively_expressed_by H;

 thus R is well_founded implies PDR[ ]
 proof assume
A1: R is well_founded;
  let V be non empty set,
      H be Function of [:c, PFuncs(c, V):], V;
     defpred P[PartFunc of c, V] means
     dom $1 is lower &
     for x being set st x in dom $1
      holds $1.x = H.[x, $1 | r-Seg x];
     consider fs being Subset of PFuncs(c, V) such that
A2: for f being PartFunc of c, V holds f in fs iff P[f] from PFSeparation;
       now let f, g be Function; assume
     A3: f in fs & g in fs;
          then reconsider ff = f, gg = g as PartFunc of c,V by PARTFUN1:120;
      assume not f tolerates g;
          then consider x being set such that
     A4: x in dom ff /\ dom gg & ff.x <> gg.x by PARTFUN1:def 6;
          reconsider x as Element of R by A4;
          defpred P[set] means $1 in dom ff & $1 in dom gg & ff.$1 <> gg.$1;
     A5: P[x] by A4,XBOOLE_0:def 3;
          consider x0 being Element of R such that
     A6: P[x0] and
     A7: not ex y being Element of R
               st x0 <> y & P[y] & [y,x0] in the InternalRel of R
                                                  from WFMin(A5, A1);
       ff | r-Seg x0 = gg | r-Seg x0
          proof set fr = ff | r-Seg x0,
                    gr = gg | r-Seg x0;
           assume
          A8: not thesis;
          A9: dom ff is lower by A2,A3;
               then r-Seg x0 c= dom ff by A6,Th5;
          then A10: dom fr = r-Seg x0 by RELAT_1:91;
          A11: dom gg is lower by A2,A3;
               then r-Seg x0 c= dom gg by A6,Th5;
               then dom fr = dom gr by A10,RELAT_1:91;
               then consider x1 being set such that
          A12: x1 in dom fr & fr.x1 <> gr.x1 by A8,FUNCT_1:9;
          A13: [x1, x0] in r by A10,A12,WELLORD1:def 1;
               reconsider x1 as Element of R by A12;
          A14: fr.x1 = ff.x1 & gr.x1 = gg.x1 by A10,A12,FUNCT_1:72;
          A15: x1 <> x0 by A10,A12,WELLORD1:def 1;
                 x1 in dom ff & x1 in dom gg by A6,A9,A11,A13,Def1;
           hence contradiction by A7,A12,A13,A14,A15;
          end;
          then ff.x0 = H.[x0, gg | r-Seg x0] by A2,A3,A6
               .= gg.x0 by A2,A3,A6;
      hence contradiction by A6;
     end;
     then reconsider ufs=union fs as Function by Th2;

A16: dom ufs c= c
     proof let y be set; assume y in dom ufs;
          then [y, ufs.y] in ufs by FUNCT_1:8;
          then consider fx being set such that
     A17: [y, ufs.y] in fx & fx in fs by TARSKI:def 4;
          consider ff being Function such that
     A18: ff = fx & dom ff c= c & rng ff c= V by A17,PARTFUN1:def 5;
            y in dom ff by A17,A18,RELAT_1:def 4;
     hence y in c by A18;
    end;

A19: rng ufs c= V
     proof let y be set; assume y in rng ufs;
          then consider x being set such that
     A20: x in dom ufs & y = ufs.x by FUNCT_1:def 5;
            [x, y] in ufs by A20,FUNCT_1:8;
          then consider fx being set such that
     A21: [x, y] in fx & fx in fs by TARSKI:def 4;
          consider ff being Function such that
     A22: ff = fx & dom ff c= c & rng ff c= V by A21,PARTFUN1:def 5;
            y in rng ff by A21,A22,RELAT_1:def 5;
      hence y in V by A22;
     end;

A23: now let x be set;
      assume x in dom ufs;
          then [x, ufs.x] in ufs by FUNCT_1:8;
          then consider fx being set such that
     A24: [x, ufs.x] in fx & fx in fs by TARSKI:def 4;
          reconsider ff = fx as PartFunc of c, V by A24,PARTFUN1:120;
     A25: x in dom ff by A24,FUNCT_1:8;
            dom ff is lower by A2,A24;
     then A26: r-Seg x c= dom ff by A25,Th5;
     A27: ff c= ufs by A24,ZFMISC_1:92;
      thus ufs.x = ff.x by A24,FUNCT_1:8
                .= H.[x, ff | r-Seg x] by A2,A24,A25
                .= H.[x, ufs | r-Seg x] by A26,A27,Th1;
     end;

A28: now let x, y be set; assume
     A29: x in dom ufs & [y, x] in r;
          then [x, ufs.x] in ufs by FUNCT_1:8;
          then consider fx being set such that
     A30: [x, ufs.x] in fx & fx in fs by TARSKI:def 4;
          reconsider ff = fx as PartFunc of c, V by A30,PARTFUN1:120;
     A31: dom ff is lower by A2,A30;
            x in dom ff by A30,FUNCT_1:8;
     then A32: y in dom ff by A29,A31,Def1;
            ff c= ufs by A30,ZFMISC_1:92;
          then dom ff c= dom ufs by GRFUNC_1:8;
      hence y in dom ufs by A32;
     end;

A33: dom ufs = c
     proof assume dom ufs <> c;
          then consider x being set such that
     A34: not (x in dom ufs iff x in c) by TARSKI:2;
          reconsider x as Element of R by A16,A34;
          defpred P[set] means $1 in c & not $1 in dom ufs;
     A35: P[x] by A34;
          consider x0 being Element of R such that
     A36: P[x0] and
     A37: not ex y being Element of R
               st x0 <> y & P[y] & [y,x0] in the InternalRel of R
                                      from WFMin(A35, A1);

        set nv = x0 .--> H.[x0, ufs | r-Seg x0],
            nf = ufs +* nv;

     A38: dom nf = dom ufs \/ dom nv by FUNCT_4:def 1;
     A39: dom nv = {x0} by CQC_LANG:5;
          then x0 in dom nv by TARSKI:def 1;
          then x0 in dom nf by A38,XBOOLE_0:def 2;
     then A40:  [x0, nf.x0] in nf by FUNCT_1:8;
     A41: dom nf c= c
          proof let x be set; assume
          A42: x in dom nf & not x in c;
               then not x in dom ufs by A16;
               then x in dom nv by A38,A42,XBOOLE_0:def 2;
           hence contradiction by A39,A42;
          end;
            rng nf c= V
          proof let x be set; assume
          A43: x in rng nf;
          A44: rng nf c= rng ufs \/ rng nv by FUNCT_4:18;
           assume
          A45: not x in V; then not x in rng ufs by A19;
          then A46: x in rng nv by A43,A44,XBOOLE_0:def 2;
                 rng nv = {H.[x0, ufs | r-Seg x0]} by CQC_LANG:5;
          then A47: x = H.[x0, ufs | r-Seg x0] by A46,TARSKI:def 1;
                 ufs in PFuncs(c, V) by A16,A19,PARTFUN1:def 5;
               then ufs is PartFunc of c, V by PARTFUN1:120;
               then ufs | r-Seg x0 is PartFunc of c, V by PARTFUN1:44;
               then ufs | r-Seg x0 in PFuncs(c, V) by PARTFUN1:119;
           hence contradiction by A45,A47,FUNCT_2:119;
          end;
          then nf in PFuncs(c, V) by A41,PARTFUN1:def 5;
          then reconsider nf as PartFunc of c, V by PARTFUN1:120;
     A48: dom nf is lower
          proof let x, y be set; assume
          A49: x in dom nf & [y,x] in r;
           assume
          A50: not y in dom nf;
          then A51: not y in dom ufs by A38,XBOOLE_0:def 2;
               then not x in dom ufs by A28,A49;
               then x in dom nv by A38,A49,XBOOLE_0:def 2;
          then A52: x = x0 by A39,TARSKI:def 1;
                 y in the carrier of R by A49,ZFMISC_1:106;
               then reconsider y as Element of R;
                 not y in dom nv by A38,A50,XBOOLE_0:def 2;
               then y <> x0 by A39,TARSKI:def 1;
           hence contradiction by A37,A49,A51,A52;
          end;

            now let x be set; assume
          A53: x in dom nf;
           per cases by A38,A53,XBOOLE_0:def 2;
           suppose
            A54: x in dom ufs;
            then A55: not x in dom nv by A36,A39,TARSKI:def 1;
            A56: {x0} misses r-Seg x
                 proof assume {x0} meets r-Seg x;
                  then consider y being set such that
                 A57: y in {x0} & y in r-Seg x by XBOOLE_0:3;
                        y = x0 by A57,TARSKI:def 1;
                      then [x0, x] in r by A57,WELLORD1:def 1;
                  hence contradiction by A28,A36,A54;
                 end;
             thus nf.x = ufs.x by A55,FUNCT_4:12
                      .= H.[x, ufs | r-Seg x] by A23,A54
                      .= H.[x, nf | r-Seg x] by A39,A56,AMI_5:7;
            suppose
             A58: x in dom nv;
             then A59: x = x0 by A39,TARSKI:def 1;
             A60: {x0} misses r-Seg x0
                  proof
                   assume {x0} meets r-Seg x0;
                   then consider x being set such that
                  A61: x in {x0} & x in r-Seg x0 by XBOOLE_0:3;
                         x = x0 by A61,TARSKI:def 1;
                   hence contradiction by A61,WELLORD1:def 1;
                  end;
              thus nf.x = nv.x0 by A58,A59,FUNCT_4:14
                       .= H.[x0, ufs | r-Seg x0] by CQC_LANG:6
                       .= H.[x, nf | r-Seg x] by A39,A59,A60,AMI_5:7;
          end; then nf in fs by A2,A48;
          then [x0, nf.x0] in ufs by A40,TARSKI:def 4;
      hence contradiction by A36,FUNCT_1:8;
     end;
     then reconsider ufs as Function of c, V by A19,FUNCT_2:def 1,RELSET_1:11;
  take ufs;
  let x be Element of c;
  thus thesis by A23,A33;
 end;

 assume
A62: PDR[ ];

   reconsider ac = alef 0 +` Card c as infinite Cardinal;
   set V = nextcard ac;
   deffunc F(Element of c, Element of PFuncs(c, V)) = sup rng $2;

A63: for x being Element of c, p being Element of PFuncs(c, V)
       holds F(x,p) in V
     proof let x be Element of c, p be Element of PFuncs(c, V);
            Card dom p c= Card c & Card rng p c= Card dom p
                                                 by CARD_1:27,28;
     then A64: Card rng p c= Card c by XBOOLE_1:1;
            Card c c= ac by CARD_4:72;
     then A65: Card rng p c= ac by A64,XBOOLE_1:1;
            ac in V by CARD_1:32;
     then A66: Card rng p in V by A65,ORDINAL1:22;
            V is regular by CARD_5:42;
      hence sup rng p in V by A66,Th3;
     end;
     consider H being Function of [:c, PFuncs(c, V):], V such that
A67: for x being Element of c,
         p being Element of PFuncs(c, V)
       holds H.[x,p] = F(x,p) from Kappa2D(A63);

     consider rk being Function of c, V such that
A68: rk is_recursively_expressed_by H by A62;
A69: dom rk = c by FUNCT_2:def 1;

 let Y be set; assume
A70: Y c= c & Y <> {}; then consider b being set such that
A71: b in Y by XBOOLE_0:def 1;
   set m = inf (rk.:Y);
       rk.b in V by A70,A71,FUNCT_2:7;
     then rk.b in rk.:Y & rk.b is Ordinal
                            by A69,A70,A71,FUNCT_1:def 12,ORDINAL1:23;
     then m in rk.:Y by ORDINAL2:25;
     then consider a being set such that
A72: a in dom rk & a in Y & rk.a = m by FUNCT_1:def 12;
 take a;
 thus a in Y by A72;
 assume r-Seg(a) /\ Y <> {};
     then consider e being set such that
A73: e in r-Seg(a) /\ Y by XBOOLE_0:def 1;
A74: e in r-Seg a & e in Y by A73,XBOOLE_0:def 3;
     then rk.e in V by A70,FUNCT_2:7;
     then reconsider rke = rk.e as Ordinal by ORDINAL1:23;
       rke in rk.:Y by A69,A70,A74,FUNCT_1:def 12;
then A75: m c= rk.e by ORDINAL2:22;
     reconsider a as Element of c by A72;
     reconsider rkra = rk | r-Seg a as Element of PFuncs(c,V)
                                                     by PARTFUN1:119;
A76: rk.a = H.[a, rkra] by A68,Def5
         .= sup rng rkra by A67;
       rke in rng rkra by A69,A70,A74,FUNCT_1:73;
     then rk.e in m by A72,A76,ORDINAL2:27;
 hence contradiction by A75,ORDINAL1:7;
end;

theorem :: Uniqueness implies well-foundedness
  for R being non empty RelStr,
    V being non trivial set
 st for H being Function of
                [:the carrier of R, PFuncs(the carrier of R, V):], V,
        F1, F2 being Function of the carrier of R, V
     st F1 is_recursively_expressed_by H &
        F2 is_recursively_expressed_by H
      holds F1 = F2
  holds R is well_founded
proof let R be non empty RelStr, V be non trivial set;
   set c = the carrier of R,
       r = the InternalRel of R,
       PF = PFuncs(c, V),
       wfp = well_founded-Part R;
     consider a0, a1 being set such that
A1: a0 in V & a1 in V & a0 <> a1 by SPPOL_1:3;
  set a01 = {a0, a1};
A2: a01 c= V by A1,ZFMISC_1:38;
  set F3 = c --> a1,
      F4 = wfp --> a0,
      F2 = F3 +* F4;
A3: dom F3 = c by FUNCOP_1:19;
A4: dom F4 = wfp by FUNCOP_1:19;
A5: dom F2 = dom F3 \/ dom F4 by FUNCT_4:def 1
           .= c by A3,A4,XBOOLE_1:12;
   reconsider F1 = c --> a0 as Function of c, V by A1,FUNCOP_1:57;
       rng F3 c= {a1} & rng F4 c= {a0} by FUNCOP_1:19;
     then rng F3 \/ rng F4 c= {a0} \/ {a1} by XBOOLE_1:13;
     then rng F3 \/ rng F4 c= a01 & rng F2 c= rng F3 \/ rng F4
                                       by ENUMSET1:41,FUNCT_4:18;
     then rng F2 c= a01 by XBOOLE_1:1;
     then rng F2 c= V by A2,XBOOLE_1:1;
   then reconsider F2 as Function of c, V by A5,FUNCT_2:def 1,RELSET_1:11;

   defpred P[set,Function,set] means
           (ex x being set st x in dom $2 & $2.x = a1) iff $3 = a1;

A6: now let x be Element of c, y be Element of PF;
        reconsider u = a1, v = a0 as Element of a01 by TARSKI:def 2;
        per cases;
        suppose
        A7: ex x being set st x in dom y & y.x = a1;
         take u; thus P[x,y,u] by A7;
        suppose
        A8: not ex x being set st x in dom y & y.x = a1;
         take v; thus P[x,y,v] by A1,A8;
       end;
     consider H being Function of [:c, PF:], a01 such that
A9: for x being Element of c,
         y being Element of PF holds P[x,y,H.[x,y]] from FuncEx2D(A6);
A10: rng H c= a01;
A11: dom H = [:c, PF:] & rng H c= V by A2,FUNCT_2:def 1,XBOOLE_1:1;
     then reconsider H as Function of [:c, PF:], V
       by FUNCT_2:def 1,RELSET_1:11;

A12: F1 is_recursively_expressed_by H
     proof let x be Element of c;
        reconsider F1r = F1 | r-Seg x as Element of PF by PARTFUN1:119;
            now let z be set; assume
          A13: z in dom F1r;
               then z in r-Seg x & z in dom F1 by RELAT_1:86;
               then F1r.z = F1.z by FUNCT_1:72 .= a0 by A13,FUNCOP_1:13;
           hence F1r.z <> a1 by A1;
          end;
     then A14: H.[x, F1r] <> a1 by A9;
            [x, F1r] in dom H by A11,ZFMISC_1:106;
          then A15: H.[x, F1r] in rng H by FUNCT_1:def 5;
      thus F1.x = a0 by FUNCOP_1:13
               .= H.[x, F1 | r-Seg x] by A10,A14,A15,TARSKI:def 2;
     end;
A16: F2 is_recursively_expressed_by H
     proof let x be Element of c;
        reconsider F2r = F2 | r-Seg x as Element of PF by PARTFUN1:119;
      per cases;
      suppose
      A17: x in wfp;
             now let z be set; assume z in dom F2r;
           then A18: z in r-Seg x & z in dom F2 by RELAT_1:86;
           A19: r-Seg x c= wfp by A17,Th5;
                  F2r.z = F2.z by A18,FUNCT_1:72
                     .= F4.z by A4,A18,A19,FUNCT_4:14
                     .= a0 by A18,A19,FUNCOP_1:13;
            hence F2r.z <> a1 by A1;
           end;
      then A20: H.[x, F2r]<>a1 by A9; [x, F2r] in dom H
                                              by A11,ZFMISC_1:106;
           then A21: H.[x, F2r] in rng H by FUNCT_1:def 5; F4.x = a0 by A17,
FUNCOP_1:13;
       hence F2.x = a0 by A4,A17,FUNCT_4:14
                 .= H.[x, F2 | r-Seg x] by A10,A20,A21,TARSKI:def 2;
      suppose
      A22: not x in wfp;
           then not r-Seg x c= wfp by Th10;
           then consider z being set such that
      A23: z in r-Seg x & not z in wfp by TARSKI:def 3;
      A24: r-Seg x c= c by Th4;
      then A25: z in dom F2r by A5,A23,RELAT_1:86;
      A26: F2r.z = F2.z by A23,FUNCT_1:72
                .= F3.z by A4,A23,FUNCT_4:12
                .= a1 by A23,A24,FUNCOP_1:13;
       thus F2.x = F3.x by A4,A22,FUNCT_4:12
                .= a1 by FUNCOP_1:13
                .= H.[x, F2 | r-Seg x] by A9,A25,A26;
     end;
 assume
A27: for H being Function of [:c, PF:], V,
         F1, F2 being Function of c, V
      st F1 is_recursively_expressed_by H &
         F2 is_recursively_expressed_by H
       holds F1 = F2;
 assume not R is well_founded; then wfp <> c by Th9;
     then consider x being set such that
A28: not (x in wfp iff x in c) by TARSKI:2;
A29: F1.x = a0 by A28,FUNCOP_1:13;
       F2.x = F3.x by A4,A28,FUNCT_4:12
         .= a1 by A28,FUNCOP_1:13;
 hence contradiction by A1,A12,A16,A27,A29;
end;

theorem :: Well-foundedness implies uniqueness
   for R being non empty well_founded RelStr,
     V being non empty set,
     H being Function of
             [:the carrier of R, PFuncs(the carrier of R, V):], V,
     F1, F2 being Function of the carrier of R, V
   st F1 is_recursively_expressed_by H &
      F2 is_recursively_expressed_by H
    holds F1 = F2
proof let R be non empty well_founded RelStr, V be non empty set;
  set c = the carrier of R,
      r = the InternalRel of R;
 let H be Function of [:c, PFuncs(c, V):], V, F1, F2 be Function of c, V;
 assume that
A1: F1 is_recursively_expressed_by H and
A2: F2 is_recursively_expressed_by H;
A3: dom F1 = c & dom F2 = c by FUNCT_2:def 1;
 assume F1 <> F2;
     then consider x being Element of c such that
A4: F1.x <> F2.x by FUNCT_2:113;
     reconsider x as Element of R;
     defpred P[set] means F1.$1 <> F2.$1;
A5: P[x] by A4;
A6: R is well_founded;
     consider x0 being Element of R such that
A7: P[x0] and
A8: not ex y being Element of R
        st x0 <> y & P[y] & [y,x0] in r from WFMin(A5, A6);
       F1 | r-Seg x0 = F2 | r-Seg x0
     proof set fr = F1 | r-Seg x0,
               gr = F2 | r-Seg x0;
            r-Seg x0 c= c by Th4;
     then A9: dom fr = r-Seg x0 & dom gr = r-Seg x0 by A3,RELAT_1:91;
      assume not thesis;
          then consider x1 being set such that
     A10: x1 in dom fr & fr.x1 <> gr.x1 by A9,FUNCT_1:9;
     A11: [x1, x0] in r by A9,A10,WELLORD1:def 1;
          reconsider x1 as Element of R by A10;
     A12: fr.x1 = F1.x1 & gr.x1 = F2.x1 by A9,A10,FUNCT_1:72;
            x1 <> x0 by A9,A10,WELLORD1:def 1;
      hence contradiction by A8,A10,A11,A12;
     end;
     then F1.x0 = H.[x0, F2 | r-Seg x0] by A1,Def5
          .= F2.x0 by A2,Def5;
 hence contradiction by A7;
end;

:: Well-foundedness and omega chains  :::::::::::::::::::::::::::::::::

definition
  let R be RelStr, f be sequence of R;
 canceled;
 attr f is descending means :Def7:
 for n being Nat
  holds f.(n+1) <> f.n & [f.(n+1), f.n] in the InternalRel of R;
end;

theorem :: omega chains
   for R being non empty RelStr holds
  R is well_founded iff not ex f being sequence of R st f is descending
proof let R be non empty RelStr;
  set c = the carrier of R,
      r = the InternalRel of R;
 hereby assume R is well_founded;
 then A1: r is_well_founded_in c by Def2;
      given f being sequence of R such that
 A2: f is descending;
 A3: dom f = NAT & rng f c= c by FUNCT_2:def 1;
      then rng f <> {} by RELAT_1:65;
      then consider a being set such that
 A4: a in rng f & r-Seg(a) misses rng f by A1,WELLORD1:def 3;
      consider n being set such that
 A5: n in dom f & a = f.n by A4,FUNCT_1:def 5;
      reconsider n as Nat by A5;
        f.(n+1)<>f.n & [f.(n+1),f.n] in the InternalRel of R by A2,Def7;
 then A6: f.(n+1) in r-Seg(f.n) by WELLORD1:def 1;
      f.(n+1) in rng f by A3,FUNCT_1:def 5;
  hence contradiction by A4,A5,A6,XBOOLE_0:3;
 end;
 assume
A7: not ex f being sequence of R st f is descending;
 assume not R is well_founded;
     then not r is_well_founded_in c by Def2;
     then consider Y being set such that
A8: Y c= c & Y <> {} and
A9: for a being set holds
       not a in Y or r-Seg(a) meets Y by WELLORD1:def 3;
     deffunc G(set,set) = choose (r-Seg($2) /\ Y);
     consider f being Function such that
A10: dom f = NAT and
A11: f.0 = choose Y and
A12: for n being Element of NAT holds f.(n+1) = G(n,f.n) from LambdaRecEx;
     defpred P[Nat] means f.$1 in Y;
A13: P[0] by A8,A11;
A14: now let n be Nat; assume P[n];
        then r-Seg(f.n) meets Y by A9;
then A15:        r-Seg(f.n) /\ Y <> {} by XBOOLE_0:def 7;
              f.(n+1) = choose (r-Seg(f.n) /\ Y) by A12;
        hence P[n+1] by A15,XBOOLE_0:def 3;
       end;
A16: for n being Nat holds P[n] from Ind(A13, A14);
       rng f c= c proof let y be set; assume y in rng f;
          then consider x being set such that
     A17: x in dom f & y = f.x by FUNCT_1:def 5;
          reconsider n = x as Nat by A10,A17;
            f.n in Y by A16;
      hence y in c by A8,A17;
     end;
     then f is Function of NAT, c by A10,FUNCT_2:4;
     then reconsider f as sequence of R by NORMSP_1:def 3;
       now let n be Nat; f.n in Y by A16;
      then r-Seg(f.n) meets Y by A9;
then A18:        r-Seg(f.n) /\ Y <> {} by XBOOLE_0:def 7;
            f.(n+1) = choose (r-Seg(f.n) /\ Y) by A12;
          then f.(n+1) in r-Seg(f.n) by A18,XBOOLE_0:def 3;
      hence f.(n+1) <> f.n & [f.(n+1), f.n] in r by WELLORD1:def 1;
     end;
     then f is descending by Def7;
 hence contradiction by A7;
end;


Back to top