ordinal6.miz



    begin

    reserve a,b,c,d for Ordinal;

    reserve l for non empty limit_ordinal Ordinal;

    reserve u for Element of l;

    reserve A for non empty Ordinal;

    reserve e for Element of A;

    reserve X,Y,x,y,z for set;

    reserve n,m for Nat;

    definition

      let X be set;

      :: ORDINAL6:def1

      attr X is ordinal-membered means

      : Def1: ex a st X c= a;

    end

    registration

      cluster ordinal -> ordinal-membered for set;

      coherence ;

      let X;

      cluster ( On X) -> ordinal-membered;

      coherence

      proof

        take ( sup X);

        thus thesis by ORDINAL2:def 3;

      end;

    end

    theorem :: ORDINAL6:1

    

     Th1: X is ordinal-membered iff for x st x in X holds x is ordinal

    proof

      thus X is ordinal-membered implies for x st x in X holds x is ordinal;

      assume

       A1: for x st x in X holds x is ordinal;

      take a = ( sup X);

      let x be object;

      assume

       A2: x in X;

      then x is Ordinal by A1;

      hence thesis by A2, ORDINAL2: 19;

    end;

    registration

      cluster ordinal-membered for set;

      existence

      proof

        take 0 , 0 ;

        thus 0 c= 0 ;

      end;

    end

    registration

      let X be ordinal-membered set;

      cluster -> ordinal for Element of X;

      coherence

      proof

        let a be Element of X;

        per cases ;

          suppose X is empty;

          hence thesis;

        end;

          suppose X is non empty;

          hence thesis by Th1;

        end;

      end;

    end

    theorem :: ORDINAL6:2

    

     Th2: X is ordinal-membered iff ( On X) = X

    proof

      hereby

        assume

         A1: X is ordinal-membered;

        thus ( On X) = X

        proof

          thus ( On X) c= X by ORDINAL2: 7;

          let x be object;

          thus thesis by A1, ORDINAL1:def 9;

        end;

      end;

      thus thesis;

    end;

    theorem :: ORDINAL6:3

    for X be ordinal-membered set holds X c= ( sup X) by ORDINAL2: 19;

    theorem :: ORDINAL6:4

    

     Th4: a c= b iff b nin a

    proof

      a c= b & b in a implies b in b;

      hence thesis by ORDINAL1: 16;

    end;

    theorem :: ORDINAL6:5

    x in (a \ b) iff b c= x & x in a

    proof

      x in (a \ b) iff x nin b & x in a by XBOOLE_0:def 5;

      hence thesis by Th4;

    end;

    registration

      let a, b;

      cluster (a \ b) -> ordinal-membered;

      coherence ;

    end

    theorem :: ORDINAL6:6

    

     Th6: for f be Function st f is_isomorphism_of (( RelIncl X),( RelIncl Y)) holds for x, y st x in X & y in X holds x c= y iff (f . x) c= (f . y)

    proof

      let f be Function;

      assume

       A1: f is_isomorphism_of (( RelIncl X),( RelIncl Y));

      let x, y such that

       A2: x in X & y in X;

      

       A3: ( field ( RelIncl X)) = X & ( field ( RelIncl Y)) = Y by WELLORD2:def 1;

      then ( dom f) = X & ( rng f) = Y by A1;

      then

       A4: (f . x) in Y & (f . y) in Y by A2, FUNCT_1:def 3;

      x c= y iff [x, y] in ( RelIncl X) by A2, WELLORD2:def 1;

      then x c= y iff [(f . x), (f . y)] in ( RelIncl Y) by A1, A2, A3;

      hence thesis by A4, WELLORD2:def 1;

    end;

    theorem :: ORDINAL6:7

    for X,Y be ordinal-membered set holds for f be Function st f is_isomorphism_of (( RelIncl X),( RelIncl Y)) holds for x, y st x in X & y in X holds x in y iff (f . x) in (f . y)

    proof

      let X,Y be ordinal-membered set;

      let f be Function;

      assume

       A1: f is_isomorphism_of (( RelIncl X),( RelIncl Y));

      let x, y;

      assume

       A2: x in X & y in X;

      ( field ( RelIncl X)) = X & ( field ( RelIncl Y)) = Y by WELLORD2:def 1;

      then ( dom f) = X & ( rng f) = Y by A1;

      then (f . x) in Y & (f . y) in Y by A2, FUNCT_1:def 3;

      then

      reconsider a = (f . x), b = (f . y), x, y as Ordinal by A2;

      y c= x iff b c= a by A1, A2, Th6;

      hence thesis by Th4;

    end;

    theorem :: ORDINAL6:8

    

     Th8: [x, y] in ( RelIncl X) implies x c= y

    proof

      assume

       A1: [x, y] in ( RelIncl X);

      ( field ( RelIncl X)) = X by WELLORD2:def 1;

      then x in X & y in X by A1, RELAT_1: 15;

      hence x c= y by A1, WELLORD2:def 1;

    end;

    theorem :: ORDINAL6:9

    

     Th9: for f1,f2 be Sequence holds f1 c= (f1 ^ f2)

    proof

      let f1,f2 be Sequence;

      ( dom (f1 ^ f2)) = (( dom f1) +^ ( dom f2)) by ORDINAL4:def 1;

      then

       A1: ( dom f1) c= ( dom (f1 ^ f2)) by ORDINAL3: 24;

      for x be object st x in ( dom f1) holds (f1 . x) = ((f1 ^ f2) . x) by ORDINAL4:def 1;

      hence f1 c= (f1 ^ f2) by A1, GRFUNC_1: 2;

    end;

    ::$Canceled

    

     Th10: for f1,f2 be Sequence holds ( rng (f1 ^ f2)) = (( rng f1) \/ ( rng f2)) by ORDINAL4: 2;

    theorem :: ORDINAL6:11

    

     Th11: a c= b iff ( epsilon_ a) c= ( epsilon_ b)

    proof

      hereby

        assume a c= b;

        then a = b or a c< b;

        then a = b or ( epsilon_ a) in ( epsilon_ b) by ORDINAL1: 11, ORDINAL5: 44;

        hence ( epsilon_ a) c= ( epsilon_ b) by ORDINAL1:def 2;

      end;

      assume

       A1: ( epsilon_ a) c= ( epsilon_ b);

      assume a c/= b;

      then ( epsilon_ b) in ( epsilon_ a) by ORDINAL1: 16, ORDINAL5: 44;

      then ( epsilon_ b) in ( epsilon_ b) by A1;

      hence thesis;

    end;

    theorem :: ORDINAL6:12

    

     Th12: a in b iff ( epsilon_ a) in ( epsilon_ b)

    proof

      b c/= a iff ( epsilon_ b) c/= ( epsilon_ a) by Th11;

      hence thesis by Th4;

    end;

    registration

      let X be ordinal-membered set;

      cluster ( union X) -> ordinal;

      coherence

      proof

        ex a st X c= a by Def1;

        hence thesis by ORDINAL3: 4;

      end;

    end

    registration

      let f be Ordinal-yielding Function;

      cluster ( rng f) -> ordinal-membered;

      coherence by ORDINAL2:def 4;

    end

    registration

      let a;

      cluster ( id a) -> Sequence-like Ordinal-yielding;

      coherence ;

    end

    registration

      let a;

      cluster ( id a) -> increasing;

      coherence

      proof

        let f be Ordinal-Sequence such that

         A1: f = ( id a);

        let b, c;

        assume

         A2: b in c & c in ( dom f);

        then b in ( dom f) & ( dom f) = a by A1, ORDINAL1: 10;

        then (f . b) = b & (f . c) = c by A1, A2, FUNCT_1: 18;

        hence thesis by A2;

      end;

    end

    registration

      let a;

      cluster ( id a) -> continuous;

      coherence

      proof

        let f be Ordinal-Sequence such that

         A1: f = ( id a);

        let b, c;

        assume

         A2: b in ( dom f) & b <> 0 & b is limit_ordinal & c = (f . b);

        set g = (f | b);

        

         A3: ( dom f) = a & ( dom ( id b)) = b by A1;

        

         A4: c = b by A1, A2, FUNCT_1: 18;

        b c= a by A2, A3, ORDINAL1:def 2;

        then

         A5: g = ( id b) by A1, FUNCT_3: 1;

        per cases ;

          case c = 0 ;

          hence thesis by A2, A1, FUNCT_1: 18;

        end;

          case c <> 0 ;

          let B,C be Ordinal;

          assume

           A6: B in c & c in C;

          take D = ( succ B);

          thus D in ( dom g) by A2, A4, A5, A6, ORDINAL1: 28;

          let E be Ordinal;

          assume

           A7: D c= E & E in ( dom g);

          then (g . E) = E by A5, FUNCT_1: 18;

          hence B in (g . E) & (g . E) in C by A4, A5, A6, A7, ORDINAL1: 10, ORDINAL1: 21;

        end;

      end;

    end

    registration

      cluster non empty increasing continuous for Ordinal-Sequence;

      existence

      proof

        set A = the non empty Ordinal;

        take ( id A);

        thus thesis;

      end;

    end

    definition

      let f be Sequence;

      :: ORDINAL6:def2

      attr f is normal means f is increasing continuous Ordinal-Sequence;

    end

    definition

      let f be Ordinal-Sequence;

      :: original: normal

      redefine

      :: ORDINAL6:def3

      attr f is normal means f is increasing continuous;

      compatibility ;

    end

    registration

      cluster normal -> Ordinal-yielding for Sequence;

      coherence ;

      cluster normal -> increasing continuous for Ordinal-Sequence;

      coherence ;

      cluster increasing continuous -> normal for Ordinal-Sequence;

      coherence ;

    end

    registration

      cluster non empty normal for Sequence;

      existence

      proof

        set A = the non empty Ordinal;

        take ( id A);

        thus thesis;

      end;

    end

    theorem :: ORDINAL6:13

    

     Th13: for f be Ordinal-Sequence holds f is non-decreasing implies (f | a) is non-decreasing

    proof

      let f be Ordinal-Sequence;

      assume

       A1: for b, c st b in c & c in ( dom f) holds (f . b) c= (f . c);

      let b, c;

      assume

       A2: b in c & c in ( dom (f | a));

      then

       A3: c in ( dom f) & c in a by RELAT_1: 57;

      then ((f | a) . b) = (f . b) & ((f | a) . c) = (f . c) by A2, FUNCT_1: 49, ORDINAL1: 10;

      hence thesis by A1, A2, A3;

    end;

    definition

      let X;

      :: ORDINAL6:def4

      func ord-type X -> Ordinal equals ( order_type_of ( RelIncl ( On X)));

      coherence ;

    end

    definition

      let X be ordinal-membered set;

      :: original: ord-type

      redefine

      :: ORDINAL6:def5

      func ord-type X equals ( order_type_of ( RelIncl X));

      compatibility by Th2;

    end

    registration

      let X be ordinal-membered set;

      cluster ( RelIncl X) -> well-ordering;

      coherence

      proof

        ex a st X c= a by Def1;

        hence thesis by WELLORD2: 8;

      end;

    end

    registration

      let E be empty set;

      cluster ( On E) -> empty;

      coherence by ORDINAL2: 7, XBOOLE_1: 3;

    end

    registration

      let E be empty set;

      cluster ( order_type_of E) -> empty;

      coherence

      proof

        ( RelIncl E) = E;

        hence thesis by ORDERS_1: 88;

      end;

    end

    theorem :: ORDINAL6:14

    ( ord-type {} ) = 0 ;

    theorem :: ORDINAL6:15

    ( ord-type {a}) = 1

    proof

      a in ( succ a) by ORDINAL1: 6;

      then

       A1: {a} c= ( succ a) by ZFMISC_1: 31;

      then ( order_type_of ( RelIncl {a})) = 1 by CARD_5: 37;

      hence thesis by A1, ORDINAL3: 6;

    end;

    theorem :: ORDINAL6:16

    a <> b implies ( ord-type {a, b}) = 2

    proof

      assume a <> b;

      then

       A1: ( card {a, b}) = 2 by CARD_2: 57;

      a c= (a \/ b) & b c= (a \/ b) by XBOOLE_1: 7;

      then a in ( succ (a \/ b)) & b in ( succ (a \/ b)) by ORDINAL1: 22;

      then

       A2: {a, b} c= ( succ (a \/ b)) by ZFMISC_1: 32;

      then ( On {a, b}) = {a, b} by ORDINAL3: 6;

      hence thesis by A1, A2, CARD_5: 36;

    end;

    theorem :: ORDINAL6:17

    ( ord-type a) = a by ORDERS_1: 88;

    definition

      let X;

      :: ORDINAL6:def6

      func numbering X -> Ordinal-Sequence equals ( canonical_isomorphism_of (( RelIncl ( ord-type X)),( RelIncl ( On X))));

      coherence

      proof

        set R1 = ( RelIncl ( ord-type X));

        set R2 = ( RelIncl ( On X));

        set f = ( canonical_isomorphism_of (R1,R2));

        consider a such that

         A1: ( On X) c= a by Def1;

        ex phi be Ordinal-Sequence st phi = f & phi is increasing & ( dom phi) = ( ord-type X) & ( rng phi) = ( On X) by A1, CARD_5: 5;

        hence thesis;

      end;

    end

    theorem :: ORDINAL6:18

    

     Th18: ( dom ( numbering X)) = ( ord-type X) & ( rng ( numbering X)) = ( On X)

    proof

      set R1 = ( RelIncl ( ord-type X));

      set R2 = ( RelIncl ( On X));

      set f = ( canonical_isomorphism_of (R1,R2));

      consider a such that

       A1: ( On X) c= a by Def1;

      ex phi be Ordinal-Sequence st phi = f & phi is increasing & ( dom phi) = ( ord-type X) & ( rng phi) = ( On X) by A1, CARD_5: 5;

      hence thesis;

    end;

    theorem :: ORDINAL6:19

    

     Th19: for X be ordinal-membered set holds ( rng ( numbering X)) = X

    proof

      let X be ordinal-membered set;

      

      thus ( rng ( numbering X)) = ( On X) by Th18

      .= X by Th2;

    end;

    theorem :: ORDINAL6:20

    ( card ( dom ( numbering X))) = ( card ( On X))

    proof

      ( dom ( numbering X)) = ( ord-type X) & ex a st ( On X) c= a by Th18, Def1;

      hence thesis by CARD_5: 7;

    end;

    theorem :: ORDINAL6:21

    

     Th21: ( numbering X) is_isomorphism_of (( RelIncl ( ord-type X)),( RelIncl ( On X)))

    proof

      set R1 = ( RelIncl ( ord-type X));

      set R2 = ( RelIncl ( On X));

      (R2,R1) are_isomorphic by WELLORD2:def 2;

      then (R1,R2) are_isomorphic by WELLORD1: 40;

      hence thesis by WELLORD1:def 9;

    end;

    reserve f for Ordinal-Sequence;

    theorem :: ORDINAL6:22

    

     Th22: f = ( numbering X) & x in ( dom f) & y in ( dom f) implies (x c= y iff (f . x) c= (f . y))

    proof

      assume

       A1: f = ( numbering X) & x in ( dom f) & y in ( dom f);

      then ( dom f) = ( ord-type X) & f is_isomorphism_of (( RelIncl ( ord-type X)),( RelIncl ( On X))) by Th18, Th21;

      hence thesis by A1, Th6;

    end;

    theorem :: ORDINAL6:23

    

     Th23: f = ( numbering X) & x in ( dom f) & y in ( dom f) implies (x in y iff (f . x) in (f . y))

    proof

      assume

       A1: f = ( numbering X) & x in ( dom f) & y in ( dom f);

      then y c= x iff (f . y) c= (f . x) by Th22;

      hence thesis by A1, Th4;

    end;

    registration

      let X;

      cluster ( numbering X) -> increasing;

      coherence

      proof

        set R1 = ( RelIncl ( ord-type X));

        set R2 = ( RelIncl ( On X));

        set f = ( canonical_isomorphism_of (R1,R2));

        consider a such that

         A1: ( On X) c= a by Def1;

        ex phi be Ordinal-Sequence st phi = f & phi is increasing & ( dom phi) = ( ord-type X) & ( rng phi) = ( On X) by A1, CARD_5: 5;

        hence thesis;

      end;

    end

    registration

      let X,Y be ordinal-membered set;

      cluster (X \/ Y) -> ordinal-membered;

      coherence

      proof

        consider a such that

         A1: X c= a by Def1;

        consider b such that

         A2: Y c= b by Def1;

        take (a \/ b);

        thus thesis by A1, A2, XBOOLE_1: 13;

      end;

    end

    registration

      let X be ordinal-membered set, Y be set;

      cluster (X \ Y) -> ordinal-membered;

      coherence

      proof

        consider a such that

         A1: X c= a by Def1;

        take a;

        thus thesis by A1;

      end;

    end

    theorem :: ORDINAL6:24

    

     Th24: for X,Y be ordinal-membered set st for x, y st x in X & y in Y holds x in y holds (( numbering X) ^ ( numbering Y)) is_isomorphism_of (( RelIncl (( ord-type X) +^ ( ord-type Y))),( RelIncl (X \/ Y)))

    proof

      let X,Y be ordinal-membered set;

      assume

       A1: for x, y st x in X & y in Y holds x in y;

      set f = ( numbering X), g = ( numbering Y);

      set a = ( ord-type X), b = ( ord-type Y);

      set R = ( RelIncl (a +^ b)), Q = ( RelIncl (X \/ Y));

      set R1 = ( RelIncl a), Q1 = ( RelIncl X);

      set R2 = ( RelIncl b), Q2 = ( RelIncl Y);

      

       A2: ( dom (f ^ g)) = (( dom f) +^ ( dom g)) by ORDINAL4:def 1;

      

       A3: ( dom f) = a & ( dom g) = b by Th18;

      

       A4: ( rng f) = X & ( rng g) = Y by Th19;

      

       A5: f is_isomorphism_of (( RelIncl a),( RelIncl ( On X))) & g is_isomorphism_of (( RelIncl b),( RelIncl ( On Y))) by Th21;

      then

       A6: f is one-to-one & g is one-to-one;

      

      thus

       A7: ( dom (f ^ g)) = (( dom f) +^ ( dom g)) by ORDINAL4:def 1

      .= ( field R) by A3, WELLORD2:def 1;

      

      thus ( rng (f ^ g)) = (( rng f) \/ ( rng g)) by Th10

      .= ( field Q) by A4, WELLORD2:def 1;

      then

       A8: ( rng (f ^ g)) = (X \/ Y) by WELLORD2:def 1;

      

       A9: ( On X) = X & ( On Y) = Y by Th2;

      thus (f ^ g) is one-to-one

      proof

        let x,y be object;

        assume

         A10: x in ( dom (f ^ g)) & y in ( dom (f ^ g)) & ((f ^ g) . x) = ((f ^ g) . y);

        then

        reconsider a = x, b = y as Ordinal;

        per cases by ORDINAL1: 16;

          suppose

           A11: x in ( dom f) & y in ( dom f);

          then ((f ^ g) . x) = (f . x) & ((f ^ g) . y) = (f . y) by ORDINAL4:def 1;

          hence thesis by A6, A10, A11;

        end;

          suppose

           A12: x in ( dom f) & ( dom f) c= b;

          then

           A13: (( dom f) +^ (b -^ ( dom f))) = y by ORDINAL3:def 5;

          then

           A14: (b -^ ( dom f)) in ( dom g) by A2, A10, ORDINAL3: 22;

          then ((f ^ g) . x) = (f . x) & ((f ^ g) . y) = (g . (b -^ ( dom f))) by A12, A13, ORDINAL4:def 1;

          then (f . x) in X & (f . x) in Y by A4, A10, A12, A14, FUNCT_1:def 3;

          then (f . x) in (f . x) by A1;

          hence thesis;

        end;

          suppose

           A15: ( dom f) c= a & y in ( dom f);

          then

           A16: (( dom f) +^ (a -^ ( dom f))) = x by ORDINAL3:def 5;

          then

           A17: (a -^ ( dom f)) in ( dom g) by A2, A10, ORDINAL3: 22;

          then ((f ^ g) . y) = (f . y) & ((f ^ g) . x) = (g . (a -^ ( dom f))) by A15, A16, ORDINAL4:def 1;

          then (f . y) in X & (f . y) in Y by A4, A10, A15, A17, FUNCT_1:def 3;

          then (f . y) in (f . y) by A1;

          hence thesis;

        end;

          suppose ( dom f) c= a & ( dom f) c= b;

          then

           A18: (( dom f) +^ (a -^ ( dom f))) = x & (( dom f) +^ (b -^ ( dom f))) = y by ORDINAL3:def 5;

          then

           A19: (a -^ ( dom f)) in ( dom g) & (b -^ ( dom f)) in ( dom g) by A2, A10, ORDINAL3: 22;

          then ((f ^ g) . y) = (g . (b -^ ( dom f))) & ((f ^ g) . x) = (g . (a -^ ( dom f))) by A18, ORDINAL4:def 1;

          hence thesis by A6, A10, A18, A19;

        end;

      end;

      let x,y be object;

      

       A20: ( field R) = (a +^ b) by WELLORD2:def 1;

      hereby

        assume

         A21: [x, y] in R;

        hence

         A22: x in ( field R) & y in ( field R) by RELAT_1: 15;

        reconsider xx = x, yy = y as set by TARSKI: 1;

        

         A23: xx c= yy by A21, A20, WELLORD2:def 1, A22;

        

         A24: ((f ^ g) . x) in (X \/ Y) & ((f ^ g) . y) in (X \/ Y) by A7, A8, A22, FUNCT_1:def 3;

        thus [((f ^ g) . x), ((f ^ g) . y)] in Q

        proof

          reconsider x, y as Ordinal by A20, A22;

          per cases by ORDINAL1: 16;

            suppose

             A25: x in ( dom f) & y in ( dom f);

            then

             A26: [x, y] in ( RelIncl a) by A3, A23, WELLORD2:def 1;

            ((f ^ g) . x) = (f . x) & ((f ^ g) . y) = (f . y) by A25, ORDINAL4:def 1;

            then

             A27: [((f ^ g) . x), ((f ^ g) . y)] in Q1 by A9, A5, A26;

            then ((f ^ g) . x) in ( field Q1) & ((f ^ g) . y) in ( field Q1) by RELAT_1: 15;

            then ((f ^ g) . x) in X & ((f ^ g) . y) in X by WELLORD2:def 1;

            then ((f ^ g) . x) c= ((f ^ g) . y) by A27, WELLORD2:def 1;

            hence thesis by A24, WELLORD2:def 1;

          end;

            suppose

             A28: x in ( dom f) & ( dom f) c= y;

            then

             A29: (( dom f) +^ (y -^ ( dom f))) = y by ORDINAL3:def 5;

            then

             A30: (y -^ ( dom f)) in ( dom g) by A3, A20, A22, ORDINAL3: 22;

            then ((f ^ g) . x) = (f . x) & ((f ^ g) . y) = (g . (y -^ ( dom f))) by A28, A29, ORDINAL4:def 1;

            then ((f ^ g) . x) in X & ((f ^ g) . y) in Y by A4, A28, A30, FUNCT_1:def 3;

            then ((f ^ g) . x) in ((f ^ g) . y) by A1;

            then ((f ^ g) . x) c= ((f ^ g) . y) by ORDINAL1:def 2;

            hence thesis by A24, WELLORD2:def 1;

          end;

            suppose ( dom f) c= x & y in ( dom f);

            then y in x;

            then y in y by A23;

            hence thesis;

          end;

            suppose ( dom f) c= x & ( dom f) c= y;

            then

             A31: (( dom f) +^ (x -^ ( dom f))) = x & (( dom f) +^ (y -^ ( dom f))) = y by ORDINAL3:def 5;

            then

             A32: (x -^ ( dom f)) in ( dom g) & (y -^ ( dom f)) in ( dom g) by A3, A20, A22, ORDINAL3: 22;

            (x -^ a) c= (y -^ a) by A23, ORDINAL3: 59;

            then

             A33: [(x -^ a), (y -^ a)] in ( RelIncl b) by A32, A3, WELLORD2:def 1;

            ((f ^ g) . y) = (g . (y -^ ( dom f))) & ((f ^ g) . x) = (g . (x -^ ( dom f))) by A31, A32, ORDINAL4:def 1;

            then

             A34: [((f ^ g) . x), ((f ^ g) . y)] in Q2 by A9, A3, A5, A33;

            then ((f ^ g) . x) in ( field Q2) & ((f ^ g) . y) in ( field Q2) by RELAT_1: 15;

            then ((f ^ g) . x) in Y & ((f ^ g) . y) in Y by WELLORD2:def 1;

            then ((f ^ g) . x) c= ((f ^ g) . y) by A34, WELLORD2:def 1;

            hence thesis by A24, WELLORD2:def 1;

          end;

        end;

      end;

      assume

       A35: x in ( field R) & y in ( field R) & [((f ^ g) . x), ((f ^ g) . y)] in Q;

      then

       A36: ((f ^ g) . x) c= ((f ^ g) . y) by Th8;

      reconsider x, y as Ordinal by A20, A35;

      per cases by ORDINAL1: 16;

        suppose

         A37: x in ( dom f) & y in ( dom f);

        then

         A38: ((f ^ g) . x) = (f . x) & ((f ^ g) . y) = (f . y) by ORDINAL4:def 1;

        (f . x) in X & (f . y) in X by A4, A37, FUNCT_1:def 3;

        then [(f . x), (f . y)] in Q1 by A38, A36, WELLORD2:def 1;

        then [x, y] in R1 by A9, A37, A5;

        then x c= y by Th8;

        hence thesis by A20, A35, WELLORD2:def 1;

      end;

        suppose x in ( dom f) & ( dom f) c= y;

        then x c= y by ORDINAL1:def 2;

        hence thesis by A20, A35, WELLORD2:def 1;

      end;

        suppose

         A39: ( dom f) c= x & y in ( dom f);

        then

         A40: ((f ^ g) . y) = (f . y) by ORDINAL4:def 1;

        

         A41: (f . y) in X by A4, A39, FUNCT_1:def 3;

        

         A42: (( dom f) +^ (x -^ ( dom f))) = x by A39, ORDINAL3:def 5;

        then

         A43: (x -^ ( dom f)) in ( dom g) by A3, A20, A35, ORDINAL3: 22;

        then

         A44: ((f ^ g) . x) = (g . (x -^ ( dom f))) by A42, ORDINAL4:def 1;

        (g . (x -^ ( dom f))) in Y by A4, A43, FUNCT_1:def 3;

        then ((f ^ g) . y) in ((f ^ g) . x) by A40, A41, A44, A1;

        then ((f ^ g) . y) in ((f ^ g) . y) by A36;

        hence thesis;

      end;

        suppose ( dom f) c= x & ( dom f) c= y;

        then

         A45: (( dom f) +^ (x -^ ( dom f))) = x & (( dom f) +^ (y -^ ( dom f))) = y by ORDINAL3:def 5;

        then

         A46: (x -^ ( dom f)) in ( dom g) & (y -^ ( dom f)) in ( dom g) by A3, A20, A35, ORDINAL3: 22;

        then

         A47: (g . (y -^ ( dom f))) in Y & (g . (x -^ ( dom f))) in Y by A4, FUNCT_1:def 3;

        ((f ^ g) . y) = (g . (y -^ ( dom f))) & ((f ^ g) . x) = (g . (x -^ ( dom f))) by A45, A46, ORDINAL4:def 1;

        then [(g . (x -^ ( dom f))), (g . (y -^ ( dom f)))] in Q2 by A47, A36, WELLORD2:def 1;

        then [(x -^ ( dom f)), (y -^ ( dom f))] in R2 by A9, A5, A46;

        then (x -^ ( dom f)) c= (y -^ ( dom f)) by Th8;

        then x c= y by A45, ORDINAL3: 18;

        hence thesis by A20, A35, WELLORD2:def 1;

      end;

    end;

    theorem :: ORDINAL6:25

    

     Th25: for X,Y be ordinal-membered set st for x, y st x in X & y in Y holds x in y holds ( numbering (X \/ Y)) = (( numbering X) ^ ( numbering Y))

    proof

      let X,Y be ordinal-membered set;

      assume

       A1: for x, y st x in X & y in Y holds x in y;

      set f = ( numbering X), g = ( numbering Y), h = ( numbering (X \/ Y));

      set a = ( ord-type X), b = ( ord-type Y);

      set P = ( RelIncl (a +^ b)), Q = ( RelIncl (X \/ Y));

      set R = ( RelIncl ( ord-type (X \/ Y)));

      

       A2: ( On (X \/ Y)) = (X \/ Y) & ( On X) = X & ( On Y) = Y by Th2;

      then

       A3: h is_isomorphism_of (R,Q) by Th21;

      

       A4: (f ^ g) is_isomorphism_of (P,Q) by A1, Th24;

      then

       A5: (P,Q) are_isomorphic & (R,Q) are_isomorphic by A3;

      then (Q,R) are_isomorphic by WELLORD1: 40;

      then (a +^ b) = ( ord-type (X \/ Y)) by A5, WELLORD1: 42, WELLORD2: 10;

      hence ( numbering (X \/ Y)) = (( numbering X) ^ ( numbering Y)) by A2, A4, A5, WELLORD1:def 9;

    end;

    theorem :: ORDINAL6:26

    for X,Y be ordinal-membered set st for x, y st x in X & y in Y holds x in y holds ( ord-type (X \/ Y)) = (( ord-type X) +^ ( ord-type Y))

    proof

      let X,Y be ordinal-membered set;

      assume for x, y st x in X & y in Y holds x in y;

      then

       A1: ( numbering (X \/ Y)) = (( numbering X) ^ ( numbering Y)) by Th25;

      

      thus ( ord-type (X \/ Y)) = ( dom ( numbering (X \/ Y))) by Th18

      .= (( dom ( numbering X)) +^ ( dom ( numbering Y))) by A1, ORDINAL4:def 1

      .= (( ord-type X) +^ ( dom ( numbering Y))) by Th18

      .= (( ord-type X) +^ ( ord-type Y)) by Th18;

    end;

    begin

    theorem :: ORDINAL6:27

    

     Th27: for f be Function st x is_a_fixpoint_of f holds x in ( rng f) by FUNCT_1:def 3;

    definition

      let f be Ordinal-Sequence;

      :: ORDINAL6:def7

      func criticals f -> Ordinal-Sequence equals ( numbering { a where a be Element of ( dom f) : a is_a_fixpoint_of f });

      coherence ;

    end

    theorem :: ORDINAL6:28

    

     Th28: ( On { a where a be Element of ( dom f) : a is_a_fixpoint_of f }) = { a where a be Element of ( dom f) : a is_a_fixpoint_of f }

    proof

      set X = { a where a be Element of ( dom f) : a is_a_fixpoint_of f };

      now

        let x;

        assume x in X;

        then ex a be Element of ( dom f) st x = a & a is_a_fixpoint_of f;

        hence x is ordinal;

      end;

      then X is ordinal-membered by Th1;

      hence thesis by Th2;

    end;

    theorem :: ORDINAL6:29

    

     Th29: x in ( dom ( criticals f)) implies (( criticals f) . x) is_a_fixpoint_of f

    proof

      set a = x;

      set X = { b where b be Element of ( dom f) : b is_a_fixpoint_of f };

      set g = ( criticals f);

      assume a in ( dom g);

      then (g . a) in ( rng g) by FUNCT_1:def 3;

      then (g . a) in ( On X) by Th18;

      then (g . a) in X by Th28;

      then ex b be Element of ( dom f) st (g . a) = b & b is_a_fixpoint_of f;

      hence thesis;

    end;

    theorem :: ORDINAL6:30

    

     Th30: ( rng ( criticals f)) = { a where a be Element of ( dom f) : a is_a_fixpoint_of f } & ( rng ( criticals f)) c= ( rng f)

    proof

      set X = { a where a be Element of ( dom f) : a is_a_fixpoint_of f };

      ( On X) = X by Th28;

      hence

       A1: ( rng ( criticals f)) = X by Th18;

      let x be object;

      assume x in ( rng ( criticals f));

      then ex a be Element of ( dom f) st x = a & a is_a_fixpoint_of f by A1;

      hence thesis by Th27;

    end;

    registration

      let f;

      cluster ( criticals f) -> increasing;

      coherence ;

    end

    theorem :: ORDINAL6:31

    x in ( dom ( criticals f)) implies x c= (( criticals f) . x) by ORDINAL4: 10;

    theorem :: ORDINAL6:32

    

     Th32: ( dom ( criticals f)) c= ( dom f)

    proof

      let x be Ordinal;

      set X = { a where a be Element of ( dom f) : a is_a_fixpoint_of f };

      assume

       A1: x in ( dom ( criticals f));

      then (( criticals f) . x) in ( rng ( criticals f)) by FUNCT_1:def 3;

      then (( criticals f) . x) in ( On X) by Th18;

      then (( criticals f) . x) in X by Th28;

      then

      consider a be Element of ( dom f) such that

       A2: (( criticals f) . x) = a & a is_a_fixpoint_of f;

      x c= a & a in ( dom f) & a = (f . a) by A1, A2, ORDINAL4: 10;

      hence thesis by ORDINAL1: 12;

    end;

    theorem :: ORDINAL6:33

    

     Th33: b is_a_fixpoint_of f implies ex a st a in ( dom ( criticals f)) & b = (( criticals f) . a)

    proof

      set X = { a where a be Element of ( dom f) : a is_a_fixpoint_of f };

      assume

       A1: b is_a_fixpoint_of f;

      b in X by A1;

      then b in ( rng ( criticals f)) by Th30;

      then ex x be object st x in ( dom ( criticals f)) & b = (( criticals f) . x) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: ORDINAL6:34

    a in ( dom ( criticals f)) & b is_a_fixpoint_of f & (( criticals f) . a) in b implies ( succ a) in ( dom ( criticals f))

    proof

      set g = ( criticals f);

      assume that

       A1: a in ( dom g) and

       A2: b is_a_fixpoint_of f and

       A3: (g . a) in b;

      consider c such that

       A4: c in ( dom g) & b = (g . c) by A2, Th33;

      a in c by A1, A3, A4, Th23;

      then ( succ a) c= c by ORDINAL1: 21;

      hence ( succ a) in ( dom ( criticals f)) by A4, ORDINAL1: 12;

    end;

    theorem :: ORDINAL6:35

    ( succ a) in ( dom ( criticals f)) & b is_a_fixpoint_of f & (( criticals f) . a) in b implies (( criticals f) . ( succ a)) c= b

    proof

      set g = ( criticals f);

      set Y = { c where c be Element of ( dom f) : c is_a_fixpoint_of f };

      set X = ( ord-type Y);

      assume

       A1: ( succ a) in ( dom g) & b is_a_fixpoint_of f & (g . a) in b;

      then

      consider c such that

       A2: c in ( dom g) & b = (g . c) by Th33;

      a in ( succ a) by ORDINAL1: 6;

      then

       A3: a in ( dom g) & (g . a) in (g . ( succ a)) by A1, ORDINAL1: 10, ORDINAL2:def 12;

      ( On Y) = Y by Th28;

      then

       A4: g is_isomorphism_of (( RelIncl X),( RelIncl Y)) by Th21;

      

       A5: ( dom g) = X by Th18;

      b c/= (g . a) by A1, Th4;

      then c c/= a by A2, A3, A4, A5, Th6;

      then a in c by Th4;

      then ( succ a) c= c by ORDINAL1: 21;

      hence (g . ( succ a)) c= b by A2, ORDINAL4: 9;

    end;

    theorem :: ORDINAL6:36

    

     Th36: f is normal & ( union X) in ( dom f) & X is non empty & (for x st x in X holds ex y st x c= y & y in X & y is_a_fixpoint_of f) implies ( union X) = (f . ( union X))

    proof

      assume that

       A1: f is normal and

       A2: ( union X) in ( dom f) & X is non empty and

       A3: for x st x in X holds ex y st x c= y & y in X & y is_a_fixpoint_of f;

      reconsider l = ( union X) as Ordinal by A2;

      per cases ;

        suppose ex a st a in X & for b st b in X holds b c= a;

        then

        consider a such that

         A4: a in X & for b st b in X holds b c= a;

        now

          let x;

          assume x in X;

          then

          consider y such that

           A5: x c= y & y in X & y is_a_fixpoint_of f by A3;

          y c= a by A4, A5;

          hence x c= a by A5;

        end;

        then ( union X) c= a & a c= ( union X) by A4, ZFMISC_1: 74, ZFMISC_1: 76;

        then

         A6: ( union X) = a;

        then

        consider y such that

         A7: ( union X) c= y & y in X & y is_a_fixpoint_of f by A3, A4;

        y c= ( union X) by A6, A7, A4;

        then y = ( union X) by A7;

        hence ( union X) = (f . ( union X)) by A7;

      end;

        suppose

         A8: not ex a st a in X & for b st b in X holds b c= a;

        set y0 = the Element of X;

        consider x0 be set such that

         A9: y0 c= x0 & x0 in X & x0 is_a_fixpoint_of f by A2, A3;

        consider b such that

         A10: b in X & b c/= x0 by A9, A8;

        now

          let a;

          assume a in l;

          then

          consider x such that

           A11: a in x & x in X by TARSKI:def 4;

          consider y such that

           A12: x c= y & y in X & y is_a_fixpoint_of f by A3, A11;

          consider b such that

           A13: b in X & b c/= y by A8, A12;

          ( succ a) c= y & y in b by A11, A12, A13, Th4, ORDINAL1: 21;

          then ( succ a) in b by ORDINAL1: 12;

          hence ( succ a) in l by A13, TARSKI:def 4;

        end;

        then

        reconsider l as non empty limit_ordinal Ordinal by A10, ORDINAL1: 28, TARSKI:def 4;

        thus ( union X) c= (f . ( union X)) by A2, A1, ORDINAL4: 10;

        reconsider g = (f | l) as increasing Ordinal-Sequence by A1, ORDINAL4: 15;

        l c= ( dom f) by A2, ORDINAL1:def 2;

        then

         A14: ( dom g) = l by RELAT_1: 62;

        then

         A15: ( Union g) is_limes_of g by ORDINAL5: 6;

        (f . l) is_limes_of g by A1, A2, ORDINAL2:def 13;

        then

         A16: (f . l) = ( lim g) & ( Union g) = ( lim g) by A15, ORDINAL2:def 10;

        let x be object;

        assume x in (f . ( union X));

        then

        consider z be object such that

         A17: z in ( dom g) & x in (g . z) by A16, CARD_5: 2;

        consider y such that

         A18: z in y & y in X by A14, A17, TARSKI:def 4;

        consider t be set such that

         A19: y c= t & t in X & t is_a_fixpoint_of f by A18, A3;

        

         A20: t in ( dom f) & t = (f . t) by A19;

        then

        reconsider z, t as Ordinal by A17;

        (f . z) = (g . z) & z in t by A17, A18, A19, FUNCT_1: 47;

        then (g . z) in t by A1, A20, ORDINAL2:def 12;

        then x in t by A17, ORDINAL1: 10;

        hence x in ( union X) by A19, TARSKI:def 4;

      end;

    end;

    theorem :: ORDINAL6:37

    

     Th37: f is normal & ( union X) in ( dom f) & X is non empty & (for x st x in X holds x is_a_fixpoint_of f) implies ( union X) = (f . ( union X))

    proof

      assume that

       A1: f is normal and

       A2: ( union X) in ( dom f) & X is non empty and

       A3: for x st x in X holds x is_a_fixpoint_of f;

      for x st x in X holds ex y st x c= y & y in X & y is_a_fixpoint_of f by A3;

      hence thesis by A1, A2, Th36;

    end;

    theorem :: ORDINAL6:38

    

     Th38: l c= ( dom ( criticals f)) & a is_a_fixpoint_of f & (for x st x in l holds (( criticals f) . x) in a) implies l in ( dom ( criticals f))

    proof

      set g = ( criticals f);

      assume that

       A1: l c= ( dom g) and

       A2: a is_a_fixpoint_of f and

       A3: for x st x in l holds (g . x) in a;

      consider b such that

       A4: b in ( dom g) & a = (g . b) by A2, Th33;

      l c= b

      proof

        let x be Ordinal;

        assume x in l;

        then x in ( dom g) & (g . x) in (g . b) by A1, A3, A4;

        hence x in b by A4, Th23;

      end;

      hence l in ( dom ( criticals f)) by A4, ORDINAL1: 12;

    end;

    theorem :: ORDINAL6:39

    

     Th39: f is normal & l in ( dom ( criticals f)) implies (( criticals f) . l) = ( Union (( criticals f) | l))

    proof

      set g = ( criticals f);

      reconsider h = (g | l) as increasing Ordinal-Sequence by ORDINAL4: 15;

      set X = ( rng h);

      assume

       A1: f is normal & l in ( dom g);

      then (g . l) is_a_fixpoint_of f by Th29;

      then

       A2: (g . l) in ( dom f) & (f . (g . l)) = (g . l);

      

       A3: l c= ( dom g) by A1, ORDINAL1:def 2;

      then

       A4: ( dom h) = l by RELAT_1: 62;

      

       A5: for x st x in X holds x is_a_fixpoint_of f

      proof

        let x;

        assume x in X;

        then

        consider y be object such that

         A6: y in ( dom h) & x = (h . y) by FUNCT_1:def 3;

        x = (g . y) & y in ( dom g) by A3, A4, A6, FUNCT_1: 47;

        hence thesis by Th29;

      end;

      reconsider u = ( union X) as Ordinal;

      

       A7: h <> {} by A4;

      now

        let x;

        assume x in X;

        then

        consider y be object such that

         A8: y in ( dom h) & x = (h . y) by FUNCT_1:def 3;

        x = (g . y) & y in ( dom g) by A3, A4, A8, FUNCT_1: 47;

        then x in (g . l) by A1, A4, A8, ORDINAL2:def 12;

        hence x c= (g . l) by ORDINAL1:def 2;

      end;

      then

       A9: ( union X) c= (g . l) by ZFMISC_1: 76;

      then

       A10: u in ( dom f) by A2, ORDINAL1: 12;

      u = (f . u) by A1, A5, A7, A9, Th37, A2, ORDINAL1: 12;

      then u is_a_fixpoint_of f by A10;

      then

      consider a such that

       A11: a in ( dom g) & u = (g . a) by Th33;

      a = l

      proof

        thus a c= l by A1, A11, A9, Th22;

        let x be Ordinal;

        assume

         A12: x in l;

        then

         A13: ( succ x) in l by ORDINAL1: 28;

        then

         A14: (g . x) = (h . x) & (g . ( succ x)) = (h . ( succ x)) & (h . ( succ x)) in X by A4, A12, FUNCT_1: 47, FUNCT_1:def 3;

        x in ( succ x) by ORDINAL1: 6;

        then (h . x) in (h . ( succ x)) by A4, A13, ORDINAL2:def 12;

        then (g . x) in u by A14, TARSKI:def 4;

        then (g . a) c/= (g . x) & x in ( dom g) by A3, A11, A12, Th4;

        then a c/= x by A11, Th22;

        hence thesis by Th4;

      end;

      hence thesis by A11;

    end;

    registration

      let f be normal Ordinal-Sequence;

      cluster ( criticals f) -> continuous;

      coherence

      proof

        set g = ( criticals f);

        let a, b;

        reconsider h = (g | a) as increasing Ordinal-Sequence by ORDINAL4: 15;

        assume

         A1: a in ( dom g) & a <> 0 & a is limit_ordinal & b = (g . a);

        then

         A2: b = ( Union h) by Th39;

        a c= ( dom g) by A1, ORDINAL1:def 2;

        then ( dom h) = a by RELAT_1: 62;

        hence b is_limes_of (g | a) by A1, A2, ORDINAL5: 6;

      end;

    end

    theorem :: ORDINAL6:40

    

     Th40: for f1,f2 be Ordinal-Sequence st f1 c= f2 holds ( criticals f1) c= ( criticals f2)

    proof

      let f1,f2 be Ordinal-Sequence;

      assume

       A1: f1 c= f2;

      then

       A2: ( dom f1) c= ( dom f2) by GRFUNC_1: 2;

      set X = { a where a be Element of ( dom f1) : a is_a_fixpoint_of f1 };

      set Z = { a where a be Element of ( dom f2) : a is_a_fixpoint_of f2 };

      ( On X) = X & ( On Z) = Z by Th28;

      then

      reconsider X, Z as ordinal-membered set;

      set Y = (Z \ X);

       A3:

      now

        let x, y;

        assume x in X;

        then

        consider a be Element of ( dom f1) such that

         A4: x = a & a is_a_fixpoint_of f1;

        assume y in Y;

        then

         A5: y in Z & not y in X by XBOOLE_0:def 5;

        then

        consider b be Element of ( dom f2) such that

         A6: y = b & b is_a_fixpoint_of f2;

        now

          assume

           A7: b in ( dom f1);

          

          then (f1 . b) = (f2 . b) by A1, GRFUNC_1: 2

          .= b by A6;

          then b is_a_fixpoint_of f1 by A7;

          hence contradiction by A5, A6;

        end;

        then ( dom f1) c= b & x in ( dom f1) by A4, Th4;

        hence x in y by A6;

      end;

      X c= Z

      proof

        let x be object;

        assume x in X;

        then

        consider a be Element of ( dom f1) such that

         A8: x = a & a is_a_fixpoint_of f1;

        a in ( dom f1) & a = (f1 . a) by A8;

        then a in ( dom f2) & a = (f2 . a) by A1, A2, GRFUNC_1: 2;

        then a is_a_fixpoint_of f2;

        hence thesis by A8;

      end;

      then (X \/ Y) = Z by XBOOLE_1: 45;

      then ( criticals f2) = (( criticals f1) ^ ( numbering Y)) by A3, Th25;

      hence ( criticals f1) c= ( criticals f2) by Th9;

    end;

    begin

    reserve U,W for Universe;

    registration

      let U;

      cluster normal for Ordinal-Sequence of U;

      existence

      proof

        reconsider F = ( id ( On U)) as Ordinal-Sequence of U;

        take F;

        thus thesis;

      end;

    end

    definition

      let U, a;

      mode Ordinal-Sequence of a,U is Function of a, ( On U);

    end

    registration

      let U, a;

      cluster -> Sequence-like Ordinal-yielding for Ordinal-Sequence of a, U;

      coherence by FUNCT_2:def 1, RELAT_1:def 19;

    end

    definition

      let U, a;

      let f be Ordinal-Sequence of a, U;

      let x;

      :: original: .

      redefine

      func f . x -> Ordinal of U ;

      coherence

      proof

        per cases by FUNCT_1:def 2;

          suppose x in ( dom f);

          then x in a by FUNCT_2:def 1;

          then (f . x) in ( On U) by FUNCT_2: 5;

          hence thesis by ORDINAL1:def 9;

        end;

          suppose (f . x) = 0 ;

          hence thesis by CLASSES2: 56;

        end;

      end;

    end

    theorem :: ORDINAL6:41

    

     Th41: a in U implies for f be Ordinal-Sequence of a, U holds ( Union f) in U

    proof

      assume

       A1: a in U;

      let f be Ordinal-Sequence of a, U;

      ( dom f) = a by FUNCT_2:def 1;

      then ( card ( dom f)) in ( card U) & ( card ( rng f)) c= ( card ( dom f)) & ( rng f) c= ( On U) & ( On U) c= U by A1, CARD_2: 61, CLASSES2: 1, ORDINAL2: 7, RELAT_1:def 19;

      then ( card ( rng f)) in ( card U) & ( rng f) c= U by ORDINAL1: 12;

      then ( rng f) in U by CLASSES1: 1;

      hence ( Union f) in U by CLASSES2: 59;

    end;

    theorem :: ORDINAL6:42

    

     Th42: a in U implies for f be Ordinal-Sequence of a, U holds ( sup f) in U

    proof

      assume

       A1: a in U;

      let f be Ordinal-Sequence of a, U;

      reconsider u = ( Union f) as Ordinal of U by Th41, A1;

      ( On ( rng f)) = ( rng f) by Th2;

      then ( sup f) c= ( succ u) by ORDINAL3: 72;

      hence ( sup f) in U by CLASSES1:def 1;

    end;

    scheme :: ORDINAL6:sch1

    CriticalNumber2 { U() -> Universe , a() -> Ordinal of U() , f() -> Ordinal-Sequence of omega , U() , phi( Ordinal) -> Ordinal } :

