ordinal1.miz



    begin

    reserve X,Y,Z,X1,X2,X3,X4,X5,X6 for set,

x,y for object;

    ::$Canceled

    theorem :: ORDINAL1:5

    

     Th1: Y in X implies not X c= Y

    proof

      assume

       A1: Y in X;

      assume X c= Y;

      then Y in Y by A1;

      hence contradiction;

    end;

    definition

      let X;

      :: ORDINAL1:def1

      func succ X -> set equals (X \/ {X});

      coherence ;

    end

    registration

      let X;

      cluster ( succ X) -> non empty;

      coherence ;

    end

    theorem :: ORDINAL1:6

    

     Th2: X in ( succ X)

    proof

      X in {X} by TARSKI:def 1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: ORDINAL1:7

    ( succ X) = ( succ Y) implies X = Y

    proof

      assume that

       A1: ( succ X) = ( succ Y) and

       A2: X <> Y;

      Y in (X \/ {X}) by A1, Th2;

      then

       A3: Y in X or Y in {X} by XBOOLE_0:def 3;

      X in (Y \/ {Y}) by A1, Th2;

      then X in Y or X in {Y} by XBOOLE_0:def 3;

      hence contradiction by A2, A3, TARSKI:def 1;

    end;

    theorem :: ORDINAL1:8

    

     Th4: x in ( succ X) iff x in X or x = X

    proof

      thus x in ( succ X) implies x in X or x = X

      proof

        assume x in ( succ X);

        then x in X or x in {X} by XBOOLE_0:def 3;

        hence thesis by TARSKI:def 1;

      end;

      assume x in X or x = X;

      then x in X or x in {X} by TARSKI:def 1;

      hence thesis by XBOOLE_0:def 3;

    end;

    theorem :: ORDINAL1:9

    

     Th5: X <> ( succ X)

    proof

      assume

       A1: X = ( succ X);

      X in ( succ X) by Th2;

      hence contradiction by A1;

    end;

    reserve a,b,c for object,

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

    definition

      let X;

      :: ORDINAL1:def2

      attr X is epsilon-transitive means

      : Def2: for x st x in X holds x c= X;

      :: ORDINAL1:def3

      attr X is epsilon-connected means

      : Def3: for x, y st x in X & y in X holds x in y or x = y or y in x;

    end

    

     Lm1: {} is epsilon-transitive epsilon-connected;

    registration

      cluster epsilon-transitive epsilon-connected for set;

      existence by Lm1;

    end

    definition

      let IT be object;

      :: ORDINAL1:def4

      attr IT is ordinal means IT is epsilon-transitive epsilon-connected set;

    end

    registration

      cluster ordinal -> epsilon-transitive epsilon-connected for set;

      coherence ;

      cluster epsilon-transitive epsilon-connected -> ordinal for set;

      coherence ;

    end

    notation

      synonym Number for object;

      synonym number for set;

    end

    registration

      cluster ordinal for number;

      existence by Lm1;

    end

    registration

      cluster ordinal for Number;

      existence by Lm1;

    end

    definition

      mode Ordinal is ordinal number;

    end

    reserve A,B,C,D for Ordinal;

    theorem :: ORDINAL1:10

    

     Th6: for A,B be set, C be epsilon-transitive set st A in B & B in C holds A in C

    proof

      let A,B be set, C be epsilon-transitive set;

      assume that

       A1: A in B and

       A2: B in C;

      B c= C by A2, Def2;

      hence thesis by A1;

    end;

    theorem :: ORDINAL1:11

    

     Th7: for x be epsilon-transitive set, A be Ordinal st x c< A holds x in A

    proof

      let x be epsilon-transitive set, A be Ordinal;

      set a = the Element of (A \ x);

      assume

       A1: x c< A;

      then

       A2: x c= A;

      (A \ x) <> {} by A1, XBOOLE_1: 37, XBOOLE_1: 60;

      then a in (A \ x);

      then

      consider y such that

       A3: y in (A \ x) and

       A4: not ex a be object st a in (A \ x) & a in y by TARSKI: 3;

      

       A5: not y in x by A3, XBOOLE_0:def 5;

      now

        let a be object;

        assume a in x;

        then

        consider z such that

         A6: z = a and

         A7: z in x;

        z c= x by A7, Def2;

        then not y in z by A3, XBOOLE_0:def 5;

        hence a in y by A2, A3, A5, A6, A7, Def3;

      end;

      then

       A8: x c= y;

      

       A9: y c= A by A3, Def2;

      now

        let a be object;

        assume

         A10: a in y;

        then not a in (A \ x) by A4;

        hence a in x by A9, A10, XBOOLE_0:def 5;

      end;

      then

       A11: y c= x;

      y in A by A3;

      hence thesis by A11, A8, XBOOLE_0:def 10;

    end;

    theorem :: ORDINAL1:12

    for A be epsilon-transitive set, B,C be Ordinal st A c= B & B in C holds A in C

    proof

      let A be epsilon-transitive set, B,C be Ordinal;

      assume that

       A1: A c= B and

       A2: B in C;

      B c= C by A2, Def2;

      then

       A3: A c= C by A1;

      A <> C by A1, A2, Th1;

      then A c< C by A3;

      hence thesis by Th7;

    end;

    theorem :: ORDINAL1:13

    

     Th9: a in A implies a is Ordinal

    proof

      assume

       A1: a in A;

      reconsider a as set by TARSKI: 1;

      

       A2: a c= A by Def2, A1;

      now

        let y;

        assume

         A3: y in a;

        then

         A4: y c= A by A2, Def2;

        assume not y c= a;

        then

        consider b be object such that

         A5: b in y & not b in a;

        b in (y \ a) by A5, XBOOLE_0:def 5;

        then

        consider z such that

         A6: z in (y \ a) and not ex c be object st c in (y \ a) & c in z by TARSKI: 3;

        z in y by A6;

        then z in a or z = a or a in z by A1, A4, Def3;

        hence contradiction by A3, A6, XBOOLE_0:def 5, XREGULAR: 7;

      end;

      then

       A7: a is epsilon-transitive;

      for y, z st y in a & z in a holds y in z or y = z or z in y by A2, Def3;

      then a is epsilon-connected;

      hence thesis by A7;

    end;

    theorem :: ORDINAL1:14

    

     Th10: A in B or A = B or B in A

    proof

      assume that

       A1: not A in B and

       A2: A <> B;

       not A c< B by A1, Th7;

      then not A c= B by A2;

      then

      consider a be object such that

       A3: a in A & not a in B;

      a in (A \ B) by A3, XBOOLE_0:def 5;

      then

      consider X such that

       A4: X in (A \ B) and

       A5: not ex a be object st a in (A \ B) & a in X by TARSKI: 3;

      

       A6: X c= A by A4, Def2;

      now

        let b be object;

        assume

         A7: b in X;

        then not b in (A \ B) by A5;

        hence b in B by A6, A7, XBOOLE_0:def 5;

      end;

      then X c= B;

      then

       A8: X c< B or X = B;

      ( not X in B) & X is Ordinal by A4, Th9, XBOOLE_0:def 5;

      hence thesis by A4, A8, Th7;

    end;

    definition

      let A, B;

      :: original: c=

      redefine

      :: ORDINAL1:def5

      pred A c= B means for C st C in A holds C in B;

      compatibility

      proof

        thus A c= B implies for C st C in A holds C in B;

        assume

         A1: for C st C in A holds C in B;

        let x be object;

        assume

         A2: x in A;

        then

        reconsider C = x as Ordinal by Th9;

        C in B by A1, A2;

        hence thesis;

      end;

      connectedness

      proof

        let A, B;

        given C such that

         A3: C in A & not C in B;

        let D;

        A in B or A = B or B in A by Th10;

        hence thesis by A3, Th6;

      end;

    end

    theorem :: ORDINAL1:15

    (A,B) are_c=-comparable

    proof

      A c= B or B c= A;

      hence thesis;

    end;

    theorem :: ORDINAL1:16

    

     Th12: A c= B or B in A

    proof

      A in B or A = B or B in A by Th10;

      hence thesis by Def2;

    end;

    registration

      cluster empty -> ordinal for number;

      coherence by Lm1;

    end

    theorem :: ORDINAL1:17

    

     Th13: x is Ordinal implies ( succ x) is Ordinal

    proof

       A1:

      now

        let y;

        

         A2: y in {x} implies y = x by TARSKI:def 1;

        assume y in ( succ x);

        hence y in x or y = x by A2, XBOOLE_0:def 3;

      end;

      assume

       A3: x is Ordinal;

      now

        let y;

        

         A4: y = x implies y c= ( succ x) by XBOOLE_1: 7;

         A5:

        now

          assume y in x;

          then

           A6: y c= x by A3, Def2;

          x c= (x \/ {x}) by XBOOLE_1: 7;

          hence y c= ( succ x) by A6;

        end;

        assume y in ( succ x);

        hence y c= ( succ x) by A1, A5, A4;

      end;

      then

       A7: ( succ x) is epsilon-transitive;

      now

        let y, z;

        assume that

         A8: y in ( succ x) and

         A9: z in ( succ x);

        

         A10: z in x or z = x by A1, A9;

        y in x or y = x by A1, A8;

        hence y in z or y = z or z in y by A3, A10, Def3;

      end;

      then ( succ x) is epsilon-connected;

      hence thesis by A7;

    end;

    theorem :: ORDINAL1:18

    

     Th14: x is ordinal implies ( union x) is epsilon-transitive epsilon-connected

    proof

      assume x is ordinal;

      then

      reconsider A = x as Ordinal;

      thus y in ( union x) implies y c= ( union x)

      proof

        assume y in ( union x);

        then

        consider z such that

         A1: y in z and

         A2: z in x by TARSKI:def 4;

        z in A by A2;

        then

        reconsider z as Ordinal by Th9;

        z c= A by A2, Def2;

        hence thesis by A1, ZFMISC_1: 74;

      end;

      let y, z;

      assume that

       A3: y in ( union x) and

       A4: z in ( union x);

      consider X such that

       A5: y in X and

       A6: X in x by A3, TARSKI:def 4;

      

       A7: X in A by A6;

      consider Y such that

       A8: z in Y and

       A9: Y in x by A4, TARSKI:def 4;

      reconsider X, Y as Ordinal by A9, A7, Th9;

      z in Y by A8;

      then

       A10: z is Ordinal by Th9;

      y in X by A5;

      then y is Ordinal by Th9;

      hence thesis by A10, Th10;

    end;

    registration

      cluster non empty for Ordinal;

      existence

      proof

        reconsider A = ( succ {} ) as Ordinal by Th13;

        take A;

        thus thesis;

      end;

    end

    registration

      let A;

      cluster ( succ A) -> non empty ordinal;

      coherence by Th13;

      cluster ( union A) -> ordinal;

      coherence by Th14;

    end

    theorem :: ORDINAL1:19

    

     Th15: (for x st x in X holds x is Ordinal & x c= X) implies X is epsilon-transitive epsilon-connected

    proof

      assume

       A1: for x st x in X holds x is Ordinal & x c= X;

      thus X is epsilon-transitive by A1;

      let x, y;

      assume x in X & y in X;

      then x is Ordinal & y is Ordinal by A1;

      hence thesis by Th10;

    end;

    theorem :: ORDINAL1:20

    

     Th16: X c= A & X <> {} implies ex C st C in X & for B st B in X holds C c= B

    proof

      set a = the Element of X;

      assume that

       A1: X c= A and

       A2: X <> {} ;

      a in X by A2;

      then

      consider Y such that

       A3: Y in X and

       A4: not ex a be object st a in X & a in Y by TARSKI: 3;

      Y is Ordinal by A1, A3, Th9;

      then

      consider C such that

       A5: C = Y;

      take C;

      thus C in X by A3, A5;

      let B;

      assume B in X;

      then not B in C by A4, A5;

      then B = C or C in B by Th10;

      hence thesis by Def2;

    end;

    theorem :: ORDINAL1:21

    

     Th17: A in B iff ( succ A) c= B

    proof

      thus A in B implies ( succ A) c= B

      proof

        assume

         A1: A in B;

        then for a be object holds a in {A} implies a in B by TARSKI:def 1;

        then

         A2: {A} c= B;

        A c= B by A1, Def2;

        hence thesis by A2, XBOOLE_1: 8;

      end;

      assume

       A3: ( succ A) c= B;

      A in ( succ A) by Th2;

      hence thesis by A3;

    end;

    theorem :: ORDINAL1:22

    

     Th18: A in ( succ C) iff A c= C

    proof

      thus A in ( succ C) implies A c= C

      proof

        assume A in ( succ C);

        then A in C or A in {C} by XBOOLE_0:def 3;

        hence thesis by Def2, TARSKI:def 1;

      end;

      assume

       A1: A c= C;

      assume not A in ( succ C);

      then A = ( succ C) or ( succ C) in A by Th10;

      then

       A2: ( succ C) c= C by A1, Def2;

      C in ( succ C) by Th2;

      then C c= ( succ C) by Def2;

      then ( succ C) = C by A2;

      hence contradiction by Th5;

    end;

    scheme :: ORDINAL1:sch1

    OrdinalMin { P[ Ordinal] } :

