ordinal3.miz



    begin

    reserve fi,psi for Ordinal-Sequence,

A,A1,B,C,D for Ordinal,

X,Y for set,

x,y for object;

    theorem :: ORDINAL3:1

    X c= ( succ X) by XBOOLE_1: 7;

    theorem :: ORDINAL3:2

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

    proof

      X c= ( succ X) by XBOOLE_1: 7;

      hence thesis;

    end;

    theorem :: ORDINAL3:3

    A in B iff ( succ A) in ( succ B)

    proof

      A in B iff ( succ A) c= B by ORDINAL1: 21;

      hence thesis by ORDINAL1: 22;

    end;

    theorem :: ORDINAL3:4

    X c= A implies ( union X) is epsilon-transitive epsilon-connected set

    proof

      assume X c= A;

      then for x st x in X holds x is Ordinal;

      hence thesis by ORDINAL1: 23;

    end;

    theorem :: ORDINAL3:5

    

     Th5: ( union ( On X)) is epsilon-transitive epsilon-connected set

    proof

      x in ( On X) implies x is Ordinal by ORDINAL1:def 9;

      hence thesis by ORDINAL1: 23;

    end;

    theorem :: ORDINAL3:6

    

     Th6: X c= A implies ( On X) = X

    proof

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

      assume X c= A;

      then

       A1: for x be object holds x in X iff P[x];

      

       A2: for x be object holds x in ( On X) iff P[x] by ORDINAL1:def 9;

      thus thesis from XBOOLE_0:sch 2( A2, A1);

    end;

    theorem :: ORDINAL3:7

    

     Th7: ( On {A}) = {A}

    proof

       {A} c= ( succ A) by XBOOLE_1: 7;

      hence thesis by Th6;

    end;

    theorem :: ORDINAL3:8

    

     Th8: A <> {} implies {} in A

    proof

      

       A1: {} c= A;

      assume A <> {} ;

      then {} c< A by A1;

      hence thesis by ORDINAL1: 11;

    end;

    theorem :: ORDINAL3:9

    ( inf A) = {}

    proof

      

       A1: ( inf A) = ( meet A) by ORDINAL2: 8;

      then A <> {} implies thesis by Th8, SETFAM_1: 4;

      hence thesis by A1, SETFAM_1:def 1;

    end;

    theorem :: ORDINAL3:10

    ( inf {A}) = A

    proof

      

      thus ( inf {A}) = ( meet {A}) by Th7

      .= A by SETFAM_1: 10;

    end;

    theorem :: ORDINAL3:11

    X c= A implies ( meet X) is Ordinal

    proof

      assume X c= A;

      then ( inf X) = ( meet X) by Th6;

      hence thesis;

    end;

    registration

      let A, B;

      cluster (A \/ B) -> ordinal;

      coherence

      proof

        A c= B or B c= A;

        hence thesis by XBOOLE_1: 12;

      end;

      cluster (A /\ B) -> ordinal;

      coherence

      proof

        A c= B or B c= A;

        hence thesis by XBOOLE_1: 28;

      end;

    end

    theorem :: ORDINAL3:12

    (A \/ B) = A or (A \/ B) = B

    proof

      A c= B or B c= A;

      hence thesis by XBOOLE_1: 12;

    end;

    theorem :: ORDINAL3:13

    (A /\ B) = A or (A /\ B) = B

    proof

      A c= B or B c= A;

      hence thesis by XBOOLE_1: 28;

    end;

    

     Lm1: 1 = ( succ 0 );

    theorem :: ORDINAL3:14

    

     Th14: A in 1 implies A = {}

    proof

      assume A in 1;

      hence A c= {} & {} c= A by Lm1, ORDINAL1: 22;

    end;

    theorem :: ORDINAL3:15

    1 = { {} } by Lm1;

    theorem :: ORDINAL3:16

    

     Th16: A c= 1 implies A = {} or A = 1

    proof

      assume that

       A1: A c= 1 and

       A2: A <> {} and

       A3: A <> 1;

      A c< 1 by A1, A3;

      hence contradiction by A2, Th14, ORDINAL1: 11;

    end;

    theorem :: ORDINAL3:17

    (A c= B or A in B) & C in D implies (A +^ C) in (B +^ D)

    proof

      assume that

       A1: A c= B or A in B and

       A2: C in D;

      

       A3: (B +^ C) in (B +^ D) by A2, ORDINAL2: 32;

      A c= B by A1, ORDINAL1:def 2;

      hence thesis by A3, ORDINAL1: 12, ORDINAL2: 34;

    end;

    theorem :: ORDINAL3:18

    A c= B & C c= D implies (A +^ C) c= (B +^ D)

    proof

      assume that

       A1: A c= B and

       A2: C c= D;

      

       A3: (B +^ C) c= (B +^ D) by A2, ORDINAL2: 33;

      (A +^ C) c= (B +^ C) by A1, ORDINAL2: 34;

      hence thesis by A3;

    end;

    theorem :: ORDINAL3:19

    

     Th19: A in B & (C c= D & D <> {} or C in D) implies (A *^ C) in (B *^ D)

    proof

      assume that

       A1: A in B and

       A2: C c= D & D <> {} or C in D;

      

       A3: C c= D by A2, ORDINAL1:def 2;

      (A *^ D) in (B *^ D) by A1, A2, ORDINAL2: 40;

      hence thesis by A3, ORDINAL1: 12, ORDINAL2: 42;

    end;

    theorem :: ORDINAL3:20

    A c= B & C c= D implies (A *^ C) c= (B *^ D)

    proof

      assume that

       A1: A c= B and

       A2: C c= D;

      

       A3: (B *^ C) c= (B *^ D) by A2, ORDINAL2: 42;

      (A *^ C) c= (B *^ C) by A1, ORDINAL2: 41;

      hence thesis by A3;

    end;

    theorem :: ORDINAL3:21

    

     Th21: (B +^ C) = (B +^ D) implies C = D

    proof

      assume that

       A1: (B +^ C) = (B +^ D) and

       A2: C <> D;

      C in D or D in C by A2, ORDINAL1: 14;

      then (B +^ C) in (B +^ C) by A1, ORDINAL2: 32;

      hence contradiction;

    end;

    theorem :: ORDINAL3:22

    

     Th22: (B +^ C) in (B +^ D) implies C in D

    proof

      assume that

       A1: (B +^ C) in (B +^ D) and

       A2: not C in D;

      D c= C by A2, ORDINAL1: 16;

      hence contradiction by A1, ORDINAL1: 5, ORDINAL2: 33;

    end;

    theorem :: ORDINAL3:23

    

     Th23: (B +^ C) c= (B +^ D) implies C c= D

    proof

      assume

       A1: (B +^ C) c= (B +^ D);

      (B +^ C) c= (B +^ D) & (B +^ C) <> (B +^ D) iff (B +^ C) c< (B +^ D);

      then C = D or C in D by A1, Th21, Th22, ORDINAL1: 11;

      hence thesis by ORDINAL1:def 2;

    end;

    theorem :: ORDINAL3:24

    

     Th24: A c= (A +^ B) & B c= (A +^ B)

    proof

      

       A1: ( {} +^ B) c= (A +^ B) by ORDINAL2: 34, XBOOLE_1: 2;

      (A +^ {} ) c= (A +^ B) by ORDINAL2: 33, XBOOLE_1: 2;

      hence thesis by A1, ORDINAL2: 27, ORDINAL2: 30;

    end;

    theorem :: ORDINAL3:25

    A in B implies A in (B +^ C) & A in (C +^ B)

    proof

      assume

       A1: A in B;

      

       A2: B c= (C +^ B) by Th24;

      B c= (B +^ C) by Th24;

      hence thesis by A1, A2;

    end;

    theorem :: ORDINAL3:26

    

     Th26: (A +^ B) = {} implies A = {} & B = {} by Th24, XBOOLE_1: 3;

    theorem :: ORDINAL3:27

    

     Th27: A c= B implies ex C st B = (A +^ C)

    proof

      defpred P[ Ordinal] means A c= $1 implies ex C st $1 = (A +^ C);

      

       A1: for B st P[B] holds P[( succ B)]

      proof

        let B such that

         A2: A c= B implies ex C st B = (A +^ C) and

         A3: A c= ( succ B);

         A4:

        now

          assume A <> ( succ B);

          then A c< ( succ B) by A3;

          then A in ( succ B) by ORDINAL1: 11;

          then

          consider C such that

           A5: B = (A +^ C) by A2, ORDINAL1: 22;

          ( succ B) = (A +^ ( succ C)) by A5, ORDINAL2: 28;

          hence thesis;

        end;

        A = ( succ B) implies ( succ B) = (A +^ {} ) by ORDINAL2: 27;

        hence thesis by A4;

      end;

      

       A6: for B st B <> 0 & B is limit_ordinal & for C st C in B holds P[C] holds P[B]

      proof

        deffunc F( Ordinal) = (A +^ $1);

        let B such that B <> 0 and

         A7: B is limit_ordinal and for C st C in B holds A c= C implies ex D st C = (A +^ D) and

         A8: A c= B;

        defpred P[ Ordinal] means B c= (A +^ $1);

        

         A9: B = ( {} +^ B) by ORDINAL2: 30;

        ( {} +^ B) c= (A +^ B) by ORDINAL2: 34, XBOOLE_1: 2;

        then

         A10: ex C st P[C] by A9;

        consider C such that

         A11: P[C] & for D st P[D] holds C c= D from ORDINAL1:sch 1( A10);

        consider L be Ordinal-Sequence such that

         A12: ( dom L) = C & for D st D in C holds (L . D) = F(D) from ORDINAL2:sch 3;

         A13:

        now

          for D st D in ( rng L) holds D in B

          proof

            let D;

            assume D in ( rng L);

            then

            consider y be object such that

             A14: y in ( dom L) and

             A15: D = (L . y) by FUNCT_1:def 3;

            reconsider y as Ordinal by A14;

            

             A16: not C c= y by A12, A14, ORDINAL1: 5;

            (L . y) = (A +^ y) by A12, A14;

            hence thesis by A11, A15, A16, ORDINAL1: 16;

          end;

          then

           A17: ( sup ( rng L)) c= B by ORDINAL2: 20;

          

           A18: C is limit_ordinal

          proof

            assume not thesis;

            then

            consider D such that

             A19: C = ( succ D) by ORDINAL1: 29;

             not C c= D by A19, ORDINAL1: 5, ORDINAL1: 6;

            then (A +^ D) in B by A11, ORDINAL1: 16;

            then

             A20: ( succ (A +^ D)) c= B by ORDINAL1: 21;

            ( succ (A +^ D)) = (A +^ ( succ D)) by ORDINAL2: 28;

            then B = ( succ (A +^ D)) by A11, A19, A20;

            hence contradiction by A7, ORDINAL1: 29;

          end;

          assume C <> {} ;

          

          then (A +^ C) = ( sup L) by A12, A18, ORDINAL2: 29

          .= ( sup ( rng L));

          then B = (A +^ C) by A11, A17;

          hence thesis;

        end;

        C = {} implies B = (A +^ {} ) by A8, A11, ORDINAL2: 27;

        hence thesis by A13;

      end;

      

       A21: P[ 0 ]

      proof

        assume A c= 0 ;

        then A = {} by XBOOLE_1: 3;

        then {} = (A +^ {} ) by ORDINAL2: 30;

        hence thesis;

      end;

      for B holds P[B] from ORDINAL2:sch 1( A21, A1, A6);

      hence thesis;

    end;

    theorem :: ORDINAL3:28

    

     Th28: A in B implies ex C st B = (A +^ C) & C <> {}

    proof

      assume

       A1: A in B;

      then A c= B by ORDINAL1:def 2;

      then

      consider C such that

       A2: B = (A +^ C) by Th27;

      take C;

      thus B = (A +^ C) by A2;

      assume C = {} ;

      then B = A by A2, ORDINAL2: 27;

      hence contradiction by A1;

    end;

    theorem :: ORDINAL3:29

    

     Th29: A <> {} & A is limit_ordinal implies (B +^ A) is limit_ordinal

    proof

      assume that

       A1: A <> {} and

       A2: A is limit_ordinal;

       {} c= A;

      then

       A3: {} c< A by A1;

      deffunc F( Ordinal) = (B +^ $1);

      consider L be Ordinal-Sequence such that

       A4: ( dom L) = A & for C st C in A holds (L . C) = F(C) from ORDINAL2:sch 3;

      

       A5: (B +^ A) = ( sup L) by A1, A2, A4, ORDINAL2: 29

      .= ( sup ( rng L));

      for C st C in (B +^ A) holds ( succ C) in (B +^ A)

      proof

        let C such that

         A6: C in (B +^ A);

         A7:

        now

          assume not C in B;

          then

          consider D such that

           A8: C = (B +^ D) by Th27, ORDINAL1: 16;

          now

            assume not D in A;

            then (B +^ A) c= (B +^ D) by ORDINAL1: 16, ORDINAL2: 33;

            then C in C by A6, A8;

            hence contradiction;

          end;

          then

           A9: ( succ D) in A by A2, ORDINAL1: 28;

          

          then (L . ( succ D)) = (B +^ ( succ D)) by A4

          .= ( succ (B +^ D)) by ORDINAL2: 28;

          then ( succ C) in ( rng L) by A4, A8, A9, FUNCT_1:def 3;

          hence thesis by A5, ORDINAL2: 19;

        end;

        now

          assume C in B;

          then

           A10: ( succ C) c= B by ORDINAL1: 21;

          

           A11: (( succ C) +^ {} ) = ( succ C) by ORDINAL2: 27;

          (B +^ {} ) in (B +^ A) by A3, ORDINAL1: 11, ORDINAL2: 32;

          hence thesis by A10, A11, ORDINAL1: 12, ORDINAL2: 34;

        end;

        hence thesis by A7;

      end;

      hence thesis by ORDINAL1: 28;

    end;

    theorem :: ORDINAL3:30

    

     Th30: ((A +^ B) +^ C) = (A +^ (B +^ C))

    proof

      defpred Sigma[ Ordinal] means ((A +^ B) +^ $1) = (A +^ (B +^ $1));

      

       A1: for C st Sigma[C] holds Sigma[( succ C)]

      proof

        let C such that

         A2: ((A +^ B) +^ C) = (A +^ (B +^ C));

        

        thus ((A +^ B) +^ ( succ C)) = ( succ ((A +^ B) +^ C)) by ORDINAL2: 28

        .= (A +^ ( succ (B +^ C))) by A2, ORDINAL2: 28

        .= (A +^ (B +^ ( succ C))) by ORDINAL2: 28;

      end;

      

       A3: for C st C <> 0 & C is limit_ordinal & for D st D in C holds Sigma[D] holds Sigma[C]

      proof

        deffunc F( Ordinal) = ((A +^ B) +^ $1);

        let C such that

         A4: C <> 0 and

         A5: C is limit_ordinal and

         A6: for D st D in C holds Sigma[D];

        consider L be Ordinal-Sequence such that

         A7: ( dom L) = C & for D st D in C holds (L . D) = F(D) from ORDINAL2:sch 3;

        deffunc F( Ordinal) = (A +^ $1);

        consider L1 be Ordinal-Sequence such that

         A8: ( dom L1) = (B +^ C) & for D st D in (B +^ C) holds (L1 . D) = F(D) from ORDINAL2:sch 3;

        

         A9: ( rng L) c= ( rng L1)

        proof

          let x be object;

          assume x in ( rng L);

          then

          consider y be object such that

           A10: y in ( dom L) and

           A11: x = (L . y) by FUNCT_1:def 3;

          reconsider y as Ordinal by A10;

          

           A12: (B +^ y) in (B +^ C) by A7, A10, ORDINAL2: 32;

          (L . y) = ((A +^ B) +^ y) by A7, A10;

          then

           A13: (L . y) = (A +^ (B +^ y)) by A6, A7, A10;

          (L1 . (B +^ y)) = (A +^ (B +^ y)) by A7, A8, A10, ORDINAL2: 32;

          hence thesis by A8, A11, A13, A12, FUNCT_1:def 3;

        end;

        

         A14: (B +^ C) <> {} by A4, Th26;

        (B +^ C) is limit_ordinal by A4, A5, Th29;

        

        then

         A15: (A +^ (B +^ C)) = ( sup L1) by A8, A14, ORDINAL2: 29

        .= ( sup ( rng L1));

        ((A +^ B) +^ C) = ( sup L) by A4, A5, A7, ORDINAL2: 29

        .= ( sup ( rng L));

        hence ((A +^ B) +^ C) c= (A +^ (B +^ C)) by A15, A9, ORDINAL2: 22;

        let x be object;

        assume

         A16: x in (A +^ (B +^ C));

        then

        reconsider x9 = x as Ordinal;

         A17:

        now

          

           A18: A c= (A +^ B) by Th24;

          assume

           A19: not x in (A +^ B);

          then (A +^ B) c= x9 by ORDINAL1: 16;

          then

          consider E be Ordinal such that

           A20: x9 = (A +^ E) by A18, Th27, XBOOLE_1: 1;

          B c= E by A19, A20, ORDINAL1: 16, ORDINAL2: 32;

          then

          consider F be Ordinal such that

           A21: E = (B +^ F) by Th27;

           A22:

          now

            assume not F in C;

            then (B +^ C) c= (B +^ F) by ORDINAL1: 16, ORDINAL2: 33;

            then (A +^ (B +^ C)) c= (A +^ (B +^ F)) by ORDINAL2: 33;

            then x9 in x9 by A16, A20, A21;

            hence contradiction;

          end;

          then x = ((A +^ B) +^ F) by A6, A20, A21;

          hence thesis by A22, ORDINAL2: 32;

        end;

        

         A23: ((A +^ B) +^ {} ) = (A +^ B) by ORDINAL2: 27;

        ((A +^ B) +^ {} ) c= ((A +^ B) +^ C) by ORDINAL2: 33, XBOOLE_1: 2;

        hence thesis by A23, A17;

      end;

      ((A +^ B) +^ {} ) = (A +^ B) by ORDINAL2: 27

      .= (A +^ (B +^ {} )) by ORDINAL2: 27;

      then

       A24: Sigma[ 0 ];

      for C holds Sigma[C] from ORDINAL2:sch 1( A24, A1, A3);

      hence thesis;

    end;

    theorem :: ORDINAL3:31

    (A *^ B) = {} implies A = {} or B = {}

    proof

      assume that

       A1: (A *^ B) = {} and

       A2: A <> {} and

       A3: B <> {} ;

       {} c= A;

      then {} c< A by A2;

      hence contradiction by A1, A3, ORDINAL1: 11, ORDINAL2: 40;

    end;

    theorem :: ORDINAL3:32

    A in B & C <> {} implies A in (B *^ C) & A in (C *^ B)

    proof

      assume that

       A1: A in B and

       A2: C <> {} ;

       {} c= C;

      then {} c< C by A2;

      then {} in C by ORDINAL1: 11;

      then

       A3: 1 c= C by Lm1, ORDINAL1: 21;

      then

       A4: (1 *^ B) c= (C *^ B) by ORDINAL2: 41;

      

       A5: (1 *^ B) = B by ORDINAL2: 39;

      

       A6: (B *^ 1) = B by ORDINAL2: 39;

      (B *^ 1) c= (B *^ C) by A3, ORDINAL2: 42;

      hence thesis by A1, A4, A6, A5;

    end;

    theorem :: ORDINAL3:33

    

     Th33: (B *^ A) = (C *^ A) & A <> {} implies B = C

    proof

      assume that

       A1: (B *^ A) = (C *^ A) and

       A2: A <> {} and

       A3: B <> C;

      B in C or C in B by A3, ORDINAL1: 14;

      then (B *^ A) in (B *^ A) by A1, A2, ORDINAL2: 40;

      hence contradiction;

    end;

    theorem :: ORDINAL3:34

    

     Th34: (B *^ A) in (C *^ A) implies B in C

    proof

      assume that

       A1: (B *^ A) in (C *^ A) and

       A2: not B in C;

      C c= B by A2, ORDINAL1: 16;

      hence contradiction by A1, ORDINAL1: 5, ORDINAL2: 41;

    end;

    theorem :: ORDINAL3:35

    

     Th35: (B *^ A) c= (C *^ A) & A <> {} implies B c= C

    proof

      assume

       A1: (B *^ A) c= (C *^ A);

      (B *^ A) c= (C *^ A) & (B *^ A) <> (C *^ A) iff (B *^ A) c< (C *^ A);

      then (A <> {} implies B = C) or B in C by A1, Th33, Th34, ORDINAL1: 11;

      hence thesis by ORDINAL1:def 2;

    end;

    theorem :: ORDINAL3:36

    

     Th36: B <> {} implies A c= (A *^ B) & A c= (B *^ A)

    proof

      assume B <> {} ;

      then {} in B by Th8;

      then

       A1: 1 c= B by Lm1, ORDINAL1: 21;

      then

       A2: (A *^ 1) c= (A *^ B) by ORDINAL2: 42;

      (1 *^ A) c= (B *^ A) by A1, ORDINAL2: 41;

      hence thesis by A2, ORDINAL2: 39;

    end;

    theorem :: ORDINAL3:37

    (A *^ B) = 1 implies A = 1 & B = 1

    proof

      assume

       A1: (A *^ B) = 1;

      then

       A2: B <> {} by ORDINAL2: 38;

       {} c= B;

      then {} c< B by A2;

      then {} in B by ORDINAL1: 11;

      then

       A3: 1 c= B by Lm1, ORDINAL1: 21;

       A4:

      now

        

         A5: B = (1 *^ B) by ORDINAL2: 39;

        assume 1 in A;

        hence contradiction by A1, A2, A3, A5, ORDINAL1: 5, ORDINAL2: 40;

      end;

      now

        assume A in 1;

        then A c= {} by Lm1, ORDINAL1: 22;

        then A = {} by XBOOLE_1: 3;

        hence contradiction by A1, ORDINAL2: 35;

      end;

      hence A = 1 by A4, ORDINAL1: 14;

      hence thesis by A1, ORDINAL2: 39;

    end;

    theorem :: ORDINAL3:38

    

     Th38: A in (B +^ C) implies A in B or ex D st D in C & A = (B +^ D)

    proof

      assume that

       A1: A in (B +^ C) and

       A2: not A in B;

      consider D such that

       A3: A = (B +^ D) by A2, Th27, ORDINAL1: 16;

      take D;

      assume not thesis;

      then C c= D by A3, ORDINAL1: 16;

      hence contradiction by A1, A3, ORDINAL1: 5, ORDINAL2: 33;

    end;

    definition

      let C, fi;

      :: ORDINAL3:def1

      func C +^ fi -> Ordinal-Sequence means

      : Def1: ( dom it ) = ( dom fi) & for A st A in ( dom fi) holds (it . A) = (C +^ (fi . A));

      existence

      proof

        deffunc F( Ordinal) = (C +^ (fi . $1));

        thus ex F be Ordinal-Sequence st ( dom F) = ( dom fi) & for A st A in ( dom fi) holds (F . A) = F(A) from ORDINAL2:sch 3;

      end;

      uniqueness

      proof

        let f1,f2 be Ordinal-Sequence such that

         A1: ( dom f1) = ( dom fi) and

         A2: for A st A in ( dom fi) holds (f1 . A) = (C +^ (fi . A)) and

         A3: ( dom f2) = ( dom fi) and

         A4: for A st A in ( dom fi) holds (f2 . A) = (C +^ (fi . A));

        now

          let x be object;

          assume

           A5: x in ( dom fi);

          then

          reconsider A = x as Ordinal;

          

          thus (f1 . x) = (C +^ (fi . A)) by A2, A5

          .= (f2 . x) by A4, A5;

        end;

        hence thesis by A1, A3, FUNCT_1: 2;

      end;

      :: ORDINAL3:def2

      func fi +^ C -> Ordinal-Sequence means ( dom it ) = ( dom fi) & for A st A in ( dom fi) holds (it . A) = ((fi . A) +^ C);

      existence

      proof

        deffunc F( Ordinal) = ((fi . $1) +^ C);

        thus ex F be Ordinal-Sequence st ( dom F) = ( dom fi) & for A st A in ( dom fi) holds (F . A) = F(A) from ORDINAL2:sch 3;

      end;

      uniqueness

      proof

        let f1,f2 be Ordinal-Sequence such that

         A6: ( dom f1) = ( dom fi) and

         A7: for A st A in ( dom fi) holds (f1 . A) = ((fi . A) +^ C) and

         A8: ( dom f2) = ( dom fi) and

         A9: for A st A in ( dom fi) holds (f2 . A) = ((fi . A) +^ C);

        now

          let x be object;

          assume

           A10: x in ( dom fi);

          then

          reconsider A = x as Ordinal;

          

          thus (f1 . x) = ((fi . A) +^ C) by A7, A10

          .= (f2 . x) by A9, A10;

        end;

        hence thesis by A6, A8, FUNCT_1: 2;

      end;

      :: ORDINAL3:def3

      func C *^ fi -> Ordinal-Sequence means ( dom it ) = ( dom fi) & for A st A in ( dom fi) holds (it . A) = (C *^ (fi . A));

      existence

      proof

        deffunc F( Ordinal) = (C *^ (fi . $1));

        thus ex F be Ordinal-Sequence st ( dom F) = ( dom fi) & for A st A in ( dom fi) holds (F . A) = F(A) from ORDINAL2:sch 3;

      end;

      uniqueness

      proof

        let f1,f2 be Ordinal-Sequence such that

         A11: ( dom f1) = ( dom fi) and

         A12: for A st A in ( dom fi) holds (f1 . A) = (C *^ (fi . A)) and

         A13: ( dom f2) = ( dom fi) and

         A14: for A st A in ( dom fi) holds (f2 . A) = (C *^ (fi . A));

        now

          let x be object;

          assume

           A15: x in ( dom fi);

          then

          reconsider A = x as Ordinal;

          

          thus (f1 . x) = (C *^ (fi . A)) by A12, A15

          .= (f2 . x) by A14, A15;

        end;

        hence thesis by A11, A13, FUNCT_1: 2;

      end;

      :: ORDINAL3:def4

      func fi *^ C -> Ordinal-Sequence means

      : Def4: ( dom it ) = ( dom fi) & for A st A in ( dom fi) holds (it . A) = ((fi . A) *^ C);

      existence

      proof

        deffunc F( Ordinal) = ((fi . $1) *^ C);

        thus ex F be Ordinal-Sequence st ( dom F) = ( dom fi) & for A st A in ( dom fi) holds (F . A) = F(A) from ORDINAL2:sch 3;

      end;

      uniqueness

      proof

        let f1,f2 be Ordinal-Sequence such that

         A16: ( dom f1) = ( dom fi) and

         A17: for A st A in ( dom fi) holds (f1 . A) = ((fi . A) *^ C) and

         A18: ( dom f2) = ( dom fi) and

         A19: for A st A in ( dom fi) holds (f2 . A) = ((fi . A) *^ C);

        now

          let x be object;

          assume

           A20: x in ( dom fi);

          then

          reconsider A = x as Ordinal;

          

          thus (f1 . x) = ((fi . A) *^ C) by A17, A20

          .= (f2 . x) by A19, A20;

        end;

        hence thesis by A16, A18, FUNCT_1: 2;

      end;

    end

    theorem :: ORDINAL3:39

    

     Th39: {} <> ( dom fi) & ( dom fi) = ( dom psi) & (for A, B st A in ( dom fi) & B = (fi . A) holds (psi . A) = (C +^ B)) implies ( sup psi) = (C +^ ( sup fi))

    proof

      assume that

       A1: {} <> ( dom fi) and

       A2: ( dom fi) = ( dom psi) and

       A3: for A, B st A in ( dom fi) & B = (fi . A) holds (psi . A) = (C +^ B);

      set z = the Element of ( dom fi);

      reconsider z9 = (fi . z) as Ordinal;

      

       A4: (C +^ ( sup ( rng fi))) c= ( sup ( rng psi))

      proof

        let x be object;

        assume

         A5: x in (C +^ ( sup ( rng fi)));

        then

        reconsider A = x as Ordinal;

         A6:

        now

          given B such that

           A7: B in ( sup ( rng fi)) and

           A8: A = (C +^ B);

          consider D such that

           A9: D in ( rng fi) and

           A10: B c= D by A7, ORDINAL2: 21;

          consider x be object such that

           A11: x in ( dom fi) and

           A12: D = (fi . x) by A9, FUNCT_1:def 3;

          reconsider x as Ordinal by A11;

          (psi . x) = (C +^ D) by A3, A11, A12;

          then (C +^ D) in ( rng psi) by A2, A11, FUNCT_1:def 3;

          then (C +^ D) in ( sup ( rng psi)) by ORDINAL2: 19;

          hence A in ( sup ( rng psi)) by A8, A10, ORDINAL1: 12, ORDINAL2: 33;

        end;

        now

          (C +^ z9) = (psi . z) by A1, A3;

          then (C +^ z9) in ( rng psi) by A1, A2, FUNCT_1:def 3;

          then

           A13: (C +^ z9) in ( sup ( rng psi)) by ORDINAL2: 19;

          assume

           A14: A in C;

          C c= (C +^ z9) by Th24;

          then A c= (C +^ z9) by A14, ORDINAL1:def 2;

          hence A in ( sup ( rng psi)) by A13, ORDINAL1: 12;

        end;

        hence thesis by A5, A6, Th38;

      end;

      ( sup ( rng psi)) c= (C +^ ( sup ( rng fi)))

      proof

        let x be object;

        assume

         A15: x in ( sup ( rng psi));

        then

        reconsider A = x as Ordinal;

        consider B such that

         A16: B in ( rng psi) and

         A17: A c= B by A15, ORDINAL2: 21;

        consider y be object such that

         A18: y in ( dom psi) and

         A19: B = (psi . y) by A16, FUNCT_1:def 3;

        reconsider y as Ordinal by A18;

        reconsider y9 = (fi . y) as Ordinal;

        y9 in ( rng fi) by A2, A18, FUNCT_1:def 3;

        then

         A20: y9 in ( sup ( rng fi)) by ORDINAL2: 19;

        B = (C +^ y9) by A2, A3, A18, A19;

        then B in (C +^ ( sup ( rng fi))) by A20, ORDINAL2: 32;

        hence thesis by A17, ORDINAL1: 12;

      end;

      hence thesis by A4;

    end;

    theorem :: ORDINAL3:40

    

     Th40: A is limit_ordinal implies (A *^ B) is limit_ordinal

    proof

       A1:

      now

        deffunc F( Ordinal) = ($1 *^ B);

        assume that

         A2: A <> {} and

         A3: A is limit_ordinal;

        consider fi such that

         A4: ( dom fi) = A & for C st C in A holds (fi . C) = F(C) from ORDINAL2:sch 3;

        

         A5: (A *^ B) = ( union ( sup fi)) by A2, A3, A4, ORDINAL2: 37

        .= ( union ( sup ( rng fi)));

        for C st C in (A *^ B) holds ( succ C) in (A *^ B)

        proof

          let C;

          assume

           A6: C in (A *^ B);

          then

          consider X such that

           A7: C in X and

           A8: X in ( sup ( rng fi)) by A5, TARSKI:def 4;

          reconsider X as Ordinal by A8;

          consider D such that

           A9: D in ( rng fi) and

           A10: X c= D by A8, ORDINAL2: 21;

          consider x be object such that

           A11: x in ( dom fi) and

           A12: D = (fi . x) by A9, FUNCT_1:def 3;

          ( succ C) c= D by A7, A10, ORDINAL1: 21;

          then

           A13: ( succ C) in ( succ D) by ORDINAL1: 22;

          reconsider x as Ordinal by A11;

          

           A14: ( succ x) in ( dom fi) by A3, A4, A11, ORDINAL1: 28;

          

          then (fi . ( succ x)) = (( succ x) *^ B) by A4

          .= ((x *^ B) +^ B) by ORDINAL2: 36;

          then ((x *^ B) +^ B) in ( rng fi) by A14, FUNCT_1:def 3;

          then

           A15: ((x *^ B) +^ B) in ( sup ( rng fi)) by ORDINAL2: 19;

          

           A16: ((x *^ B) +^ ( succ {} )) = ( succ ((x *^ B) +^ {} )) by ORDINAL2: 28;

          B <> {} by A6, ORDINAL2: 38;

          then {} in B by Th8;

          then

           A17: ( succ {} ) c= B by ORDINAL1: 21;

          

           A18: ((x *^ B) +^ {} ) = (x *^ B) by ORDINAL2: 27;

          (x *^ B) = (fi . x) by A4, A11;

          then ( succ D) in ( sup ( rng fi)) by A12, A17, A16, A18, A15, ORDINAL1: 12, ORDINAL2: 33;

          hence thesis by A5, A13, TARSKI:def 4;

        end;

        hence thesis by ORDINAL1: 28;

      end;

      assume A is limit_ordinal;

      hence thesis by A1, ORDINAL2: 35;

    end;

    theorem :: ORDINAL3:41

    

     Th41: A in (B *^ C) & B is limit_ordinal implies ex D st D in B & A in (D *^ C)

    proof

      assume that

       A1: A in (B *^ C) and

       A2: B is limit_ordinal;

      deffunc F( Ordinal) = ($1 *^ C);

      consider fi such that

       A3: ( dom fi) = B & for D st D in B holds (fi . D) = F(D) from ORDINAL2:sch 3;

      B <> {} by A1, ORDINAL2: 35;

      

      then (B *^ C) = ( union ( sup fi)) by A2, A3, ORDINAL2: 37

      .= ( union ( sup ( rng fi)));

      then

      consider X such that

       A4: A in X and

       A5: X in ( sup ( rng fi)) by A1, TARSKI:def 4;

      reconsider X as Ordinal by A5;

      consider D such that

       A6: D in ( rng fi) and

       A7: X c= D by A5, ORDINAL2: 21;

      consider x be object such that

       A8: x in ( dom fi) and

       A9: D = (fi . x) by A6, FUNCT_1:def 3;

      reconsider x as Ordinal by A8;

      take E = ( succ x);

      thus E in B by A2, A3, A8, ORDINAL1: 28;

      

       A10: (D +^ {} ) = D by ORDINAL2: 27;

      

       A11: C <> {} by A1, ORDINAL2: 38;

      (E *^ C) = ((x *^ C) +^ C) by ORDINAL2: 36

      .= (D +^ C) by A3, A8, A9;

      then D in (E *^ C) by A11, A10, Th8, ORDINAL2: 32;

      hence thesis by A4, A7, ORDINAL1: 10;

    end;

    theorem :: ORDINAL3:42

    

     Th42: ( dom fi) = ( dom psi) & C <> {} & ( sup fi) is limit_ordinal & (for A, B st A in ( dom fi) & B = (fi . A) holds (psi . A) = (B *^ C)) implies ( sup psi) = (( sup fi) *^ C)

    proof

      assume that

       A1: ( dom fi) = ( dom psi) and

       A2: C <> {} and

       A3: ( sup fi) is limit_ordinal and

       A4: for A, B st A in ( dom fi) & B = (fi . A) holds (psi . A) = (B *^ C);

      

       A5: (( sup ( rng fi)) *^ C) c= ( sup ( rng psi))

      proof

        let x be object;

        assume

         A6: x in (( sup ( rng fi)) *^ C);

        then

        reconsider A = x as Ordinal;

        consider B such that

         A7: B in ( sup ( rng fi)) and

         A8: A in (B *^ C) by A3, A6, Th41;

        consider D such that

         A9: D in ( rng fi) and

         A10: B c= D by A7, ORDINAL2: 21;

        consider y be object such that

         A11: y in ( dom fi) and

         A12: D = (fi . y) by A9, FUNCT_1:def 3;

        reconsider y as Ordinal by A11;

        reconsider y9 = (psi . y) as Ordinal;

        

         A13: y9 in ( rng psi) by A1, A11, FUNCT_1:def 3;

        y9 = (D *^ C) by A4, A11, A12;

        then

         A14: (D *^ C) in ( sup ( rng psi)) by A13, ORDINAL2: 19;

        (B *^ C) c= (D *^ C) by A10, ORDINAL2: 41;

        hence thesis by A8, A14, ORDINAL1: 10;

      end;

      ( sup ( rng psi)) c= (( sup ( rng fi)) *^ C)

      proof

        let x be object;

        assume

         A15: x in ( sup ( rng psi));

        then

        reconsider A = x as Ordinal;

        consider B such that

         A16: B in ( rng psi) and

         A17: A c= B by A15, ORDINAL2: 21;

        consider y be object such that

         A18: y in ( dom psi) and

         A19: B = (psi . y) by A16, FUNCT_1:def 3;

        reconsider y as Ordinal by A18;

        reconsider y9 = (fi . y) as Ordinal;

        y9 in ( rng fi) by A1, A18, FUNCT_1:def 3;

        then

         A20: y9 in ( sup ( rng fi)) by ORDINAL2: 19;

        B = (y9 *^ C) by A1, A4, A18, A19;

        then B in (( sup ( rng fi)) *^ C) by A2, A20, ORDINAL2: 40;

        hence thesis by A17, ORDINAL1: 12;

      end;

      hence thesis by A5;

    end;

    theorem :: ORDINAL3:43

    

     Th43: {} <> ( dom fi) implies ( sup (C +^ fi)) = (C +^ ( sup fi))

    proof

      

       A1: for A, B st A in ( dom fi) & B = (fi . A) holds ((C +^ fi) . A) = (C +^ B) by Def1;

      ( dom (C +^ fi)) = ( dom fi) by Def1;

      hence thesis by A1, Th39;

    end;

    theorem :: ORDINAL3:44

    

     Th44: {} <> ( dom fi) & C <> {} & ( sup fi) is limit_ordinal implies ( sup (fi *^ C)) = (( sup fi) *^ C)

    proof

      

       A1: for A, B st A in ( dom fi) & B = (fi . A) holds ((fi *^ C) . A) = (B *^ C) by Def4;

      ( dom (fi *^ C)) = ( dom fi) by Def4;

      hence thesis by A1, Th42;

    end;

    theorem :: ORDINAL3:45

    

     Th45: B <> {} implies ( union (A +^ B)) = (A +^ ( union B))

    proof

      assume

       A1: B <> {} ;

       A2:

      now

        assume not ex C st B = ( succ C);

        then

         A3: B is limit_ordinal by ORDINAL1: 29;

        then (A +^ B) is limit_ordinal by A1, Th29;

        then ( union (A +^ B)) = (A +^ B);

        hence thesis by A3;

      end;

      now

        given C such that

         A4: B = ( succ C);

        

        thus ( union (A +^ B)) = ( union ( succ (A +^ C))) by A4, ORDINAL2: 28

        .= (A +^ C) by ORDINAL2: 2

        .= (A +^ ( union B)) by A4, ORDINAL2: 2;

      end;

      hence thesis by A2;

    end;

    theorem :: ORDINAL3:46

    

     Th46: ((A +^ B) *^ C) = ((A *^ C) +^ (B *^ C))

    proof

      defpred S[ Ordinal] means ((A +^ $1) *^ C) = ((A *^ C) +^ ($1 *^ C));

      

       A1: for B st S[B] holds S[( succ B)]

      proof

        let B such that

         A2: ((A +^ B) *^ C) = ((A *^ C) +^ (B *^ C));

        

        thus ((A +^ ( succ B)) *^ C) = (( succ (A +^ B)) *^ C) by ORDINAL2: 28

        .= (((A *^ C) +^ (B *^ C)) +^ C) by A2, ORDINAL2: 36

        .= ((A *^ C) +^ ((B *^ C) +^ C)) by Th30

        .= ((A *^ C) +^ (( succ B) *^ C)) by ORDINAL2: 36;

      end;

      

       A3: for B st B <> 0 & B is limit_ordinal & for D st D in B holds S[D] holds S[B]

      proof

        deffunc F( Ordinal) = (A +^ $1);

        let B such that

         A4: B <> 0 and

         A5: B is limit_ordinal and

         A6: for D st D in B holds S[D];

        consider fi such that

         A7: ( dom fi) = B & for D st D in B holds (fi . D) = F(D) from ORDINAL2:sch 3;

        (A +^ B) is limit_ordinal by A4, A5, Th29;

        then

         A8: ((A +^ B) *^ C) is limit_ordinal by Th40;

        

         A9: ( dom (fi *^ C)) = ( dom fi) by Def4;

         A10:

        now

          assume

           A11: C = {} ;

          then

           A12: (A *^ C) = {} by ORDINAL2: 38;

          

           A13: (B *^ C) = {} by A11, ORDINAL2: 38;

          ((A +^ B) *^ C) = {} by A11, ORDINAL2: 38;

          hence thesis by A12, A13, ORDINAL2: 27;

        end;

        deffunc F( Ordinal) = ($1 *^ C);

        consider psi such that

         A14: ( dom psi) = B & for D st D in B holds (psi . D) = F(D) from ORDINAL2:sch 3;

         A15:

        now

          let x be object;

          assume

           A16: x in B;

          then

          reconsider k = x as Ordinal;

          reconsider m = (fi . k), n = (psi . k) as Ordinal;

          

          thus ((fi *^ C) . x) = (m *^ C) by A7, A16, Def4

          .= ((A +^ k) *^ C) by A7, A16

          .= ((A *^ C) +^ (k *^ C)) by A6, A16

          .= ((A *^ C) +^ n) by A14, A16

          .= (((A *^ C) +^ psi) . x) by A14, A16, Def1;

        end;

        reconsider k = (psi . {} ) as Ordinal;

         {} in B by A4, Th8;

        then k in ( rng psi) by A14, FUNCT_1:def 3;

        then

         A17: k in ( sup ( rng psi)) by ORDINAL2: 19;

        ( dom ((A *^ C) +^ psi)) = ( dom psi) by Def1;

        then

         A18: (fi *^ C) = ((A *^ C) +^ psi) by A7, A14, A9, A15, FUNCT_1: 2;

        

         A19: (A +^ B) = ( sup fi) by A4, A5, A7, ORDINAL2: 29;

        now

          assume C <> {} ;

          

          then ((A +^ B) *^ C) = ( sup (fi *^ C)) by A4, A5, A7, A19, Th29, Th44

          .= ((A *^ C) +^ ( sup psi)) by A4, A14, A18, Th43;

          

          hence ((A +^ B) *^ C) = ( union ((A *^ C) +^ ( sup psi))) by A8

          .= ((A *^ C) +^ ( union ( sup psi))) by A17, Th45

          .= ((A *^ C) +^ (B *^ C)) by A4, A5, A14, ORDINAL2: 37;

        end;

        hence thesis by A10;

      end;

      ((A +^ {} ) *^ C) = (A *^ C) by ORDINAL2: 27

      .= ((A *^ C) +^ {} ) by ORDINAL2: 27

      .= ((A *^ C) +^ ( {} *^ C)) by ORDINAL2: 35;

      then

       A20: S[ 0 ];

      for B holds S[B] from ORDINAL2:sch 1( A20, A1, A3);

      hence thesis;

    end;

    theorem :: ORDINAL3:47

    

     Th47: A <> {} implies ex C, D st B = ((C *^ A) +^ D) & D in A

    proof

      defpred I[ Ordinal] means ex C, D st $1 = ((C *^ A) +^ D) & D in A;

      assume

       A1: A <> {} ;

      

       A2: for B st B <> 0 & B is limit_ordinal & for A1 st A1 in B holds I[A1] holds I[B]

      proof

         {} in A by A1, Th8;

        then

         A3: ( succ 0 ) c= A by ORDINAL1: 21;

        let B such that B <> 0 and

         A4: B is limit_ordinal and for A1 st A1 in B holds I[A1];

        defpred P[ Ordinal] means $1 in B & B in ($1 *^ A);

        (B *^ 1) = B by ORDINAL2: 39;

        then

         A5: B c= (B *^ A) by A3, ORDINAL2: 42;

         A6:

        now

          assume B <> (B *^ A);

          then B c< (B *^ A) by A5;

          then B in (B *^ A) by ORDINAL1: 11;

          then

           A7: ex C st P[C] by A4, Th41;

          consider C such that

           A8: P[C] and

           A9: for C1 be Ordinal st P[C1] holds C c= C1 from ORDINAL1:sch 1( A7);

          now

            assume C is limit_ordinal;

            then

            consider C1 be Ordinal such that

             A10: C1 in C and

             A11: B in (C1 *^ A) by A8, Th41;

            C1 in B by A8, A10, ORDINAL1: 10;

            hence contradiction by A9, A10, A11, ORDINAL1: 5;

          end;

          then

          consider C1 be Ordinal such that

           A12: C = ( succ C1) by ORDINAL1: 29;

          

           A13: C1 in C by A12, ORDINAL1: 6;

          then C1 in B by A8, ORDINAL1: 10;

          then not B in (C1 *^ A) by A9, A13, ORDINAL1: 5;

          then

          consider D such that

           A14: B = ((C1 *^ A) +^ D) by Th27, ORDINAL1: 16;

          thus I[B]

          proof

            take C1, D;

            thus B = ((C1 *^ A) +^ D) by A14;

            ((C1 *^ A) +^ D) in ((C1 *^ A) +^ A) by A8, A12, A14, ORDINAL2: 36;

            hence thesis by Th22;

          end;

        end;

        B = (B *^ A) implies B = ((B *^ A) +^ {} ) & {} in A by A1, Th8, ORDINAL2: 27;

        hence thesis by A6;

      end;

      

       A15: for B st I[B] holds I[( succ B)]

      proof

        let B;

        given C, D such that

         A16: B = ((C *^ A) +^ D) and

         A17: D in A;

         A18:

        now

          assume not ( succ D) in A;

          then

           A19: A c= ( succ D) by ORDINAL1: 16;

          take C1 = ( succ C), D1 = {} ;

          ( succ D) c= A by A17, ORDINAL1: 21;

          then

           A20: A = ( succ D) by A19;

          

          thus ((C1 *^ A) +^ D1) = (C1 *^ A) by ORDINAL2: 27

          .= ((C *^ A) +^ A) by ORDINAL2: 36

          .= ( succ B) by A16, A20, ORDINAL2: 28;

          thus D1 in A by A1, Th8;

        end;

        now

          assume

           A21: ( succ D) in A;

          take C1 = C, D1 = ( succ D);

          thus ((C1 *^ A) +^ D1) = ( succ B) by A16, ORDINAL2: 28;

          thus D1 in A by A21;

        end;

        hence thesis by A18;

      end;

      

       A22: I[ 0 ]

      proof

        take C = {} , D = {} ;

        

        thus 0 = ( {} +^ {} ) by ORDINAL2: 27

        .= ((C *^ A) +^ D) by ORDINAL2: 35;

        thus thesis by A1, Th8;

      end;

      for B holds I[B] from ORDINAL2:sch 1( A22, A15, A2);

      hence thesis;

    end;

    theorem :: ORDINAL3:48

    

     Th48: for C1,D1,C2,D2 be Ordinal st ((C1 *^ A) +^ D1) = ((C2 *^ A) +^ D2) & D1 in A & D2 in A holds C1 = C2 & D1 = D2

    proof

      let C1,D1,C2,D2 be Ordinal such that

       A1: ((C1 *^ A) +^ D1) = ((C2 *^ A) +^ D2) and

       A2: D1 in A and

       A3: D2 in A;

      set B = ((C1 *^ A) +^ D1);

       A4:

      now

        assume C2 in C1;

        then

        consider C such that

         A5: C1 = (C2 +^ C) and

         A6: C <> {} by Th28;

        B = (((C2 *^ A) +^ (C *^ A)) +^ D1) by A5, Th46

        .= ((C2 *^ A) +^ ((C *^ A) +^ D1)) by Th30;

        then

         A7: D2 = ((C *^ A) +^ D1) by A1, Th21;

        

         A8: (C *^ A) c= ((C *^ A) +^ D1) by Th24;

        A c= (C *^ A) by A6, Th36;

        hence contradiction by A3, A7, A8, ORDINAL1: 5;

      end;

      now

        assume C1 in C2;

        then

        consider C such that

         A9: C2 = (C1 +^ C) and

         A10: C <> {} by Th28;

        B = (((C1 *^ A) +^ (C *^ A)) +^ D2) by A1, A9, Th46

        .= ((C1 *^ A) +^ ((C *^ A) +^ D2)) by Th30;

        then

         A11: D1 = ((C *^ A) +^ D2) by Th21;

        

         A12: (C *^ A) c= ((C *^ A) +^ D2) by Th24;

        A c= (C *^ A) by A10, Th36;

        hence contradiction by A2, A11, A12, ORDINAL1: 5;

      end;

      hence C1 = C2 by A4, ORDINAL1: 14;

      hence thesis by A1, Th21;

    end;

    theorem :: ORDINAL3:49

    

     Th49: 1 in B & A <> {} & A is limit_ordinal implies for fi st ( dom fi) = A & for C st C in A holds (fi . C) = (C *^ B) holds (A *^ B) = ( sup fi)

    proof

      assume that

       A1: 1 in B and

       A2: A <> {} and

       A3: A is limit_ordinal;

      let fi;

      assume that

       A4: ( dom fi) = A and

       A5: for C st C in A holds (fi . C) = (C *^ B);

      now

        given C such that

         A6: ( sup fi) = ( succ C);

        consider D such that

         A7: D in ( rng fi) and

         A8: C c= D by A6, ORDINAL1: 6, ORDINAL2: 21;

        D in ( sup fi) by A7, ORDINAL2: 19;

        then

         A9: ( succ D) c= ( succ C) by A6, ORDINAL1: 21;

        ( succ C) c= ( succ D) by A8, ORDINAL2: 1;

        then ( succ C) = ( succ D) by A9;

        then C = D by ORDINAL1: 7;

        then

        consider x be object such that

         A10: x in ( dom fi) and

         A11: C = (fi . x) by A7, FUNCT_1:def 3;

        reconsider x as Ordinal by A10;

        

         A12: C = (x *^ B) by A4, A5, A10, A11;

        (C +^ 1) in (C +^ B) by A1, ORDINAL2: 32;

        then

         A13: ( sup fi) in (C +^ B) by A6, ORDINAL2: 31;

        

         A14: (( succ x) *^ B) = ((x *^ B) +^ B) by ORDINAL2: 36;

        

         A15: ( succ x) in ( dom fi) by A3, A4, A10, ORDINAL1: 28;

        then (fi . ( succ x)) = (( succ x) *^ B) by A4, A5;

        then (C +^ B) in ( rng fi) by A15, A12, A14, FUNCT_1:def 3;

        hence contradiction by A13, ORDINAL2: 19;

      end;

      then

       A16: ( sup fi) is limit_ordinal by ORDINAL1: 29;

      (A *^ B) = ( union ( sup fi)) by A2, A3, A4, A5, ORDINAL2: 37;

      hence thesis by A16;

    end;

    theorem :: ORDINAL3:50

    ((A *^ B) *^ C) = (A *^ (B *^ C))

    proof

      defpred P[ Ordinal] means (($1 *^ B) *^ C) = ($1 *^ (B *^ C));

      

       A1: ( {} *^ C) = {} by ORDINAL2: 35;

      

       A2: for A st P[A] holds P[( succ A)]

      proof

        let A such that

         A3: ((A *^ B) *^ C) = (A *^ (B *^ C));

        

        thus ((( succ A) *^ B) *^ C) = (((A *^ B) +^ B) *^ C) by ORDINAL2: 36

        .= ((A *^ (B *^ C)) +^ (B *^ C)) by A3, Th46

        .= ((A *^ (B *^ C)) +^ (1 *^ (B *^ C))) by ORDINAL2: 39

        .= ((A +^ 1) *^ (B *^ C)) by Th46

        .= (( succ A) *^ (B *^ C)) by ORDINAL2: 31;

      end;

      

       A4: for A st A <> 0 & A is limit_ordinal & for D st D in A holds P[D] holds P[A]

      proof

        let A such that

         A5: A <> 0 and

         A6: A is limit_ordinal and

         A7: for D st D in A holds ((D *^ B) *^ C) = (D *^ (B *^ C));

         A8:

        now

          deffunc F( Ordinal) = ($1 *^ B);

          assume that

           A9: 1 in B and

           A10: 1 in C;

          consider fi such that

           A11: ( dom fi) = A & for D st D in A holds (fi . D) = F(D) from ORDINAL2:sch 3;

          

           A12: ( dom (fi *^ C)) = A & for D st D in A holds ((fi *^ C) . D) = (D *^ (B *^ C))

          proof

            thus ( dom (fi *^ C)) = A by A11, Def4;

            let D;

            assume

             A13: D in A;

            then

             A14: (fi . D) = (D *^ B) by A11;

            ((fi *^ C) . D) = ((fi . D) *^ C) by A11, A13, Def4;

            hence thesis by A7, A13, A14;

          end;

          1 = (1 *^ 1) by ORDINAL2: 39;

          then 1 in (B *^ C) by A9, A10, Th19;

          then

           A15: (A *^ (B *^ C)) = ( sup (fi *^ C)) by A5, A6, A12, Th49;

          (A *^ B) = ( sup fi) by A5, A6, A9, A11, Th49;

          hence thesis by A5, A6, A10, A11, A15, Th40, Th44;

        end;

        now

          assume not (1 in B & 1 in C);

          then

           A16: B = {} or B = 1 or C = {} or C = 1 by Th16, ORDINAL1: 16;

          

           A17: ( {} *^ C) = {} by ORDINAL2: 35;

          

           A18: ((A *^ B) *^ 1) = (A *^ B) by ORDINAL2: 39;

          

           A19: ((A *^ B) *^ {} ) = {} by ORDINAL2: 38;

          

           A20: (A *^ 1) = A by ORDINAL2: 39;

          (A *^ {} ) = {} by ORDINAL2: 38;

          hence thesis by A16, A17, A20, A19, A18, ORDINAL2: 38, ORDINAL2: 39;

        end;

        hence thesis by A8;

      end;

      ( {} *^ B) = {} by ORDINAL2: 35;

      then

       A21: P[ 0 ] by A1, ORDINAL2: 35;

      for A holds P[A] from ORDINAL2:sch 1( A21, A2, A4);

      hence thesis;

    end;

    definition

      let A, B;

      :: ORDINAL3:def5

      func A -^ B -> Ordinal means

      : Def5: A = (B +^ it ) if B c= A

      otherwise it = {} ;

      existence by Th27;

      uniqueness by Th21;

      consistency ;

      :: ORDINAL3:def6

      func A div^ B -> Ordinal means

      : Def6: ex C st A = ((it *^ B) +^ C) & C in B if B <> {}

      otherwise it = {} ;

      consistency ;

      existence by Th47;

      uniqueness by Th48;

    end

    definition

      let A, B;

      :: ORDINAL3:def7

      func A mod^ B -> Ordinal equals (A -^ ((A div^ B) *^ B));

      correctness ;

    end

    theorem :: ORDINAL3:51

    A in B implies B = (A +^ (B -^ A))

    proof

      assume A in B;

      then A c= B by ORDINAL1:def 2;

      hence thesis by Def5;

    end;

    theorem :: ORDINAL3:52

    

     Th52: ((A +^ B) -^ A) = B

    proof

      A c= (A +^ B) by Th24;

      hence thesis by Def5;

    end;

    theorem :: ORDINAL3:53

    

     Th53: A in B & (C c= A or C in A) implies (A -^ C) in (B -^ C)

    proof

      assume that

       A1: A in B and

       A2: C c= A or C in A;

      A c= B by A1, ORDINAL1:def 2;

      then C c= B by A2, ORDINAL1:def 2;

      then

       A3: B = (C +^ (B -^ C)) by Def5;

      C c= A by A2, ORDINAL1:def 2;

      then A = (C +^ (A -^ C)) by Def5;

      hence thesis by A1, A3, Th22;

    end;

    theorem :: ORDINAL3:54

    

     Th54: (A -^ A) = {}

    proof

      (A +^ {} ) = A by ORDINAL2: 27;

      hence thesis by Def5;

    end;

    theorem :: ORDINAL3:55

    A in B implies (B -^ A) <> {} & {} in (B -^ A)

    proof

      assume A in B;

      then (A -^ A) in (B -^ A) by Th53;

      hence thesis by Th54;

    end;

    theorem :: ORDINAL3:56

    

     Th56: (A -^ {} ) = A & ( {} -^ A) = {}

    proof

      

       A1: ( {} +^ A) = A by ORDINAL2: 30;

       {} c= A;

      hence (A -^ {} ) = A by A1, Def5;

       not A c= {} or A c= {} ;

      then thesis or A = {} by Def5, XBOOLE_1: 3;

      hence thesis by A1, Def5;

    end;

    theorem :: ORDINAL3:57

    (A -^ (B +^ C)) = ((A -^ B) -^ C)

    proof

      now

        per cases ;

          suppose (B +^ C) c= A;

          then A = ((B +^ C) +^ (A -^ (B +^ C))) by Def5;

          then A = (B +^ (C +^ (A -^ (B +^ C)))) by Th30;

          then (C +^ (A -^ (B +^ C))) = (A -^ B) by Th52;

          hence thesis by Th52;

        end;

          suppose

           A1: not (B +^ C) c= A;

           A2:

          now

            assume A = (B +^ (A -^ B));

            then not C c= (A -^ B) by A1, ORDINAL2: 33;

            hence ((A -^ B) -^ C) = {} by Def5;

          end;

          B c= A or not B c= A;

          then

           A3: A = (B +^ (A -^ B)) or (A -^ B) = {} by Def5;

          (A -^ (B +^ C)) = {} by A1, Def5;

          hence thesis by A3, A2, Th56;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL3:58

    A c= B implies (C -^ B) c= (C -^ A)

    proof

      assume

       A1: A c= B;

      then

       A2: B = (A +^ (B -^ A)) by Def5;

       A3:

      now

        assume

         A4: B c= C;

        then

         A5: C = (B +^ (C -^ B)) by Def5;

        A c= C by A1, A4;

        then (B +^ (C -^ B)) = (A +^ (C -^ A)) by A5, Def5;

        then (A +^ ((B -^ A) +^ (C -^ B))) = (A +^ (C -^ A)) by A2, Th30;

        then ((B -^ A) +^ (C -^ B)) = (C -^ A) by Th21;

        hence thesis by Th24;

      end;

       not B c= C implies thesis by Def5;

      hence thesis by A3;

    end;

    theorem :: ORDINAL3:59

    A c= B implies (A -^ C) c= (B -^ C)

    proof

      assume

       A1: A c= B;

       A2:

      now

        assume

         A3: C c= A;

        then

         A4: A = (C +^ (A -^ C)) by Def5;

        C c= B by A1, A3;

        then (C +^ (A -^ C)) c= (C +^ (B -^ C)) by A1, A4, Def5;

        hence thesis by Th23;

      end;

       not C c= A implies thesis by Def5;

      hence thesis by A2;

    end;

    theorem :: ORDINAL3:60

    C <> {} & A in (B +^ C) implies (A -^ B) in C

    proof

      assume

       A1: C <> {} ;

      

       A2: ((B +^ C) -^ B) = C by Th52;

       not B c= A implies (A -^ B) = {} by Def5;

      hence thesis by A1, A2, Th8, Th53;

    end;

    theorem :: ORDINAL3:61

    (A +^ B) in C implies B in (C -^ A)

    proof

      

       A1: ((A +^ B) -^ A) = B by Th52;

      A c= (A +^ B) by Th24;

      hence thesis by A1, Th53;

    end;

    theorem :: ORDINAL3:62

    A c= (B +^ (A -^ B))

    proof

      now

        per cases ;

          suppose B c= A;

          hence thesis by Def5;

        end;

          suppose

           A1: not B c= A;

          then (A -^ B) = {} by Def5;

          hence thesis by A1, ORDINAL2: 27;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL3:63

    ((A *^ C) -^ (B *^ C)) = ((A -^ B) *^ C)

    proof

       A1:

      now

        assume

         A2: not B c= A;

        then

         A3: not (B *^ C) c= (A *^ C) or C = {} by Th35;

        

         A4: ( {} *^ C) = {} by ORDINAL2: 35;

        

         A5: (A *^ {} ) = {} by ORDINAL2: 38;

        (A -^ B) = {} by A2, Def5;

        hence thesis by A3, A5, A4, Def5, Th56;

      end;

      now

        assume B c= A;

        then A = (B +^ (A -^ B)) by Def5;

        then (A *^ C) = ((B *^ C) +^ ((A -^ B) *^ C)) by Th46;

        hence thesis by Th52;

      end;

      hence thesis by A1;

    end;

    theorem :: ORDINAL3:64

    

     Th64: ((A div^ B) *^ B) c= A

    proof

      now

        per cases ;

          suppose B <> {} ;

          then ex C st A = (((A div^ B) *^ B) +^ C) & C in B by Def6;

          hence thesis by Th24;

        end;

          suppose B = {} ;

          then (A div^ B) = {} by Def6;

          then ((A div^ B) *^ B) = {} by ORDINAL2: 35;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: ORDINAL3:65

    

     Th65: A = (((A div^ B) *^ B) +^ (A mod^ B))

    proof

      ((A div^ B) *^ B) c= A by Th64;

      hence thesis by Def5;

    end;

    theorem :: ORDINAL3:66

    A = ((B *^ C) +^ D) & D in C implies B = (A div^ C) & D = (A mod^ C)

    proof

      assume that

       A1: A = ((B *^ C) +^ D) and

       A2: D in C;

      thus B = (A div^ C) by A1, A2, Def6;

      hence thesis by A1, Th52;

    end;

    theorem :: ORDINAL3:67

    A in (B *^ C) implies (A div^ C) in B & (A mod^ C) in C

    proof

      

       A1: A = (((A div^ C) *^ C) +^ (A mod^ C)) by Th65;

      assume

       A2: A in (B *^ C);

      then C <> {} by ORDINAL2: 38;

      then

       A3: ex D st A = (((A div^ C) *^ C) +^ D) & D in C by Def6;

      then

       A4: ((A div^ C) *^ C) c= A by Th24;

      assume not thesis;

      then (B *^ C) c= ((A div^ C) *^ C) by A3, A1, Th21, ORDINAL1: 16, ORDINAL2: 41;

      hence contradiction by A2, A4, ORDINAL1: 5;

    end;

    theorem :: ORDINAL3:68

    

     Th68: B <> {} implies ((A *^ B) div^ B) = A

    proof

      assume B <> {} ;

      then

       A1: {} in B by Th8;

      (A *^ B) = ((A *^ B) +^ {} ) by ORDINAL2: 27;

      hence thesis by A1, Def6;

    end;

    theorem :: ORDINAL3:69

    ((A *^ B) mod^ B) = {}

    proof

      

       A1: (A *^ {} ) = {} by ORDINAL2: 38;

      

       A2: ((A *^ B) -^ (A *^ B)) = {} by Th54;

      ( {} -^ (((A *^ B) div^ B) *^ B)) = {} by Th56;

      hence thesis by A1, A2, Th68;

    end;

    theorem :: ORDINAL3:70

    ( {} div^ A) = {} & ( {} mod^ A) = {} & (A mod^ {} ) = A

    proof

      

       A1: A = {} or A <> {} ;

       {} = ( {} *^ A) by ORDINAL2: 35;

      hence ( {} div^ A) = {} by A1, Def6, Th68;

      thus ( {} mod^ A) = {} by Th56;

      

      thus (A mod^ {} ) = (A -^ {} ) by ORDINAL2: 38

      .= A by Th56;

    end;

    theorem :: ORDINAL3:71

    (A div^ 1) = A & (A mod^ 1) = {}

    proof

      

       A1: A = (A *^ 1) by ORDINAL2: 39;

      

       A2: A = (A +^ {} ) by ORDINAL2: 27;

      1 = ( succ 0 )

      .= { 0 };

      then

       A3: {} in 1 by Th8;

      hence (A div^ 1) = A by A1, A2, Def6;

      

      thus (A mod^ 1) = (A -^ A) by A1, A2, A3, Def6

      .= {} by Th54;

    end;

    begin

    theorem :: ORDINAL3:72

    ( sup X) c= ( succ ( union ( On X)))

    proof

      reconsider A = ( union ( On X)) as Ordinal by Th5;

      ( On X) c= ( succ A)

      proof

        let x be object;

        assume

         A1: x in ( On X);

        then

        reconsider a = x as Ordinal by ORDINAL1:def 9;

        a c= A by A1, ZFMISC_1: 74;

        hence thesis by ORDINAL1: 22;

      end;

      hence thesis by ORDINAL2:def 3;

    end;

    reserve e,u for set;

    theorem :: ORDINAL3:73

    ( succ A) is_cofinal_with 1

    proof

      deffunc F( set) = A;

      consider psi such that

       A1: ( dom psi) = 1 & for B st B in 1 holds (psi . B) = F(B) from ORDINAL2:sch 3;

      take psi;

      thus ( dom psi) = 1 by A1;

      thus ( rng psi) c= ( succ A)

      proof

        let e be object;

        assume e in ( rng psi);

        then

        consider u be object such that

         A2: u in 1 and

         A3: e = (psi . u) by A1, FUNCT_1:def 3;

        reconsider u as Ordinal by A2;

        (psi . u) = A by A1, A2;

        hence thesis by A3, ORDINAL1: 6;

      end;

      thus psi is increasing by A1, Th14;

      

       A4: (psi . {} ) = A by A1, Lm1, ORDINAL1: 6;

      ( rng psi) = {(psi . {} )} by A1, Lm1, FUNCT_1: 4;

      hence thesis by A4, ORDINAL2: 23;

    end;

    theorem :: ORDINAL3:74

    

     Th74: for a,b be Ordinal st (a +^ b) is natural holds a in omega & b in omega by Th24, ORDINAL1: 12;

    registration

      let a,b be natural Ordinal;

      cluster (a -^ b) -> natural;

      coherence

      proof

         not b c= a or b c= a;

        then (a -^ b) = {} or a = (b +^ (a -^ b)) by Def5;

        hence (a -^ b) in omega by Th74, ORDINAL1:def 11;

      end;

      cluster (a *^ b) -> natural;

      coherence

      proof

        defpred P[ natural Ordinal] means ($1 *^ b) is natural;

         A1:

        now

          let a be natural Ordinal;

          assume P[a];

          then

          reconsider c = (a *^ b) as natural Ordinal;

          (( succ a) *^ b) = (c +^ b) by ORDINAL2: 36;

          hence P[( succ a)];

        end;

        

         A2: P[ 0 ] by ORDINAL2: 35;

         P[a] from ORDINAL2:sch 17( A2, A1);

        hence thesis;

      end;

    end

    theorem :: ORDINAL3:75

    for a,b be Ordinal st (a *^ b) is natural non empty holds a in omega & b in omega

    proof

      let x,y be Ordinal such that

       A1: (x *^ y) in omega ;

      assume

       A2: (x *^ y) is non empty;

      then y <> {} by ORDINAL2: 38;

      then

       A3: x c= (x *^ y) by Th36;

      x <> {} by A2, ORDINAL2: 35;

      then y c= (x *^ y) by Th36;

      hence thesis by A1, A3, ORDINAL1: 12;

    end;

    definition

      let a,b be natural Ordinal;

      :: original: +^

      redefine

      func a +^ b;

      commutativity

      proof

        let a,b be natural Ordinal;

        defpred R[ natural Ordinal] means (a +^ $1) = ($1 +^ a);

         A1:

        now

          let b be natural Ordinal;

          assume

           A2: R[b];

          defpred P[ natural Ordinal] means (( succ b) +^ $1) = ( succ (b +^ $1));

           A3:

          now

            let a be natural Ordinal;

            assume

             A4: P[a];

            (( succ b) +^ ( succ a)) = ( succ (( succ b) +^ a)) by ORDINAL2: 28

            .= ( succ (b +^ ( succ a))) by A4, ORDINAL2: 28;

            hence P[( succ a)];

          end;

          (( succ b) +^ {} ) = ( succ b) by ORDINAL2: 27

          .= ( succ (b +^ {} )) by ORDINAL2: 27;

          then

           A5: P[ 0 ];

           P[a] from ORDINAL2:sch 17( A5, A3);

          hence R[( succ b)] by A2, ORDINAL2: 28;

        end;

        (a +^ {} ) = a by ORDINAL2: 27

        .= ( {} +^ a) by ORDINAL2: 30;

        then

         A6: R[ 0 ];

        thus R[b] from ORDINAL2:sch 17( A6, A1);

      end;

    end

    definition

      let a,b be natural Ordinal;

      :: original: *^

      redefine

      func a *^ b;

      commutativity

      proof

        let a,b be natural Ordinal;

        defpred R[ natural Ordinal] means (a *^ $1) = ($1 *^ a);

         A1:

        now

          let b be natural Ordinal;

          defpred P[ natural Ordinal] means ($1 *^ ( succ b)) = (($1 *^ b) +^ $1);

          assume

           A2: R[b];

           A3:

          now

            let a be natural Ordinal;

            assume

             A4: P[a];

            (( succ a) *^ ( succ b)) = ((a *^ ( succ b)) +^ ( succ b)) by ORDINAL2: 36

            .= ((a *^ b) +^ (a +^ ( succ b))) by A4, Th30

            .= ((a *^ b) +^ ( succ (a +^ b))) by ORDINAL2: 28

            .= ( succ ((a *^ b) +^ (a +^ b))) by ORDINAL2: 28

            .= ( succ (((a *^ b) +^ b) +^ a)) by Th30

            .= ( succ ((( succ a) *^ b) +^ a)) by ORDINAL2: 36

            .= ((( succ a) *^ b) +^ ( succ a)) by ORDINAL2: 28;

            hence P[( succ a)];

          end;

          ( {} *^ ( succ b)) = {} by ORDINAL2: 35

          .= ( {} +^ {} ) by ORDINAL2: 27

          .= (( {} *^ b) +^ {} ) by ORDINAL2: 35;

          then

           A5: P[ 0 ];

           P[a] from ORDINAL2:sch 17( A5, A3);

          hence R[( succ b)] by A2, ORDINAL2: 36;

        end;

        (a *^ {} ) = {} by ORDINAL2: 38

        .= ( {} *^ a) by ORDINAL2: 35;

        then

         A6: R[ 0 ];

        thus R[b] from ORDINAL2:sch 17( A6, A1);

      end;

    end