a() c= ( Union f()) & phi(Union) = ( Union f()) & for b st a() c= b & b in U() & phi(b) = b holds ( Union f()) c= b

      provided

       A1: omega in U()

       and

       A2: for a st a in U() holds phi(a) in U()

       and

       A3: for a, b st a in b & b in U() holds phi(a) in phi(b)

       and

       A4: for a be Ordinal of U() st a is non empty limit_ordinal holds for phi be Ordinal-Sequence st ( dom phi) = a & for b st b in a holds (phi . b) = phi(b) holds phi(a) is_limes_of phi

       and

       A5: (f() . 0 ) = a()

       and

       A6: for a st a in omega holds (f() . ( succ a)) = phi(.);

      

       A7: ( dom f()) = omega by FUNCT_2:def 1;

      

       A8: a() in ( rng f()) by A5, A7, FUNCT_1:def 3;

      hence a() c= ( Union f()) by ZFMISC_1: 74;

      set phi = f();

       A9:

      now

        defpred P[ Ordinal] means $1 in U() & $1 c/= phi($1);

        assume

         A10: ex a st P[a];

        consider a such that

         A11: P[a] and

         A12: for b st P[b] holds a c= b from ORDINAL1:sch 1( A10);

        phi(phi) in phi(a) by A3, A11, ORDINAL1: 16;

        then phi(a) c/= phi(phi) by ORDINAL1: 5;

        hence contradiction by A2, A11, A12;

      end;

      then a() c= phi(a);

      then

       A13: a() c< phi(a) or a() = phi(a);

      per cases by A13, ORDINAL1: 11;

        suppose

         A14: phi(a) = a();

        

         A15: for a be set st a in omega holds (f() . a) = a()

        proof

          let a be set;

          assume a in omega ;

          then

          reconsider a as Element of omega ;

          defpred P[ Nat] means (f() . $1) = a();

          

           A16: P[ 0 ] by A5;

           A17:

          now

            let n be Nat;

            assume

             A18: P[n];

            

             A19: ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

            n in omega by ORDINAL1:def 12;

            then (f() . ( succ n)) = phi(a) by A6, A18;

            hence P[(n + 1)] by A14, A19;

          end;

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

          then P[a];

          hence thesis;

        end;

        ( rng f()) = {a()}

        proof

          thus ( rng f()) c= {a()}

          proof

            let x be object;

            assume x in ( rng f());

            then

            consider a be object such that

             A20: a in ( dom f()) & x = (f() . a) by FUNCT_1:def 3;

            x = a() by A15, A20, A7;

            hence thesis by TARSKI:def 1;

          end;

          thus thesis by A8, ZFMISC_1: 31;

        end;

        then ( Union f()) = a() by ZFMISC_1: 25;

        hence phi(Union) = ( Union f()) & for b st a() c= b & b in U() & phi(b) = b holds ( Union f()) c= b by A14;

      end;

        suppose

         A21: a() in phi(a);

        deffunc F( Ordinal, Ordinal) = phi($2);

        deffunc G( Ordinal, Sequence) = {} ;

         A22:

        now

          let a such that

           A23: ( succ a) in omega ;

          a in ( succ a) by ORDINAL1: 6;

          hence (phi . ( succ a)) = F(a,.) by A6, A23, ORDINAL1: 10;

        end;

        

         A24: for a st a in omega holds a() c= (phi . a) & (phi . a) in (phi . ( succ a))

        proof

          let a;

          assume a in omega ;

          then

          reconsider a as Element of omega ;

          defpred N[ Nat] means a() c= (phi . $1) & (phi . $1) in (phi . ( succ ( Segm $1)));

          

           A25: N[ 0 ] by A21, A5, A6;

           A26:

          now

            let n be Nat;

            assume

             A27: N[n];

            

             A28: ( Segm (n + 1)) = ( succ ( Segm n)) & ( Segm ((n + 1) + 1)) = ( succ ( Segm (n + 1))) & (n + 1) in omega & ((n + 1) + 1) in omega by NAT_1: 38;

            then (phi . (n + 1)) = phi(.) & (phi . ((n + 1) + 1)) = phi(.) by A22;

            then (phi . n) c= (phi . (n + 1)) & (phi . (n + 1)) in (phi . ((n + 1) + 1)) by A3, A9, A27, A28;

            hence N[(n + 1)] by A27, XBOOLE_1: 1, A28;

          end;

          for n be Nat holds N[n] from NAT_1:sch 2( A25, A26);

          then N[a];

          hence thesis;

        end;

        deffunc phi( Ordinal) = phi($1);

        consider fi be Ordinal-Sequence such that

         A29: ( dom fi) = ( Union phi) & for a st a in ( Union phi) holds (fi . a) = phi(a) from ORDINAL2:sch 3;

        1 = ( succ 0 );

        then (f() . 1) = phi(a) by A5, A6;

        then phi(a) in ( rng phi) by A7, FUNCT_1:def 3;

        then

         A30: phi(a) c= ( Union phi) by ZFMISC_1: 74;

        

         A31: ( Union phi) in U() by A1, Th41;

        now

          let c;

          assume c in ( Union phi);

          then

          consider x be object such that

           A32: x in ( dom phi) & c in (phi . x) by CARD_5: 2;

          reconsider x as Element of omega by A32, FUNCT_2:def 1;

          ( succ c) c= (phi . x) & (phi . x) in (phi . ( succ x)) by A24, A32, ORDINAL1: 21;

          then ( succ c) in (phi . ( succ x)) & ( succ x) in omega by ORDINAL1: 12, ORDINAL1:def 12;

          hence ( succ c) in ( Union phi) by A7, CARD_5: 2;

        end;

        then

         A33: ( Union phi) is limit_ordinal by ORDINAL1: 28;

        then

         A34: phi(Union) is_limes_of fi by A4, A21, A29, A30, A31;

        fi is increasing

        proof

          let a, b;

          assume

           A35: a in b & b in ( dom fi);

          then (fi . a) = phi(a) & (fi . b) = phi(b) & b in U() by A31, A29, ORDINAL1: 10;

          hence thesis by A3, A35;

        end;

        

        then

         A36: ( sup fi) = ( lim fi) by A21, A29, A30, A33, ORDINAL4: 8

        .= phi(Union) by A34, ORDINAL2:def 10;

        thus phi(Union) c= ( Union phi)

        proof

          let x be Ordinal;

          assume

           A37: x in phi(Union);

          reconsider A = x as Ordinal;

          consider b such that

           A38: b in ( rng fi) & A c= b by A36, A37, ORDINAL2: 21;

          consider y be object such that

           A39: y in ( dom fi) & b = (fi . y) by A38, FUNCT_1:def 3;

          reconsider y as Ordinal by A39;

          consider z be object such that

           A40: z in ( dom phi) & y in (phi . z) by A29, A39, CARD_5: 2;

          reconsider z as Ordinal by A40;

          set c = (phi . z);

          ( succ z) in omega by A7, A40, ORDINAL1: 28;

          then

           A41: (phi . ( succ z)) = phi(c) & (phi . ( succ z)) in ( rng phi) & b = phi(y) by A7, A22, A29, A39, FUNCT_1:def 3;

          b in phi(c) & phi(c) c= ( Union phi) by A41, A3, A40, ZFMISC_1: 74;

          hence thesis by A38, ORDINAL1: 12;

        end;

        thus ( Union f()) c= phi(Union) by A9, A1, Th41;

        let b;

        assume

         A42: a() c= b & b in U() & phi(b) = b;

        ( rng f()) c= b

        proof

          let x be object;

          assume x in ( rng f());

          then

          consider a be object such that

           A43: a in ( dom f()) & x = (f() . a) by FUNCT_1:def 3;

          reconsider a as Element of omega by A43, FUNCT_2:def 1;

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

          a() <> b by A21, A42;

          then a() c< b by A42;

          then

           A44: P[ 0 ] by A5, ORDINAL1: 11;

           A45:

          now

            let n be Nat;

            assume P[n];

            then phi(.) in b & n in omega by A3, A42, ORDINAL1:def 12;

            then

             A46: (f() . ( succ n)) in b by A6;

            ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

            hence P[(n + 1)] by A46;

          end;

          for n be Nat holds P[n] from NAT_1:sch 2( A44, A45);

          then P[a];

          hence thesis by A43;

        end;

        then ( Union f()) c= ( union b) & ( union b) c= b by ORDINAL2: 5, ZFMISC_1: 77;

        hence ( Union f()) c= b;

      end;

    end;

    scheme :: ORDINAL6:sch2

    CriticalNumber3 { U() -> Universe , a() -> Ordinal of U() , phi( Ordinal) -> Ordinal } :