ex A st P[A] & for B st P[B] holds A c= B

      provided

       A1: ex A st P[A];

      consider A such that

       A2: P[A] by A1;

      defpred R[ object] means ex B st $1 = B & P[B];

      consider X such that

       A3: for x be object holds x in X iff x in ( succ A) & R[x] from XBOOLE_0:sch 1;

      for a be object holds a in X implies a in ( succ A) by A3;

      then

       A4: X c= ( succ A);

      A in ( succ A) by Th2;

      then X <> {} by A2, A3;

      then

      consider C such that

       A5: C in X and

       A6: for B st B in X holds C c= B by A4, Th16;

      C in ( succ A) by A3, A5;

      then

       A7: C c= ( succ A) by Def2;

      take C;

      ex B st C = B & P[B] by A3, A5;

      hence P[C];

      let B;

      assume

       A8: P[B];

      assume

       A9: not C c= B;

      then B c< C;

      then B in C by Th7;

      then B in X by A3, A8, A7;

      hence contradiction by A6, A9;

    end;

    ::$Notion-Name

    scheme :: ORDINAL1:sch2

    TransfiniteInd { P[ Ordinal] } :

for A holds P[A]

      provided

       A1: for A st for C st C in A holds P[C] holds P[A];

      defpred R[ object] means ex B st $1 = B & P[B];

      let A;

      set Y = ( succ A);

      consider Z such that

       A2: for x be object holds x in Z iff x in Y & R[x] from XBOOLE_0:sch 1;

      now

        assume (Y \ Z) <> {} ;

        then

        consider C such that

         A3: C in (Y \ Z) and

         A4: for B st B in (Y \ Z) holds C c= B by Th16;

        now

          let B such that

           A5: B in C;

          

           A6: C c= Y by A3, Def2;

          now

            assume not B in Z;

            then B in (Y \ Z) by A5, A6, XBOOLE_0:def 5;

            then

             A7: C c= B by A4;

            C <> B by A5;

            then C c< B by A7;

            hence contradiction by A5, Th7;

          end;

          then ex B9 be Ordinal st B = B9 & P[B9] by A2;

          hence P[B];

        end;

        then

         A8: P[C] by A1;

         not C in Z by A3, XBOOLE_0:def 5;

        hence contradiction by A2, A3, A8;

      end;

      then not A in Y or A in Z by XBOOLE_0:def 5;

      then ex B st A = B & P[B] by A2, Th2;

      hence thesis;

    end;

    theorem :: ORDINAL1:23

    

     Th19: for X st for a st a in X holds a is Ordinal holds ( union X) is epsilon-transitive epsilon-connected

    proof

      let X such that

       A1: for a st a in X holds a is Ordinal;

      thus ( union X) is epsilon-transitive

      proof

        let x;

        assume x in ( union X);

        then

        consider Y such that

         A2: x in Y and

         A3: Y in X by TARSKI:def 4;

        Y is Ordinal by A1, A3;

        then

         A4: x c= Y by A2, Def2;

        let a be object;

        assume a in x;

        hence thesis by A3, A4, TARSKI:def 4;

      end;

      let x, y;

      assume that

       A5: x in ( union X) and

       A6: y in ( union X);

      consider Z such that

       A7: y in Z and

       A8: Z in X by A6, TARSKI:def 4;

      Z is Ordinal by A1, A8;

      then

       A9: y is Ordinal by A7, Th9;

      consider Y such that

       A10: x in Y and

       A11: Y in X by A5, TARSKI:def 4;

      Y is Ordinal by A1, A11;

      then x is Ordinal by A10, Th9;

      hence thesis by A9, Th10;

    end;

    theorem :: ORDINAL1:24

    

     Th20: for X st for a st a in X holds a is Ordinal holds ex A st X c= A

    proof

      let X;

      assume

       A1: for a st a in X holds a is Ordinal;

      then

       A2: ( union X) is epsilon-transitive epsilon-connected by Th19;

      then

      reconsider A = ( succ ( union X)) as Ordinal;

      take A;

      let a be object;

      assume

       A3: a in X;

      then

      reconsider B = a as Ordinal by A1;

      for b be object holds b in B implies b in ( union X) by A3, TARSKI:def 4;

      then B c= ( union X);

      hence thesis by A2, Th18;

    end;

    theorem :: ORDINAL1:25

    

     Th21: not ex X st for x holds x in X iff x is Ordinal

    proof

      given X such that

       A1: for x holds x in X iff x is Ordinal;

      

       A2: X is epsilon-transitive

      proof

        let x;

        assume x in X;

        then

         A3: x is Ordinal by A1;

        thus thesis

        proof

          let a be object;

          assume a in x;

          then a is Ordinal by A3, Th9;

          hence thesis by A1;

        end;

      end;

      X is epsilon-connected

      proof

        let x, y;

        assume x in X & y in X;

        then x is Ordinal & y is Ordinal by A1;

        hence thesis by Th10;

      end;

      then X in X by A1, A2;

      hence contradiction;

    end;

    theorem :: ORDINAL1:26

    

     Th22: not ex X st for A holds A in X

    proof

      defpred P[ object] means $1 is Ordinal;

      given X such that

       A1: A in X;

      consider Y such that

       A2: for a be object holds a in Y iff a in X & P[a] from XBOOLE_0:sch 1;

      for x st x is Ordinal holds x in Y by A1, A2;

      then x in Y iff x is Ordinal by A2;

      hence contradiction by Th21;

    end;

    theorem :: ORDINAL1:27

    for X holds ex A st not A in X & for B st not B in X holds A c= B

    proof

      let X;

      defpred P[ object] means not $1 in X;

      consider B such that

       A1: not B in X by Th22;

      consider Y such that

       A2: for a be object holds a in Y iff a in ( succ B) & P[a] from XBOOLE_0:sch 1;

      for a be object holds a in Y implies a in ( succ B) by A2;

      then

       A3: Y c= ( succ B);

      B in ( succ B) by Th2;

      then Y <> {} by A1, A2;

      then

      consider A such that

       A4: A in Y and

       A5: for B st B in Y holds A c= B by A3, Th16;

      A in ( succ B) by A2, A4;

      then

       A6: A c= ( succ B) by Def2;

      take A;

      thus not A in X by A2, A4;

      let C;

      assume

       A7: not C in X;

      assume

       A8: not A c= C;

      then not A in C by Def2;

      then C in A by A8, Th10;

      then C in Y by A2, A7, A6;

      hence contradiction by A5, A8;

    end;

    definition

      let A be set;

      :: ORDINAL1:def6

      attr A is limit_ordinal means A = ( union A);

    end

    theorem :: ORDINAL1:28

    

     Th24: for A holds A is limit_ordinal iff for C st C in A holds ( succ C) in A

    proof

      let A;

      thus A is limit_ordinal implies for C st C in A holds ( succ C) in A

      proof

        assume A is limit_ordinal;

        then

         A1: A = ( union A);

        let C;

        assume C in A;

        then

        consider z such that

         A2: C in z and

         A3: z in A by A1, TARSKI:def 4;

        for b be object holds b in {C} implies b in z by A2, TARSKI:def 1;

        then

         A4: {C} c= z;

        

         A5: z is Ordinal by A3, Th9;

        then C c= z by A2, Def2;

        then ( succ C) c= z by A4, XBOOLE_1: 8;

        then ( succ C) = z or ( succ C) c< z;

        then

         A6: ( succ C) = z or ( succ C) in z by A5, Th7;

        z c= A by A3, Def2;

        hence thesis by A3, A6;

      end;

      assume

       A7: for C st C in A holds ( succ C) in A;

      now

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume

         A8: a in A;

        then a is Ordinal by Th9;

        then

         A9: ( succ aa) in A by A7, A8;

        a in ( succ aa) by Th2;

        hence a in ( union A) by A9, TARSKI:def 4;

      end;

      then

       A10: A c= ( union A);

      now

        let a be object;

        assume a in ( union A);

        then

        consider z such that

         A11: a in z and

         A12: z in A by TARSKI:def 4;

        z c= A by A12, Def2;

        hence a in A by A11;

      end;

      then ( union A) c= A;

      then A = ( union A) by A10;

      hence thesis;

    end;

    theorem :: ORDINAL1:29

     not A is limit_ordinal iff ex B st A = ( succ B)

    proof

      thus not A is limit_ordinal implies ex B st A = ( succ B)

      proof

        assume not A is limit_ordinal;

        then

        consider B such that

         A1: B in A and

         A2: not ( succ B) in A by Th24;

        take B;

        assume

         A3: A <> ( succ B);

        ( succ B) c= A by A1, Th17;

        then ( succ B) c< A by A3;

        hence contradiction by A2, Th7;

      end;

      given B such that

       A4: A = ( succ B);

      B in A & not ( succ B) in A by A4, Th2;

      hence thesis by Th24;

    end;

    reserve F,G for Function;

    definition

      let IT be set;

      :: ORDINAL1:def7

      attr IT is Sequence-like means

      : Def7: ( proj1 IT) is epsilon-transitive epsilon-connected;

    end

    registration

      cluster empty -> Sequence-like for set;

      coherence ;

    end

    definition

      mode Sequence is Sequence-like Function;

    end

    registration

      let Z;

      cluster Z -valued for Sequence;

      existence

      proof

        reconsider L = {} as Sequence;

        take L;

        thus ( rng L) c= Z;

      end;

    end

    definition

      let Z;

      mode Sequence of Z is Z -valued Sequence;

    end

    theorem :: ORDINAL1:30

     {} is Sequence of Z

    proof

      reconsider L = {} as Sequence;

      ( rng L) c= Z;

      hence thesis by RELAT_1:def 19;

    end;

    reserve L,L1 for Sequence;

    theorem :: ORDINAL1:31

    ( dom F) is Ordinal implies F is Sequence of ( rng F) by Def7, RELAT_1:def 19;

    registration

      let L;

      cluster ( dom L) -> ordinal;

      coherence by Def7;

    end

    theorem :: ORDINAL1:32

    X c= Y implies for L be Sequence of X holds L is Sequence of Y

    proof

      assume

       A1: X c= Y;

      let L be Sequence of X;

      ( rng L) c= X by RELAT_1:def 19;

      then ( rng L) c= Y by A1;

      hence thesis by RELAT_1:def 19;

    end;

    registration

      let L, A;

      cluster (L | A) -> ( rng L) -valued Sequence-like;

      coherence

      proof

        

         A1: ( rng (L | A)) c= ( rng L) by RELAT_1: 70;

        A c= ( dom L) implies ( dom (L | A)) = A by RELAT_1: 62;

        hence thesis by A1, RELAT_1: 68;

      end;

    end

    theorem :: ORDINAL1:33

    for L be Sequence of X holds for A holds (L | A) is Sequence of X;

    definition

      let IT be set;

      :: ORDINAL1:def8

      attr IT is c=-linear means

      : Def8: for x,y be set st x in IT & y in IT holds (x,y) are_c=-comparable ;

    end

    theorem :: ORDINAL1:34

    (for a st a in X holds a is Sequence) & X is c=-linear implies ( union X) is Sequence

    proof

      assume that

       A1: for a st a in X holds a is Sequence and

       A2: X is c=-linear;

      ( union X) is Relation-like Function-like

      proof

        thus for a be object st a in ( union X) holds ex b,c be object st [b, c] = a

        proof

          let a be object;

          assume a in ( union X);

          then

          consider x such that

           A3: a in x and

           A4: x in X by TARSKI:def 4;

          reconsider x as Sequence by A1, A4;

          for a be object st a in x holds ex b,c be object st [b, c] = a by RELAT_1:def 1;

          hence thesis by A3;

        end;

        let a,b,c be object;

        assume that

         A5: [a, b] in ( union X) and

         A6: [a, c] in ( union X);

        consider y such that

         A7: [a, c] in y and

         A8: y in X by A6, TARSKI:def 4;

        reconsider y as Sequence by A1, A8;

        consider x such that

         A9: [a, b] in x and

         A10: x in X by A5, TARSKI:def 4;

        reconsider x as Sequence by A1, A10;

        (x,y) are_c=-comparable by A2, A10, A8;

        then x c= y or y c= x;

        hence thesis by A9, A7, FUNCT_1:def 1;

      end;

      then

      reconsider F = ( union X) as Function;

      defpred P[ object, object] means $1 in X & for L st L = $1 holds ( dom L) = $2;

      

       A11: for a,b,c be object st P[a, b] & P[a, c] holds b = c

      proof

        let a,b,c be object;

        assume that

         A12: a in X and

         A13: for L st L = a holds ( dom L) = b and a in X and

         A14: for L st L = a holds ( dom L) = c;

        reconsider a as Sequence by A1, A12;

        ( dom a) = b by A13;

        hence thesis by A14;

      end;

      consider G such that

       A15: for a,b be object holds [a, b] in G iff a in X & P[a, b] from FUNCT_1:sch 1( A11);

      

       A16: for a,b be object holds [a, b] in G implies b is Ordinal

      proof

        let a,b be object;

        assume

         A17: [a, b] in G;

        then a in X by A15;

        then

        reconsider a as Sequence by A1;

        ( dom a) = b by A15, A17;

        hence thesis;

      end;

      a in ( rng G) implies a is Ordinal

      proof

        assume a in ( rng G);

        then

        consider b be object such that

         A18: b in ( dom G) & a = (G . b) by FUNCT_1:def 3;

         [b, a] in G by A18, FUNCT_1: 1;

        hence thesis by A16;

      end;

      then

      consider A such that

       A19: ( rng G) c= A by Th20;

      defpred P[ Ordinal] means for B st B in ( rng G) holds B c= $1;

      for B st B in ( rng G) holds B c= A by A19, Def2;

      then

       A20: ex A st P[A];

      consider A such that

       A21: P[A] & for C st P[C] holds A c= C from OrdinalMin( A20);

      ( dom F) = A

      proof

        thus for a be object holds a in ( dom F) implies a in A

        proof

          let a be object;

          assume a in ( dom F);

          then

          consider b be object such that

           A22: [a, b] in F by XTUPLE_0:def 12;

          consider x such that

           A23: [a, b] in x and

           A24: x in X by A22, TARSKI:def 4;

          reconsider x as Sequence by A1, A24;

          for L st L = x holds ( dom L) = ( dom x);

          then [x, ( dom x)] in G by A15, A24;

          then x in ( dom G) & ( dom x) = (G . x) by FUNCT_1: 1;

          then ( dom x) in ( rng G) by FUNCT_1:def 3;

          then

           A25: ( dom x) c= A by A21;

          a in ( dom x) by A23, XTUPLE_0:def 12;

          hence thesis by A25;

        end;

        let a be object;

        assume

         A26: a in A;

        then

        reconsider a9 = a as Ordinal by Th9;

        now

          assume

           A27: for L st L in X holds not a9 in ( dom L);

          now

            let B;

            assume B in ( rng G);

            then

            consider c be object such that

             A28: c in ( dom G) & B = (G . c) by FUNCT_1:def 3;

            

             A29: [c, B] in G by A28, FUNCT_1: 1;

            then c in X by A15;

            then

            reconsider c as Sequence by A1;

            c in X & ( dom c) = B by A15, A29;

            hence B c= a9 by A27, Th12;

          end;

          then

           A30: A c= a9 by A21;

          a9 c= A by A26, Def2;

          then

           A: A = a by A30, XBOOLE_0:def 10;

          reconsider aa = a as set by TARSKI: 1;

           not aa in aa;

          hence contradiction by A, A26;

        end;

        then

        consider L such that

         A31: L in X & a in ( dom L);

        L c= F & ex b be object st [a, b] in L by A31, XTUPLE_0:def 12, ZFMISC_1: 74;

        hence thesis by XTUPLE_0:def 12;

      end;

      hence thesis by Def7;

    end;

    scheme :: ORDINAL1:sch3

    TSUniq { A() -> Ordinal , H( Sequence) -> set , L1,L2() -> Sequence } :

