wellord2.miz



    begin

    reserve X,Y,Z for set,

a,b,c,d,x,y,z,u for object,

R for Relation,

A,B,C for Ordinal;

    definition

      let X;

      :: WELLORD2:def1

      func RelIncl X -> Relation means

      : Def1: ( field it ) = X & for Y, Z st Y in X & Z in X holds [Y, Z] in it iff Y c= Z;

      existence

      proof

        defpred P[ object, object] means ex D1,D2 be set st D1 = $1 & D2 = $2 & D1 c= D2;

        consider R such that

         A1: for x,y be object holds [x, y] in R iff x in X & y in X & P[x, y] from RELAT_1:sch 1;

        take R;

        thus ( field R) = X

        proof

          thus for x be object holds x in ( field R) implies x in X

          proof

            let x be object;

             A2:

            now

              assume x in ( dom R);

              then ex y be object st [x, y] in R by XTUPLE_0:def 12;

              hence thesis by A1;

            end;

             A3:

            now

              assume x in ( rng R);

              then ex y be object st [y, x] in R by XTUPLE_0:def 13;

              hence thesis by A1;

            end;

            assume x in ( field R);

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

          end;

          let x be object;

          assume x in X;

          then [x, x] in R by A1;

          hence thesis by RELAT_1: 15;

        end;

        let Y, Z such that

         A4: Y in X & Z in X;

        hereby

          assume [Y, Z] in R;

          then P[Y, Z] by A1;

          hence Y c= Z;

        end;

        thus thesis by A1, A4;

      end;

      uniqueness

      proof

        let R1,R2 be Relation such that

         A5: ( field R1) = X and

         A6: for Y, Z st Y in X & Z in X holds [Y, Z] in R1 iff Y c= Z and

         A7: ( field R2) = X and

         A8: for Y, Z st Y in X & Z in X holds [Y, Z] in R2 iff Y c= Z;

        let x,y be object;

        thus [x, y] in R1 implies [x, y] in R2

        proof

          assume

           A9: [x, y] in R1;

          then

           A10: x in ( field R1) & y in ( field R1) by RELAT_1: 15;

          reconsider x, y as set by TARSKI: 1;

          x c= y by A5, A6, A9, A10;

          hence thesis by A5, A8, A10;

        end;

        assume

         A11: [x, y] in R2;

        then

         A12: x in ( field R2) & y in ( field R2) by RELAT_1: 15;

        reconsider x, y as set by TARSKI: 1;

        x c= y by A7, A8, A11, A12;

        hence thesis by A6, A7, A12;

      end;

    end

    ::$Canceled

    registration

      let X;

      cluster ( RelIncl X) -> reflexive;

      coherence

      proof

        

         A1: ( field ( RelIncl X)) = X by Def1;

        let a be object;

        assume a in ( field ( RelIncl X));

        hence thesis by A1, Def1;

      end;

      cluster ( RelIncl X) -> transitive;

      coherence

      proof

        let a,b,c be object such that

         A2: a in ( field ( RelIncl X)) and

         A3: b in ( field ( RelIncl X)) and

         A4: c in ( field ( RelIncl X)) and

         A5: [a, b] in ( RelIncl X) & [b, c] in ( RelIncl X);

        reconsider a, b, c as set by TARSKI: 1;

        ( field ( RelIncl X)) = X by Def1;

        then a c= b & b c= c by A2, A3, A4, A5, Def1;

        then

         A6: a c= c;

        a in X & c in X by A2, A4, Def1;

        hence thesis by A6, Def1;

      end;

      cluster ( RelIncl X) -> antisymmetric;

      coherence

      proof

        

         A7: ( field ( RelIncl X)) = X by Def1;

        let a,b be object;

        assume

         A8: a in ( field ( RelIncl X)) & b in ( field ( RelIncl X)) & [a, b] in ( RelIncl X) & [b, a] in ( RelIncl X);

        reconsider a, b as set by TARSKI: 1;

        a c= b & b c= a by A7, Def1, A8;

        hence thesis by XBOOLE_0:def 10;

      end;

    end

    registration

      let A;

      cluster ( RelIncl A) -> connected;

      coherence

      proof

        let a,b be object such that

         A1: a in ( field ( RelIncl A)) & b in ( field ( RelIncl A)) and a <> b;

        

         A2: ( field ( RelIncl A)) = A by Def1;

        then

        reconsider Y = a, Z = b as Ordinal by A1;

        Y c= Z or Z c= Y;

        hence thesis by A1, A2, Def1;

      end;

      cluster ( RelIncl A) -> well_founded;

      coherence

      proof

        let Y;

        assume that

         A3: Y c= ( field ( RelIncl A)) and

         A4: Y <> {} ;

        defpred P[ set] means $1 in Y;

        set x = the Element of Y;

        

         A5: ( field ( RelIncl A)) = A by Def1;

        then x in A by A3, A4;

        then

        reconsider x as Ordinal;

        x in Y by A4;

        then

         A6: ex B st P[B];

        consider B such that

         A7: P[B] & for C st P[C] holds B c= C from ORDINAL1:sch 1( A6);

        reconsider x = B as set;

        take x;

        thus x in Y by A7;

        set y = the Element of ((( RelIncl A) -Seg x) /\ Y);

        assume

         A8: ((( RelIncl A) -Seg x) /\ Y) <> {} ;

        then

         A9: y in Y by XBOOLE_0:def 4;

        then

        reconsider C = y as Ordinal by A3, A5;

        

         A10: y in (( RelIncl A) -Seg x) by A8, XBOOLE_0:def 4;

        then [y, x] in ( RelIncl A) by WELLORD1: 1;

        then

         A11: C c= B by A3, A5, A7, A9, Def1;

        

         A12: y <> x by A10, WELLORD1: 1;

        B c= C by A7, A9;

        hence contradiction by A12, A11;

      end;

    end

    theorem :: WELLORD2:7

    

     Th1: Y c= X implies (( RelIncl X) |_2 Y) = ( RelIncl Y)

    proof

      assume

       A1: Y c= X;

      let a,b be object;

      thus [a, b] in (( RelIncl X) |_2 Y) implies [a, b] in ( RelIncl Y)

      proof

        assume

         A2: [a, b] in (( RelIncl X) |_2 Y);

        then [a, b] in [:Y, Y:] by XBOOLE_0:def 4;

        then

         A3: a in Y & b in Y by ZFMISC_1: 87;

        reconsider a, b as set by TARSKI: 1;

         [a, b] in ( RelIncl X) by A2, XBOOLE_0:def 4;

        then a c= b by A1, A3, Def1;

        hence thesis by A3, Def1;

      end;

      assume

       A4: [a, b] in ( RelIncl Y);

      then

       A5: a in ( field ( RelIncl Y)) & b in ( field ( RelIncl Y)) by RELAT_1: 15;

      reconsider a, b as set by TARSKI: 1;

      

       A6: ( field ( RelIncl Y)) = Y by Def1;

      then a c= b by A4, A5, Def1;

      then

       A7: [a, b] in ( RelIncl X) by A1, A5, A6, Def1;

       [a, b] in [:Y, Y:] by A5, A6, ZFMISC_1: 87;

      hence thesis by A7, XBOOLE_0:def 4;

    end;

    theorem :: WELLORD2:8

    

     Th2: for A, X st X c= A holds ( RelIncl X) is well-ordering

    proof

      let A, X;

      (( RelIncl A) |_2 X) is well-ordering by WELLORD1: 25;

      hence thesis by Th1;

    end;

    reserve H for Function;

    theorem :: WELLORD2:9

    

     Th3: A in B implies A = (( RelIncl B) -Seg A)

    proof

      assume

       A1: A in B;

      thus for a be object holds a in A implies a in (( RelIncl B) -Seg A)

      proof

        let a be object;

        assume

         A2: a in A;

        then

        reconsider C = a as Ordinal;

        reconsider a as set by TARSKI: 1;

         not a in a;

        then

         A3: a <> A by A2;

        

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

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

        then [C, A] in ( RelIncl B) by A1, A2, A4, Def1;

        hence thesis by A3, WELLORD1: 1;

      end;

      let a be object;

      assume

       A5: a in (( RelIncl B) -Seg A);

      then

       A6: a <> A by WELLORD1: 1;

      

       A7: [a, A] in ( RelIncl B) by A5, WELLORD1: 1;

      then

       A8: a in ( field ( RelIncl B)) by RELAT_1: 15;

      

       A9: ( field ( RelIncl B)) = B by Def1;

      then

      reconsider C = a as Ordinal by A8;

      C c= A by A1, A7, A8, A9, Def1;

      then C c< A by A6;

      hence thesis by ORDINAL1: 11;

    end;

    theorem :: WELLORD2:10

    

     Th4: (( RelIncl A),( RelIncl B)) are_isomorphic implies A = B

    proof

      

       A1: ( field ( RelIncl A)) = A by Def1;

      assume

       A2: (( RelIncl A),( RelIncl B)) are_isomorphic ;

       A3:

      now

        

         A4: ( field ( RelIncl B)) = B by Def1;

        assume

         A5: A in B;

        then A = (( RelIncl B) -Seg A) by Th3;

        then ( RelIncl A) = (( RelIncl B) |_2 (( RelIncl B) -Seg A)) by A4, Th1, WELLORD1: 9;

        hence contradiction by A2, A5, A4, WELLORD1: 40, WELLORD1: 46;

      end;

      assume A <> B;

      then

       A6: A in B or B in A by ORDINAL1: 14;

      then B = (( RelIncl A) -Seg B) by A3, Th3;

      then ( RelIncl B) = (( RelIncl A) |_2 (( RelIncl A) -Seg B)) by A1, Th1, WELLORD1: 9;

      hence contradiction by A2, A6, A3, A1, WELLORD1: 46;

    end;

    theorem :: WELLORD2:11

    

     Th5: (R,( RelIncl A)) are_isomorphic & (R,( RelIncl B)) are_isomorphic implies A = B

    proof

      assume that

       A1: (R,( RelIncl A)) are_isomorphic and

       A2: (R,( RelIncl B)) are_isomorphic ;

      (( RelIncl A),R) are_isomorphic by A1, WELLORD1: 40;

      hence thesis by A2, Th4, WELLORD1: 42;

    end;

    theorem :: WELLORD2:12

    

     Th6: for R st R is well-ordering & for a be object st a in ( field R) holds ex A st ((R |_2 (R -Seg a)),( RelIncl A)) are_isomorphic holds ex A st (R,( RelIncl A)) are_isomorphic

    proof

      let R such that

       A1: R is well-ordering;

      defpred P[ object, object] means for A holds A = $2 iff ((R |_2 (R -Seg $1)),( RelIncl A)) are_isomorphic ;

      assume

       A2: for a be object st a in ( field R) holds ex A st ((R |_2 (R -Seg a)),( RelIncl A)) are_isomorphic ;

      

       A3: for a be object st a in ( field R) holds ex b be object st P[a, b]

      proof

        let a be object;

        assume a in ( field R);

        then

        consider A such that

         A4: ((R |_2 (R -Seg a)),( RelIncl A)) are_isomorphic by A2;

        reconsider b = A as set;

        take b;

        let B;

        thus B = b implies ((R |_2 (R -Seg a)),( RelIncl B)) are_isomorphic by A4;

        assume ((R |_2 (R -Seg a)),( RelIncl B)) are_isomorphic ;

        hence thesis by A4, Th5;

      end;

      

       A5: for b,c,d be object st b in ( field R) & P[b, c] & P[b, d] holds c = d

      proof

        let b,c,d be object such that

         A6: b in ( field R) and

         A7: A = c iff ((R |_2 (R -Seg b)),( RelIncl A)) are_isomorphic and

         A8: B = d iff ((R |_2 (R -Seg b)),( RelIncl B)) are_isomorphic ;

        consider A such that

         A9: ((R |_2 (R -Seg b)),( RelIncl A)) are_isomorphic by A2, A6;

        A = c by A7, A9;

        hence thesis by A8, A9;

      end;

      consider H such that

       A10: ( dom H) = ( field R) & for b be object st b in ( field R) holds P[b, (H . b)] from FUNCT_1:sch 2( A5, A3);

      for a st a in ( rng H) holds a is Ordinal

      proof

        let b;

        assume b in ( rng H);

        then

        consider c be object such that

         A11: c in ( dom H) and

         A12: b = (H . c) by FUNCT_1:def 3;

        ex A st ((R |_2 (R -Seg c)),( RelIncl A)) are_isomorphic by A2, A10, A11;

        hence thesis by A10, A11, A12;

      end;

      then

      consider C such that

       A13: ( rng H) c= C by ORDINAL1: 24;

       A14:

      now

        let b be object;

        assume

         A15: b in ( rng H);

        then

        consider b9 be object such that

         A16: b9 in ( dom H) and

         A17: b = (H . b9) by FUNCT_1:def 3;

        set V = (R -Seg b9);

        set P = (R |_2 V);

        consider A such that

         A18: (P,( RelIncl A)) are_isomorphic by A2, A10, A16;

        let c be object such that

         A19: [c, b] in ( RelIncl C);

        

         A20: A = b by A10, A16, A17, A18;

        now

          

           A21: C = ( field ( RelIncl C)) by Def1;

          then

           A22: c in C by A19, RELAT_1: 15;

          then

          reconsider B = c as Ordinal;

          b in C by A19, A21, RELAT_1: 15;

          then

           A23: B c= A by A20, A19, A22, Def1;

          then

           A24: (( RelIncl A) |_2 B) = ( RelIncl B) by Th1;

          assume c <> b;

          then

           A25: B c< A by A20, A23;

          then

           A26: B = (( RelIncl A) -Seg B) by Th3, ORDINAL1: 11;

          

           A27: A = ( field ( RelIncl A)) by Def1;

          (( RelIncl A),P) are_isomorphic by A18, WELLORD1: 40;

          then ( canonical_isomorphism_of (( RelIncl A),P)) is_isomorphism_of (( RelIncl A),P) by WELLORD1:def 9;

          then

          consider d be object such that

           A28: d in ( field P) and

           A29: ((( RelIncl A) |_2 (( RelIncl A) -Seg B)),(P |_2 (P -Seg d))) are_isomorphic by A25, A27, ORDINAL1: 11, WELLORD1: 50;

          

           A30: d in ( field R) by A28, WELLORD1: 12;

          

           A31: (P -Seg d) = (R -Seg d) by A1, A28, WELLORD1: 12, WELLORD1: 27;

          d in V by A28, WELLORD1: 12;

          then [d, b9] in R by WELLORD1: 1;

          then (R -Seg d) c= (R -Seg b9) by A1, A10, A16, A30, WELLORD1: 29;

          then (( RelIncl B),(R |_2 (R -Seg d))) are_isomorphic by A29, A26, A24, A31, WELLORD1: 22;

          then ((R |_2 (R -Seg d)),( RelIncl B)) are_isomorphic by WELLORD1: 40;

          then B = (H . d) by A10, A30;

          hence c in ( rng H) by A10, A30, FUNCT_1:def 3;

        end;

        hence c in ( rng H) by A15;

      end;

      

       A32: (ex a be object st a in C & ( rng H) = (( RelIncl C) -Seg a)) implies ( rng H) is Ordinal by Th3;

      C = ( field ( RelIncl C)) & ( RelIncl C) is well-ordering by Def1;

      then

      reconsider A = ( rng H) as Ordinal by A13, A14, A32, WELLORD1: 28;

      take A;

      take H;

      thus ( dom H) = ( field R) by A10;

      thus ( rng H) = ( field ( RelIncl A)) by Def1;

      

       A33: a in ( dom H) implies (H . a) is Ordinal

      proof

        assume a in ( dom H);

        then (H . a) in A by FUNCT_1:def 3;

        hence thesis;

      end;

      thus

       A34: H is one-to-one

      proof

        let a,b be object;

        assume that

         A35: a in ( dom H) and

         A36: b in ( dom H) and

         A37: (H . a) = (H . b);

        reconsider B = (H . a) as Ordinal by A33, A35;

        ((R |_2 (R -Seg b)),( RelIncl B)) are_isomorphic by A10, A36, A37;

        then

         A38: (( RelIncl B),(R |_2 (R -Seg b))) are_isomorphic by WELLORD1: 40;

        ((R |_2 (R -Seg a)),( RelIncl B)) are_isomorphic by A10, A35;

        then ((R |_2 (R -Seg a)),(R |_2 (R -Seg b))) are_isomorphic by A38, WELLORD1: 42;

        hence thesis by A1, A10, A35, A36, WELLORD1: 47;

      end;

      let a,b be object;

      thus [a, b] in R implies a in ( field R) & b in ( field R) & [(H . a), (H . b)] in ( RelIncl A)

      proof

        set Z = (R -Seg b);

        set P = (R |_2 Z);

        

         A39: A = ( field ( RelIncl A)) & P is well-ordering by A1, Def1, WELLORD1: 25;

        assume

         A40: [a, b] in R;

        hence

         A41: a in ( field R) & b in ( field R) by RELAT_1: 15;

        then

        reconsider A9 = (H . a), B9 = (H . b) as Ordinal by A10, A33;

        

         A42: ((R |_2 (R -Seg b)),( RelIncl B9)) are_isomorphic by A10, A41;

        

         A43: A9 in A by A10, A41, FUNCT_1:def 3;

        

         A44: B9 in A by A10, A41, FUNCT_1:def 3;

        

         A45: ((R |_2 (R -Seg a)),( RelIncl A9)) are_isomorphic by A10, A41;

        now

          assume a <> b;

          then

           A46: a in Z by A40, WELLORD1: 1;

          then

           A47: (P -Seg a) = (R -Seg a) by A1, WELLORD1: 27;

          Z c= ( field R) by WELLORD1: 9;

          then

           A48: a in ( field P) by A1, A46, WELLORD1: 31;

          A9 c= A by A43, ORDINAL1:def 2;

          then

           A49: (( RelIncl A) |_2 A9) = ( RelIncl A9) by Th1;

          A9 = (( RelIncl A) -Seg A9) & (R -Seg a) c= (R -Seg b) by A1, A40, A41, A43, Th3, WELLORD1: 29;

          then

           A50: ((P |_2 (P -Seg a)),(( RelIncl A) |_2 (( RelIncl A) -Seg A9))) are_isomorphic by A45, A49, A47, WELLORD1: 22;

          B9 = (( RelIncl A) -Seg B9) & B9 c= A by A44, Th3, ORDINAL1:def 2;

          then (P,(( RelIncl A) |_2 (( RelIncl A) -Seg B9))) are_isomorphic by A42, Th1;

          hence [A9, B9] in ( RelIncl A) by A43, A44, A39, A48, A50, WELLORD1: 51;

        end;

        hence thesis by A43, Def1;

      end;

      assume that

       A51: a in ( field R) and

       A52: b in ( field R) and

       A53: [(H . a), (H . b)] in ( RelIncl A);

      assume

       A54: not [a, b] in R;

      R is_reflexive_in ( field R) by A1, RELAT_2:def 9;

      then

       A55: a <> b by A51, A54;

      R is_connected_in ( field R) by A1, RELAT_2:def 14;

      then

       A56: [b, a] in R by A51, A52, A54, A55;

      then

       A57: (R -Seg b) c= (R -Seg a) by A1, A51, A52, WELLORD1: 29;

      

       A58: ( RelIncl A) is_antisymmetric_in ( field ( RelIncl A)) by RELAT_2:def 12;

      

       A59: A = ( field ( RelIncl A)) by Def1;

      reconsider A9 = (H . a), B9 = (H . b) as Ordinal by A10, A33, A51, A52;

      

       A60: ((R |_2 (R -Seg a)),( RelIncl A9)) are_isomorphic by A10, A51;

      

       A61: ((R |_2 (R -Seg b)),( RelIncl B9)) are_isomorphic by A10, A52;

      

       A62: B9 in A by A10, A52, FUNCT_1:def 3;

      then B9 c= A by ORDINAL1:def 2;

      then

       A63: (( RelIncl A) |_2 B9) = ( RelIncl B9) by Th1;

      set Z = (R -Seg a);

      set P = (R |_2 Z);

      

       A64: A9 in A by A10, A51, FUNCT_1:def 3;

      then A9 = (( RelIncl A) -Seg A9) & A9 c= A by Th3, ORDINAL1:def 2;

      then

       A65: (P,(( RelIncl A) |_2 (( RelIncl A) -Seg A9))) are_isomorphic by A60, Th1;

      

       A66: b in Z by A54, A56, WELLORD1: 1;

      then

       A67: (P -Seg b) = (R -Seg b) by A1, WELLORD1: 27;

      B9 = (( RelIncl A) -Seg B9) by A62, Th3;

      then

       A68: ((P |_2 (P -Seg b)),(( RelIncl A) |_2 (( RelIncl A) -Seg B9))) are_isomorphic by A61, A63, A67, A57, WELLORD1: 22;

      Z c= ( field R) by WELLORD1: 9;

      then

       A69: b in ( field P) by A1, A66, WELLORD1: 31;

      P is well-ordering by A1, WELLORD1: 25;

      then [B9, A9] in ( RelIncl A) by A69, A64, A62, A59, A65, A68, WELLORD1: 51;

      then (H . a) = (H . b) by A53, A58, A64, A62, A59;

      hence contradiction by A10, A34, A51, A52, A55;

    end;

    theorem :: WELLORD2:13

    

     Th7: for R st R is well-ordering holds ex A st (R,( RelIncl A)) are_isomorphic

    proof

      let R such that

       A1: R is well-ordering;

      defpred P[ object] means ex A st ((R |_2 (R -Seg $1)),( RelIncl A)) are_isomorphic ;

      consider Z such that

       A2: for a be object holds a in Z iff a in ( field R) & P[a] from XBOOLE_0:sch 1;

      now

        let a be object such that

         A3: a in ( field R) and

         A4: (R -Seg a) c= Z;

        set P = (R |_2 (R -Seg a));

        now

          let b be object;

          assume

           A5: b in ( field P);

          then

           A6: b in (R -Seg a) by WELLORD1: 12;

          then

           A7: [b, a] in R by WELLORD1: 1;

          b in ( field R) by A5, WELLORD1: 12;

          then

           A8: (R -Seg b) c= (R -Seg a) by A1, A3, A7, WELLORD1: 29;

          consider A such that

           A9: ((R |_2 (R -Seg b)),( RelIncl A)) are_isomorphic by A2, A4, A6;

          take A;

          (P -Seg b) = (R -Seg b) by A1, A5, WELLORD1: 12, WELLORD1: 27;

          hence ((P |_2 (P -Seg b)),( RelIncl A)) are_isomorphic by A9, A8, WELLORD1: 22;

        end;

        then ex A st (P,( RelIncl A)) are_isomorphic by A1, Th6, WELLORD1: 25;

        hence a in Z by A2, A3;

      end;

      then ( field R) c= Z by A1, WELLORD1: 33;

      then for a be object st a in ( field R) holds ex A st ((R |_2 (R -Seg a)),( RelIncl A)) are_isomorphic by A2;

      hence thesis by A1, Th6;

    end;

    definition

      let R;

      assume

       A1: R is well-ordering;

      :: WELLORD2:def2

      func order_type_of R -> Ordinal means

      : Def2: (R,( RelIncl it )) are_isomorphic ;

      existence by A1, Th7;

      uniqueness by Th5;

    end

    definition

      let A, R;

      :: WELLORD2:def3

      pred A is_order_type_of R means A = ( order_type_of R);

    end

    theorem :: WELLORD2:14

    X c= A implies ( order_type_of ( RelIncl X)) c= A

    proof

      assume

       A1: X c= A;

      then

       A2: (( RelIncl A) |_2 X) = ( RelIncl X) by Th1;

      

       A3: ( RelIncl X) is well-ordering by A1, Th2;

       A4:

      now

        assume (( RelIncl A),(( RelIncl A) |_2 X)) are_isomorphic ;

        then (( RelIncl X),( RelIncl A)) are_isomorphic by A2, WELLORD1: 40;

        hence thesis by A3, Def2;

      end;

       A5:

      now

        given a be object such that

         A6: a in A and

         A7: ((( RelIncl A) |_2 (( RelIncl A) -Seg a)),(( RelIncl A) |_2 X)) are_isomorphic ;

        reconsider a as Ordinal by A6;

        

         A8: (( RelIncl A) -Seg a) = a by A6, Th3;

        

         A9: a c= A by A6, ORDINAL1:def 2;

        then (( RelIncl A) |_2 a) = ( RelIncl a) by Th1;

        then (( RelIncl X),( RelIncl a)) are_isomorphic by A2, A7, A8, WELLORD1: 40;

        hence thesis by A3, A9, Def2;

      end;

      ( field ( RelIncl A)) = A by Def1;

      hence thesis by A1, A4, A5, WELLORD1: 53;

    end;

    reserve f,g for Function;

    definition

      let X, Y;

      :: original: are_equipotent

      redefine

      :: WELLORD2:def4

      pred X,Y are_equipotent means ex f st f is one-to-one & ( dom f) = X & ( rng f) = Y;

      compatibility

      proof

        thus (X,Y) are_equipotent implies ex f st f is one-to-one & ( dom f) = X & ( rng f) = Y

        proof

          assume (X,Y) are_equipotent ;

          then

          consider Z such that

           A1: for x be object st x in X holds ex y be object st y in Y & [x, y] in Z and

           A2: for y be object st y in Y holds ex x be object st x in X & [x, y] in Z and

           A3: for x,y,z,u be object st [x, y] in Z & [z, u] in Z holds x = z iff y = u;

          set F = (Z /\ [:X, Y:]);

          for x,y,z be object st [x, y] in F & [x, z] in F holds y = z

          proof

            let x,y,z be object;

            assume [x, y] in F & [x, z] in F;

            then [x, y] in Z & [x, z] in Z by XBOOLE_0:def 4;

            hence thesis by A3;

          end;

          then

          reconsider F as Function by FUNCT_1:def 1;

          take f = F;

          thus f is one-to-one

          proof

            let x,y be object;

            assume that

             A4: x in ( dom f) and

             A5: y in ( dom f) and

             A6: (f . x) = (f . y);

             [y, (f . y)] in f by A5, FUNCT_1: 1;

            then

             A7: [y, (f . y)] in Z by XBOOLE_0:def 4;

             [x, (f . x)] in f by A4, FUNCT_1: 1;

            then [x, (f . x)] in Z by XBOOLE_0:def 4;

            hence thesis by A3, A6, A7;

          end;

          thus ( dom f) c= X

          proof

            let x be object;

            assume x in ( dom f);

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

            then [x, (f . x)] in [:X, Y:] by XBOOLE_0:def 4;

            hence thesis by ZFMISC_1: 87;

          end;

          thus X c= ( dom f)

          proof

            let x be object;

            assume

             A8: x in X;

            then

            consider y be object such that

             A9: y in Y and

             A10: [x, y] in Z by A1;

             [x, y] in [:X, Y:] by A8, A9, ZFMISC_1: 87;

            then [x, y] in f by A10, XBOOLE_0:def 4;

            hence thesis by FUNCT_1: 1;

          end;

          thus ( rng f) c= Y

          proof

            let y be object;

            assume y in ( rng f);

            then

            consider x be object such that

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

             [x, y] in f by A11, FUNCT_1: 1;

            then [x, y] in [:X, Y:] by XBOOLE_0:def 4;

            hence thesis by ZFMISC_1: 87;

          end;

          thus Y c= ( rng f)

          proof

            let y be object;

            assume

             A12: y in Y;

            then

            consider x be object such that

             A13: x in X and

             A14: [x, y] in Z by A2;

             [x, y] in [:X, Y:] by A12, A13, ZFMISC_1: 87;

            then [x, y] in f by A14, XBOOLE_0:def 4;

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

            hence thesis by FUNCT_1:def 3;

          end;

        end;

        (ex f st f is one-to-one & ( dom f) = X & ( rng f) = Y) implies ex Z st (for x be object st x in X holds ex y be object st y in Y & [x, y] in Z) & (for y be object st y in Y holds ex x be object st x in X & [x, y] in Z) & for x,y,z,u be object st [x, y] in Z & [z, u] in Z holds x = z iff y = u

        proof

          given f such that

           A15: f is one-to-one and

           A16: ( dom f) = X and

           A17: ( rng f) = Y;

          take Z = f;

          thus for x be object holds x in X implies ex y be object st y in Y & [x, y] in Z

          proof

            let x be object;

            assume

             A18: x in X;

            take (f . x);

            thus (f . x) in Y by A16, A17, A18, FUNCT_1:def 3;

            thus thesis by A16, A18, FUNCT_1: 1;

          end;

          thus for y be object st y in Y holds ex x be object st x in X & [x, y] in Z

          proof

            let y be object such that

             A19: y in Y;

            take ((f " ) . y);

            

             A20: ( dom (f " )) = ( rng f) by A15, FUNCT_1: 33;

            then

             A21: ((f " ) . y) in ( rng (f " )) by A17, A19, FUNCT_1:def 3;

            

             A22: ( rng (f " )) = ( dom f) by A15, FUNCT_1: 33;

            hence ((f " ) . y) in X by A16, A17, A19, A20, FUNCT_1:def 3;

            y = (f . ((f " ) . y)) by A15, A17, A19, FUNCT_1: 35;

            hence thesis by A22, A21, FUNCT_1: 1;

          end;

          let x,y,z,u be object;

          assume

           A23: [x, y] in Z & [z, u] in Z;

          then

           A24: x in ( dom f) & z in ( dom f) by FUNCT_1: 1;

          y = (f . x) & u = (f . z) by A23, FUNCT_1: 1;

          hence thesis by A15, A24;

        end;

        hence thesis;

      end;

      reflexivity

      proof

        let X;

        take ( id X);

        thus thesis;

      end;

      symmetry

      proof

        let X, Y;

        given f such that

         A25: f is one-to-one & ( dom f) = X & ( rng f) = Y;

        take (f " );

        thus thesis by A25, FUNCT_1: 33;

      end;

    end

    theorem :: WELLORD2:15

    (X,Y) are_equipotent & (Y,Z) are_equipotent implies (X,Z) are_equipotent

    proof

      given f such that

       A1: f is one-to-one & ( dom f) = X & ( rng f) = Y;

      given g such that

       A2: g is one-to-one & ( dom g) = Y & ( rng g) = Z;

      take (g * f);

      thus thesis by A1, A2, RELAT_1: 27, RELAT_1: 28;

    end;

    theorem :: WELLORD2:16

    

     Th10: R well_orders X implies ( field (R |_2 X)) = X & (R |_2 X) is well-ordering

    proof

      assume that

       A1: R is_reflexive_in X and

       A2: R is_transitive_in X and

       A3: R is_antisymmetric_in X and

       A4: R is_connected_in X and

       A5: R is_well_founded_in X;

      

       A6: (R |_2 X) is_antisymmetric_in X

      proof

        let x,y be object;

        assume that

         A7: x in X & y in X and

         A8: [x, y] in (R |_2 X) & [y, x] in (R |_2 X);

         [x, y] in R & [y, x] in R by A8, XBOOLE_0:def 4;

        hence thesis by A3, A7;

      end;

      

       A9: (R |_2 X) is_well_founded_in X

      proof

        let Y;

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

        then

        consider a be object such that

         A10: a in Y and

         A11: (R -Seg a) misses Y by A5;

        take a;

        thus a in Y by A10;

        assume not thesis;

        then

        consider x be object such that

         A12: x in ((R |_2 X) -Seg a) and

         A13: x in Y by XBOOLE_0: 3;

         [x, a] in (R |_2 X) by A12, WELLORD1: 1;

        then

         A14: [x, a] in R by XBOOLE_0:def 4;

        x <> a by A12, WELLORD1: 1;

        then x in (R -Seg a) by A14, WELLORD1: 1;

        hence contradiction by A11, A13, XBOOLE_0: 3;

      end;

      

       A15: (R |_2 X) is_transitive_in X

      proof

        let x,y,z be object;

        assume that

         A16: x in X and

         A17: y in X and

         A18: z in X and

         A19: [x, y] in (R |_2 X) & [y, z] in (R |_2 X);

         [x, y] in R & [y, z] in R by A19, XBOOLE_0:def 4;

        then

         A20: [x, z] in R by A2, A16, A17, A18;

         [x, z] in [:X, X:] by A16, A18, ZFMISC_1: 87;

        hence thesis by A20, XBOOLE_0:def 4;

      end;

      

       A21: (R |_2 X) is_connected_in X

      proof

        let x,y be object;

        assume that

         A22: x in X & y in X and

         A23: x <> y;

        

         A24: [x, y] in [:X, X:] & [y, x] in [:X, X:] by A22, ZFMISC_1: 87;

         [x, y] in R or [y, x] in R by A4, A22, A23;

        hence thesis by A24, XBOOLE_0:def 4;

      end;

      thus

       A25: ( field (R |_2 X)) = X

      proof

        thus ( field (R |_2 X)) c= X by WELLORD1: 13;

        let x be object;

        assume x in X;

        then [x, x] in R & [x, x] in [:X, X:] by A1, ZFMISC_1: 87;

        then [x, x] in (R |_2 X) by XBOOLE_0:def 4;

        hence thesis by RELAT_1: 15;

      end;

      (R |_2 X) is_reflexive_in X

      proof

        let x be object;

        assume x in X;

        then [x, x] in R & [x, x] in [:X, X:] by A1, ZFMISC_1: 87;

        hence thesis by XBOOLE_0:def 4;

      end;

      then (R |_2 X) well_orders X by A15, A6, A21, A9;

      hence thesis by A25, WELLORD1: 4;

    end;

    

     Lm1: R is well-ordering & (X,( field R)) are_equipotent implies ex R st R well_orders X

    proof

      assume

       A1: R is well-ordering;

      given f such that

       A2: f is one-to-one and

       A3: ( dom f) = X and

       A4: ( rng f) = ( field R);

      defpred P[ object, object] means [(f . $1), (f . $2)] in R;

      consider Q be Relation such that

       A5: for x,y be object holds [x, y] in Q iff x in X & y in X & P[x, y] from RELAT_1:sch 1;

      take Q;

      

       A6: R is_reflexive_in ( field R) by A1, RELAT_2:def 9;

      

       A7: ( field Q) = X

      proof

        thus ( field Q) c= X

        proof

          let x be object;

          assume that

           A8: x in ( field Q) and

           A9: not x in X;

          for y be object holds not [y, x] in Q by A5, A9;

          then

           A10: not x in ( rng Q) by XTUPLE_0:def 13;

          for y be object holds not [x, y] in Q by A5, A9;

          then not x in ( dom Q) by XTUPLE_0:def 12;

          hence contradiction by A8, A10, XBOOLE_0:def 3;

        end;

        let x be object;

        assume

         A11: x in X;

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

        then [(f . x), (f . x)] in R by A6, A4;

        then [x, x] in Q by A5, A11;

        hence thesis by RELAT_1: 15;

      end;

      f is_isomorphism_of (Q,R) by A2, A3, A4, A7, A5;

      then (f " ) is_isomorphism_of (R,Q) by WELLORD1: 39;

      then Q is well-ordering by A1, WELLORD1: 44;

      hence thesis by A7, WELLORD1: 4;

    end;

    ::$Notion-Name

    theorem :: WELLORD2:17

    

     Th11: for X holds ex R st R well_orders X

    proof

      deffunc F( object) = {$1};

      defpred P[ object] means $1 is Ordinal;

      let X;

      consider Class be set such that

       A1: X in Class and

       A2: Y in Class & Z c= Y implies Z in Class and Y in Class implies ( bool Y) in Class and

       A3: Y c= Class implies (Y,Class) are_equipotent or Y in Class by ZFMISC_1: 112;

      consider ON be set such that

       A4: for x be object holds x in ON iff x in Class & P[x] from XBOOLE_0:sch 1;

      for Y st Y in ON holds Y is Ordinal & Y c= ON

      proof

        let Y;

        assume

         A5: Y in ON;

        hence Y is Ordinal by A4;

        reconsider A = Y as Ordinal by A4, A5;

        let x be object;

        assume

         A6: x in Y;

        then x in A;

        then

        reconsider B = x as Ordinal;

        

         A7: B c= A by A6, ORDINAL1:def 2;

        A in Class by A4, A5;

        then B in Class by A2, A7;

        hence thesis by A4;

      end;

      then

      reconsider ON as epsilon-transitive epsilon-connected set by ORDINAL1: 19;

      

       A8: ON c= Class by A4;

      

       A9: (ON,Class) are_equipotent

      proof

        assume not thesis;

        then ON in Class by A3, A8;

        then ON in ON by A4;

        hence contradiction;

      end;

      ( field ( RelIncl ON)) = ON by Def1;

      then

      consider R such that

       A10: R well_orders Class by A9, Lm1;

      consider f such that

       A11: ( dom f) = X & for x be object st x in X holds (f . x) = F(x) from FUNCT_1:sch 3;

      

       A12: ( rng f) c= Class

      proof

        let x be object;

        assume x in ( rng f);

        then

        consider y be object such that

         A13: y in ( dom f) and

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

        

         A15: {y} c= X by A11, A13, TARSKI:def 1;

        (f . y) = {y} by A11, A13;

        hence thesis by A1, A2, A14, A15;

      end;

      

       A16: (X,( rng f)) are_equipotent

      proof

        take f;

        thus f is one-to-one

        proof

          let x,y be object;

          assume that

           A17: x in ( dom f) & y in ( dom f) and

           A18: (f . x) = (f . y);

          (f . x) = {x} & (f . y) = {y} by A11, A17;

          hence thesis by A18, ZFMISC_1: 3;

        end;

        thus thesis by A11;

      end;

      set Q = (R |_2 Class);

      ( field Q) = Class by A10, Th10;

      then

       A19: ( field (Q |_2 ( rng f))) = ( rng f) by A10, A12, Th10, WELLORD1: 31;

      Q is well-ordering by A10, Th10;

      hence thesis by A16, A19, Lm1, WELLORD1: 25;

    end;

    reserve M for non empty set;

    ::$Notion-Name

    theorem :: WELLORD2:18

    (for X st X in M holds X <> {} ) & (for X, Y st X in M & Y in M & X <> Y holds X misses Y) implies ex Choice be set st for X st X in M holds ex x be object st (Choice /\ X) = {x}

    proof

      assume that

       A1: for X st X in M holds X <> {} and

       A2: for X, Y st X in M & Y in M & X <> Y holds X misses Y;

      consider R such that

       A3: R well_orders ( union M) by Th11;

      

       A4: R is_reflexive_in ( union M) by A3;

      

       A5: R is_connected_in ( union M) by A3;

      defpred Ch[ object, object] means ex D1 be set st D1 = $1 & $2 in D1 & for z st z in D1 holds [$2, z] in R;

      

       A6: R is_antisymmetric_in ( union M) by A3;

      

       A7: for x,y,z be object st x in M & Ch[x, y] & Ch[x, z] holds y = z

      proof

        let x,y,z be object such that

         A8: x in M;

        given X such that

         A9: X = x and

         A10: y in X and

         A11: for u st u in X holds [y, u] in R;

        

         A12: y in ( union M) by A8, A10, TARSKI:def 4, A9;

        given X such that

         A13: X = x and

         A14: z in X and

         A15: for u st u in X holds [z, u] in R;

        

         A16: z in ( union M) by A8, A14, TARSKI:def 4, A13;

         [y, z] in R & [z, y] in R by A10, A11, A14, A15, A9, A13;

        hence thesis by A6, A12, A16;

      end;

      

       A17: R is_well_founded_in ( union M) by A3;

      

       A18: for x be object st x in M holds ex y be object st Ch[x, y]

      proof

        let x be object;

        assume

         A19: x in M;

        reconsider xx = x as set by TARSKI: 1;

        

         A20: xx c= ( union M) by ZFMISC_1: 74, A19;

        x <> {} by A1, A19;

        then

        consider y be object such that

         A21: y in xx and

         A22: (R -Seg y) misses xx by A17, A20;

        take y;

        take xx;

        thus xx = x;

        thus y in xx by A21;

        let z;

        assume

         A23: z in xx;

        then

         A24: not z in (R -Seg y) by A22, XBOOLE_0: 3;

        y <> z implies [y, z] in R or [z, y] in R by A5, A20, A21, A23;

        hence thesis by A4, A20, A23, A24, WELLORD1: 1;

      end;

      consider f such that

       A25: ( dom f) = M & for x be object st x in M holds Ch[x, (f . x)] from FUNCT_1:sch 2( A7, A18);

      take Choice = ( rng f);

      let X such that

       A26: X in M;

      take x = (f . X);

      thus (Choice /\ X) c= {x}

      proof

        let y be object;

        assume

         A27: y in (Choice /\ X);

        then

         A28: y in X by XBOOLE_0:def 4;

        y in Choice by A27, XBOOLE_0:def 4;

        then

        consider z be object such that

         A29: z in ( dom f) and

         A30: y = (f . z) by FUNCT_1:def 3;

        reconsider z as set by TARSKI: 1;

        assume not y in {x};

        then X <> z by A30, TARSKI:def 1;

        then X misses z by A2, A25, A26, A29;

        then

         A31: (X /\ z) = {} ;

         Ch[z, (f . z)] by A25, A29;

        then (f . z) in z;

        hence contradiction by A28, A30, A31, XBOOLE_0:def 4;

      end;

      let y be object;

      assume y in {x};

      then

       A32: y = x by TARSKI:def 1;

       Ch[X, (f . X)] by A25, A26;

      then

       A33: y in X by A32;

      y in Choice by A25, A26, A32, FUNCT_1:def 3;

      hence thesis by A33, XBOOLE_0:def 4;

    end;

    begin

    theorem :: WELLORD2:19

    for X be set holds ( RelIncl X) is_reflexive_in X by Def1;

    theorem :: WELLORD2:20

    for X be set holds ( RelIncl X) is_transitive_in X

    proof

      let X be set;

      ( RelIncl X) is transitive & ( field ( RelIncl X)) = X by Def1;

      hence thesis;

    end;

    theorem :: WELLORD2:21

    for X be set holds ( RelIncl X) is_antisymmetric_in X

    proof

      let X be set;

      ( RelIncl X) is antisymmetric & ( field ( RelIncl X)) = X by Def1;

      hence thesis;

    end;

    registration

      cluster ( RelIncl {} ) -> empty;

      coherence

      proof

        for Y,Z be set st Y in {} & Z in {} holds [Y, Z] in {} iff Y c= Z;

        hence thesis by Def1, RELAT_1: 40;

      end;

    end

    registration

      let X be non empty set;

      cluster ( RelIncl X) -> non empty;

      coherence

      proof

        set a = the Element of X;

         [a, a] in ( RelIncl X) by Def1;

        hence thesis;

      end;

    end

    theorem :: WELLORD2:22

    ( RelIncl {x}) = { [x, x]}

    proof

      

       A1: for Y,Z be set st Y in {x} & Z in {x} holds [Y, Z] in { [x, x]} iff Y c= Z

      proof

        let Y,Z be set;

        assume that

         A2: Y in {x} and

         A3: Z in {x};

        

         A4: Y = x by A2, TARSKI:def 1;

        hence [Y, Z] in { [x, x]} implies Y c= Z by A3, TARSKI:def 1;

        Z = x by A3, TARSKI:def 1;

        hence thesis by A4, TARSKI:def 1;

      end;

      ( field { [x, x]}) = {x} by RELAT_1: 173;

      hence thesis by A1, Def1;

    end;

    theorem :: WELLORD2:23

    ( RelIncl X) c= [:X, X:]

    proof

      set R = ( RelIncl X);

      let a,b be object;

      assume

       A1: [a, b] in R;

      then b in ( field R) by RELAT_1: 15;

      then

       A2: b in X by Def1;

      a in ( field R) by A1, RELAT_1: 15;

      then a in X by Def1;

      hence thesis by A2, ZFMISC_1: 87;

    end;