ex a be Ordinal of U() st a() in a & phi(a) = a

      provided

       A1: omega in U()

       and

       A2: for a st a in U() holds phi(a) in U()

       and

       A3: for a, b st a in b & b in U() holds phi(a) in phi(b)

       and

       A4: for a be Ordinal of U() st a is non empty limit_ordinal holds for phi be Ordinal-Sequence st ( dom phi) = a & for b st b in a holds (phi . b) = phi(b) holds phi(a) is_limes_of phi;

      assume

       A5: not thesis;

      deffunc F( Ordinal, Ordinal) = phi($2);

      deffunc G( Ordinal, Sequence) = {} ;

      consider phi be Ordinal-Sequence such that

       A6: ( dom phi) = omega and

       A7: 0 in omega implies (phi . 0 ) = ( succ a()) and

       A8: for a st ( succ a) in omega holds (phi . ( succ a)) = F(a,.) and for a st a in omega & a <> 0 & a is limit_ordinal holds (phi . a) = G(a,|) from ORDINAL2:sch 11;

      

       A9: ( rng phi) c= ( On U())

      proof

        let y be object;

        assume y in ( rng phi);

        then

        consider x be object such that

         A10: x in ( dom phi) & y = (phi . x) by FUNCT_1:def 3;

        reconsider x as Element of NAT by A6, A10;

        defpred P[ Nat] means (phi . $1) in ( On U());

        

         A11: P[ 0 ] by A7, ORDINAL1:def 9;

        

         A12: P[n] implies P[(n + 1)]

        proof

          assume P[n];

          then

           A13: (phi . n) in U() by ORDINAL1:def 9;

          

           A14: ( Segm (n + 1)) = ( succ ( Segm n)) by NAT_1: 38;

          (phi . (n + 1)) = phi(.) & phi(.) in U() by A8, A14, A13, A2;

          hence P[(n + 1)] by ORDINAL1:def 9;

        end;

         P[n] from NAT_1:sch 2( A11, A12);

        then P[x];

        hence thesis by A10;

      end;

      then

      reconsider phi as Ordinal-Sequence of omega , U() by A6, FUNCT_2: 2;

       A15:

      now

        defpred P[ Ordinal] means $1 in U() & $1 c/= phi($1);

        assume

         A16: ex a st P[a];

        consider a such that

         A17: P[a] and

         A18: for b st P[b] holds a c= b from ORDINAL1:sch 1( A16);

        phi(phi) in phi(a) by A3, A17, ORDINAL1: 16;

        then phi(a) c/= phi(phi) by ORDINAL1: 5;

        hence contradiction by A17, A18, A2;

      end;

       A19:

      now

        let a;

        assume a() in a & a in U();

        then a c= phi(a) & a <> phi(a) by A5, A15;

        then a c< phi(a);

        hence a in phi(a) by ORDINAL1: 11;

      end;

      

       A20: for a st a in omega holds a() in (phi . a)

      proof

        let a;

        assume a in omega ;

        then

        reconsider a as Element of omega ;

        defpred N[ Nat] means a() in (phi . $1);

        

         A21: N[ 0 ] by A7, ORDINAL1: 6;

         A22:

        now

          let n be Nat;

          assume

           A23: N[n];

          ( Segm (n + 1)) = ( succ ( Segm n)) & (n + 1) in omega by NAT_1: 38;

          then (phi . (n + 1)) = phi(.) by A8;

          then (phi . n) in (phi . (n + 1)) by A23, A19;

          hence N[(n + 1)] by A23, ORDINAL1: 10;

        end;

        for n be Nat holds N[n] from NAT_1:sch 2( A21, A22);

        then N[a];

        hence thesis;

      end;

      

       A24: phi is increasing

      proof

        let a, b;

        assume

         A25: a in b & b in ( dom phi);

        then

         A26: ex c st b = (a +^ c) & c <> {} by ORDINAL3: 28;

        defpred R[ Ordinal] means (a +^ $1) in omega & $1 <> {} implies (phi . a) in (phi . (a +^ $1));

        

         A27: R[ 0 ];

        

         A28: for c st R[c] holds R[( succ c)]

        proof

          let c such that

           A29: (a +^ c) in omega & c <> {} implies (phi . a) in (phi . (a +^ c)) and

           A30: (a +^ ( succ c)) in omega & ( succ c) <> {} ;

          

           A31: (a +^ c) in ( succ (a +^ c)) & (a +^ ( succ c)) = ( succ (a +^ c)) by ORDINAL1: 6, ORDINAL2: 28;

          reconsider d = (phi . (a +^ c)) as Ordinal;

          (a +^ c) in omega by A30, A31, ORDINAL1: 10;

          then (phi . (a +^ ( succ c))) = phi(d) & d in phi(d) & (a +^ {} qua Ordinal) = a by A8, A19, A30, A31, A20, ORDINAL2: 27;

          hence thesis by A29, A30, A31, ORDINAL1: 10;

        end;

        

         A32: for b st b <> 0 & b is limit_ordinal & for c st c in b holds R[c] holds R[b]

        proof

          let b such that

           A33: b <> 0 & b is limit_ordinal and for c st c in b holds (a +^ c) in omega & c <> {} implies (phi . a) in (phi . (a +^ c)) and

           A34: (a +^ b) in omega & b <> {} ;

          (a +^ b) is limit_ordinal & {} in (a +^ b) by A33, ORDINAL3: 8, ORDINAL3: 29;

          hence thesis by A34;

        end;

        for c holds R[c] from ORDINAL2:sch 1( A27, A28, A32);

        hence thesis by A6, A25, A26;

      end;

      

       A35: ( sup phi) in U() by A1, Th42;

      deffunc phi( Ordinal) = phi($1);

      consider fi be Ordinal-Sequence such that

       A36: ( dom fi) = ( sup phi) & for a st a in ( sup phi) holds (fi . a) = phi(a) from ORDINAL2:sch 3;

      ( succ a()) in ( rng phi) & ( sup ( rng phi)) = ( sup phi) by A6, A7, FUNCT_1:def 3;

      then

       A37: ( sup phi) <> {} & ( sup phi) is limit_ordinal by A6, A24, ORDINAL2: 19, ORDINAL4: 16;

      then

       A38: phi(sup) is_limes_of fi by A35, A4, A36;

      fi is increasing

      proof

        let a, b;

        assume

         A39: a in b & b in ( dom fi);

        then (fi . a) = phi(a) & (fi . b) = phi(b) & b in U() by A35, A36, ORDINAL1: 10;

        hence thesis by A3, A39;

      end;

      

      then

       A40: ( sup fi) = ( lim fi) by A36, A37, ORDINAL4: 8

      .= phi(sup) by A38, ORDINAL2:def 10;

      

       A41: ( sup fi) c= ( sup phi)

      proof

        let x be Ordinal;

        assume

         A42: x in ( sup fi);

        reconsider A = x as Ordinal;

        consider b such that

         A43: b in ( rng fi) & A c= b by A42, ORDINAL2: 21;

        consider y be object such that

         A44: y in ( dom fi) & b = (fi . y) by A43, FUNCT_1:def 3;

        reconsider y as Ordinal by A44;

        consider c such that

         A45: c in ( rng phi) & y c= c by A36, A44, ORDINAL2: 21;

        

         A46: c in U() by A9, A45, ORDINAL1:def 9;

        consider z be object such that

         A47: z in ( dom phi) & c = (phi . z) by A45, FUNCT_1:def 3;

        reconsider z as Ordinal by A47;

        ( succ z) in omega by A6, A47, ORDINAL1: 28;

        then

         A48: (phi . ( succ z)) = phi(c) & (phi . ( succ z)) in ( rng phi) & b = phi(y) by A6, A8, A36, A44, A47, FUNCT_1:def 3;

        y c< c iff y <> c & y c= c;

        then phi(y) in phi(c) or y = c by A46, A3, A45, ORDINAL1: 11;

        then b c= phi(c) & phi(c) in ( sup phi) by A48, ORDINAL1:def 2, ORDINAL2: 19;

        then b in ( sup phi) by ORDINAL1: 12;

        hence thesis by A43, ORDINAL1: 12;

      end;

      (phi . 0 ) in ( rng phi) by A6, FUNCT_1:def 3;

      then a() in (phi . 0 ) & (phi . 0 ) in ( sup phi) by A20, ORDINAL2: 19;

      then a() in ( sup phi) by ORDINAL1: 10;

      hence contradiction by A35, A19, A40, A41, ORDINAL1: 5;

    end;

    reserve F,phi for normal Ordinal-Sequence of W;

    theorem :: ORDINAL6:43

    

     Th43: omega in W & b in W implies ex a st b in a & a is_a_fixpoint_of phi

    proof

      assume that

       A1: omega in W and

       A2: b in W;

      reconsider b1 = b as Ordinal of W by A2;

      

       A3: ( dom phi) = ( On W) by FUNCT_2:def 1;

      deffunc phi( set) = (phi . $1);

      

       A4: for a st a in W holds phi(a) in W;

      

       A5: for a, b st a in b & b in W holds phi(a) in phi(b)

      proof

        let a, b;

        b in W implies b in ( dom phi) by A3, ORDINAL1:def 9;

        hence thesis by ORDINAL2:def 12;

      end;

      

       A6: for a be Ordinal of W st a is non empty limit_ordinal holds for f be Ordinal-Sequence st ( dom f) = a & for b st b in a holds (f . b) = phi(b) holds phi(a) is_limes_of f

      proof

        let a be Ordinal of W;

        assume

         A7: a is non empty limit_ordinal;

        let f be Ordinal-Sequence such that

         A8: ( dom f) = a and

         A9: for b st b in a holds (f . b) = phi(b);

        

         A10: a in ( dom phi) by A3, ORDINAL1:def 9;

        then a c= ( dom phi) by ORDINAL1:def 2;

        then

         A11: ( dom (phi | a)) = a by RELAT_1: 62;

        now

          let x be object;

          assume

           A12: x in a;

          reconsider xx = x as set by TARSKI: 1;

          

          thus ((phi | a) . x) = phi(xx) by A12, FUNCT_1: 49

          .= (f . x) by A12, A9;

        end;

        then f = (phi | a) by A8, A11;

        hence phi(a) is_limes_of f by A7, A10, ORDINAL2:def 13;

      end;

      consider a be Ordinal of W such that

       A13: b1 in a & phi(a) = a from CriticalNumber3( A1, A4, A5, A6);

      take a;

      thus b in a & a in ( dom phi) & a = (phi . a) by A3, A13, ORDINAL1:def 9;

    end;

    theorem :: ORDINAL6:44

    

     Th44: omega in W implies ( criticals F) is Ordinal-Sequence of W

    proof

      assume

       A1: omega in W;

      set G = ( criticals F);

      

       A2: ( dom F) = ( On W) & ( rng F) c= ( On W) by FUNCT_2:def 1, RELAT_1:def 19;

      

       A3: ( rng G) c= ( rng F) by Th30;

      then

       A4: ( rng G) c= ( On W) by A2;

      ( dom G) = ( On W)

      proof

        thus ( dom G) c= ( On W) by A2, Th32;

        let a;

        assume a in ( On W);

        then

         A5: a in W by ORDINAL1:def 9;

        defpred P[ Ordinal] means $1 in W implies $1 in ( dom G);

        consider a0 be Ordinal such that

         A6: ( 0-element_of W) in a0 & a0 is_a_fixpoint_of F by A1, Th43;

        consider a1 be Ordinal such that

         A7: a1 in ( dom G) & a0 = (G . a1) by A6, Th33;

        

         A8: P[ 0 ] by A7, ORDINAL1: 12, XBOOLE_1: 2;

        

         A9: for a st P[a] holds P[( succ a)]

        proof

          let a;

          assume

           A10: P[a] & ( succ a) in W;

          

           A11: a c= ( succ a) by ORDINAL3: 1;

          then (G . a) in ( rng G) by A10, CLASSES1:def 1, FUNCT_1:def 3;

          then (G . a) in W by A4, ORDINAL1:def 9;

          then

          consider b such that

           A12: (G . a) in b & b is_a_fixpoint_of F by A1, Th43;

          consider c such that

           A13: c in ( dom G) & b = (G . c) by A12, Th33;

          a in c by A10, A11, A12, A13, Th23, CLASSES1:def 1;

          then ( succ a) c= c by ORDINAL1: 21;

          hence thesis by A13, ORDINAL1: 12;

        end;

        

         A14: for a st a <> 0 & a is limit_ordinal & for b st b in a holds P[b] holds P[a]

        proof

          let a such that

           A15: a <> 0 & a is limit_ordinal and

           A16: for b st b in a holds P[b] and

           A17: a in W;

          set X = (G .: a);

          ( card X) c= ( card a) & ( card a) c= a by CARD_1: 8, CARD_1: 67;

          then ( card X) c= a;

          then ( card X) in W by A17, CLASSES1:def 1;

          then ( card X) in ( On W) by ORDINAL1:def 9;

          then

           A18: ( card X) in ( card W) by CLASSES2: 9;

          

           A19: X c= ( rng G) by RELAT_1: 111;

          then

           A20: X c= ( On W) by A4;

          reconsider u = ( union X) as Ordinal by A19, A4, ORDINAL3: 4, XBOOLE_1: 1;

          ( On W) c= W by ORDINAL2: 7;

          then X c= W by A20;

          then X in W by A18, CLASSES1: 1;

          then u in W by CLASSES2: 59;

          then

          consider b such that

           A21: u in b & b is_a_fixpoint_of F by A1, Th43;

          

           A22: a c= ( dom G)

          proof

            let c;

            assume

             A23: c in a;

            then c in W by A17, ORDINAL1: 10;

            hence thesis by A16, A23;

          end;

          now

            let x;

            assume x in a;

            then (G . x) in X by A22, FUNCT_1:def 6;

            then (G . x) is Ordinal & (G . x) c= u by ZFMISC_1: 74;

            hence (G . x) in b by A21, ORDINAL1: 12;

          end;

          hence thesis by A15, A22, A21, Th38;

        end;

         P[b] from ORDINAL2:sch 1( A8, A9, A14);

        hence thesis by A5;

      end;

      hence thesis by A3, A2, FUNCT_2: 2, XBOOLE_1: 1;

    end;

    theorem :: ORDINAL6:45

    

     Th45: f is normal implies for a st a in ( dom ( criticals f)) holds (f . a) c= (( criticals f) . a)

    proof

      assume

       A1: f is normal;

      set g = ( criticals f);

      

       A2: ( dom g) c= ( dom f) by Th32;

      defpred P[ Ordinal] means $1 in ( dom g) implies (f . $1) c= (g . $1);

      

       A3: P[ 0 ]

      proof

        assume 0 in ( dom g);

        then (g . 0 ) is_a_fixpoint_of f by Th29;

        then (f . (g . 0 )) = (g . 0 ) & (g . 0 ) in ( dom f);

        hence thesis by A1, ORDINAL4: 9, XBOOLE_1: 2;

      end;

      

       A4: P[a] implies P[( succ a)]

      proof

        assume that P[a] and

         A5: ( succ a) in ( dom g);

        (g . ( succ a)) is_a_fixpoint_of f by A5, Th29;

        then (g . ( succ a)) in ( dom f) & (f . (g . ( succ a))) = (g . ( succ a));

        hence (f . ( succ a)) c= (g . ( succ a)) by A1, A5, ORDINAL4: 9, ORDINAL4: 10;

      end;

      

       A6: for a st a <> 0 & a is limit_ordinal & for b st b in a holds P[b] holds P[a]

      proof

        let a such that

         A7: a <> 0 & a is limit_ordinal and

         A8: for b st b in a holds P[b] and

         A9: a in ( dom g);

        (f . a) is_limes_of (f | a) & (g . a) is_limes_of (g | a) by A1, A2, A7, A9, ORDINAL2:def 13;

        then

         A10: (f . a) = ( lim (f | a)) & (g . a) = ( lim (g | a)) by ORDINAL2:def 10;

        

         A11: (f | a) is increasing & (g | a) is increasing by A1, ORDINAL4: 15;

        

         A12: a c= ( dom f) & a c= ( dom g) by A2, A9, ORDINAL1:def 2;

        then

         A13: ( dom (f | a)) = a & ( dom (g | a)) = a by RELAT_1: 62;

        then ( Union (f | a)) is_limes_of (f | a) & ( Union (g | a)) is_limes_of (g | a) by A7, A11, ORDINAL5: 6;

        then

         A14: (f . a) = ( Union (f | a)) & (g . a) = ( Union (g | a)) by A10, ORDINAL2:def 10;

        let b;

        assume b in (f . a);

        then

        consider x be object such that

         A15: x in a & b in ((f | a) . x) by A13, A14, CARD_5: 2;

        ((f | a) . x) = (f . x) & ((g | a) . x) = (g . x) & (f . x) c= (g . x) by A12, A8, A15, FUNCT_1: 49;

        hence b in (g . a) by A15, A13, A14, CARD_5: 2;

      end;

      thus P[a] from ORDINAL2:sch 1( A3, A4, A6);

    end;

    begin

    definition

      let U;

      let a,b be Ordinal of U;

      :: original: exp

      redefine

      func exp (a,b) -> Ordinal of U ;

      coherence

      proof

        per cases by ORDINAL3: 8;

          suppose a = 0 & b = 0 ;

          then ( exp (a,b)) = ( 1-element_of U) by ORDINAL2: 43;

          hence thesis;

        end;

          suppose a = 0 & b <> 0 ;

          hence thesis;

        end;

          suppose

           A1: 0 in a;

          defpred P[ Ordinal] means $1 in U implies ( exp (a,$1)) in U;

          ( exp (a, 0 )) = ( succ 0 ) by ORDINAL2: 43;

          then

           A2: P[ 0 ] by CLASSES2: 5;

          

           A3: for b holds P[b] implies P[( succ b)]

          proof

            let b such that

             A4: P[b] and

             A5: ( succ b) in U;

            b in ( succ b) by ORDINAL1: 6;

            then

            reconsider b as Ordinal of U by A5, ORDINAL1: 10;

            reconsider ab = ( exp (a,b)) as Ordinal of U by A4;

            ( exp (a,( succ b))) = (a *^ ab) by ORDINAL2: 44;

            hence thesis;

          end;

          

           A6: for b st b <> 0 & b is limit_ordinal & for c st c in b holds P[c] holds P[b]

          proof

            let b such that

             A7: b <> 0 & b is limit_ordinal and

             A8: for c st c in b holds P[c] and

             A9: b in U;

            deffunc F( Ordinal) = ( exp (a,$1));

            consider f such that

             A10: ( dom f) = b & for c st c in b holds (f . c) = F(c) from ORDINAL2:sch 3;

            ( rng f) c= ( On U)

            proof

              let x be object;

              assume x in ( rng f);

              then

              consider y be object such that

               A11: y in b & x = (f . y) by A10, FUNCT_1:def 3;

              reconsider y as Ordinal by A11;

               P[y] & y in U & x = F(y) by A9, A8, A10, A11, ORDINAL1: 10;

              hence thesis by ORDINAL1:def 9;

            end;

            then

            reconsider f as Ordinal-Sequence of b, U by A10, FUNCT_2: 2;

            

             A12: ( exp (a,b)) = ( lim f) by A7, A10, ORDINAL2: 45;

            f is non-decreasing by A1, A10, ORDINAL5: 8;

            then ( Union f) is_limes_of f by A7, ORDINAL5: 6;

            then ( exp (a,b)) = ( Union f) by A12, ORDINAL2:def 10;

            hence thesis by A9, Th41;

          end;

          for b holds P[b] from ORDINAL2:sch 1( A2, A3, A6);

          hence thesis;

        end;

      end;

    end

    definition

      let U, a;

      :: ORDINAL6:def8

      func U exp a -> Ordinal-Sequence of U means

      : Def8: for b be Ordinal of U holds (it . b) = ( exp (a,b));

      existence

      proof

        reconsider a as Ordinal of U by A1;

        deffunc F( Ordinal of U) = ( exp (a,$1));

        ex f be Ordinal-Sequence of U st for b be Ordinal of U holds (f . b) = F(b) from ORDINAL4:sch 2;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Ordinal-Sequence of U such that

         A2: for b be Ordinal of U holds (f1 . b) = ( exp (a,b)) and

         A3: for b be Ordinal of U holds (f2 . b) = ( exp (a,b));

        now

          let x be Element of ( On U);

          x in U by ORDINAL1:def 9;

          then (f1 . x) = ( exp (a,x)) & (f2 . x) = ( exp (a,x)) by A2, A3;

          hence (f1 . x) = (f2 . x);

        end;

        hence thesis by FUNCT_2: 63;

      end;

    end

    registration

      cluster omega -> non trivial;

      coherence ;

    end

    registration

      let U;

      cluster non trivial finite for Ordinal of U;

      existence

      proof

        ( succ ( 1-element_of U)) is non trivial by NAT_2:def 1;

        hence thesis;

      end;

    end

    registration

      cluster non trivial finite for Ordinal;

      existence

      proof

        2 is non trivial by NAT_2:def 1;

        hence thesis;

      end;

    end

    registration

      let U;

      let a be non trivial Ordinal of U;

      cluster (U exp a) -> normal;

      coherence

      proof

        set f = (U exp a);

        

         A1: ( dom f) = ( On U) by FUNCT_2:def 1;

        

         A2: 0 in a by ORDINAL3: 8;

        ( succ 0 ) c= a;

        then 1 c< a;

        then

         A3: 1 in a by ORDINAL1: 11;

         A4:

        now

          let b;

          assume b in ( dom f);

          then b in U by A1, ORDINAL1:def 9;

          hence (f . b) = ( exp (a,b)) by Def8;

        end;

        hence f is increasing by A3, ORDINAL5: 10;

        let b, c;

        assume

         A5: b in ( dom f) & b <> 0 & b is limit_ordinal & c = (f . b);

        then b c= ( dom f) by ORDINAL1:def 2;

        then

         A6: ( dom (f | b)) = b by RELAT_1: 62;

        

         A7: (f | b) is increasing by A4, A3, ORDINAL4: 15, ORDINAL5: 10;

        

         A8: b in U by A1, A5, ORDINAL1:def 9;

        then

         A9: (f . b) = ( exp (a,b)) by Def8;

        (f . b) = ( Union (f | b))

        proof

          thus (f . b) c= ( Union (f | b))

          proof

            let c;

            assume c in (f . b);

            then

            consider d such that

             A10: d in b & c in ( exp (a,d)) by A2, A5, A9, ORDINAL5: 11;

            d in U by A8, A10, ORDINAL1: 10;

            

            then ( exp (a,d)) = (f . d) by Def8

            .= ((f | b) . d) by A10, FUNCT_1: 49;

            hence c in ( Union (f | b)) by A6, A10, CARD_5: 2;

          end;

          let c;

          assume c in ( Union (f | b));

          then

          consider x be object such that

           A11: x in b & c in ((f | b) . x) by A6, CARD_5: 2;

          reconsider x as Ordinal by A11;

          x in U by A8, A11, ORDINAL1: 10;

          

          then ( exp (a,x)) = (f . x) by Def8

          .= ((f | b) . x) by A11, FUNCT_1: 49;

          hence thesis by A2, A11, A5, A9, ORDINAL5: 11;

        end;

        hence thesis by A5, A7, A6, ORDINAL5: 6;

      end;

    end

    definition

      let g be Function;

      :: ORDINAL6:def9

      attr g is Ordinal-Sequence-valued means

      : Def9: x in ( rng g) implies x is Ordinal-Sequence;

    end

    registration

      let f be Ordinal-Sequence;

      cluster <%f%> -> Ordinal-Sequence-valued;

      coherence

      proof

        let x;

        assume x in ( rng <%f%>);

        then x in {f} by AFINSQ_1: 33;

        hence thesis by TARSKI:def 1;

      end;

    end

    definition

      let f be Function;

      :: ORDINAL6:def10

      attr f is with_the_same_dom means ( rng f) is with_common_domain;

    end

    registration

      let f be Function;

      cluster {f} -> with_common_domain;

      coherence

      proof

        let g,h be Function;

        assume g in {f} & h in {f};

        then g = f & h = f by TARSKI:def 1;

        hence thesis;

      end;

    end

    registration

      let f be Function;

      cluster <%f%> -> with_the_same_dom;

      coherence

      proof

        ( rng <%f%>) = {f} by AFINSQ_1: 33;

        hence ( rng <%f%>) is with_common_domain;

      end;

    end

    registration

      cluster non empty Ordinal-Sequence-valued with_the_same_dom for Sequence;

      existence

      proof

        set f = the Ordinal-Sequence;

        take <%f%>;

        thus thesis;

      end;

    end

    registration

      let g be Ordinal-Sequence-valued Function;

      let x be object;

      cluster (g . x) -> Relation-like Function-like;

      coherence

      proof

        per cases by FUNCT_1:def 2;

          suppose (g . x) = {} ;

          hence thesis;

        end;

          suppose x in ( dom g);

          then (g . x) in ( rng g) by FUNCT_1:def 3;

          hence thesis by Def9;

        end;

      end;

    end

    registration

      let g be Ordinal-Sequence-valued Function;

      let x;

      cluster (g . x) -> Sequence-like Ordinal-yielding;

      coherence

      proof

        per cases by FUNCT_1:def 2;

          suppose (g . x) = {} ;

          hence thesis;

        end;

          suppose x in ( dom g);

          then (g . x) in ( rng g) by FUNCT_1:def 3;

          hence thesis by Def9;

        end;

      end;

    end

    registration

      let g be Sequence;

      let a;

      cluster (g | a) -> Sequence-like;

      coherence ;

    end

    registration

      let g be Ordinal-Sequence-valued Function;

      let X;

      cluster (g | X) -> Ordinal-Sequence-valued;

      coherence

      proof

        let x;

        ( rng (g | X)) c= ( rng g) by RELAT_1: 70;

        hence thesis by Def9;

      end;

    end

    registration

      let a, b;

      cluster -> Ordinal-yielding Sequence-like for Function of a, b;

      coherence

      proof

        let f be Function of a, b;

        ( rng f) c= b by RELAT_1:def 19;

        hence ex c st ( rng f) c= c;

        b = {} implies f = {} ;

        hence ( dom f) is epsilon-transitive epsilon-connected by FUNCT_2:def 1;

      end;

    end

    definition

      let g be Ordinal-Sequence-valued Sequence;

      :: ORDINAL6:def11

      func criticals g -> Ordinal-Sequence equals ( numbering { a where a be Element of ( dom (g . 0 )) : a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f });

      coherence ;

    end

    reserve g for Ordinal-Sequence-valued Sequence;

    theorem :: ORDINAL6:46

    

     Th46: for g holds { a where a be Element of ( dom (g . 0 )) : a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f } is ordinal-membered

    proof

      let g;

      now

        let x;

        assume x in { a where a be Element of ( dom (g . 0 )) : a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f };

        then ex a be Element of ( dom (g . 0 )) st x = a & a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f;

        hence x is ordinal;

      end;

      hence thesis by Th1;

    end;

    theorem :: ORDINAL6:47

    

     Th47: a in ( dom g) & b in ( dom ( criticals g)) implies (( criticals g) . b) is_a_fixpoint_of (g . a)

    proof

      assume that

       A1: a in ( dom g) and

       A2: b in ( dom ( criticals g));

      set h = ( criticals g);

      set X = { c where c be Element of ( dom (g . 0 )) : c in ( dom (g . 0 )) & for f st f in ( rng g) holds c is_a_fixpoint_of f };

      X is ordinal-membered by Th46;

      then ( rng h) = X by Th19;

      then (h . b) in X by A2, FUNCT_1:def 3;

      then

      consider c be Element of ( dom (g . 0 )) such that

       A3: (h . b) = c & c in ( dom (g . 0 )) & for f st f in ( rng g) holds c is_a_fixpoint_of f;

      (g . a) in ( rng g) by A1, FUNCT_1:def 3;

      hence (( criticals g) . b) is_a_fixpoint_of (g . a) by A3;

    end;

    theorem :: ORDINAL6:48

    x in ( dom ( criticals g)) implies x c= (( criticals g) . x) by ORDINAL4: 10;

    theorem :: ORDINAL6:49

    

     Th49: f in ( rng g) implies ( dom ( criticals g)) c= ( dom f)

    proof

      assume

       A1: f in ( rng g);

      let x be Ordinal;

      set X = { a where a be Element of ( dom (g . 0 )) : a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f };

      assume

       A2: x in ( dom ( criticals g));

      then (( criticals g) . x) in ( rng ( criticals g)) by FUNCT_1:def 3;

      then (( criticals g) . x) in ( On X) & X is ordinal-membered by Th18, Th46;

      then (( criticals g) . x) in X by Th2;

      then

      consider a be Element of ( dom (g . 0 )) such that

       A3: (( criticals g) . x) = a & a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f;

      a is_a_fixpoint_of f by A1, A3;

      then x c= a & a in ( dom f) & a = (f . a) by A2, A3, ORDINAL4: 10;

      hence thesis by ORDINAL1: 12;

    end;

    theorem :: ORDINAL6:50

    

     Th50: ( dom g) <> {} & (for c st c in ( dom g) holds b is_a_fixpoint_of (g . c)) implies ex a st a in ( dom ( criticals g)) & b = (( criticals g) . a)

    proof

      reconsider X = { a where a be Element of ( dom (g . 0 )) : a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f } as ordinal-membered set by Th46;

      assume that

       A1: ( dom g) <> {} and

       A2: for c st c in ( dom g) holds b is_a_fixpoint_of (g . c);

      b is_a_fixpoint_of (g . 0 ) by A2, A1, ORDINAL3: 8;

      then

       A3: b in ( dom (g . 0 ));

      now

        let f;

        assume f in ( rng g);

        then ex x be object st x in ( dom g) & f = (g . x) by FUNCT_1:def 3;

        hence b is_a_fixpoint_of f by A2;

      end;

      then b in X by A3;

      then b in ( rng ( criticals g)) by Th19;

      then ex x be object st x in ( dom ( criticals g)) & b = (( criticals g) . x) by FUNCT_1:def 3;

      hence thesis;

    end;

    theorem :: ORDINAL6:51

    ( dom g) <> {} & l c= ( dom ( criticals g)) & (for f st f in ( rng g) holds a is_a_fixpoint_of f) & (for x st x in l holds (( criticals g) . x) in a) implies l in ( dom ( criticals g))

    proof

      set h = ( criticals g);

      assume that

       A1: ( dom g) <> {} and

       A2: l c= ( dom h) and

       A3: for f st f in ( rng g) holds a is_a_fixpoint_of f and

       A4: for x st x in l holds (h . x) in a;

      now

        let c;

        assume c in ( dom g);

        then (g . c) in ( rng g) by FUNCT_1:def 3;

        hence a is_a_fixpoint_of (g . c) by A3;

      end;

      then

      consider b such that

       A5: b in ( dom h) & a = (h . b) by A1, Th50;

      l c= b

      proof

        let x be Ordinal;

        assume x in l;

        then x in ( dom h) & (h . x) in (h . b) by A2, A4, A5;

        hence x in b by A5, Th23;

      end;

      hence l in ( dom ( criticals g)) by A5, ORDINAL1: 12;

    end;

    theorem :: ORDINAL6:52

    

     Th52: for g st ( dom g) <> {} & for a st a in ( dom g) holds (g . a) is normal holds l in ( dom ( criticals g)) implies (( criticals g) . l) = ( Union (( criticals g) | l))

    proof

      let F be Ordinal-Sequence-valued Sequence such that

       A1: ( dom F) <> {} ;

      set g = ( criticals F);

      reconsider h = (g | l) as increasing Ordinal-Sequence by ORDINAL4: 15;

      set X = ( rng h);

      assume

       A2: (for a st a in ( dom F) holds (F . a) is normal) & l in ( dom g);

       A3:

      now

        let a;

        set f = (F . a);

        assume a in ( dom F);

        then (g . l) is_a_fixpoint_of (F . a) by A2, Th47;

        hence (g . l) in ( dom f) & (f . (g . l)) = (g . l);

      end;

      

       A4: l c= ( dom g) by A2, ORDINAL1:def 2;

      then

       A5: ( dom h) = l by RELAT_1: 62;

      

       A6: for a, x st a in ( dom F) & x in X holds x is_a_fixpoint_of (F . a)

      proof

        let a, x;

        assume

         A7: a in ( dom F) & x in X;

        then

        consider y be object such that

         A8: y in ( dom h) & x = (h . y) by FUNCT_1:def 3;

        x = (g . y) & y in ( dom g) by A4, A5, A8, FUNCT_1: 47;

        hence thesis by A7, Th47;

      end;

      reconsider u = ( union X) as Ordinal;

      

       A9: h <> {} by A5;

      now

        let x;

        assume x in X;

        then

        consider y be object such that

         A10: y in ( dom h) & x = (h . y) by FUNCT_1:def 3;

        x = (g . y) & y in ( dom g) by A4, A5, A10, FUNCT_1: 47;

        then x in (g . l) by A2, A5, A10, ORDINAL2:def 12;

        hence x c= (g . l) by ORDINAL1:def 2;

      end;

      then

       A11: u c= (g . l) by ZFMISC_1: 76;

      now

        let c;

        set f = (F . c);

        assume

         A12: c in ( dom F);

        then

         A13: (g . l) in ( dom f) by A3;

        then

         A14: u in ( dom f) by A11, ORDINAL1: 12;

        

         A15: f is normal by A2, A12;

        for x st x in X holds x is_a_fixpoint_of f by A6, A12;

        then u = (f . u) by A9, A13, A15, Th37, A11, ORDINAL1: 12;

        hence u is_a_fixpoint_of f by A14;

      end;

      then

      consider a such that

       A16: a in ( dom g) & u = (g . a) by A1, Th50;

      a = l

      proof

        thus a c= l by A2, A16, A11, Th22;

        let x be Ordinal;

        assume

         A17: x in l;

        then

         A18: ( succ x) in l by ORDINAL1: 28;

        then

         A19: (g . x) = (h . x) & (g . ( succ x)) = (h . ( succ x)) & (h . ( succ x)) in X by A5, A17, FUNCT_1: 47, FUNCT_1:def 3;

        x in ( succ x) by ORDINAL1: 6;

        then (h . x) in (h . ( succ x)) by A5, A18, ORDINAL2:def 12;

        then (g . x) in u by A19, TARSKI:def 4;

        then (g . a) c/= (g . x) & x in ( dom g) by A4, A16, A17, Th4;

        then a c/= x by A16, Th22;

        hence thesis by Th4;

      end;

      hence thesis by A16;

    end;

    theorem :: ORDINAL6:53

    

     Th53: for g st ( dom g) <> {} & for a st a in ( dom g) holds (g . a) is normal holds ( criticals g) is continuous

    proof

      let g;

      assume

       A1: ( dom g) <> {} ;

      assume

       A2: for a st a in ( dom g) holds (g . a) is normal;

      set f = ( criticals g);

      let a, b;

      reconsider h = (f | a) as increasing Ordinal-Sequence by ORDINAL4: 15;

      assume

       A3: a in ( dom f) & a <> 0 & a is limit_ordinal & b = (f . a);

      then

       A4: b = ( Union h) by A1, A2, Th52;

      a c= ( dom f) by A3, ORDINAL1:def 2;

      then ( dom h) = a by RELAT_1: 62;

      hence b is_limes_of (f | a) by A3, A4, ORDINAL5: 6;

    end;

    theorem :: ORDINAL6:54

    

     Th54: for g st ( dom g) <> {} & for a st a in ( dom g) holds (g . a) is normal holds for a, f st a in ( dom ( criticals g)) & f in ( rng g) holds (f . a) c= (( criticals g) . a)

    proof

      let F be Ordinal-Sequence-valued Sequence such that

       A1: ( dom F) <> {} and

       A2: for a st a in ( dom F) holds (F . a) is normal;

      let a, f such that

       A3: a in ( dom ( criticals F)) and

       A4: f in ( rng F);

      consider x be object such that

       A5: x in ( dom F) & f = (F . x) by A4, FUNCT_1:def 3;

      

       A6: f is normal by A5, A2;

      set g = ( criticals F);

      

       A7: ( dom g) c= ( dom f) by A4, Th49;

      defpred P[ Ordinal] means $1 in ( dom g) implies (f . $1) c= (g . $1);

      

       A8: P[ 0 ]

      proof

        assume 0 in ( dom g);

        then (g . 0 ) is_a_fixpoint_of f by A5, Th47;

        then (f . (g . 0 )) = (g . 0 ) & (g . 0 ) in ( dom f);

        hence thesis by A6, ORDINAL4: 9, XBOOLE_1: 2;

      end;

      

       A9: for a holds P[a] implies P[( succ a)]

      proof

        let a such that P[a] and

         A10: ( succ a) in ( dom g);

        (g . ( succ a)) is_a_fixpoint_of f by A5, A10, Th47;

        then (g . ( succ a)) in ( dom f) & (f . (g . ( succ a))) = (g . ( succ a));

        hence (f . ( succ a)) c= (g . ( succ a)) by A6, A10, ORDINAL4: 9, ORDINAL4: 10;

      end;

      

       A11: for a st a <> 0 & a is limit_ordinal & for b st b in a holds P[b] holds P[a]

      proof

        let a such that

         A12: a <> 0 & a is limit_ordinal and

         A13: for b st b in a holds P[b] and

         A14: a in ( dom g);

        g is continuous by A1, A2, Th53;

        then (f . a) is_limes_of (f | a) & (g . a) is_limes_of (g | a) by A6, A7, A12, A14, ORDINAL2:def 13;

        then

         A15: (f . a) = ( lim (f | a)) & (g . a) = ( lim (g | a)) by ORDINAL2:def 10;

        

         A16: (f | a) is increasing & (g | a) is increasing by A6, ORDINAL4: 15;

        

         A17: a c= ( dom f) & a c= ( dom g) by A7, A14, ORDINAL1:def 2;

        then

         A18: ( dom (f | a)) = a & ( dom (g | a)) = a by RELAT_1: 62;

        then ( Union (f | a)) is_limes_of (f | a) & ( Union (g | a)) is_limes_of (g | a) by A12, A16, ORDINAL5: 6;

        then

         A19: (f . a) = ( Union (f | a)) & (g . a) = ( Union (g | a)) by A15, ORDINAL2:def 10;

        let b;

        assume b in (f . a);

        then

        consider x be object such that

         A20: x in a & b in ((f | a) . x) by A18, A19, CARD_5: 2;

        ((f | a) . x) = (f . x) & ((g | a) . x) = (g . x) & (f . x) c= (g . x) by A17, A13, A20, FUNCT_1: 49;

        hence b in (g . a) by A20, A18, A19, CARD_5: 2;

      end;

      for a holds P[a] from ORDINAL2:sch 1( A8, A9, A11);

      hence thesis by A3;

    end;

    theorem :: ORDINAL6:55

    

     Th55: for g1,g2 be Ordinal-Sequence-valued Sequence st ( dom g1) = ( dom g2) & ( dom g1) <> {} & for a st a in ( dom g1) holds (g1 . a) c= (g2 . a) holds ( criticals g1) c= ( criticals g2)

    proof

      let g1,g2 be Ordinal-Sequence-valued Sequence;

      assume

       A1: ( dom g1) = ( dom g2);

      assume

       A2: ( dom g1) <> {} ;

      assume

       A3: for a st a in ( dom g1) holds (g1 . a) c= (g2 . a);

      set f1 = (g1 . 0 ), f2 = (g2 . 0 );

       0 in ( dom g1) by A2, ORDINAL3: 8;

      then f1 c= f2 & f1 in ( rng g1) & f2 in ( rng g2) by A1, A3, FUNCT_1:def 3;

      then

       A4: ( dom f1) c= ( dom f2) by GRFUNC_1: 2;

      set X = { a where a be Element of ( dom f1) : a in ( dom f1) & for f st f in ( rng g1) holds a is_a_fixpoint_of f };

      set Z = { a where a be Element of ( dom f2) : a in ( dom f2) & for f st f in ( rng g2) holds a is_a_fixpoint_of f };

      reconsider X, Z as ordinal-membered set by Th46;

      set Y = (Z \ X);

       A5:

      now

        let x, y;

        assume x in X;

        then

        consider a be Element of ( dom f1) such that

         A6: x = a & a in ( dom f1) & for f st f in ( rng g1) holds a is_a_fixpoint_of f;

        assume y in Y;

        then

         A7: y in Z & not y in X by XBOOLE_0:def 5;

        then

        consider b be Element of ( dom f2) such that

         A8: y = b & b in ( dom f2) & for f st f in ( rng g2) holds b is_a_fixpoint_of f;

        assume not x in y;

        then

         A9: b c= a by A6, A8, ORDINAL1: 16;

        then

         A10: b in ( dom f1) by A6, ORDINAL1: 12;

        now

          let f;

          assume

           A11: f in ( rng g1);

          then

          consider z be object such that

           A12: z in ( dom g1) & f = (g1 . z) by FUNCT_1:def 3;

          reconsider z as set by TARSKI: 1;

          

           A13: f c= (g2 . z) by A3, A12;

          (g2 . z) in ( rng g2) by A1, A12, FUNCT_1:def 3;

          then

           A14: b is_a_fixpoint_of (g2 . z) by A8;

          a is_a_fixpoint_of f by A6, A11;

          then a in ( dom f);

          then

           A15: b in ( dom f) by A9, ORDINAL1: 12;

          

          then (f . b) = ((g2 . z) . b) by A13, GRFUNC_1: 2

          .= b by A14;

          hence b is_a_fixpoint_of f by A15;

        end;

        hence contradiction by A7, A8, A10;

      end;

      X c= Z

      proof

        let x be object;

        assume x in X;

        then

        consider a be Element of ( dom f1) such that

         A16: x = a & a in ( dom f1) & for f st f in ( rng g1) holds a is_a_fixpoint_of f;

        now

          let f;

          assume f in ( rng g2);

          then

          consider z be object such that

           A17: z in ( dom g2) & f = (g2 . z) by FUNCT_1:def 3;

          reconsider z as set by TARSKI: 1;

          

           A18: (g1 . z) c= f by A1, A3, A17;

          then

           A19: ( dom (g1 . z)) c= ( dom f) by GRFUNC_1: 2;

          (g1 . z) in ( rng g1) by A1, A17, FUNCT_1:def 3;

          then a is_a_fixpoint_of (g1 . z) by A16;

          then a in ( dom (g1 . z)) & a = ((g1 . z) . a);

          then a in ( dom f) & a = (f . a) by A18, A19, GRFUNC_1: 2;

          hence a is_a_fixpoint_of f;

        end;

        hence thesis by A16, A4;

      end;

      then (X \/ Y) = Z by XBOOLE_1: 45;

      then ( criticals g2) = (( criticals g1) ^ ( numbering Y)) by A5, Th25;

      hence ( criticals g1) c= ( criticals g2) by Th9;

    end;

    definition

      let g be Ordinal-Sequence-valued Sequence;

      :: ORDINAL6:def12

      func lims g -> Ordinal-Sequence means

      : Def12: ( dom it ) = ( dom (g . 0 )) & for a st a in ( dom it ) holds (it . a) = ( union { ((g . b) . a) where b be Element of ( dom g) : b in ( dom g) });

      existence

      proof

        deffunc X( Ordinal) = { ((g . b) . $1) where b be Element of ( dom g) : b in ( dom g) };

        deffunc F( Ordinal) = ( union ( On X($1)));

        consider f such that

         A1: ( dom f) = ( dom (g . 0 )) & for a st a in ( dom (g . 0 )) holds (f . a) = F(a) from ORDINAL2:sch 3;

        take f;

        thus ( dom f) = ( dom (g . 0 )) by A1;

        let a;

        assume a in ( dom f);

        then

         A2: (f . a) = F(a) by A1;

        now

          let x;

          assume x in X(a);

          then ex b be Element of ( dom g) st x = ((g . b) . a) & b in ( dom g);

          hence x is ordinal;

        end;

        then X(a) is ordinal-membered by Th1;

        hence thesis by A2, Th2;

      end;

      uniqueness

      proof

        let f1,f2 be Ordinal-Sequence such that

         A3: ( dom f1) = ( dom (g . 0 )) & for a st a in ( dom f1) holds (f1 . a) = ( union { ((g . b) . a) where b be Element of ( dom g) : b in ( dom g) }) and

         A4: ( dom f2) = ( dom (g . 0 )) & for a st a in ( dom f2) holds (f2 . a) = ( union { ((g . b) . a) where b be Element of ( dom g) : b in ( dom g) });

        thus ( dom f1) = ( dom f2) by A3, A4;

        let x be object;

        assume

         A5: x in ( dom f1);

        then (f1 . x) = ( union { ((g . b) . x) where b be Element of ( dom g) : b in ( dom g) }) by A3;

        hence thesis by A3, A4, A5;

      end;

    end

    theorem :: ORDINAL6:56

    

     Th56: for g be Ordinal-Sequence-valued Sequence st ( dom g) <> {} & ( dom g) in U & for a st a in ( dom g) holds (g . a) is Ordinal-Sequence of U holds ( lims g) is Ordinal-Sequence of U

    proof

      let g be Ordinal-Sequence-valued Sequence;

      assume

       A1: ( dom g) <> {} & ( dom g) in U;

      assume

       A2: for a st a in ( dom g) holds (g . a) is Ordinal-Sequence of U;

      reconsider g0 = (g . 0 ) as Ordinal-Sequence of U by A2, A1, ORDINAL3: 8;

      

       A3: ( dom ( lims g)) = ( dom g0) by Def12

      .= ( On U) by FUNCT_2:def 1;

      ( rng ( lims g)) c= ( On U)

      proof

        let x be object;

        assume x in ( rng ( lims g));

        then

        consider y be object such that

         A4: y in ( dom ( lims g)) & x = (( lims g) . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A4;

        set X = { ((g . b) . y) where b be Element of ( dom g) : b in ( dom g) };

        

         A5: x = ( union X) by A4, Def12;

        reconsider a = ( dom g) as non empty Ordinal of U by A1;

        deffunc F( set) = ((g . $1) . y);

        

         A6: ( card { F(b) where b be Element of a : b in a }) c= ( card a) from TREES_2:sch 2;

        ( card a) c= a by CARD_1: 8;

        then ( card X) c= a by A6;

        then ( card X) in U by CLASSES1:def 1;

        then ( card X) in ( On U) by ORDINAL1:def 9;

        then

         A7: ( card X) in ( card U) by CLASSES2: 9;

        

         A8: X c= ( On U)

        proof

          let z be object;

          assume z in X;

          then

          consider b be Element of a such that

           A9: z = ((g . b) . y) & b in a;

          reconsider f = (g . b) as Ordinal-Sequence of U by A2;

          z = (f . y) by A9;

          hence thesis by ORDINAL1:def 9;

        end;

        then

        reconsider u = ( union X) as Ordinal by ORDINAL3: 4;

        ( On U) c= U by ORDINAL2: 7;

        then X c= U by A8;

        then X in U by A7, CLASSES1: 1;

        then u in U by CLASSES2: 59;

        hence thesis by A5, ORDINAL1:def 9;

      end;

      hence ( lims g) is Ordinal-Sequence of U by A3, FUNCT_2: 2;

    end;

    begin

    definition

      let x;

      :: ORDINAL6:def13

      func OS@ x -> Ordinal-Sequence equals

      : Def13: x if x is Ordinal-Sequence

      otherwise the Ordinal-Sequence;

      correctness ;

      :: ORDINAL6:def14

      func OSV@ x -> Ordinal-Sequence-valued Sequence equals

      : Def14: x if x is Ordinal-Sequence-valued Sequence

      otherwise the Ordinal-Sequence-valued Sequence;

      correctness ;

    end

    definition

      let U;

      :: ORDINAL6:def15

      func U -Veblen -> Ordinal-Sequence-valued Sequence means

      : Def15: ( dom it ) = ( On U) & (it . 0 ) = (U exp omega ) & (for b st ( succ b) in ( On U) holds (it . ( succ b)) = ( criticals (it . b))) & (for l st l in ( On U) holds (it . l) = ( criticals (it | l)));

      existence

      proof

        reconsider o = omega as non trivial Ordinal;

        deffunc C( set, set) = ( criticals ( OS@ $2));

        deffunc D( set, set) = ( criticals ( OSV@ $2));

        consider L be Sequence such that

         A1: ( dom L) = ( On U) and

         A2: 0 in ( On U) implies (L . 0 ) = (U exp o) and

         A3: for b st ( succ b) in ( On U) holds (L . ( succ b)) = C(b,.) and

         A4: for b st b in ( On U) & b <> 0 & b is limit_ordinal holds (L . b) = D(b,|) from ORDINAL2:sch 5;

        defpred P[ Ordinal] means $1 in ( On U) implies (L . $1) is Ordinal-Sequence;

        

         A5: P[ 0 ] by A2;

        

         A6: P[b] implies P[( succ b)]

        proof

          assume that

           A7: P[b] and

           A8: ( succ b) in ( On U);

          b in ( succ b) by ORDINAL1: 6;

          then

          reconsider f = (L . b) as Ordinal-Sequence by A7, A8, ORDINAL1: 10;

          (L . ( succ b)) = C(b,f) by A3, A8

          .= ( criticals f) by Def13;

          hence thesis;

        end;

        

         A9: for b st b <> 0 & b is limit_ordinal & for c st c in b holds P[c] holds P[b]

        proof

          let b;

          assume that

           A10: b <> 0 & b is limit_ordinal and for c st c in b holds P[c] and

           A11: b in ( On U);

          (L . b) = D(b,|) by A4, A10, A11;

          hence thesis;

        end;

        

         A12: P[b] from ORDINAL2:sch 1( A5, A6, A9);

        L is Ordinal-Sequence-valued

        proof

          let x;

          assume x in ( rng L);

          then ex y be object st y in ( dom L) & x = (L . y) by FUNCT_1:def 3;

          hence thesis by A1, A12;

        end;

        then

        reconsider L as Ordinal-Sequence-valued Sequence;

        take L;

        ( 0-element_of U) in ( On U) by ORDINAL1:def 9;

        hence ( dom L) = ( On U) & (L . 0 ) = (U exp omega ) by A1, A2;

        hereby

          let b;

          assume

           A13: ( succ b) in ( On U);

          reconsider f = (L . b) as Ordinal-Sequence;

          

          thus (L . ( succ b)) = C(b,f) by A13, A3

          .= ( criticals (L . b)) by Def13;

        end;

        let l;

        assume l in ( On U);

        

        hence (L . l) = D(l,|) by A4

        .= ( criticals (L | l)) by Def14;

      end;

      uniqueness

      proof

        let g1,g2 be Ordinal-Sequence-valued Sequence such that

         A14: ( dom g1) = ( On U) and

         A15: (g1 . 0 ) = (U exp omega ) and

         A16: (for b st ( succ b) in ( On U) holds (g1 . ( succ b)) = ( criticals (g1 . b))) and

         A17: (for l st l in ( On U) holds (g1 . l) = ( criticals (g1 | l))) and

         A18: ( dom g2) = ( On U) and

         A19: (g2 . 0 ) = (U exp omega ) and

         A20: (for b st ( succ b) in ( On U) holds (g2 . ( succ b)) = ( criticals (g2 . b))) and

         A21: (for l st l in ( On U) holds (g2 . l) = ( criticals (g2 | l)));

        deffunc C( set, Ordinal-Sequence) = ( criticals $2);

        deffunc D( set, Ordinal-Sequence-valued Sequence) = ( criticals $2);

        

         A22: 0 in ( On U) implies (g1 . 0 ) = (U exp omega ) by A15;

        

         A23: for b st ( succ b) in ( On U) holds (g1 . ( succ b)) = C(b,.) by A16;

        

         A24: for a st a in ( On U) & a <> 0 & a is limit_ordinal holds (g1 . a) = D(a,|) by A17;

        

         A25: 0 in ( On U) implies (g2 . 0 ) = (U exp omega ) by A19;

        

         A26: for b st ( succ b) in ( On U) holds (g2 . ( succ b)) = C(b,.) by A20;

        

         A27: for a st a in ( On U) & a <> 0 & a is limit_ordinal holds (g2 . a) = D(a,|) by A21;

        thus g1 = g2 from ORDINAL2:sch 4( A14, A22, A23, A24, A18, A25, A26, A27);

      end;

    end

    registration

      cluster uncountable for Universe;

      existence

      proof

        take U = ( Tarski-Class omega );

         omega in U by CLASSES1: 2;

        then ( card omega ) in ( card U) by CLASSES2: 1;

        hence ( card U) c/= omega ;

      end;

    end

    theorem :: ORDINAL6:57

    

     Th57: for U be Universe holds U is uncountable iff omega in U

    proof

      let U be Universe;

      thus U is uncountable implies omega in U

      proof

        assume ( card U) c/= omega ;

        then omega in ( card U) by Th4;

        then omega in ( On U) by CLASSES2: 9;

        hence omega in U by ORDINAL1:def 9;

      end;

      assume omega in U;

      then ( card omega ) in ( card U) by CLASSES2: 1;

      hence ( card U) c/= omega ;

    end;

    theorem :: ORDINAL6:58

    

     Th58: a in b & b in U & omega in U & c in ( dom ((U -Veblen ) . b)) implies (((U -Veblen ) . b) . c) is_a_fixpoint_of ((U -Veblen ) . a)

    proof

      assume

       A1: a in b & b in U & omega in U;

      set F = (U -Veblen );

      defpred P[ Ordinal] means $1 in U implies for a, c st a in $1 & c in ( dom (F . $1)) holds ((F . $1) . c) is_a_fixpoint_of (F . a);

      

       A2: P[ 0 ];

      

       A3: for b st P[b] holds P[( succ b)]

      proof

        let b such that

         A4: P[b] and

         A5: ( succ b) in U;

        

         A6: b in ( succ b) by ORDINAL1: 6;

        let a, c;

        assume a in ( succ b);

        then

         A7: a in b or a in {b} by XBOOLE_0:def 3;

        ( succ b) in ( On U) by A5, ORDINAL1:def 9;

        then

         A8: (F . ( succ b)) = ( criticals (F . b)) by Def15;

        assume c in ( dom (F . ( succ b)));

        then ((F . ( succ b)) . c) is_a_fixpoint_of (F . b) by A8, Th29;

        then ((F . ( succ b)) . c) in ( dom (F . b)) & ((F . ( succ b)) . c) = ((F . b) . ((F . ( succ b)) . c));

        hence thesis by A4, A5, A6, A7, ORDINAL1: 10, TARSKI:def 1;

      end;

      

       A9: ( dom F) = ( On U) by Def15;

      

       A10: for b st b <> 0 & b is limit_ordinal & for d st d in b holds P[d] holds P[b]

      proof

        let b such that

         A11: b <> 0 & b is limit_ordinal and for d st d in b holds P[d] and

         A12: b in U;

        

         A13: b in ( On U) by A12, ORDINAL1:def 9;

        then

         A14: (F . b) = ( criticals (F | b)) by A11, Def15;

        b c= ( On U) by A13, ORDINAL1:def 2;

        then

         A15: ( dom (F | b)) = b by A9, RELAT_1: 62;

        let a, c;

        assume

         A16: a in b;

        then

         A17: (F . a) = ((F | b) . a) by FUNCT_1: 49;

        set g = (F | b);

        set X = { z where z be Element of ( dom (g . 0 )) : z in ( dom (g . 0 )) & for f st f in ( rng g) holds z is_a_fixpoint_of f };

        now

          let x;

          assume x in X;

          then ex a be Element of ( dom (g . 0 )) st x = a & a in ( dom (g . 0 )) & for f st f in ( rng g) holds a is_a_fixpoint_of f;

          hence x is ordinal;

        end;

        then

        reconsider X as ordinal-membered set by Th1;

        assume c in ( dom (F . b));

        then ((F . b) . c) in ( rng (F . b)) by FUNCT_1:def 3;

        then ((F . b) . c) in X by A14, Th19;

        then

        consider z be Element of ( dom (g . 0 )) such that

         A18: ((F . b) . c) = z & z in ( dom (g . 0 )) & for f st f in ( rng g) holds z is_a_fixpoint_of f;

        (F . a) in ( rng g) by A15, A17, A16, FUNCT_1:def 3;

        hence thesis by A18;

      end;

      for b holds P[b] from ORDINAL2:sch 1( A2, A3, A10);

      hence thesis by A1;

    end;

    theorem :: ORDINAL6:59

    l in U & (for c st c in l holds a is_a_fixpoint_of ((U -Veblen ) . c)) implies a is_a_fixpoint_of ( lims ((U -Veblen ) | l))

    proof

      assume

       A1: l in U;

      assume

       A2: for c st c in l holds a is_a_fixpoint_of ((U -Veblen ) . c);

      set F = (U -Veblen );

      set g = (F | l);

      set X = { ((g . d) . a) where d be Element of ( dom g) : d in ( dom g) };

      set u = ( union X);

      

       A3: 0 in l by ORDINAL3: 8;

      then omega c= l by ORDINAL1:def 11;

      then

      reconsider o = omega as non trivial Ordinal of U by A1, CLASSES1:def 1;

      (F . 0 ) = (U exp o) by Def15;

      then

      reconsider f0 = (F . 0 ) as normal Ordinal-Sequence of U;

      

       A4: f0 = (g . 0 ) by FUNCT_1: 49, ORDINAL3: 8;

      then

       A5: ( dom ( lims g)) = ( dom f0) & ( dom f0) = ( On U) by Def12, FUNCT_2:def 1;

      

       A6: a is_a_fixpoint_of f0 by A2, ORDINAL3: 8;

      then

       A7: a in ( On U) & a = (f0 . a) by A5;

      

       A8: ( dom F) = ( On U) by Def15;

      l in ( On U) by A1, ORDINAL1:def 9;

      then l c= ( dom F) by A8, ORDINAL1:def 2;

      then

       A9: ( dom g) = l by RELAT_1: 62;

      set lg = ( lims g);

      thus a in ( dom ( lims g)) by A5, A6;

      

       A10: (lg . a) = u by A5, A7, Def12;

       {a} = X

      proof

        a in X by A3, A9, A7, A4;

        hence {a} c= X by ZFMISC_1: 31;

        let x be object;

        assume x in X;

        then

        consider d be Element of ( dom g) such that

         A11: x = ((g . d) . a) & d in ( dom g);

        (g . d) = (F . d) by A11, FUNCT_1: 47;

        then a is_a_fixpoint_of (g . d) by A2, A9;

        then x = a by A11;

        hence thesis by TARSKI:def 1;

      end;

      hence a = (( lims g) . a) by A10, ZFMISC_1: 25;

    end;

    theorem :: ORDINAL6:60

    

     Th60: a c= b & b in U & omega in U & c in ( dom ((U -Veblen ) . b)) & (for c st c in b holds ((U -Veblen ) . c) is normal) implies (((U -Veblen ) . a) . c) c= (((U -Veblen ) . b) . c)

    proof

      assume

       A1: a c= b & b in U & omega in U & c in ( dom ((U -Veblen ) . b));

      set F = (U -Veblen );

      defpred P[ Ordinal] means for a, c st a c= $1 & $1 in U & c in ( dom (F . $1)) & for c st c in $1 holds ((U -Veblen ) . c) is normal holds ((F . a) . c) c= ((F . $1) . c);

      

       A2: P[ 0 ];

      

       A3: for b st P[b] holds P[( succ b)]

      proof

        let b such that

         A4: P[b];

        let a, c such that

         A5: a c= ( succ b) and

         A6: ( succ b) in U and

         A7: c in ( dom (F . ( succ b)));

        assume

         A8: for c st c in ( succ b) holds ((U -Veblen ) . c) is normal;

        ( succ b) in ( On U) by A6, ORDINAL1:def 9;

        then

         A9: (F . ( succ b)) = ( criticals (F . b)) by Def15;

        then

         A10: ( dom (F . ( succ b))) c= ( dom (F . b)) by Th32;

        

         A11: b in ( succ b) by ORDINAL1: 6;

        then

         A12: b in U by A6, ORDINAL1: 10;

        (F . b) is normal by A8, ORDINAL1: 6;

        then

         A13: ((F . b) . c) c= ((F . ( succ b)) . c) by A7, A9, Th45;

        

         A14: for c st c in b holds (F . c) is normal by A8, A11, ORDINAL1: 10;

        per cases by A5, ORDINAL5: 1;

          suppose a = ( succ b);

          hence thesis;

        end;

          suppose a c= b;

          then ((F . a) . c) c= ((F . b) . c) by A4, A7, A10, A12, A14;

          hence thesis by A13;

        end;

      end;

      

       A15: for b st b <> 0 & b is limit_ordinal & for d st d in b holds P[d] holds P[b]

      proof

        let b;

        assume

         A16: b <> 0 & b is limit_ordinal;

        assume for d st d in b holds P[d];

        let a, c;

        assume

         A17: a c= b;

        per cases by A17;

          suppose a = b;

          hence thesis;

        end;

          suppose

           A18: a c< b;

          then

           A19: a in b by ORDINAL1: 11;

          assume b in U;

          then

           A20: b in ( On U) by ORDINAL1:def 9;

          then

           A21: (F . b) = ( criticals (F | b)) by A16, Def15;

          ( dom F) = ( On U) by Def15;

          then b c= ( dom F) by A20, ORDINAL1:def 2;

          then

           A22: ( dom (F | b)) = b by RELAT_1: 62;

          assume

           A23: c in ( dom (F . b));

          assume

           A24: for c st c in b holds ((U -Veblen ) . c) is normal;

           A25:

          now

            let c;

            assume c in ( dom (F | b));

            then c in b & ((F | b) . c) = (F . c) by A22, FUNCT_1: 49;

            hence ((F | b) . c) is normal by A24;

          end;

          

           A26: ((F | b) . a) in ( rng (F | b)) by A19, A22, FUNCT_1:def 3;

          ((F | b) . a) = (F . a) by A18, FUNCT_1: 49, ORDINAL1: 11;

          hence ((F . a) . c) c= ((F . b) . c) by A19, A21, A22, A23, A25, A26, Th54;

        end;

      end;

      for b holds P[b] from ORDINAL2:sch 1( A2, A3, A15);

      hence thesis by A1;

    end;

    theorem :: ORDINAL6:61

    

     Th61: l in U & a in U & b in l & (for c st c in l holds ((U -Veblen ) . c) is normal Ordinal-Sequence of U) implies (( lims ((U -Veblen ) | l)) . a) is_a_fixpoint_of ((U -Veblen ) . b)

    proof

      assume that

       A1: l in U and

       A2: a in U and

       A3: b in l and

       A4: for c st c in l holds ((U -Veblen ) . c) is normal Ordinal-Sequence of U;

      set F = (U -Veblen );

      set g = (F | l);

      set X = { ((g . d) . a) where d be Element of ( dom g) : d in ( dom g) };

      set u = ( union X);

      

       A5: 0 in l by ORDINAL3: 8;

      reconsider f0 = (F . 0 ), f = (F . b) as normal Ordinal-Sequence of U by A3, A4, ORDINAL3: 8;

      

       A6: f0 = (g . 0 ) & f = (g . b) by A3, FUNCT_1: 49, ORDINAL3: 8;

      

      then

       A7: ( dom ( lims g)) = ( dom f0) by Def12

      .= ( On U) by FUNCT_2:def 1;

      

       A8: ( dom F) = ( On U) by Def15;

      l in ( On U) by A1, ORDINAL1:def 9;

      then l c= ( dom F) by A8, ORDINAL1:def 2;

      then

       A9: ( dom g) = l by RELAT_1: 62;

      then

       A10: ((g . b) . a) in X by A3;

      now

        let c;

        assume

         A11: c in ( dom g);

        then (g . c) = (F . c) by FUNCT_1: 47;

        hence (g . c) is Ordinal-Sequence of U by A9, A11, A4;

      end;

      then

      reconsider lg = ( lims g) as Ordinal-Sequence of U by A1, A9, Th56;

      

       A12: a in ( On U) by A2, ORDINAL1:def 9;

      then

       A13: (lg . a) = u by A7, Def12;

      

       A14: ( dom f) = ( On U) & ( dom f0) = ( On U) by FUNCT_2:def 1;

      

       A15: for x st x in X holds ex y st x c= y & y in X & y is_a_fixpoint_of f

      proof

        let x;

        assume

         A16: x in X;

        then

        consider d be Element of ( dom g) such that

         A17: x = ((g . d) . a) & d in ( dom g);

        reconsider f2 = (F . d) as normal Ordinal-Sequence of U by A4, A9;

        

         A18: f2 = (g . d) by A9, FUNCT_1: 49;

        

         A19: ( dom f2) = ( On U) by FUNCT_2:def 1;

         omega c= l by A5, ORDINAL1:def 11;

        then

         A20: d in U & omega in U by A9, A1, CLASSES1:def 1, ORDINAL1: 10;

        

         A21: b in U by A1, A3, ORDINAL1: 10;

        

         A22: for c st c in b holds ((U -Veblen ) . c) is normal by A4, A3, ORDINAL1: 10;

        per cases by ORDINAL1: 16;

          suppose d c= b;

          then

           A23: x c= ((g . b) . a) by A12, A6, A14, A17, A18, A20, A21, A22, Th60;

          take y = ((g . ( succ b)) . a);

          

           A24: b in ( succ b) & ( succ b) in l by A3, ORDINAL1: 6, ORDINAL1: 28;

          then

          reconsider f1 = (F . ( succ b)) as normal Ordinal-Sequence of U by A4;

          

           A25: f1 = (g . ( succ b)) by A24, FUNCT_1: 49;

          ( succ b) in U by A24, A1, ORDINAL1: 10;

          then ( succ b) in ( On U) by ORDINAL1:def 9;

          then

           A26: f1 = ( criticals f) & ( dom f1) = ( On U) by Def15, FUNCT_2:def 1;

          then (f . a) c= y by A12, A25, Th45;

          hence x c= y by A23, A6;

          thus y in X by A9, A24;

          thus thesis by A12, A25, A26, Th29;

        end;

          suppose

           A27: b in d;

          take y = x;

          thus x c= y & y in X by A16;

          thus thesis by A12, A17, A27, A18, A19, A20, Th58;

        end;

      end;

      thus (( lims ((U -Veblen ) | l)) . a) in ( dom ((U -Veblen ) . b)) by A13, A14, ORDINAL1:def 9;

      hence thesis by A13, A10, A15, Th36;

    end;

    

     Lm1: omega in U implies ((U -Veblen ) . 0 ) is normal Ordinal-Sequence of U

    proof

      assume omega in U;

      then

      reconsider o = omega as non trivial Ordinal of U;

      ((U -Veblen ) . 0 ) = (U exp o) by Def15;

      hence ((U -Veblen ) . 0 ) is normal Ordinal-Sequence of U;

    end;

    

     Lm2: omega in U & a in U & ((U -Veblen ) . a) is normal Ordinal-Sequence of U implies ((U -Veblen ) . ( succ a)) is normal Ordinal-Sequence of U

    proof

      assume that

       A1: omega in U and

       A2: a in U;

      assume ((U -Veblen ) . a) is normal Ordinal-Sequence of U;

      then

      reconsider f = ((U -Veblen ) . a) as normal Ordinal-Sequence of U;

      ( succ a) in U by A2, CLASSES2: 5;

      then ( succ a) in ( On U) by ORDINAL1:def 9;

      then ((U -Veblen ) . ( succ a)) = ( criticals f) by Def15;

      hence ((U -Veblen ) . ( succ a)) is normal Ordinal-Sequence of U by A1, Th44;

    end;

    

     Lm3: l in U & (for a st a in l holds ((U -Veblen ) . a) is normal Ordinal-Sequence of U) implies ((U -Veblen ) . l) is normal Ordinal-Sequence of U

    proof

      assume

       A1: l in U;

      assume

       A2: for a st a in l holds ((U -Veblen ) . a) is normal Ordinal-Sequence of U;

      

       A3: l in ( On U) by A1, ORDINAL1:def 9;

      then

       A4: ((U -Veblen ) . l) = ( criticals ((U -Veblen ) | l)) by Def15;

      

       A5: ( dom (U -Veblen )) = ( On U) by Def15;

      l c= ( On U) by A3, ORDINAL1:def 2;

      then

       A6: ( dom ((U -Veblen ) | l)) = l by A5, RELAT_1: 62;

      

       A7: ( dom ((U -Veblen ) . l)) = ( On U)

      proof

        set F = (U -Veblen );

        set G = (F . l);

        

         A8: 0 in l by ORDINAL3: 8;

        reconsider f0 = (F . 0 ) as normal Ordinal-Sequence of U by A2, ORDINAL3: 8;

        

         A9: ( dom f0) = ( On U) by FUNCT_2:def 1;

        

         A10: f0 = ((F | l) . 0 ) by FUNCT_1: 49, ORDINAL3: 8;

        then f0 in ( rng (F | l)) by A6, A8, FUNCT_1:def 3;

        hence ( dom G) c= ( On U) by A4, A9, Th49;

        now

          let c;

          assume

           A11: c in ( dom (F | l));

          then ((F | l) . c) = (F . c) by FUNCT_1: 47;

          hence ((F | l) . c) is Ordinal-Sequence of U by A6, A11, A2;

        end;

        then

        reconsider lg = ( lims (F | l)) as Ordinal-Sequence of U by A1, A6, Th56;

        

         A12: ( dom lg) = ( On U) by FUNCT_2:def 1;

        ( rng lg) c= ( rng G)

        proof

          let y be object;

          assume y in ( rng lg);

          then

          consider x be object such that

           A13: x in ( dom lg) & y = (lg . x) by FUNCT_1:def 3;

          reconsider x as Ordinal by A13;

          y = (lg . x) by A13;

          then

           A14: x in U & y in ( On U) by A12, A13, ORDINAL1:def 9;

          set Y = { a where a be Element of ( dom ((F | l) . 0 )) : a in ( dom ((F | l) . 0 )) & for f st f in ( rng (F | l)) holds a is_a_fixpoint_of f };

          

           A15: Y is ordinal-membered by Th46;

          now

            let f;

            assume f in ( rng (F | l));

            then

            consider z be object such that

             A16: z in l & f = ((F | l) . z) by A6, FUNCT_1:def 3;

            f = (F . z) by A16, FUNCT_1: 49;

            hence y is_a_fixpoint_of f by A1, A2, A16, A13, A14, Th61;

          end;

          then y in Y by A9, A10, A14;

          hence thesis by A4, A15, Th19;

        end;

        then

         A17: ( Union lg) c= ( Union G) by ZFMISC_1: 77;

        ( On U) c= ( Union lg)

        proof

          let a;

          assume

           A18: a in ( On U);

          

           A19: a in ( succ a) by ORDINAL1: 6;

          set X = { (((F | l) . b) . ( succ a)) where b be Element of ( dom (F | l)) : b in ( dom (F | l)) };

          ( On U) is limit_ordinal by CLASSES2: 51;

          then

           A20: ( succ a) in ( On U) by A18, ORDINAL1: 28;

          then

           A21: (lg . ( succ a)) = ( union X) by A12, Def12;

          

           A22: (f0 . ( succ a)) in X by A10, A6, A8;

          

           A23: (f0 . a) in (f0 . ( succ a)) by A19, A20, A9, ORDINAL2:def 12;

          a c= (f0 . a) by A9, A18, ORDINAL4: 10;

          then a in (f0 . ( succ a)) by A23, ORDINAL1: 12;

          then a in (lg . ( succ a)) by A21, A22, TARSKI:def 4;

          hence thesis by A12, A20, CARD_5: 2;

        end;

        then

         A24: ( On U) c= ( Union G) by A17;

        

         A25: ( rng G) c= U

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in ( rng G);

          then

          consider y be object such that

           A26: y in ( dom G) & x = (G . y) by FUNCT_1:def 3;

          x is_a_fixpoint_of f0 by A4, A6, A8, A10, A26, Th47;

          then xx in ( dom f0) & xx = (f0 . xx);

          hence thesis;

        end;

        assume ( On U) c/= ( dom G);

        then ( dom G) in ( On U) by ORDINAL1: 16;

        then

        reconsider d = ( dom G) as Ordinal of U by ORDINAL1:def 9;

        

         A27: ( card d) in ( card U) by CLASSES2: 1;

        ( card ( rng G)) c= ( card d) by CARD_1: 12;

        then ( card ( rng G)) in ( card U) by A27, ORDINAL1: 12;

        then

        reconsider r = ( rng G) as Element of U by A25, CLASSES1: 1;

        ( union r) in U;

        then ( Union G) in ( On U) by ORDINAL1:def 9;

        then ( Union G) in ( Union G) by A24;

        hence thesis;

      end;

      

       A28: ( rng ((U -Veblen ) . l)) c= ( On U)

      proof

        let x be object;

        assume x in ( rng ((U -Veblen ) . l));

        then

        consider y be object such that

         A29: y in ( dom ((U -Veblen ) . l)) & x = (((U -Veblen ) . l) . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A29;

        

         A30: 0 in l by ORDINAL3: 8;

        then x is_a_fixpoint_of (((U -Veblen ) | l) . 0 ) by A4, A29, A6, Th47;

        then x in ( dom (((U -Veblen ) | l) . 0 ));

        then x in ( dom ((U -Veblen ) . 0 )) & ((U -Veblen ) . 0 ) is Ordinal-Sequence of U by A2, A30, FUNCT_1: 49;

        hence thesis by FUNCT_2:def 1;

      end;

      now

        let a;

        assume

         A31: a in l;

        then (((U -Veblen ) | l) . a) = ((U -Veblen ) . a) by FUNCT_1: 49;

        hence (((U -Veblen ) | l) . a) is normal by A2, A31;

      end;

      then ((U -Veblen ) . l) is continuous by A4, A6, Th53;

      hence ((U -Veblen ) . l) is normal Ordinal-Sequence of U by A4, A7, A28, FUNCT_2: 2;

    end;

    theorem :: ORDINAL6:62

    

     Th62: omega in U & a in U implies ((U -Veblen ) . a) is normal Ordinal-Sequence of U

    proof

      assume

       A1: omega in U;

      defpred P[ Ordinal] means $1 in U implies ((U -Veblen ) . $1) is normal Ordinal-Sequence of U;

      

       A2: P[ 0 ] by A1, Lm1;

      

       A3: P[b] implies P[( succ b)]

      proof

        b in ( succ b) by ORDINAL1: 6;

        then ( succ b) in U implies b in U by ORDINAL1: 10;

        hence thesis by A1, Lm2;

      end;

      

       A4: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]

      proof

        assume that

         A5: b <> 0 & b is limit_ordinal and

         A6: for c st c in b holds P[c] and

         A7: b in U;

        now

          let a;

          assume

           A8: a in b;

          then a in U by A7, ORDINAL1: 10;

          hence ((U -Veblen ) . a) is normal Ordinal-Sequence of U by A6, A8;

        end;

        hence thesis by A5, A7, Lm3;

      end;

       P[b] from ORDINAL2:sch 1( A2, A3, A4);

      hence thesis;

    end;

    theorem :: ORDINAL6:63

    

     Th63: omega in U & U c= W & a in U implies ((U -Veblen ) . a) c= ((W -Veblen ) . a)

    proof

      assume

       A1: omega in U & U c= W;

      then

       A2: ( On U) c= ( On W) by ORDINAL2: 9;

      defpred P[ Ordinal] means $1 in U implies ((U -Veblen ) . $1) c= ((W -Veblen ) . $1);

      

       A3: ((U -Veblen ) . 0 ) = (U exp omega ) & ((W -Veblen ) . 0 ) = (W exp omega ) by Def15;

      

       A4: ( dom (U exp omega )) = ( On U) & ( dom (W exp omega )) = ( On W) by FUNCT_2:def 1;

      now

        let x be object;

        assume x in ( On U);

        then

        reconsider a = x as Ordinal of U by ORDINAL1:def 9;

        reconsider b = a as Ordinal of W by A1;

        ((U exp omega ) . a) = ( exp ( omega ,b)) by A1, Def8;

        hence ((U exp omega ) . x) = ((W exp omega ) . x) by A1, Def8;

      end;

      then

       A5: P[ 0 ] by A2, A3, A4, GRFUNC_1: 2;

      

       A6: P[b] implies P[( succ b)]

      proof

        assume

         A7: P[b];

        assume

         A8: ( succ b) in U;

        

         A9: b in ( succ b) by ORDINAL1: 6;

        ( succ b) in ( On U) & ( succ b) in ( On W) by A1, A8, ORDINAL1:def 9;

        then ((U -Veblen ) . ( succ b)) = ( criticals ((U -Veblen ) . b)) & ((W -Veblen ) . ( succ b)) = ( criticals ((W -Veblen ) . b)) by Def15;

        hence thesis by A7, A9, Th40, A8, ORDINAL1: 10;

      end;

      

       A10: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]

      proof

        assume that

         A11: b <> 0 & b is limit_ordinal and

         A12: for c st c in b holds P[c] and

         A13: b in U;

        set g1 = ((U -Veblen ) | b), g2 = ((W -Veblen ) | b);

        

         A14: b in ( On U) & b in ( On W) by A1, A13, ORDINAL1:def 9;

        then

         A15: ((U -Veblen ) . b) = ( criticals g1) & ((W -Veblen ) . b) = ( criticals g2) by A11, Def15;

        ( dom (U -Veblen )) = ( On U) & ( dom (W -Veblen )) = ( On W) by Def15;

        then b c= ( dom (U -Veblen )) & b c= ( dom (W -Veblen )) by A14, ORDINAL1:def 2;

        then

         A16: ( dom g1) = b & ( dom g2) = b by RELAT_1: 62;

        now

          let a;

          assume

           A17: a in ( dom g1);

          then

           A18: (g1 . a) = ((U -Veblen ) . a) & (g2 . a) = ((W -Veblen ) . a) by A16, FUNCT_1: 47;

          a in U by A13, A16, A17, ORDINAL1: 10;

          hence (g1 . a) c= (g2 . a) by A12, A16, A17, A18;

        end;

        hence thesis by A11, A15, A16, Th55;

      end;

       P[b] from ORDINAL2:sch 1( A5, A6, A10);

      hence thesis;

    end;

    theorem :: ORDINAL6:64

    

     Th64: omega in U & a in U & b in U & omega in W & a in W & b in W implies (((U -Veblen ) . b) . a) = (((W -Veblen ) . b) . a)

    proof

      assume

       A1: omega in U & a in U & b in U & omega in W & a in W & b in W;

      then

       A2: a in ( On U) & a in ( On W) by ORDINAL1:def 9;

      ((W -Veblen ) . b) is Ordinal-Sequence of W & ((U -Veblen ) . b) is Ordinal-Sequence of U by A1, Th62;

      then

       A3: ( dom ((U -Veblen ) . b)) = ( On U) & ( dom ((W -Veblen ) . b)) = ( On W) by FUNCT_2:def 1;

      U c= W or W in U by CLASSES2: 53;

      then U c= W or W c= U by ORDINAL1:def 2;

      then ((U -Veblen ) . b) c= ((W -Veblen ) . b) or ((W -Veblen ) . b) c= ((U -Veblen ) . b) by A1, Th63;

      hence thesis by A2, A3, GRFUNC_1: 2;

    end;

    theorem :: ORDINAL6:65

    l in U & (for a st a in l holds ((U -Veblen ) . a) is normal Ordinal-Sequence of U) implies ( lims ((U -Veblen ) | l)) is non-decreasing continuous Ordinal-Sequence of U

    proof

      set G = (U -Veblen );

      assume that

       A1: l in U and

       A2: for a st a in l holds (G . a) is normal Ordinal-Sequence of U;

       0 in l by ORDINAL3: 8;

      then omega c= l by ORDINAL1:def 11;

      then

       A3: omega in U & l in ( On U) by A1, CLASSES1:def 1, ORDINAL1:def 9;

      then

       A4: (G . l) = ( criticals (G | l)) & ( dom G) = ( On U) by Def15;

      l c= ( On U) by A3, ORDINAL1:def 2;

      then

       A5: ( dom (G | l)) = l by A4, RELAT_1: 62;

      set g = (G | l);

      now

        let a;

        assume

         A6: a in ( dom g);

        then (g . a) = (G . a) by A5, FUNCT_1: 49;

        hence (g . a) is Ordinal-Sequence of U by A2, A5, A6;

      end;

      then

      reconsider f = ( lims g) as Ordinal-Sequence of U by A1, A5, Th56;

      (g . 0 ) = (G . 0 ) by FUNCT_1: 49, ORDINAL3: 8;

      then

      reconsider g0 = (g . 0 ) as Ordinal-Sequence of U by A2, ORDINAL3: 8;

      

       A7: ( dom f) = ( On U) by FUNCT_2:def 1;

      deffunc X( object) = { ((g . b) . $1) where b be Element of ( dom g) : b in ( dom g) };

      

       A8: f is non-decreasing

      proof

        let a, b;

        assume

         A9: a in b & b in ( dom f);

        then a in ( dom f) by ORDINAL1: 10;

        then

         A10: (f . a) = ( union X(a)) & (f . b) = ( union X(b)) by A9, Def12;

        let c;

        assume c in (f . a);

        then

        consider x such that

         A11: c in x & x in X(a) by A10, TARSKI:def 4;

        consider xa be Element of ( dom g) such that

         A12: x = ((g . xa) . a) & xa in ( dom g) by A11;

        (g . xa) = (G . xa) by A5, FUNCT_1: 49;

        then

        reconsider h = (g . xa) as increasing Ordinal-Sequence of U by A2, A5;

        ( dom h) = ( On U) by FUNCT_2:def 1;

        then (h . a) in (h . b) by A7, A9, ORDINAL2:def 12;

        then (h . a) c= (h . b) by ORDINAL1:def 2;

        then c in (h . b) & (h . b) in X(b) by A11, A12;

        hence c in (f . b) by A10, TARSKI:def 4;

      end;

      f is continuous

      proof

        let a, b;

        assume

         A13: a in ( dom f) & a <> 0 & a is limit_ordinal & b = (f . a);

        then

         A14: b = ( union X(a)) by Def12;

        

         A15: a c= ( dom f) by A13, ORDINAL1:def 2;

        then

         A16: ( dom (f | a)) = a by RELAT_1: 62;

        

         A17: b = ( Union (f | a))

        proof

          thus b c= ( Union (f | a))

          proof

            let c;

            assume c in b;

            then

            consider x such that

             A18: c in x & x in X(a) by A14, TARSKI:def 4;

            consider xa be Element of ( dom g) such that

             A19: x = ((g . xa) . a) & xa in ( dom g) by A18;

            (g . xa) = (G . xa) by A5, FUNCT_1: 49;

            then

            reconsider h = (g . xa) as normal Ordinal-Sequence of U by A2, A5;

            

             A20: ( dom h) = ( On U) by FUNCT_2:def 1;

            then

             A21: (h . a) is_limes_of (h | a) by A7, A13, ORDINAL2:def 13;

            

             A22: (h | a) is increasing by ORDINAL4: 15;

            

             A23: ( dom (h | a)) = a by A7, A15, A20, RELAT_1: 62;

            then ( Union (h | a)) is_limes_of (h | a) by A13, A22, ORDINAL5: 6;

            then ( lim (h | a)) = ( Union (h | a)) by ORDINAL2:def 10;

            then (h . a) = ( Union (h | a)) by A21, ORDINAL2:def 10;

            then

            consider y be object such that

             A24: y in a & c in ((h | a) . y) by A18, A19, A23, CARD_5: 2;

            

             A25: y in ( On U) by A7, A13, A24, ORDINAL1: 10;

            ((h | a) . y) = (h . y) by A24, FUNCT_1: 49;

            then ((h | a) . y) in X(y) by A19;

            then c in ( union X(y)) by A24, TARSKI:def 4;

            then c in (f . y) by A7, A25, Def12;

            then c in ((f | a) . y) by A24, FUNCT_1: 49;

            hence thesis by A16, A24, CARD_5: 2;

          end;

          let c;

          assume c in ( Union (f | a));

          then

          consider x be object such that

           A26: x in ( dom (f | a)) & c in ((f | a) . x) by CARD_5: 2;

          

           A27: ((f | a) . x) = (f . x) by A16, A26, FUNCT_1: 49;

          x in ( dom f) by A26, RELAT_1: 57;

          then (f . x) = ( union X(x)) by Def12;

          then

          consider y such that

           A28: c in y & y in X(x) by A26, A27, TARSKI:def 4;

          consider z be Element of ( dom g) such that

           A29: y = ((g . z) . x) & z in ( dom g) by A28;

          (g . z) = (G . z) by A5, FUNCT_1: 49;

          then

          reconsider h = (g . z) as normal Ordinal-Sequence of U by A2, A5;

          ( dom h) = ( On U) by FUNCT_2:def 1;

          then (h . x) in (h . a) by A26, A16, A13, A7, ORDINAL2:def 12;

          then (h . x) c= (h . a) by ORDINAL1:def 2;

          then c in (h . a) & (h . a) in X(a) by A28, A29;

          hence c in b by A14, TARSKI:def 4;

        end;

        (f | a) is non-decreasing by A8, Th13;

        hence b is_limes_of (f | a) by A13, A16, A17, ORDINAL5: 6;

      end;

      hence thesis by A8;

    end;

    registration

      let a;

      cluster ( Tarski-Class (a \/ omega )) -> uncountable;

      coherence

      proof

        set U = ( Tarski-Class (a \/ omega ));

         omega c= (a \/ omega ) & (a \/ omega ) in U by CLASSES1: 2, XBOOLE_1: 7;

        then omega in U by CLASSES1:def 1;

        hence thesis by Th57;

      end;

    end

    definition

      let a, b;

      :: ORDINAL6:def16

      func a -Veblen (b) -> Ordinal equals (((( Tarski-Class ((a \/ b) \/ omega )) -Veblen ) . a) . b);

      coherence ;

    end

    definition

      let n, b;

      :: original: -Veblen

      redefine

      :: ORDINAL6:def17

      func n -Veblen (b) -> Ordinal equals (((( Tarski-Class (b \/ omega )) -Veblen ) . n) . b);

      coherence ;

      compatibility

      proof

        n c= omega ;

        then (n \/ omega ) = omega by XBOOLE_1: 12;

        hence thesis by XBOOLE_1: 4;

      end;

    end

    theorem :: ORDINAL6:66

    

     Th66: a in ( Tarski-Class ((a \/ b) \/ c))

    proof

      set U = ( Tarski-Class ((a \/ b) \/ c));

      a c= (a \/ b) & (a \/ b) c= ((a \/ b) \/ c) by XBOOLE_1: 7;

      then a c= ((a \/ b) \/ c) & ((a \/ b) \/ c) in U by CLASSES1: 2;

      hence thesis by CLASSES1:def 1;

    end;

    theorem :: ORDINAL6:67

    

     Th67: omega in U & a in U & b in U implies (b -Veblen a) = (((U -Veblen ) . b) . a)

    proof

      assume

       A1: omega in U & a in U & b in U;

      set W = ( Tarski-Class ((b \/ a) \/ omega ));

       omega in W & a in W & b in W by Th57, Th66;

      hence (b -Veblen a) = (((U -Veblen ) . b) . a) by A1, Th64;

    end;

    theorem :: ORDINAL6:68

    

     Th68: ( 0 -Veblen a) = ( exp ( omega ,a))

    proof

      set b = (( 0 \/ a) \/ omega );

      set U = ( Tarski-Class b);

      b in U by CLASSES1: 2;

      then

       A1: b in ( On U) by ORDINAL1:def 9;

       omega in ( On U) by A1, ORDINAL1: 12, XBOOLE_1: 7;

      then

       A2: omega in U by ORDINAL1:def 9;

      a in ( On U) by A1, ORDINAL1: 12, XBOOLE_1: 7;

      then

       A3: a in U by ORDINAL1:def 9;

      

      thus ( 0 -Veblen a) = ((U exp omega ) . a) by Def15

      .= ( exp ( omega ,a)) by A3, A2, Def8;

    end;

    theorem :: ORDINAL6:69

    

     Th69: (b -Veblen (( succ b) -Veblen a)) = (( succ b) -Veblen a)

    proof

      set U = ( Tarski-Class ((b \/ a) \/ omega ));

      

       A1: omega in U by Th57;

      reconsider b1 = b as Ordinal of U by Th66;

      ( succ b1) in ( On U) by ORDINAL1:def 9;

      then

       A2: ((U -Veblen ) . ( succ b)) = ( criticals ((U -Veblen ) . b)) by Def15;

      reconsider f = ((U -Veblen ) . b1), g = ((U -Veblen ) . ( succ b1)) as normal Ordinal-Sequence of U by A1, Th62;

      

       A3: a in U by Th66;

      then

       A4: a in ( On U) by ORDINAL1:def 9;

      

       A5: ( dom f) = ( On U) & ( dom g) = ( On U) by FUNCT_2:def 1;

      set W = ( Tarski-Class ((b \/ (g . a)) \/ omega ));

       omega in U by Th57;

      then

       A6: (( succ b1) -Veblen a) = (g . a) & (b1 -Veblen (g . a)) = (f . (g . a)) by A3, Th67;

      then (( succ b) -Veblen a) is_a_fixpoint_of ((U -Veblen ) . b) by A4, A2, A5, Th29;

      hence (b -Veblen (( succ b) -Veblen a)) = (( succ b) -Veblen a) by A6;

    end;

    theorem :: ORDINAL6:70

    

     Th70: b in c implies (b -Veblen (c -Veblen a)) = (c -Veblen a)

    proof

      assume

       A1: b in c;

      set U = ( Tarski-Class ((c \/ a) \/ omega ));

      

       A2: omega in U by Th57;

      

       A3: a in U & c in U by Th66;

      then

       A4: b in U by A1, ORDINAL1: 10;

      then

      reconsider f = ((U -Veblen ) . b), g = ((U -Veblen ) . c) as normal Ordinal-Sequence of U by A2, Th66, Th62;

      ( dom g) = ( On U) by FUNCT_2:def 1;

      then a in ( dom g) by A3, ORDINAL1:def 9;

      then (g . a) is_a_fixpoint_of f by A1, A2, Th66, Th58;

      then (g . a) = (f . (g . a));

      hence (b -Veblen (c -Veblen a)) = (c -Veblen a) by A2, A4, Th67;

    end;

    theorem :: ORDINAL6:71

    

     Th71: a c= b iff (c -Veblen a) c= (c -Veblen b)

    proof

      set U = ( Tarski-Class ((c \/ b) \/ omega ));

      set W = ( Tarski-Class ((c \/ a) \/ omega ));

      

       A1: n in omega & omega in U & omega in W by Th57, ORDINAL1:def 12;

      

       A2: b in U & c in U by Th66;

      

       A3: a in W & c in W by Th66;

      reconsider f = ((U -Veblen ) . c) as increasing Ordinal-Sequence of U by A1, Th66, Th62;

      reconsider g = ((W -Veblen ) . c) as increasing Ordinal-Sequence of W by A1, Th66, Th62;

      

       A4: ( dom f) = ( On U) & ( dom g) = ( On W) by FUNCT_2:def 1;

      

       A5: b in ( On U) & a in ( On W) by A2, A3, ORDINAL1:def 9;

      hereby

        assume

         A6: a c= b;

        then

         A7: a in U by A2, CLASSES1:def 1;

        per cases by A6;

          suppose a = b;

          hence (c -Veblen a) c= (c -Veblen b);

        end;

          suppose a c< b;

          then a in b by ORDINAL1: 11;

          then (f . a) in (f . b) by A4, A5, ORDINAL2:def 12;

          then (c -Veblen a) in (c -Veblen b) by A7, A1, A2, A3, Th64;

          hence (c -Veblen a) c= (c -Veblen b) by ORDINAL1:def 2;

        end;

      end;

      assume

       A8: (c -Veblen a) c= (c -Veblen b) & a c/= b;

      then

       A9: b in a by ORDINAL1: 16;

      then

       A10: b in W by A3, ORDINAL1: 10;

      (g . b) in (g . a) by A4, A5, A9, ORDINAL2:def 12;

      then (c -Veblen b) in (c -Veblen a) by A1, A2, A3, A10, Th64;

      then (c -Veblen b) in (c -Veblen b) by A8;

      hence thesis;

    end;

    theorem :: ORDINAL6:72

    

     Th72: a in b iff (c -Veblen a) in (c -Veblen b)

    proof

      b c= a iff (c -Veblen b) c= (c -Veblen a) by Th71;

      hence thesis by Th4;

    end;

    theorem :: ORDINAL6:73

    (a -Veblen b) in (c -Veblen d) iff a = c & b in d or a in c & b in (c -Veblen d) or c in a & (a -Veblen b) in d

    proof

      hereby

        assume

         A1: (a -Veblen b) in (c -Veblen d);

        per cases by ORDINAL1: 14;

          case a = c;

          hence b in d by A1, Th72;

        end;

          case a in c;

          then (a -Veblen (c -Veblen d)) = (c -Veblen d) by Th70;

          hence b in (c -Veblen d) by A1, Th72;

        end;

          case c in a;

          then (c -Veblen (a -Veblen b)) = (a -Veblen b) by Th70;

          hence (a -Veblen b) in d by A1, Th72;

        end;

      end;

      assume

       A2: a = c & b in d or a in c & b in (c -Veblen d) or c in a & (a -Veblen b) in d;

      per cases by A2;

        suppose a = c & b in d;

        hence (a -Veblen b) in (c -Veblen d) by Th72;

      end;

        suppose

         A3: a in c & b in (c -Veblen d);

        then (a -Veblen (c -Veblen d)) = (c -Veblen d) by Th70;

        hence (a -Veblen b) in (c -Veblen d) by A3, Th72;

      end;

        suppose

         A4: c in a & (a -Veblen b) in d;

        then (c -Veblen (a -Veblen b)) = (a -Veblen b) by Th70;

        hence (a -Veblen b) in (c -Veblen d) by A4, Th72;

      end;

    end;

    begin

    reserve U for uncountable Universe;

    theorem :: ORDINAL6:74

    

     Th74: ((U -Veblen ) . 1) = ( criticals (U exp omega ))

    proof

      set o = ( succ ( 0-element_of U));

      o in ( On U) by ORDINAL1:def 9;

      then ((U -Veblen ) . 1) = ( criticals ((U -Veblen ) . 0 )) by Def15;

      hence thesis by Def15;

    end;

    theorem :: ORDINAL6:75

    

     Th75: (1 -Veblen a) is epsilon

    proof

      set U = ( Tarski-Class (a \/ omega ));

      ( 0 -Veblen (1 -Veblen a)) = (( succ 0 ) -Veblen a) by Th69;

      hence ( exp ( omega ,(1 -Veblen a))) = (1 -Veblen a) by Th68;

    end;

    theorem :: ORDINAL6:76

    

     Th76: for e be epsilon Ordinal holds ex a st e = (1 -Veblen a)

    proof

      let e be epsilon Ordinal;

      set U = ( Tarski-Class (e \/ omega ));

      

       A1: omega in U by Th57;

      ( 0-element_of U) = 0 & ( 1-element_of U) = 1;

      then

      reconsider f = ((U -Veblen ) . 0 ), g = ((U -Veblen ) . 1) as normal Ordinal-Sequence of U by A1, Th62;

      

       A2: g = ( criticals (U exp omega )) by Th74

      .= ( criticals f) by Def15;

      

       A3: (f . e) = ( 0 -Veblen e)

      .= ( exp ( omega ,e)) by Th68

      .= e by ORDINAL5:def 5;

      

       A4: ( dom f) = ( On U) by FUNCT_2:def 1;

      e c= (e \/ omega ) & (e \/ omega ) in U by CLASSES1: 2, XBOOLE_1: 7;

      then

       A5: e in U by CLASSES1:def 1;

      then e in ( On U) by ORDINAL1:def 9;

      then e is_a_fixpoint_of f by A3, A4;

      then

      consider a such that

       A6: a in ( dom ( criticals f)) & e = (( criticals f) . a) by Th33;

      take a;

      set W = ( Tarski-Class (a \/ omega ));

      

       A7: a c= (a \/ omega ) & (a \/ omega ) in W by CLASSES1: 2, XBOOLE_1: 7;

      a c= e by A6, ORDINAL4: 10;

      then omega in W & a in W & a in U & ( 1-element_of U) = ( 1-element_of W) by A5, A7, Th57, CLASSES1:def 1;

      hence e = (1 -Veblen a) by A1, A2, A6, Th64;

    end;

    

     Lm4: (1 -Veblen 0 ) = ( epsilon_ 0 )

    proof

      consider b such that

       A1: (1 -Veblen 0 ) = ( epsilon_ b) by Th75, ORDINAL5: 51;

      consider a such that

       A2: ( epsilon_ 0 ) = (1 -Veblen a) by Th76;

      now

        assume b <> 0 ;

        then ( epsilon_ 0 ) in ( epsilon_ b) by ORDINAL3: 8, ORDINAL5: 44;

        hence contradiction by A1, A2, Th72;

      end;

      hence thesis by A1;

    end;

    

     Lm5: (1 -Veblen a) = ( epsilon_ a) implies (1 -Veblen ( succ a)) = ( epsilon_ ( succ a))

    proof

      assume

       A1: (1 -Veblen a) = ( epsilon_ a);

      consider b such that

       A2: (1 -Veblen ( succ a)) = ( epsilon_ b) by Th75, ORDINAL5: 51;

      consider c such that

       A3: ( epsilon_ ( succ a)) = (1 -Veblen c) by Th76;

      

       A4: a in ( succ a) by ORDINAL1: 6;

      ( epsilon_ a) in ( epsilon_ ( succ a)) by ORDINAL1: 6, ORDINAL5: 44;

      then a in c by A1, A3, Th72;

      then ( succ a) c= c by ORDINAL1: 21;

      hence (1 -Veblen ( succ a)) c= ( epsilon_ ( succ a)) by A3, Th71;

      assume ( epsilon_ ( succ a)) c/= (1 -Veblen ( succ a));

      then ( epsilon_ b) in ( epsilon_ ( succ a)) by A2, Th4;

      then b in ( succ a) by Th12;

      then b c= a by ORDINAL1: 22;

      then ( epsilon_ b) c= ( epsilon_ a) by Th11;

      then ( succ a) c= a by A1, A2, Th71;

      then a in a by A4;

      hence thesis;

    end;

    

     Lm6: (for a st a in l holds (1 -Veblen a) = ( epsilon_ a)) implies (1 -Veblen l) = ( epsilon_ l)

    proof

      assume

       A1: for a st a in l holds (1 -Veblen a) = ( epsilon_ a);

      set U = ( Tarski-Class (l \/ omega ));

       0 in l by ORDINAL3: 8;

      then omega c= l by ORDINAL1:def 11;

      then (l \/ omega ) = l by XBOOLE_1: 12;

      then

       A2: l in U by CLASSES1: 2;

      

       A3: omega in U by Th57;

      ( 1-element_of U) = 1;

      then

      reconsider g = ((U -Veblen ) . 1) as normal Ordinal-Sequence of U by A3, Th62;

      reconsider o = omega as non trivial Ordinal of U by Th57;

      set f = (U exp o);

      

       A4: g = ( criticals f) by Th74;

      

       A5: ( dom g) = ( On U) by FUNCT_2:def 1;

      then

       A6: l in ( dom g) by A2, ORDINAL1:def 9;

      

      then

       A7: (g . l) = ( Union (g | l)) by A4, Th39

      .= ( union ( rng (g | l)));

      l c= ( dom g) by A6, ORDINAL1:def 2;

      then

       A8: ( dom (g | l)) = l by RELAT_1: 62;

      now

        let x;

        assume x in ( rng (g | l));

        then

        consider y be object such that

         A9: y in ( dom (g | l)) & x = ((g | l) . y) by FUNCT_1:def 3;

        reconsider y as Ordinal by A9;

        

         A10: x = (g . y) by A9, FUNCT_1: 47;

        y in ( dom g) by A6, A8, A9, ORDINAL1: 10;

        then y in U & ( 1-element_of U) in U by A5, ORDINAL1:def 9;

        then x = (1 -Veblen y) by A3, A10, Th67;

        then x = ( epsilon_ y) by A1, A8, A9;

        then x in ( epsilon_ l) by A8, A9, Th12;

        hence x c= ( epsilon_ l) by ORDINAL1:def 2;

      end;

      hence (1 -Veblen l) c= ( epsilon_ l) by A7, ZFMISC_1: 76;

      let a;

      assume a in ( epsilon_ l);

      then

      consider b such that

       A11: b in l & a in ( epsilon_ b) by ORDINAL5: 47;

      ( epsilon_ b) = (1 -Veblen b) by A1, A11;

      then ( epsilon_ b) in (1 -Veblen l) by A11, Th72;

      hence thesis by A11, ORDINAL1: 10;

    end;

    theorem :: ORDINAL6:77

    (1 -Veblen a) = ( epsilon_ a)

    proof

      set U = ( Tarski-Class (a \/ omega ));

      defpred P[ Ordinal] means (1 -Veblen $1) = ( epsilon_ $1);

      

       A1: P[ 0 ] by Lm4;

      

       A2: P[b] implies P[( succ b)] by Lm5;

      

       A3: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b] by Lm6;

       P[b] from ORDINAL2:sch 1( A1, A2, A3);

      hence thesis;

    end;