L1() = L2()

      provided

       A1: ( dom L1()) = A() & for B, L st B in A() & L = (L1() | B) holds (L1() . B) = H(L)

       and

       A2: ( dom L2()) = A() & for B, L st B in A() & L = (L2() | B) holds (L2() . B) = H(L);

      defpred P[ object] means (L1() . $1) <> (L2() . $1);

      consider X such that

       A3: for x be object holds x in X iff x in A() & P[x] from XBOOLE_0:sch 1;

      for b be object holds b in X implies b in A() by A3;

      then

       A4: X c= A();

      assume L1() <> L2();

      then ex a be object st a in A() & (L1() . a) <> (L2() . a) by A1, A2;

      then X <> {} by A3;

      then

      consider B such that

       A5: B in X and

       A6: for C st C in X holds B c= C by A4, Th16;

      

       A7: B in A() by A3, A5;

      then

       A8: B c= A() by Def2;

      then

       A9: ( dom (L1() | B)) = B by A1, RELAT_1: 62;

      

       A10: ( dom (L2() | B)) = B by A2, A8, RELAT_1: 62;

       A11:

      now

        let C;

        assume

         A12: C in B;

        then not C in X by A6, Th1;

        hence (L1() . C) = (L2() . C) by A3, A8, A12;

      end;

      now

        let a be object;

        assume

         A13: a in B;

        then

        reconsider a9 = a as Ordinal by Th9;

        (L1() . a9) = (L2() . a9) & ((L1() | B) . a) = (L1() . a) by A11, A9, A13, FUNCT_1: 47;

        hence ((L1() | B) . a) = ((L2() | B) . a) by A10, A13, FUNCT_1: 47;

      end;

      then

       A14: (L1() | B) = (L2() | B) by A9, A10;

      (L1() . B) = H(|) & (L2() . B) = H(|) by A1, A2, A7;

      hence contradiction by A3, A5, A14;

    end;

    scheme :: ORDINAL1:sch4

    TSExist { A() -> Ordinal , H( Sequence) -> set } :

