wellfnd1.miz



    begin

    theorem :: WELLFND1:1

    

     Th1: for X be functional set st for f,g be 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 be Function st f in X & g in X holds f tolerates g;

      

       A2: ( union X) is Function-like

      proof

        let x,y1,y2 be object;

        assume that

         A3: [x, y1] in ( union X) and

         A4: [x, y2] in ( union X) and

         A5: y1 <> y2;

        consider gx be set such that

         A6: [x, y2] in gx and

         A7: gx in X by A4, TARSKI:def 4;

        consider fx be set such that

         A8: [x, y1] in fx and

         A9: fx in X by A3, TARSKI:def 4;

        reconsider fx, gx as Function by A9, A7;

        fx tolerates gx by A1, A9, A7;

        then ex h be Function st fx c= h & gx c= h by PARTFUN1: 52;

        hence contradiction by A5, A8, A6, FUNCT_1:def 1;

      end;

      ( union X) is Relation-like

      proof

        let x be object;

        assume x in ( union X);

        then ex ux be set st x in ux & ux in X by TARSKI:def 4;

        hence thesis by RELAT_1:def 1;

      end;

      hence thesis by A2;

    end;

    scheme :: WELLFND1:sch1

    PFSeparation { X,Y() -> set , P[ set] } :

ex PFS be Subset of ( PFuncs (X(),Y())) st for pfs be PartFunc of X(), Y() holds pfs in PFS iff P[pfs];

      consider fs be Subset of ( PFuncs (X(),Y())) such that

       A1: for f be set holds f in fs iff f in ( PFuncs (X(),Y())) & P[f] from SUBSET_1:sch 1;

      take fs;

      let pfs be PartFunc of X(), Y();

      pfs in ( PFuncs (X(),Y())) by PARTFUN1: 45;

      hence thesis by A1;

    end;

    registration

      let X be set;

      cluster ( nextcard X) -> non empty;

      coherence by CARD_1:def 3;

    end

    registration

      cluster regular for Aleph;

      existence by CARD_5: 30;

    end

    theorem :: WELLFND1:2

    

     Th2: for M be regular Aleph, X be 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 3;

      hence thesis by CARD_5: 26;

    end;

    theorem :: WELLFND1:3

    

     Th3: for R be RelStr, x be 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: 8, WELLORD1: 9;

      hence thesis;

    end;

    definition

      let R be RelStr, X be Subset of R;

      :: original: lower

      redefine

      :: WELLFND1:def1

      attr X is lower means

      : Def1: for x,y be object 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 object such that

           A2: x in X and

           A3: [y, x] in the InternalRel of R;

          reconsider x9 = x, y9 = y as Element of R by A3, ZFMISC_1: 87;

          y9 <= x9 by A3, ORDERS_2:def 5;

          hence y in X by A1, A2;

        end;

        assume

         A4: for x,y be object 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_2:def 5;

        hence thesis by A4, A5;

      end;

    end

    theorem :: WELLFND1:4

    

     Th4: for R be RelStr, X be Subset of R, x be 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 object;

      assume z in (the InternalRel of R -Seg x);

      then [z, x] in the InternalRel of R by WELLORD1: 1;

      hence thesis by A1;

    end;

    theorem :: WELLFND1:5

    

     Th5: for R be RelStr, X be lower Subset of R, Y be Subset of R, x be 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 that

       A1: Y = (X \/ {x}) and

       A2: (r -Seg x) c= X;

      let z,y be object;

      assume that

       A3: z in Y and

       A4: [y, z] in r;

      per cases by A1, A3, XBOOLE_0:def 3;

        suppose z in X;

        then y in X by A4, Def1;

        hence thesis by A1, XBOOLE_0:def 3;

      end;

        suppose z in {x} & y = z;

        hence thesis by A3;

      end;

        suppose

         A5: z in {x} & y <> z;

        then z = x by TARSKI:def 1;

        then y in (r -Seg x) by A4, A5, WELLORD1: 1;

        hence thesis by A1, A2, XBOOLE_0:def 3;

      end;

    end;

    begin

    definition

      let R be RelStr;

      :: WELLFND1:def2

      attr R is well_founded means the InternalRel of R is_well_founded_in the carrier of R;

    end

    registration

      cluster non empty well_founded for RelStr;

      existence

      proof

        reconsider er = {} as Relation of { {} } by RELSET_1: 12;

        take R = RelStr (# { {} }, er #);

        thus R is non empty;

        let Y be set;

        assume

         A1: Y c= the carrier of R & Y <> {} ;

        take e = {} ;

        Y = { {} } by A1, ZFMISC_1: 33;

        hence e in Y by TARSKI:def 1;

        assume ((the InternalRel of R -Seg e) /\ Y) <> {} ;

        then

        consider x be object 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) by A2, XBOOLE_0:def 4;

        hence contradiction by WELLORD1: 1;

      end;

    end

    definition

      let R be RelStr, X be Subset of R;

      :: WELLFND1:def3

      attr X is well_founded means

      : Def3: the InternalRel of R is_well_founded_in X;

    end

    registration

      let R be RelStr;

      cluster well_founded for Subset of R;

      existence

      proof

        reconsider e = {} as Subset of R by XBOOLE_1: 2;

        take e;

        let Y be set;

        assume Y c= e & Y <> {} ;

        hence thesis;

      end;

    end

    definition

      let R be RelStr;

      :: WELLFND1:def4

      func well_founded-Part R -> Subset of R means

      : Def4: it = ( union { S where S be Subset of R : S is well_founded lower });

      existence

      proof

        set IT = { S where S be Subset of R : S is well_founded lower };

        IT c= ( bool the carrier of R)

        proof

          let x be object;

          assume x in IT;

          then ex S be Subset of R st x = S & S is well_founded lower;

          hence thesis;

        end;

        then

        reconsider IT as Subset-Family of R;

        ( union IT) is Subset of R;

        hence thesis;

      end;

      uniqueness ;

    end

    registration

      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 be Subset of R : S is well_founded lower };

        

         A1: wfp = ( union IT) by Def4;

        hereby

          let x,y be object;

          assume that

           A2: x in wfp and

           A3: [y, x] in r;

          consider Y be set such that

           A4: x in Y and

           A5: Y in IT by A1, A2, TARSKI:def 4;

          consider S be Subset of R such that

           A6: Y = S and

           A7: S is well_founded lower by A5;

          y in S by A3, A4, A6, A7;

          hence y in wfp by A1, A5, A6, TARSKI:def 4;

        end;

        let Y be set;

        assume that

         A8: Y c= wfp and

         A9: Y <> {} ;

        consider y be object such that

         A10: y in Y by A9, XBOOLE_0:def 1;

        consider YY be set such that

         A11: y in YY and

         A12: YY in IT by A1, A8, A10, TARSKI:def 4;

        consider S be Subset of R such that

         A13: YY = S and

         A14: S is well_founded lower by A12;

        set YS = (Y /\ S);

        

         A15: r is_well_founded_in S by A14;

        YS c= S & YS <> {} by A10, A11, A13, XBOOLE_0:def 4;

        then

        consider a be object such that

         A16: a in YS and

         A17: (r -Seg a) misses YS by A15;

        

         A18: a in Y by A16, XBOOLE_0:def 4;

        a in S by A16, XBOOLE_0:def 4;

        

        then

         A19: ((r -Seg a) /\ Y) = (((r -Seg a) /\ S) /\ Y) by A14, Th4, XBOOLE_1: 28

        .= ((r -Seg a) /\ YS) by XBOOLE_1: 16;

        ((r -Seg a) /\ YS) = {} by A17;

        then (r -Seg a) misses Y by A19;

        hence thesis by A18;

      end;

    end

    theorem :: WELLFND1:6

    

     Th6: for R be 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 that

         A1: Y c= sx and

         A2: Y <> {} ;

        take x;

        Y = sx by A1, A2, ZFMISC_1: 33;

        hence x in Y by TARSKI:def 1;

        assume not thesis;

        then

        consider a be object such that

         A3: a in ((r -Seg x) /\ Y) by XBOOLE_0: 4;

        a in (r -Seg x) by A3, XBOOLE_0:def 4;

        then

         A4: a <> x by WELLORD1: 1;

        a in Y by A3, XBOOLE_0:def 4;

        hence contradiction by A1, A4, TARSKI:def 1;

      end;

      hence thesis;

    end;

    theorem :: WELLFND1:7

    

     Th7: for R be RelStr, X,Y be 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;

      reconsider XY = (X \/ Y) as Subset of R;

      

       A2: r is_well_founded_in Y by Def3;

      

       A3: r is_well_founded_in X by Def3;

      XY is well_founded

      proof

        let Z be set such that

         A4: Z c= XY and

         A5: Z <> {} ;

        set XZ = (X /\ Z);

        

         A6: XZ c= X by XBOOLE_1: 17;

        per cases ;

          suppose XZ = {} ;

          then X misses Z;

          then Z c= Y by A4, XBOOLE_1: 73;

          hence thesis by A2, A5;

        end;

          suppose XZ <> {} ;

          then

          consider a be object such that

           A7: a in XZ and

           A8: (r -Seg a) misses XZ by A3, A6;

          

           A9: a in X by A7, XBOOLE_0:def 4;

          take a;

          thus a in Z by A7, XBOOLE_0:def 4;

          assume ((r -Seg a) /\ Z) <> {} ;

          then

          consider b be object such that

           A10: b in ((r -Seg a) /\ Z) by XBOOLE_0:def 1;

          

           A11: b in Z by A10, XBOOLE_0:def 4;

          

           A12: b in (r -Seg a) by A10, XBOOLE_0:def 4;

          then [b, a] in r by WELLORD1: 1;

          then b in X by A1, A9;

          then b in XZ by A11, XBOOLE_0:def 4;

          hence contradiction by A8, A12, XBOOLE_0: 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: WELLFND1:8

    

     Th8: for R be 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);

      set IT = { S where S be Subset of R : S is well_founded lower };

      c c= c;

      then

      reconsider cs = c as Subset of R;

      

       A1: wfp = ( union IT) by Def4;

      hereby

        

         A2: cs is lower;

        assume R is well_founded;

        then r is_well_founded_in cs;

        then cs is well_founded;

        then cs in IT by A2;

        then cs c= wfp by A1, ZFMISC_1: 74;

        hence wfp = c;

      end;

      assume

       A3: wfp = c;

      let Y be set;

      assume that

       A4: Y c= c and

       A5: Y <> {} ;

      consider y be object such that

       A6: y in Y by A5, XBOOLE_0:def 1;

      consider YY be set such that

       A7: y in YY and

       A8: YY in IT by A1, A3, A4, A6, TARSKI:def 4;

      consider S be Subset of R such that

       A9: YY = S and

       A10: S is well_founded lower by A8;

      set YS = (Y /\ S);

      

       A11: r is_well_founded_in S by A10;

      YS c= S & YS <> {} by A6, A7, A9, XBOOLE_0:def 4;

      then

      consider a be object such that

       A12: a in YS and

       A13: (r -Seg a) misses YS by A11;

      

       A14: a in Y by A12, XBOOLE_0:def 4;

      a in S by A12, XBOOLE_0:def 4;

      

      then

       A15: ((r -Seg a) /\ Y) = (((r -Seg a) /\ S) /\ Y) by A10, Th4, XBOOLE_1: 28

      .= ((r -Seg a) /\ YS) by XBOOLE_1: 16;

      ((r -Seg a) /\ YS) = {} by A13;

      then (r -Seg a) misses Y by A15;

      hence thesis by A14;

    end;

    theorem :: WELLFND1:9

    

     Th9: for R be non empty RelStr, x be 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 be 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 3;

      reconsider xwfp as Subset of R;

       {x} is well_founded Subset of R by Th6;

      then

       A3: xwfp is well_founded by Th7;

      assume (the InternalRel of R -Seg x) c= wfp;

      then xwfp is lower by Th5;

      then xwfp in IT by A3;

      hence thesis by A1, A2, TARSKI:def 4;

    end;

    scheme :: WELLFND1:sch2

    WFMin { R() -> non empty RelStr , x() -> Element of R() , P[ set] } :