ex L st ( dom L) = A() & for B, L1 st B in A() & L1 = (L | B) holds (L . B) = H(L1);

      defpred S[ Ordinal] means ex L st ( dom L) = $1 & for B st B in $1 holds (L . B) = H(|);

      

       A1: for B st for C st C in B holds S[C] holds S[B]

      proof

        defpred P[ object, object] means $1 is Ordinal & $2 is Sequence & for A, L st A = $1 & L = $2 holds ( dom L) = A & for B st B in A holds (L . B) = H(|);

        let B such that

         A2: for C st C in B holds ex L st ( dom L) = C & for D st D in C holds (L . D) = H(|);

        

         A3: for a,b,c be object st P[a, b] & P[a, c] holds b = c

        proof

          let a,b,c be object;

          assume that

           A4: a is Ordinal and

           A5: b is Sequence and

           A6: for A, L st A = a & L = b holds ( dom L) = A & for B st B in A holds (L . B) = H(|) and a is Ordinal and

           A7: c is Sequence and

           A8: for A, L st A = a & L = c holds ( dom L) = A & for B st B in A holds (L . B) = H(|);

          reconsider c as Sequence by A7;

          reconsider a as Ordinal by A4;

          

           A9: ( dom c) = a & for B, L st B in a & L = (c | B) holds (c . B) = H(L) by A8;

          reconsider b as Sequence by A5;

          

           A10: ( dom b) = a & for B, L st B in a & L = (b | B) holds (b . B) = H(L) by A6;

          b = c from TSUniq( A10, A9);

          hence thesis;

        end;

        consider G such that

         A11: for a,b be object holds [a, b] in G iff a in B & P[a, b] from FUNCT_1:sch 1( A3);

        defpred R[ object, object] means ex L st L = (G . $1) & $2 = H(L);

        

         A12: ( dom G) = B

        proof

          thus for a be object holds a in ( dom G) implies a in B

          proof

            let a be object;

            assume a in ( dom G);

            then ex b be object st [a, b] in G by XTUPLE_0:def 12;

            hence thesis by A11;

          end;

          let a be object;

          assume

           A13: a in B;

          then

          reconsider a9 = a as Ordinal by Th9;

          consider L such that

           A14: ( dom L) = a9 & for D st D in a9 holds (L . D) = H(|) by A2, A13;

          for A holds for K be Sequence holds A = a9 & K = L implies ( dom K) = A & for B holds B in A implies (K . B) = H(|) by A14;

          then [a9, L] in G by A11, A13;

          hence thesis by XTUPLE_0:def 12;

        end;

        

         A15: for a be object st a in B holds ex b be object st R[a, b]

        proof

          let a be object;

          assume a in B;

          then

          consider c be object such that

           A16: [a, c] in G by A12, XTUPLE_0:def 12;

          reconsider L = c as Sequence by A11, A16;

          take H(L), L;

          thus L = (G . a) by A16, FUNCT_1: 1;

          thus thesis;

        end;

        

         A17: for a,b,c be object st a in B & R[a, b] & R[a, c] holds b = c;

        consider F such that

         A18: ( dom F) = B & for a be object st a in B holds R[a, (F . a)] from FUNCT_1:sch 2( A17, A15);

        reconsider L = F as Sequence by A18, Def7;

        take L;

        thus ( dom L) = B by A18;

        let D;

        assume

         A19: D in B;

        then

        consider K be Sequence such that

         A20: K = (G . D) and

         A21: (F . D) = H(K) by A18;

        

         A22: [D, K] in G by A12, A19, A20, FUNCT_1: 1;

        then

         A23: ( dom K) = D by A11;

         A24:

        now

          let C;

          assume

           A25: C in D;

           A26:

          now

            let A, L such that

             A27: A = C and

             A28: L = (K | C);

            

             A29: C c= D by A25, Def2;

            hence

             A30: ( dom L) = A by A23, A27, A28, RELAT_1: 62;

            let B;

            assume

             A31: B in A;

            then B c= A by Def2;

            then

             A32: (K | B) = (L | B) by A27, A28, FUNCT_1: 51;

            (K . B) = H(|) by A11, A22, A27, A29, A31;

            hence (L . B) = H(|) by A28, A30, A31, A32, FUNCT_1: 47;

          end;

          C in B by A19, A25, Th6;

          then [C, (K | C)] in G by A11, A26;

          hence (G . C) = (K | C) by FUNCT_1: 1;

        end;

         A33:

        now

          let a be object;

          assume

           A34: a in D;

          then

          reconsider A = a as Ordinal by Th9;

          

           A35: (G . A) = (K | A) & ((L | D) . A) = (L . A) by A24, A34, FUNCT_1: 49;

          ex J be Sequence st J = (G . A) & (F . A) = H(J) by A18, A19, A34, Th6;

          hence ((L | D) . a) = (K . a) by A11, A22, A34, A35;

        end;

        D c= ( dom L) by A18, A19, Def2;

        then ( dom (L | D)) = D by RELAT_1: 62;

        hence thesis by A21, A23, A33, FUNCT_1: 2;

      end;

      for A holds S[A] from TransfiniteInd( A1);

      then

      consider L such that

       A36: ( dom L) = A() and

       A37: for B st B in A() holds (L . B) = H(|);

      take L;

      thus ( dom L) = A() by A36;

      let B, L1;

      assume B in A() & L1 = (L | B);

      hence thesis by A37;

    end;

    scheme :: ORDINAL1:sch5

    FuncTS { L() -> Sequence , F( Ordinal) -> set , H( Sequence) -> set } :