ex x be Element of R() st P[x] & not ex y be 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;

      set c = the carrier of R(), r = the InternalRel of R(), Z = { x where x be Element of c : P[x] };

      

       A3: x() in Z by A1;

      Z is Subset of c from DOMAIN_1:sch 7;

      then

      reconsider Z as non empty Subset of c by A3;

      r is_well_founded_in c by A2;

      then

      consider a be object such that

       A4: a in Z and

       A5: (r -Seg a) misses Z;

      reconsider a as Element of R() by A4;

      take a;

      ex a9 be Element of c st a9 = a & P[a9] by A4;

      hence P[a];

      given y be Element of R() such that

       A6: a <> y & P[y] & [y, a] in r;

      y in Z & y in (r -Seg a) by A6, WELLORD1: 1;

      hence contradiction by A5, XBOOLE_0: 3;

    end;

    theorem :: WELLFND1:10

    

     Th10: for R be non empty RelStr holds R is well_founded iff for S be set st for x be 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 be Element of c st (r -Seg x) c= S holds x in S;

        defpred P[ set] means $1 in c & not $1 in S;

        assume not c c= S;

        then

        consider x be object such that

         A3: x in c and

         A4: not x in S;

        reconsider x as Element of R by A3;

        

         A5: P[x] by A4;

        consider x0 be Element of R such that

         A6: P[x0] and

         A7: not ex y be Element of R st x0 <> y & P[y] & [y, x0] in r from WFMin( A5, A1);

        now

          assume not (r -Seg x0) c= S;

          then

          consider z be object such that

           A8: z in (r -Seg x0) and

           A9: not z in S;

          

           A10: x0 <> z by A8, WELLORD1: 1;

          

           A11: [z, x0] in r by A8, WELLORD1: 1;

          then

          reconsider z as Element of R by ZFMISC_1: 87;

          z = z;

          hence contradiction by A7, A9, A10, A11;

        end;

        hence contradiction by A2, A6;

      end;

      assume

       A12: for S be set st for x be 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;

      then

      consider Y be set such that

       A13: Y c= c & Y <> {} and

       A14: not ex a be object st a in Y & (r -Seg a) misses Y;

      now

        let x be Element of c such that

         A15: (r -Seg x) c= (c \ Y);

        assume not x in (c \ Y);

        then x in Y by XBOOLE_0:def 5;

        then (r -Seg x) meets Y by A14;

        then ex z be object st z in (r -Seg x) & z in Y by XBOOLE_0: 3;

        hence contradiction by A15, XBOOLE_0:def 5;

      end;

      then c c= (c \ Y) by A12;

      hence contradiction by A13, XBOOLE_1: 1, XBOOLE_1: 38;

    end;

    scheme :: WELLFND1:sch3

    WFInduction { R() -> non empty RelStr , P[ set] } :