for B st B in ( dom L()) holds (L() . B) = H(|)

      provided

       A1: for A, a holds a = F(A) iff ex L st a = H(L) & ( dom L) = A & for B st B in A holds (L . B) = H(|)

       and

       A2: for A st A in ( dom L()) holds (L() . A) = F(A);

      consider L such that F(dom) = H(L) and

       A3: ( dom L) = ( dom L()) and

       A4: for B st B in ( dom L()) holds (L . B) = H(|) by A1;

      now

        let b be object;

        assume

         A5: b in ( dom L);

        then

        reconsider B = b as Ordinal by Th9;

        now

          take K = (L | B);

          thus H(|) = H(K);

          

           A6: B c= ( dom L) by A5, Def2;

          hence ( dom K) = B by RELAT_1: 62;

          let C;

          assume

           A7: C in B;

          then C c= B by Def2;

          then

           A8: (L | C) = (K | C) by FUNCT_1: 51;

          (K . C) = (L . C) by A7, FUNCT_1: 49;

          hence (K . C) = H(|) by A3, A4, A6, A7, A8;

        end;

        

        then F(B) = H(|) by A1

        .= (L . B) by A3, A4, A5;

        hence (L() . b) = (L . b) by A2, A3, A5;

      end;

      then L() = L by A3;

      hence thesis by A4;

    end;

    theorem :: ORDINAL1:35

    A c< B or A = B or B c< A

    proof

      assume that

       A1: ( not A c< B) & not A = B and

       A2: not B c< A;

       not A c= B by A1;

      hence contradiction by A2;

    end;

    begin

    definition

      let X;

      :: ORDINAL1:def9

      func On X -> set means

      : Def9: for x be object holds x in it iff x in X & x is Ordinal;

      existence

      proof

        defpred P[ object] means $1 is Ordinal;

        thus ex Y be set st for x be object holds x in Y iff x in X & P[x] from XBOOLE_0:sch 1;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 in X & $1 is Ordinal;

        let Y, Z such that

         A1: for x be object holds x in Y iff P[x] and

         A2: for x be object holds x in Z iff P[x];

        thus Y = Z from XBOOLE_0:sch 2( A1, A2);

      end;

      :: ORDINAL1:def10

      func Lim X -> set means for x be object holds x in it iff x in X & ex A st x = A & A is limit_ordinal;

      existence

      proof

        defpred P[ object] means ex A st $1 = A & A is limit_ordinal;

        thus ex Y be set st for x be object holds x in Y iff x in X & P[x] from XBOOLE_0:sch 1;

      end;

      uniqueness

      proof

        defpred P[ object] means $1 in X & ex A st $1 = A & A is limit_ordinal;

        let Y, Z such that

         A3: for x be object holds x in Y iff P[x] and

         A4: for x be object holds x in Z iff P[x];

        thus Y = Z from XBOOLE_0:sch 2( A3, A4);

      end;

    end

    ::$Notion-Name

    theorem :: ORDINAL1:36

    

     Th32: for D holds ex A st D in A & A is limit_ordinal

    proof

      let D;

      consider Field be set such that

       A1: D in Field and

       A2: for X, Y holds X in Field & Y c= X implies Y in Field and

       A3: for X holds X in Field implies ( bool X) in Field and for X holds X c= Field implies (X,Field) are_equipotent or X in Field by ZFMISC_1: 112;

      for X st X in ( On Field) holds X is Ordinal & X c= ( On Field)

      proof

        let X;

        assume

         A4: X in ( On Field);

        then

        reconsider A = X as Ordinal by Def9;

        

         A5: A in Field by A4, Def9;

        thus X is Ordinal by A4, Def9;

        let y be object;

        assume

         A6: y in X;

        then y in A;

        then

        reconsider B = y as Ordinal by Th9;

        B c= A by A6, Def2;

        then B in Field by A2, A5;

        hence thesis by Def9;

      end;

      then

      reconsider ON = ( On Field) as epsilon-transitive epsilon-connected set by Th15;

      take ON;

      thus D in ON by A1, Def9;

      A in ON implies ( succ A) in ON

      proof

        

         A7: ( succ A) c= ( bool A)

        proof

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          assume x in ( succ A);

          then x in A or x = A by Th4;

          then xx c= A by Def2;

          hence thesis;

        end;

        assume A in ON;

        then A in Field by Def9;

        then ( bool A) in Field by A3;

        then ( succ A) in Field by A2, A7;

        hence thesis by Def9;

      end;

      hence thesis by Th24;

    end;

    definition

      :: ORDINAL1:def11

      func omega -> set means

      : Def11: {} in it & it is limit_ordinal & it is ordinal & for A st {} in A & A is limit_ordinal holds it c= A;

      existence

      proof

        defpred P[ Ordinal] means {} in $1 & $1 is limit_ordinal;

        

         A1: ex A st P[A] by Th32;

        ex C st P[C] & for A st P[A] holds C c= A from OrdinalMin( A1);

        hence thesis;

      end;

      uniqueness ;

    end

    registration

      cluster omega -> non empty ordinal;

      coherence by Def11;

    end

    definition

      let A be object;

      :: ORDINAL1:def12

      attr A is natural means

      : Def12: A in omega ;

    end

    registration

      cluster natural for Number;

      existence

      proof

        take the Element of omega ;

        thus thesis;

      end;

      cluster natural for set;

      existence

      proof

        take the Element of omega ;

        thus thesis;

      end;

    end

    definition

      mode Nat is natural set;

    end

    registration

      sethood of Nat

      proof

        take omega ;

        let y be Nat;

        thus y in omega by Def12;

      end;

    end

    registration

      let A be Ordinal;

      cluster -> ordinal for Element of A;

      coherence

      proof

        let x be Element of A;

        A is empty or A is non empty;

        hence thesis by Th9, SUBSET_1:def 1;

      end;

    end

    registration

      cluster natural -> ordinal for number;

      coherence ;

    end

    scheme :: ORDINAL1:sch6

    ALFA { D() -> non empty set , P[ object, object] } :