for x be Element of R() holds P[x]

      provided

       A1: for x be Element of R() st for y be 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;

      set c = the carrier of R(), r = the InternalRel of R(), Z = { x where x be Element of c : P[x] };

      now

        let x be Element of c such that

         A3: (r -Seg x) c= Z;

        reconsider x9 = x as Element of R();

        now

          let y9 be Element of R();

          assume y9 <> x9 & [y9, x9] in r;

          then y9 in (r -Seg x9) by WELLORD1: 1;

          then y9 in Z by A3;

          then ex y be Element of c st y = y9 & P[y];

          hence P[y9];

        end;

        then P[x9] by A1;

        hence x in Z;

      end;

      then

       A4: c c= Z by A2, Th10;

      let x be Element of R();

      x in Z by A4;

      then ex x9 be Element of c st x = x9 & P[x9];

      hence thesis;

    end;

    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;

      :: WELLFND1:def5

      pred F is_recursively_expressed_by H means for x be Element of R holds (F . x) = (H . (x,(F | (the InternalRel of R -Seg x))));

    end

    theorem :: WELLFND1:11

    for R be non empty RelStr holds R is well_founded iff for V be non empty set, H be Function of [:the carrier of R, ( PFuncs (the carrier of R,V)):], V holds ex F be 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 be non empty set, H be Function of [:c, ( PFuncs (c,V)):], V holds ex F be Function of c, V st F is_recursively_expressed_by H;

      reconsider ac = ( omega +` ( card c)) as infinite Cardinal;

      set V = ( nextcard ac);

      deffunc F( Element of c, Element of ( PFuncs (c,V))) = ( sup ( rng $2));

      

       A1: for x be Element of c, p be 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: 11, CARD_1: 12;

        then

         A2: ( card ( rng p)) c= ( card c);

        ( card c) c= ac by CARD_2: 94;

        then ( card ( rng p)) c= ac by A2;

        then

         A3: ( card ( rng p)) in V by CARD_1: 18, ORDINAL1: 12;

        V is regular by CARD_5: 30;

        hence thesis by A3, Th2;

      end;

      consider H be Function of [:c, ( PFuncs (c,V)):], V such that

       A4: for x be Element of c, p be Element of ( PFuncs (c,V)) holds (H . (x,p)) = F(x,p) from FUNCT_7:sch 1( A1);

      thus R is well_founded implies PDR[]

      proof

        assume

         A5: 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 be set st x in ( dom $1) holds ($1 . x) = (H . [x, ($1 | (r -Seg x))]);

        consider fs be Subset of ( PFuncs (c,V)) such that

         A6: for f be PartFunc of c, V holds f in fs iff P[f] from PFSeparation;

        now

          let f,g be Function;

          assume that

           A7: f in fs and

           A8: g in fs;

          reconsider ff = f, gg = g as PartFunc of c, V by A7, A8, PARTFUN1: 46;

          defpred P[ set] means $1 in ( dom ff) & $1 in ( dom gg) & (ff . $1) <> (gg . $1);

          assume not f tolerates g;

          then

          consider x be object such that

           A9: x in (( dom ff) /\ ( dom gg)) and

           A10: (ff . x) <> (gg . x) by PARTFUN1:def 4;

          reconsider x as Element of R by A9;

          

           A11: P[x] by A9, A10, XBOOLE_0:def 4;

          consider x0 be Element of R such that

           A12: P[x0] and

           A13: not ex y be Element of R st x0 <> y & P[y] & [y, x0] in the InternalRel of R from WFMin( A11, A5);

          (ff | (r -Seg x0)) = (gg | (r -Seg x0))

          proof

            set fr = (ff | (r -Seg x0)), gr = (gg | (r -Seg x0));

            assume

             A14: not thesis;

            

             A15: ( dom ff) is lower by A6, A7;

            then

             A16: ( dom fr) = (r -Seg x0) by A12, Th4, RELAT_1: 62;

            

             A17: ( dom gg) is lower by A6, A8;

            then ( dom fr) = ( dom gr) by A12, A16, Th4, RELAT_1: 62;

            then

            consider x1 be object such that

             A18: x1 in ( dom fr) and

             A19: (fr . x1) <> (gr . x1) by A14;

            

             A20: [x1, x0] in r by A16, A18, WELLORD1: 1;

            reconsider x1 as Element of R by A18;

            

             A21: (fr . x1) = (ff . x1) & (gr . x1) = (gg . x1) by A16, A18, FUNCT_1: 49;

            

             A22: x1 <> x0 by A16, A18, WELLORD1: 1;

            

             A23: x1 in ( dom gg) by A12, A17, A20;

            x1 in ( dom ff) by A12, A15, A20;

            hence contradiction by A13, A19, A20, A21, A22, A23;

          end;

          

          then (ff . x0) = (H . [x0, (gg | (r -Seg x0))]) by A6, A7, A12

          .= (gg . x0) by A6, A8, A12;

          hence contradiction by A12;

        end;

        then

        reconsider ufs = ( union fs) as Function by Th1;

         A24:

        now

          let x be set;

          assume x in ( dom ufs);

          then [x, (ufs . x)] in ufs by FUNCT_1: 1;

          then

          consider fx be set such that

           A25: [x, (ufs . x)] in fx and

           A26: fx in fs by TARSKI:def 4;

          reconsider ff = fx as PartFunc of c, V by A26, PARTFUN1: 46;

          

           A27: x in ( dom ff) by A25, FUNCT_1: 1;

          

           A28: ( dom ff) is lower & ff c= ufs by A6, A26, ZFMISC_1: 74;

          

          thus (ufs . x) = (ff . x) by A25, FUNCT_1: 1

          .= (H . [x, (ff | (r -Seg x))]) by A6, A26, A27

          .= (H . [x, (ufs | (r -Seg x))]) by A27, A28, Th4, GRFUNC_1: 27;

        end;

        

         A29: ( dom ufs) c= c

        proof

          let y be object;

          assume y in ( dom ufs);

          then [y, (ufs . y)] in ufs by FUNCT_1: 1;

          then

          consider fx be set such that

           A30: [y, (ufs . y)] in fx and

           A31: fx in fs by TARSKI:def 4;

          consider ff be Function such that

           A32: ff = fx and

           A33: ( dom ff) c= c and ( rng ff) c= V by A31, PARTFUN1:def 3;

          y in ( dom ff) by A30, A32, XTUPLE_0:def 12;

          hence thesis by A33;

        end;

        

         A34: ( rng ufs) c= V

        proof

          let y be object;

          assume y in ( rng ufs);

          then

          consider x be object such that

           A35: x in ( dom ufs) & y = (ufs . x) by FUNCT_1:def 3;

           [x, y] in ufs by A35, FUNCT_1: 1;

          then

          consider fx be set such that

           A36: [x, y] in fx and

           A37: fx in fs by TARSKI:def 4;

          consider ff be Function such that

           A38: ff = fx and ( dom ff) c= c and

           A39: ( rng ff) c= V by A37, PARTFUN1:def 3;

          y in ( rng ff) by A36, A38, XTUPLE_0:def 13;

          hence thesis by A39;

        end;

         A40:

        now

          let x,y be object;

          assume that

           A41: x in ( dom ufs) and

           A42: [y, x] in r;

           [x, (ufs . x)] in ufs by A41, FUNCT_1: 1;

          then

          consider fx be set such that

           A43: [x, (ufs . x)] in fx and

           A44: fx in fs by TARSKI:def 4;

          reconsider ff = fx as PartFunc of c, V by A44, PARTFUN1: 46;

          ff c= ufs by A44, ZFMISC_1: 74;

          then

           A45: ( dom ff) c= ( dom ufs) by GRFUNC_1: 2;

          ( dom ff) is lower & x in ( dom ff) by A6, A43, A44, FUNCT_1: 1;

          then y in ( dom ff) by A42;

          hence y in ( dom ufs) by A45;

        end;

        

         A46: ( dom ufs) = c

        proof

          defpred P[ set] means $1 in c & not $1 in ( dom ufs);

          assume ( dom ufs) <> c;

          then

          consider x be object such that

           A47: not (x in ( dom ufs) iff x in c) by TARSKI: 2;

          reconsider x as Element of R by A29, A47;

          

           A48: P[x] by A47;

          consider x0 be Element of R such that

           A49: P[x0] and

           A50: not ex y be Element of R st x0 <> y & P[y] & [y, x0] in the InternalRel of R from WFMin( A48, A5);

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

          

           A51: ( dom nv) = {x0};

          

           A52: ( rng nf) c= V

          proof

            ufs in ( PFuncs (c,V)) by A29, A34, PARTFUN1:def 3;

            then ufs is PartFunc of c, V by PARTFUN1: 46;

            then (ufs | (r -Seg x0)) is PartFunc of c, V by PARTFUN1: 11;

            then

             A53: (ufs | (r -Seg x0)) in ( PFuncs (c,V)) by PARTFUN1: 45;

            let x be object;

            assume

             A54: x in ( rng nf);

            assume

             A55: not x in V;

            then ( rng nf) c= (( rng ufs) \/ ( rng nv)) & not x in ( rng ufs) by A34, FUNCT_4: 17;

            then

             A56: x in ( rng nv) by A54, XBOOLE_0:def 3;

            ( rng nv) = {(H . [x0, (ufs | (r -Seg x0))])} by FUNCOP_1: 8;

            then x = (H . (x0,(ufs | (r -Seg x0)))) by A56, TARSKI:def 1;

            hence contradiction by A55, A53, BINOP_1: 17;

          end;

          

           A57: ( dom nf) = (( dom ufs) \/ ( dom nv)) by FUNCT_4:def 1;

          ( dom nf) c= c

          proof

            let x be object;

            assume that

             A58: x in ( dom nf) and

             A59: not x in c;

             not x in ( dom ufs) by A29, A59;

            then x in ( dom nv) by A57, A58, XBOOLE_0:def 3;

            hence contradiction by A51, A59;

          end;

          then

           A60: nf in ( PFuncs (c,V)) by A52, PARTFUN1:def 3;

          x0 in ( dom nv) by TARSKI:def 1;

          then x0 in ( dom nf) by A57, XBOOLE_0:def 3;

          then

           A61: [x0, (nf . x0)] in nf by FUNCT_1: 1;

          reconsider nf as PartFunc of c, V by A60, PARTFUN1: 46;

           A62:

          now

            let x be set;

            assume

             A63: x in ( dom nf);

            per cases by A57, A63, XBOOLE_0:def 3;

              suppose

               A64: x in ( dom ufs);

              

               A65: {x0} misses (r -Seg x)

              proof

                assume {x0} meets (r -Seg x);

                then

                consider y be object such that

                 A66: y in {x0} and

                 A67: y in (r -Seg x) by XBOOLE_0: 3;

                y = x0 by A66, TARSKI:def 1;

                then [x0, x] in r by A67, WELLORD1: 1;

                hence contradiction by A40, A49, A64;

              end;

               not x in ( dom nv) by A49, A64, TARSKI:def 1;

              

              hence (nf . x) = (ufs . x) by FUNCT_4: 11

              .= (H . [x, (ufs | (r -Seg x))]) by A24, A64

              .= (H . [x, (nf | (r -Seg x))]) by A51, A65, FUNCT_4: 72;

            end;

              suppose

               A68: x in ( dom nv);

              

               A69: {x0} misses (r -Seg x0)

              proof

                assume {x0} meets (r -Seg x0);

                then

                consider x be object such that

                 A70: x in {x0} and

                 A71: x in (r -Seg x0) by XBOOLE_0: 3;

                x = x0 by A70, TARSKI:def 1;

                hence contradiction by A71, WELLORD1: 1;

              end;

              

               A72: x = x0 by A68, TARSKI:def 1;

              

              hence (nf . x) = (nv . x0) by A68, FUNCT_4: 13

              .= (H . [x0, (ufs | (r -Seg x0))]) by FUNCOP_1: 72

              .= (H . [x, (nf | (r -Seg x))]) by A51, A72, A69, FUNCT_4: 72;

            end;

          end;

          ( dom nf) is lower

          proof

            let x,y be object;

            assume that

             A73: x in ( dom nf) and

             A74: [y, x] in r;

            assume

             A75: not y in ( dom nf);

            then

             A76: not y in ( dom ufs) by A57, XBOOLE_0:def 3;

            then not x in ( dom ufs) by A40, A74;

            then x in ( dom nv) by A57, A73, XBOOLE_0:def 3;

            then

             A77: x = x0 by TARSKI:def 1;

            reconsider y as Element of R by A74, ZFMISC_1: 87;

             not y in ( dom nv) by A57, A75, XBOOLE_0:def 3;

            then y <> x0 by TARSKI:def 1;

            hence contradiction by A50, A74, A76, A77;

          end;

          then nf in fs by A6, A62;

          then [x0, (nf . x0)] in ufs by A61, TARSKI:def 4;

          hence contradiction by A49, FUNCT_1: 1;

        end;

        then

        reconsider ufs as Function of c, V by A34, FUNCT_2:def 1, RELSET_1: 4;

        take ufs;

        let x be Element of c;

        thus thesis by A24, A46;

      end;

      assume PDR[];

      then

      consider rk be Function of c, V such that

       A78: rk is_recursively_expressed_by H;

      let Y be set;

      assume that

       A79: Y c= c and

       A80: Y <> {} ;

      set m = ( inf (rk .: Y));

      consider b be object such that

       A81: b in Y by A80, XBOOLE_0:def 1;

      

       A82: ( dom rk) = c by FUNCT_2:def 1;

      then (rk . b) in (rk .: Y) by A79, A81, FUNCT_1:def 6;

      then m in (rk .: Y) by ORDINAL2: 17;

      then

      consider a be object such that

       A83: a in ( dom rk) and

       A84: a in Y and

       A85: (rk . a) = m by FUNCT_1:def 6;

      reconsider a as set by TARSKI: 1;

      take a;

      thus a in Y by A84;

      assume ((r -Seg a) /\ Y) <> {} ;

      then

      consider e be object such that

       A86: e in ((r -Seg a) /\ Y) by XBOOLE_0:def 1;

      

       A87: e in (r -Seg a) by A86, XBOOLE_0:def 4;

      reconsider a as Element of c by A83;

      reconsider rkra = (rk | (r -Seg a)) as Element of ( PFuncs (c,V)) by PARTFUN1: 45;

      

       A88: (rk . a) = (H . (a,rkra)) by A78

      .= ( sup ( rng rkra)) by A4;

      

       A89: e in Y by A86, XBOOLE_0:def 4;

      then

      reconsider rke = (rk . e) as Ordinal by A79, FUNCT_2: 5, ORDINAL1: 13;

      rke in (rk .: Y) by A82, A79, A89, FUNCT_1:def 6;

      then

       A90: m c= (rk . e) by ORDINAL2: 14;

      rke in ( rng rkra) by A82, A79, A87, A89, FUNCT_1: 50;

      hence contradiction by A85, A90, A88, ORDINAL1: 5, ORDINAL2: 19;

    end;

    theorem :: WELLFND1:12

    for R be non empty RelStr, V be non trivial set st for H be Function of [:the carrier of R, ( PFuncs (the carrier of R,V)):], V, F1,F2 be 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 be object such that

       A1: a0 in V and

       A2: a1 in V and

       A3: a0 <> a1 by ZFMISC_1:def 10;

      set F3 = (c --> a1), F4 = (wfp --> a0), F2 = (F3 +* F4);

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

      reconsider a0, a1 as set by TARSKI: 1;

      set a01 = {a0, a1};

       A5:

      now

        reconsider u = a1, v = a0 as Element of a01 by TARSKI:def 2;

        let x be Element of c, y be Element of PF;

        per cases ;

          suppose

           A6: ex x be set st x in ( dom y) & (y . x) = a1;

          take u;

          thus P[x, y, u] by A6;

        end;

          suppose

           A7: not ex x be set st x in ( dom y) & (y . x) = a1;

          take v;

          thus P[x, y, v] by A3, A7;

        end;

      end;

      consider H be Function of [:c, PF:], a01 such that

       A8: for x be Element of c, y be Element of PF holds P[x, y, (H . (x,y))] from BINOP_1:sch 3( A5);

      

       A9: a01 c= V by A1, A2, ZFMISC_1: 32;

      then

       A10: ( rng H) c= V;

      (( rng F3) \/ ( rng F4)) c= ( {a0} \/ {a1}) by XBOOLE_1: 13;

      then

       A11: (( rng F3) \/ ( rng F4)) c= a01 by ENUMSET1: 1;

      ( rng F2) c= (( rng F3) \/ ( rng F4)) by FUNCT_4: 17;

      then ( rng F2) c= a01 by A11;

      then

       A12: ( rng F2) c= V by A9;

      

       A13: ( rng H) c= a01;

      

       A14: ( dom H) = [:c, PF:] by FUNCT_2:def 1;

      then

      reconsider H as Function of [:c, PF:], V by A10, FUNCT_2:def 1, RELSET_1: 4;

      

       A15: ( dom F4) = wfp;

      

       A16: ( dom F2) = (( dom F3) \/ ( dom F4)) by FUNCT_4:def 1

      .= c by XBOOLE_1: 12;

      then

      reconsider F2 as Function of c, V by A12, FUNCT_2:def 1, RELSET_1: 4;

      

       A17: 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: 45;

        per cases ;

          suppose

           A18: x in wfp;

          now

            let z be set;

            

             A19: (r -Seg x) c= wfp by A18, Th4;

            assume z in ( dom F2r);

            then

             A20: z in (r -Seg x) by RELAT_1: 57;

            

            then (F2r . z) = (F2 . z) by FUNCT_1: 49

            .= (F4 . z) by A15, A20, A19, FUNCT_4: 13

            .= a0 by A20, A19, FUNCOP_1: 7;

            hence (F2r . z) <> a1 by A3;

          end;

          then

           A21: (H . (x,F2r)) <> a1 by A8;

          

           A22: (H . [x, F2r]) in ( rng H) by A14, FUNCT_1:def 3;

          (F4 . x) = a0 by A18, FUNCOP_1: 7;

          

          hence (F2 . x) = a0 by A15, A18, FUNCT_4: 13

          .= (H . (x,(F2 | (r -Seg x)))) by A13, A21, A22, TARSKI:def 2;

        end;

          suppose

           A23: not x in wfp;

          then not (r -Seg x) c= wfp by Th9;

          then

          consider z be object such that

           A24: z in (r -Seg x) and

           A25: not z in wfp;

          

           A26: (r -Seg x) c= c by Th3;

          then

           A27: z in ( dom F2r) by A16, A24, RELAT_1: 57;

          

           A28: (F2r . z) = (F2 . z) by A24, FUNCT_1: 49

          .= (F3 . z) by A15, A25, FUNCT_4: 11

          .= a1 by A24, A26, FUNCOP_1: 7;

          

          thus (F2 . x) = (F3 . x) by A15, A23, FUNCT_4: 11

          .= a1

          .= (H . (x,(F2 | (r -Seg x)))) by A8, A27, A28;

        end;

      end;

      reconsider F1 = (c --> a0) as Function of c, V by A1, FUNCOP_1: 45;

      assume

       A29: for H be Function of [:c, PF:], V, F1,F2 be 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 Th8;

      then

      consider x be object such that

       A30: not (x in wfp iff x in c) by TARSKI: 2;

      

       A31: 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: 45;

        

         A32: (H . [x, F1r]) in ( rng H) by A14, FUNCT_1:def 3;

        now

          let z be set;

          assume

           A33: z in ( dom F1r);

          then z in (r -Seg x) by RELAT_1: 57;

          

          then (F1r . z) = (F1 . z) by FUNCT_1: 49

          .= a0 by A33, FUNCOP_1: 7;

          hence (F1r . z) <> a1 by A3;

        end;

        then

         A34: (H . (x,F1r)) <> a1 by A8;

        

        thus (F1 . x) = a0

        .= (H . (x,(F1 | (r -Seg x)))) by A13, A34, A32, TARSKI:def 2;

      end;

      

       A35: (F1 . x) = a0 by A30, FUNCOP_1: 7;

      (F2 . x) = (F3 . x) by A15, A30, FUNCT_4: 11

      .= a1 by A30, FUNCOP_1: 7;

      hence contradiction by A3, A31, A17, A29, A35;

    end;

    theorem :: WELLFND1:13

    for R be non empty well_founded RelStr, V be non empty set, H be Function of [:the carrier of R, ( PFuncs (the carrier of R,V)):], V, F1,F2 be 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;

      defpred P[ set] means (F1 . $1) <> (F2 . $1);

      

       A3: ( dom F2) = c by FUNCT_2:def 1;

      assume F1 <> F2;

      then

      consider x be Element of c such that

       A4: (F1 . x) <> (F2 . x) by FUNCT_2: 63;

      reconsider x as Element of R;

      

       A5: R is well_founded;

      

       A6: P[x] by A4;

      consider x0 be Element of R such that

       A7: P[x0] and

       A8: not ex y be Element of R st x0 <> y & P[y] & [y, x0] in r from WFMin( A6, A5);

      

       A9: ( dom F1) = c by FUNCT_2:def 1;

      (F1 | (r -Seg x0)) = (F2 | (r -Seg x0))

      proof

        set fr = (F1 | (r -Seg x0)), gr = (F2 | (r -Seg x0));

        assume

         A10: not thesis;

        

         A11: ( dom fr) = (r -Seg x0) by A9, Th3, RELAT_1: 62;

        ( dom gr) = (r -Seg x0) by A3, Th3, RELAT_1: 62;

        then

        consider x1 be object such that

         A12: x1 in ( dom fr) and

         A13: (fr . x1) <> (gr . x1) by A11, A10;

        

         A14: [x1, x0] in r by A11, A12, WELLORD1: 1;

        reconsider x1 as Element of R by A12;

        

         A15: x1 <> x0 by A11, A12, WELLORD1: 1;

        (fr . x1) = (F1 . x1) & (gr . x1) = (F2 . x1) by A11, A12, FUNCT_1: 49;

        hence contradiction by A8, A13, A14, A15;

      end;

      

      then (F1 . x0) = (H . (x0,(F2 | (r -Seg x0)))) by A1

      .= (F2 . x0) by A2;

      hence contradiction by A7;

    end;

    definition

      let R be RelStr, f be sequence of R;

      :: WELLFND1:def6

      attr f is descending means for n be Nat holds (f . (n + 1)) <> (f . n) & [(f . (n + 1)), (f . n)] in the InternalRel of R;

    end

    theorem :: WELLFND1:14

    for R be non empty RelStr holds R is well_founded iff not ex f be 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;

        given f be sequence of R such that

         A2: f is descending;

        

         A3: ( dom f) = NAT by FUNCT_2:def 1;

        then ( rng f) <> {} by RELAT_1: 42;

        then

        consider a be object such that

         A4: a in ( rng f) and

         A5: (r -Seg a) misses ( rng f) by A1;

        consider n be object such that

         A6: n in ( dom f) and

         A7: a = (f . n) by A4, FUNCT_1:def 3;

        reconsider n as Element of NAT by A6;

        (f . (n + 1)) <> (f . n) & [(f . (n + 1)), (f . n)] in the InternalRel of R by A2;

        then

         A8: (f . (n + 1)) in (r -Seg (f . n)) by WELLORD1: 1;

        (f . (n + 1)) in ( rng f) by A3, FUNCT_1:def 3;

        hence contradiction by A5, A7, A8, XBOOLE_0: 3;

      end;

      assume

       A9: not ex f be sequence of R st f is descending;

      assume not R is well_founded;

      then not r is_well_founded_in c;

      then

      consider Y be set such that

       A10: Y c= c and

       A11: Y <> {} and

       A12: for a be object holds not a in Y or (r -Seg a) meets Y;

      deffunc G( set, set) = the Element of ((r -Seg $2) /\ Y);

      consider f be Function such that

       A13: ( dom f) = NAT and

       A14: (f . 0 ) = the Element of Y and

       A15: for n be Nat holds (f . (n + 1)) = G(n,.) from NAT_1:sch 11;

      defpred P[ Nat] means (f . $1) in Y;

       A16:

      now

        let n be Nat;

        assume P[n];

        then (r -Seg (f . n)) meets Y by A12;

        then

         A17: ((r -Seg (f . n)) /\ Y) <> {} ;

        (f . (n + 1)) = the Element of ((r -Seg (f . n)) /\ Y) by A15;

        hence P[(n + 1)] by A17, XBOOLE_0:def 4;

      end;

      

       A18: P[ 0 ] by A11, A14;

      

       A19: for n be Nat holds P[n] from NAT_1:sch 2( A18, A16);

      ( rng f) c= c

      proof

        let y be object;

        assume y in ( rng f);

        then

        consider x be object such that

         A20: x in ( dom f) and

         A21: y = (f . x) by FUNCT_1:def 3;

        reconsider n = x as Element of NAT by A13, A20;

        (f . n) in Y by A19;

        hence thesis by A10, A21;

      end;

      then

      reconsider f as sequence of R by A13, FUNCT_2: 2;

      now

        let n be Nat;

        (r -Seg (f . n)) meets Y by A12, A19;

        then

         A22: ((r -Seg (f . n)) /\ Y) <> {} ;

        (f . (n + 1)) = the Element of ((r -Seg (f . n)) /\ Y) by A15;

        then (f . (n + 1)) in (r -Seg (f . n)) by A22, XBOOLE_0:def 4;

        hence (f . (n + 1)) <> (f . n) & [(f . (n + 1)), (f . n)] in r by WELLORD1: 1;

      end;

      then f is descending;

      hence contradiction by A9;

    end;