ex F st ( dom F) = D() & for d be Element of D() holds ex A st A = (F . d) & P[d, A] & for B st P[d, B] holds A c= B

      provided

       A1: for d be Element of D() holds ex A st P[d, A];

      defpred Q[ object, object] means ex A st A = $2 & P[$1, A] & for B st P[$1, B] holds A c= B;

      

       A2: for x be object st x in D() holds ex y be object st Q[x, y]

      proof

        let x be object;

        assume x in D();

        then

        reconsider d = x as Element of D();

        defpred Q[ Ordinal] means P[d, $1];

        

         A3: ex A st Q[A] by A1;

        consider A such that

         A4: Q[A] & for B st Q[B] holds A c= B from OrdinalMin( A3);

        reconsider y = A as set;

        take y, A;

        thus thesis by A4;

      end;

      

       A5: for x,y,z be object st x in D() & Q[x, y] & Q[x, z] holds y = z

      proof

        let x,y,z be object such that x in D();

        given A1 be Ordinal such that

         A6: A1 = y and

         A7: P[x, A1] & for B st P[x, B] holds A1 c= B;

        given A2 be Ordinal such that

         A8: A2 = z and

         A9: P[x, A2] & for B st P[x, B] holds A2 c= B;

        A1 c= A2 & A2 c= A1 by A7, A9;

        hence thesis by A6, A8, XBOOLE_0:def 10;

      end;

      consider F such that

       A10: ( dom F) = D() & for x be object st x in D() holds Q[x, (F . x)] from FUNCT_1:sch 2( A5, A2);

      take F;

      thus ( dom F) = D() by A10;

      let d be Element of D();

      thus thesis by A10;

    end;

    theorem :: ORDINAL1:37

    (( succ X) \ {X}) = X

    proof

      thus (( succ X) \ {X}) c= X

      proof

        let x be object;

        assume

         A1: x in (( succ X) \ {X});

        then

         A2: not x in {X} by XBOOLE_0:def 5;

        x in X or x = X by A1, Th4;

        hence thesis by A2, TARSKI:def 1;

      end;

      let x be object;

      assume

       A3: x in X;

      then

      reconsider xx = x as set;

       not xx in xx;

      then x <> X by A3;

      then

       A4: not x in {X} by TARSKI:def 1;

      x in ( succ X) by A3, Th4;

      hence thesis by A4, XBOOLE_0:def 5;

    end;

    registration

      cluster empty -> natural for number;

      coherence by Def11;

      cluster -> natural for Element of omega ;

      coherence ;

    end

    registration

      cluster non empty natural for number;

      existence

      proof

        take ( succ {} );

        thus ( succ {} ) is non empty;

         omega is limit_ordinal & {} in omega by Def11;

        hence ( succ {} ) in omega by Th24;

      end;

    end

    registration

      let a be natural Ordinal;

      cluster ( succ a) -> natural;

      coherence

      proof

         omega is limit_ordinal & a in omega by Def11, Def12;

        hence ( succ a) in omega by Th24;

      end;

    end

    registration

      cluster empty -> c=-linear for set;

      coherence ;

    end

    registration

      let X be c=-linear set;

      cluster -> c=-linear for Subset of X;

      coherence by Def8;

    end

    ::$Canceled

    definition

      :: ORDINAL1:def13

      func 0 -> number equals {} ;

      coherence ;

    end

    registration

      cluster 0 -> natural;

      coherence ;

    end

    definition

      let x be Number;

      :: ORDINAL1:def14

      attr x is zero means

      : Def14: x = 0 ;

    end

    registration

      cluster 0 -> zero;

      coherence ;

      cluster zero for Number;

      existence

      proof

        take 0 ;

        thus 0 = 0 ;

      end;

      cluster zero for set;

      existence

      proof

        take 0 ;

        thus 0 = 0 ;

      end;

    end

    registration

      cluster zero -> natural for Number;

      coherence ;

    end

    registration

      cluster non zero for Number;

      existence

      proof

        take { 0 };

        thus { 0 } <> 0 ;

      end;

    end

    registration

      cluster zero -> trivial for set;

      coherence ;

      cluster non trivial -> non zero for set;

      coherence ;

    end

    definition

      let R be Relation;

      :: ORDINAL1:def15

      attr R is non-zero means

      : Def15: not 0 in ( rng R);

    end

    definition

      let X be set;

      :: ORDINAL1:def16

      attr X is with_zero means

      : Def16: 0 in X;

    end

    notation

      let X be set;

      antonym X is without_zero for X is with_zero;

    end

    registration

      cluster empty -> without_zero for set;

      coherence ;

    end

    registration

      cluster empty -> non-zero for Relation;

      coherence ;

    end

    registration

      cluster without_zero non empty for set;

      existence

      proof

        take { { 0 }};

        thus not 0 in { { 0 }} by TARSKI:def 1;

        thus thesis;

      end;

    end

    registration

      let X be without_zero non empty set;

      cluster -> non zero for Element of X;

      coherence by Def16;

    end

    registration

      cluster non-zero for Relation;

      existence

      proof

        take {} ;

        thus not 0 in ( rng {} );

      end;

      cluster non non-zero for Relation;

      existence

      proof

        take R = { [ 0 , 0 ]};

         [ 0 , 0 ] in R by TARSKI:def 1;

        hence 0 in ( rng R) by XTUPLE_0:def 13;

      end;

    end

    registration

      let R be non-zero Relation;

      cluster ( rng R) -> without_zero;

      coherence by Def15;

    end

    registration

      let R be non non-zero Relation;

      cluster ( rng R) -> with_zero;

      coherence by Def15;

    end

    registration

      let R be non-zero Relation, S be Relation;

      cluster (S * R) -> non-zero;

      coherence

      proof

        ( rng (S * R)) c= ( rng R) by RELAT_1: 26;

        hence not 0 in ( rng (S * R));

      end;

    end

    registration

      cluster without_zero -> with_non-empty_elements for set;

      coherence

      proof

        let X be set;

        assume X is without_zero;

        hence not {} in X;

      end;

      cluster with_zero -> non with_non-empty_elements for set;

      coherence

      proof

        let X be set;

        assume X is with_zero;

        hence {} in X;

      end;

      cluster with_non-empty_elements -> without_zero for set;

      coherence ;

      cluster non with_non-empty_elements -> with_zero for set;

      coherence ;

    end

    definition

      let o be object;

      :: ORDINAL1:def17

      func Segm o -> set equals o;

      coherence by TARSKI: 1;

    end

    registration

      let n be Ordinal;

      cluster ( Segm n) -> ordinal;

      coherence ;

    end

    registration

      let n be zero Ordinal;

      cluster ( Segm n) -> empty;

      coherence by Def14;

    end