:: WELLORD2 semantic presentation

begin


definition
let X be set ;
func RelIncl X ->  Relation means :Def1: :: WELLORD2:def 1
( field it = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in it iff Y c= Z ) ) );
existence
 ex b1 being Relation st
( field b1 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b1 iff Y c= Z ) ) )
proof
defpred S1[ set , set ] means $1 c= $2;
consider R being Relation such that
A1: for x, y being set holds
( [x,y] in R iff ( x in X & y in X & S1[x,y] ) ) from RELAT_1:sch_1();
take  R ; ::_thesis: ( field R = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in R iff Y c= Z ) ) )
thus  field R = X ::_thesis: for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in R iff Y c= Z )
proof
thus  for x being set st x in field R holds
x in X :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: X c= field R
proof
let x be set ; ::_thesis: ( x in field R implies x in X )
A2: now__::_thesis:_(_x_in_dom_R_&_x_in_field_R_implies_x_in_X_)
assume  x in dom R ; ::_thesis: ( x in field R implies x in X )
then  ex y being set st [x,y] in R by XTUPLE_0:def_12;
hence  ( x in field R implies x in X ) by A1; ::_thesis: verum
end;
A3: now__::_thesis:_(_x_in_rng_R_&_x_in_field_R_implies_x_in_X_)
assume  x in rng R ; ::_thesis: ( x in field R implies x in X )
then  ex y being set st [y,x] in R by XTUPLE_0:def_13;
hence  ( x in field R implies x in X ) by A1; ::_thesis: verum
end;
assume  x in field R ; ::_thesis: x in X
hence  x in X by A2, A3, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in field R )
assume  x in X ; ::_thesis: x in field R
then  [x,x] in R by A1;
hence  x in field R by RELAT_1:15; ::_thesis: verum
end;
let Y, Z be set ; ::_thesis: ( Y in X & Z in X implies ( [Y,Z] in R iff Y c= Z ) )
assume A4: ( Y in X & Z in X ) ; ::_thesis: ( [Y,Z] in R iff Y c= Z )
thus  ( [Y,Z] in R implies Y c= Z ) by A1; ::_thesis: ( Y c= Z implies [Y,Z] in R )
thus  ( Y c= Z implies [Y,Z] in R ) by A1, A4; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Relation st field b1 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b1 iff Y c= Z ) ) & field b2 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b2 iff Y c= Z ) ) holds
b1 = b2
proof
let R1, R2 be Relation; ::_thesis: ( field R1 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in R1 iff Y c= Z ) ) & field R2 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in R2 iff Y c= Z ) ) implies R1 = R2 )
assume that
A5: field R1 = X and
A6: for Y, Z being set 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 being set st Y in X & Z in X holds
( [Y,Z] in R2 iff Y c= Z ) ; ::_thesis: R1 = R2
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in R1 or [x,b1] in R2 ) & ( not [x,b1] in R2 or [x,b1] in R1 ) )
let y be set ; ::_thesis: ( ( not [x,y] in R1 or [x,y] in R2 ) & ( not [x,y] in R2 or [x,y] in R1 ) )
thus  ( [x,y] in R1 implies [x,y] in R2 ) ::_thesis: ( not [x,y] in R2 or [x,y] in R1 )
proof
assume A9: [x,y] in R1 ; ::_thesis: [x,y] in R2
then A10: ( x in field R1 & y in field R1 ) by RELAT_1:15;
then  x c= y by A5, A6, A9;
hence  [x,y] in R2 by A5, A8, A10; ::_thesis: verum
end;
assume A11: [x,y] in R2 ; ::_thesis: [x,y] in R1
then A12: ( x in field R2 & y in field R2 ) by RELAT_1:15;
then  x c= y by A7, A8, A11;
hence  [x,y] in R1 by A6, A7, A12; ::_thesis: verum
end;
end;

:: deftheorem Def1 defines RelIncl WELLORD2:def_1_:_
 for X being set
for b2 being Relation holds
( b2 = RelIncl X iff ( field b2 = X & ( for Y, Z being set st Y in X & Z in X holds
( [Y,Z] in b2 iff Y c= Z ) ) ) );

theorem :: WELLORD2:1
canceled;

theorem :: WELLORD2:2
canceled;

theorem :: WELLORD2:3
canceled;

theorem :: WELLORD2:4
canceled;

theorem :: WELLORD2:5
canceled;

theorem :: WELLORD2:6
canceled;

registration
let X be set ;
cluster RelIncl X ->  reflexive ;
coherence
 RelIncl X is reflexive
proof
A1: field (RelIncl X) = X by Def1;
let a be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not a in field (RelIncl X) or [a,a] in RelIncl X )
assume  a in field (RelIncl X) ; ::_thesis: [a,a] in RelIncl X
hence  [a,a] in RelIncl X by A1, Def1; ::_thesis: verum
end;
cluster RelIncl X ->  transitive ;
coherence
 RelIncl X is transitive
proof
let a be set ; :: according to RELAT_2:def_8,RELAT_2:def_16 ::_thesis: for b1, b2 being set holds
( not a in field (RelIncl X) or not b1 in field (RelIncl X) or not b2 in field (RelIncl X) or not [a,b1] in RelIncl X or not [b1,b2] in RelIncl X or [a,b2] in RelIncl X )
let b, c be set ; ::_thesis: ( not a in field (RelIncl X) or not b in field (RelIncl X) or not c in field (RelIncl X) or not [a,b] in RelIncl X or not [b,c] in RelIncl X or [a,c] in RelIncl X )
assume 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 ) ; ::_thesis: [a,c] in RelIncl X
 field (RelIncl X) = X by Def1;
then  ( a c= b & b c= c ) by A2, A3, A4, A5, Def1;
then A6: a c= c by XBOOLE_1:1;
 ( a in X & c in X ) by A2, A4, Def1;
hence  [a,c] in RelIncl X by A6, Def1; ::_thesis: verum
end;
cluster RelIncl X ->  antisymmetric ;
coherence
 RelIncl X is antisymmetric
proof
A7: field (RelIncl X) = X by Def1;
let a be set ; :: according to RELAT_2:def_4,RELAT_2:def_12 ::_thesis: for b1 being set holds
( not a in field (RelIncl X) or not b1 in field (RelIncl X) or not [a,b1] in RelIncl X or not [b1,a] in RelIncl X or a = b1 )
let b be set ; ::_thesis: ( not a in field (RelIncl X) or not b in field (RelIncl X) or not [a,b] in RelIncl X or not [b,a] in RelIncl X or a = b )
assume  ( a in field (RelIncl X) & b in field (RelIncl X) & [a,b] in RelIncl X & [b,a] in RelIncl X ) ; ::_thesis: a = b
then  ( a c= b & b c= a ) by A7, Def1;
hence  a = b by XBOOLE_0:def_10; ::_thesis: verum
end;
end;

registration
let A be Ordinal;
cluster RelIncl A ->  connected ;
coherence
 RelIncl A is connected
proof
let a be set ; :: according to RELAT_2:def_6,RELAT_2:def_14 ::_thesis: for b1 being set holds
( not a in field (RelIncl A) or not b1 in field (RelIncl A) or a = b1 or [a,b1] in RelIncl A or [b1,a] in RelIncl A )
let b be set ; ::_thesis: ( not a in field (RelIncl A) or not b in field (RelIncl A) or a = b or [a,b] in RelIncl A or [b,a] in RelIncl A )
assume that
A1: ( a in field (RelIncl A) & b in field (RelIncl A) ) and
 a <> b ; ::_thesis: ( [a,b] in RelIncl A or [b,a] in RelIncl A )
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  ( [a,b] in RelIncl A or [b,a] in RelIncl A ) by A1, A2, Def1; ::_thesis: verum
end;
cluster RelIncl A ->  well_founded ;
coherence
 RelIncl A is well_founded
proof
let Y be set ; :: according to WELLORD1:def_2 ::_thesis: ( not Y c= field (RelIncl A) or Y = {} or ex b1 being set st
( b1 in Y & (RelIncl A) -Seg b1 misses Y ) )
assume that
A3: Y c= field (RelIncl A) and
A4: Y <> {} ; ::_thesis: ex b1 being set st
( b1 in Y & (RelIncl A) -Seg b1 misses Y )
defpred S1[ set ] means A in Y;
set x = the Element of Y;
A5: field (RelIncl A) = A by Def1;
then  the Element of Y in A by A3, A4, TARSKI:def_3;
then reconsider x = the Element of Y as Ordinal ;
 x in Y by A4;
then A6: ex B being Ordinal st S1[B] ;
consider B being Ordinal such that
A7: ( S1[B] & ( for C being Ordinal st S1[C] holds
B c= C ) ) from ORDINAL1:sch_1(A6);
reconsider x = B as set ;
take  x ; ::_thesis: ( x in Y & (RelIncl A) -Seg x misses Y )
thus  x in Y by A7; ::_thesis: (RelIncl A) -Seg x misses Y
set y = the Element of ((RelIncl A) -Seg x) /\ Y;
assume A8: ((RelIncl A) -Seg x) /\ Y <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction
then A9: the Element of ((RelIncl A) -Seg x) /\ Y in Y by XBOOLE_0:def_4;
then reconsider C = the Element of ((RelIncl A) -Seg x) /\ Y as Ordinal by A3, A5;
A10: the Element of ((RelIncl A) -Seg x) /\ Y in (RelIncl A) -Seg x by A8, XBOOLE_0:def_4;
then  [ the Element of ((RelIncl A) -Seg x) /\ Y,x] in RelIncl A by WELLORD1:1;
then A11: C c= B by A3, A5, A7, A9, Def1;
A12: the Element of ((RelIncl A) -Seg x) /\ Y <> x by A10, WELLORD1:1;
 B c= C by A7, A9;
hence  contradiction by A12, A11, XBOOLE_0:def_10; ::_thesis: verum
end;
end;

theorem Th7: :: WELLORD2:7
for Y, X being set st Y c= X holds
(RelIncl X) |_2 Y = RelIncl Y
proof
let Y, X be set ; ::_thesis: ( Y c= X implies (RelIncl X) |_2 Y = RelIncl Y )
assume A1: Y c= X ; ::_thesis: (RelIncl X) |_2 Y = RelIncl Y
let a be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [a,b1] in (RelIncl X) |_2 Y or [a,b1] in RelIncl Y ) & ( not [a,b1] in RelIncl Y or [a,b1] in (RelIncl X) |_2 Y ) )
let b be set ; ::_thesis: ( ( not [a,b] in (RelIncl X) |_2 Y or [a,b] in RelIncl Y ) & ( not [a,b] in RelIncl Y or [a,b] in (RelIncl X) |_2 Y ) )
thus  ( [a,b] in (RelIncl X) |_2 Y implies [a,b] in RelIncl Y ) ::_thesis: ( not [a,b] in RelIncl Y or [a,b] in (RelIncl X) |_2 Y )
proof
assume A2: [a,b] in (RelIncl X) |_2 Y ; ::_thesis: [a,b] in RelIncl Y
then  [a,b] in [:Y,Y:] by XBOOLE_0:def_4;
then A3: ( a in Y & b in Y ) by ZFMISC_1:87;
 [a,b] in RelIncl X by A2, XBOOLE_0:def_4;
then  a c= b by A1, A3, Def1;
hence  [a,b] in RelIncl Y by A3, Def1; ::_thesis: verum
end;
assume A4: [a,b] in RelIncl Y ; ::_thesis: [a,b] in (RelIncl X) |_2 Y
then A5: ( a in field (RelIncl Y) & b in field (RelIncl Y) ) by RELAT_1:15;
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  [a,b] in (RelIncl X) |_2 Y by A7, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th8: :: WELLORD2:8
for A being Ordinal
for X being set st X c= A holds
RelIncl X is well-ordering
proof
let A be Ordinal; ::_thesis: for X being set st X c= A holds
RelIncl X is well-ordering
let X be set ; ::_thesis: ( X c= A implies RelIncl X is well-ordering )
 (RelIncl A) |_2 X is well-ordering by WELLORD1:25;
hence  ( X c= A implies RelIncl X is well-ordering ) by Th7; ::_thesis: verum
end;

theorem Th9: :: WELLORD2:9
for A, B being Ordinal st A in B holds
A = (RelIncl B) -Seg A
proof
let A, B be Ordinal; ::_thesis: ( A in B implies A = (RelIncl B) -Seg A )
assume A1: A in B ; ::_thesis: A = (RelIncl B) -Seg A
thus  for a being set st a in A holds
a in (RelIncl B) -Seg A :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: (RelIncl B) -Seg A c= A
proof
let a be set ; ::_thesis: ( a in A implies a in (RelIncl B) -Seg A )
assume A2: a in A ; ::_thesis: a in (RelIncl B) -Seg A
then reconsider C = a as Ordinal ;
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  a in (RelIncl B) -Seg A by A3, WELLORD1:1; ::_thesis: verum
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (RelIncl B) -Seg A or a in A )
assume A5: a in (RelIncl B) -Seg A ; ::_thesis: a in 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, XBOOLE_0:def_8;
hence  a in A by ORDINAL1:11; ::_thesis: verum
end;

theorem Th10: :: WELLORD2:10
for A, B being Ordinal st RelIncl A, RelIncl B are_isomorphic holds
A = B
proof
let A, B be Ordinal; ::_thesis: ( RelIncl A, RelIncl B are_isomorphic implies A = B )
A1: field (RelIncl A) = A by Def1;
assume A2: RelIncl A, RelIncl B are_isomorphic ; ::_thesis: A = B
A3: now__::_thesis:_not_A_in_B
A4: field (RelIncl B) = B by Def1;
assume A5: A in B ; ::_thesis: contradiction
then  A = (RelIncl B) -Seg A by Th9;
then  RelIncl A = (RelIncl B) |_2 ((RelIncl B) -Seg A) by A4, Th7, WELLORD1:9;
hence  contradiction by A2, A5, A4, WELLORD1:40, WELLORD1:46; ::_thesis: verum
end;
assume  A <> B ; ::_thesis: contradiction
then A6: ( A in B or B in A ) by ORDINAL1:14;
then  B = (RelIncl A) -Seg B by A3, Th9;
then  RelIncl B = (RelIncl A) |_2 ((RelIncl A) -Seg B) by A1, Th7, WELLORD1:9;
hence  contradiction by A2, A6, A3, A1, WELLORD1:46; ::_thesis: verum
end;

theorem Th11: :: WELLORD2:11
for R being Relation
for A, B being Ordinal st R, RelIncl A are_isomorphic & R, RelIncl B are_isomorphic holds
A = B
proof
let R be Relation; ::_thesis: for A, B being Ordinal st R, RelIncl A are_isomorphic & R, RelIncl B are_isomorphic holds
A = B
let A, B be Ordinal; ::_thesis: ( R, RelIncl A are_isomorphic & R, RelIncl B are_isomorphic implies A = B )
assume that
A1: R, RelIncl A are_isomorphic and
A2: R, RelIncl B are_isomorphic ; ::_thesis: A = B
 RelIncl A,R are_isomorphic by A1, WELLORD1:40;
hence  A = B by A2, Th10, WELLORD1:42; ::_thesis: verum
end;

theorem Th12: :: WELLORD2:12
for R being Relation st R is well-ordering & ( for a being set st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic ) holds
ex A being Ordinal st R, RelIncl A are_isomorphic
proof
let R be Relation; ::_thesis: ( R is well-ordering & ( for a being set st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic ) implies ex A being Ordinal st R, RelIncl A are_isomorphic )
assume A1: R is well-ordering ; ::_thesis: ( ex a being set st
( a in field R & ( for A being Ordinal holds not R |_2 (R -Seg a), RelIncl A are_isomorphic ) ) or ex A being Ordinal st R, RelIncl A are_isomorphic )
defpred S1[ set , set ] means  for A being Ordinal holds
( A = $2 iff R |_2 (R -Seg $1), RelIncl A are_isomorphic );
assume A2: for a being set st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic ; ::_thesis: ex A being Ordinal st R, RelIncl A are_isomorphic
A3: for a being set st a in field R holds
ex b being set st S1[a,b]
proof
let a be set ; ::_thesis: ( a in field R implies ex b being set st S1[a,b] )
assume  a in field R ; ::_thesis: ex b being set st S1[a,b]
then consider A being Ordinal such that
A4: R |_2 (R -Seg a), RelIncl A are_isomorphic by A2;
reconsider b = A as set ;
take  b ; ::_thesis: S1[a,b]
let B be Ordinal; ::_thesis: ( B = b iff R |_2 (R -Seg a), RelIncl B are_isomorphic )
thus  ( B = b implies R |_2 (R -Seg a), RelIncl B are_isomorphic ) by A4; ::_thesis: ( R |_2 (R -Seg a), RelIncl B are_isomorphic implies B = b )
assume  R |_2 (R -Seg a), RelIncl B are_isomorphic ; ::_thesis: B = b
hence  B = b by A4, Th11; ::_thesis: verum
end;
A5: for b, c, d being set st b in field R & S1[b,c] & S1[b,d] holds
c = d
proof
let b, c, d be set ; ::_thesis: ( b in field R & S1[b,c] & S1[b,d] implies c = d )
assume that
A6: b in field R and
A7: for A being Ordinal holds
( A = c iff R |_2 (R -Seg b), RelIncl A are_isomorphic ) and
A8: for B being Ordinal holds
( B = d iff R |_2 (R -Seg b), RelIncl B are_isomorphic ) ; ::_thesis: c = d
consider A being Ordinal such that
A9: R |_2 (R -Seg b), RelIncl A are_isomorphic by A2, A6;
 A = c by A7, A9;
hence  c = d by A8, A9; ::_thesis: verum
end;
consider H being Function such that
A10: ( dom H = field R & ( for b being set st b in field R holds
S1[b,H . b] ) ) from FUNCT_1:sch_2(A5, A3);
 for a being set st a in rng H holds
a is Ordinal
proof
let b be set ; ::_thesis: ( b in rng H implies b is Ordinal )
assume  b in rng H ; ::_thesis: b is Ordinal
then consider c being set  such that
A11: c in dom H and
A12: b = H . c by FUNCT_1:def_3;
 ex A being Ordinal st R |_2 (R -Seg c), RelIncl A are_isomorphic by A2, A10, A11;
hence  b is Ordinal by A10, A11, A12; ::_thesis: verum
end;
then consider C being Ordinal such that
A13: rng H c= C by ORDINAL1:24;
A14: now__::_thesis:_for_b_being_set_st_b_in_rng_H_holds_
for_c_being_set_st_[c,b]_in_RelIncl_C_holds_
c_in_rng_H
let b be set ; ::_thesis: ( b in rng H implies for c being set st [c,b] in RelIncl C holds
c in rng H )
assume A15: b in rng H ; ::_thesis: for c being set st [c,b] in RelIncl C holds
c in rng H
then consider b9 being set  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 (R -Seg b9);
consider A being Ordinal such that
A18: R |_2 (R -Seg b9), RelIncl A are_isomorphic by A2, A10, A16;
let c be set ; ::_thesis: ( [c,b] in RelIncl C implies c in rng H )
assume A19: [c,b] in RelIncl C ; ::_thesis: c in rng H
A20: A = b by A10, A16, A17, A18;
now__::_thesis:_(_c_<>_b_implies_c_in_rng_H_)
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 Th7;
assume  c <> b ; ::_thesis: c in rng H
then A25: B c< A by A20, A23, XBOOLE_0:def_8;
then A26: B = (RelIncl A) -Seg B by Th9, ORDINAL1:11;
A27: A = field (RelIncl A) by Def1;
 RelIncl A,R |_2 (R -Seg b9) are_isomorphic by A18, WELLORD1:40;
then  canonical_isomorphism_of ((RelIncl A),(R |_2 (R -Seg b9))) is_isomorphism_of RelIncl A,R |_2 (R -Seg b9) by WELLORD1:def_9;
then consider d being set  such that
A28: d in field (R |_2 (R -Seg b9)) and
A29: (RelIncl A) |_2 ((RelIncl A) -Seg B),(R |_2 (R -Seg b9)) |_2 ((R |_2 (R -Seg b9)) -Seg d) are_isomorphic by A25, A27, ORDINAL1:11, WELLORD1:50;
A30: d in field R by A28, WELLORD1:12;
A31: (R |_2 (R -Seg b9)) -Seg d = R -Seg d by A1, A28, WELLORD1:12, WELLORD1:27;
 d in R -Seg b9 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; ::_thesis: verum
end;
hence  c in rng H by A15; ::_thesis: verum
end;
A32: ( ex a being set st
( a in C & rng H = (RelIncl C) -Seg a ) implies rng H is Ordinal ) by Th9;
 ( 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 ; ::_thesis: R, RelIncl A are_isomorphic
take  H ; :: according to WELLORD1:def_8 ::_thesis: H is_isomorphism_of R, RelIncl A
thus  dom H = field R by A10; :: according to WELLORD1:def_7 ::_thesis: ( rng H = field (RelIncl A) & H is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(H . b1),(H . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(H . b1),(H . b2)] in RelIncl A or [b1,b2] in R ) ) ) )
thus  rng H = field (RelIncl A) by Def1; ::_thesis: ( H is one-to-one & ( for b1, b2 being set holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(H . b1),(H . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(H . b1),(H . b2)] in RelIncl A or [b1,b2] in R ) ) ) )
A33: for a being set st a in dom H holds
H . a is Ordinal
proof
let a be set ; ::_thesis: ( a in dom H implies H . a is Ordinal )
assume  a in dom H ; ::_thesis: H . a is Ordinal
then  H . a in A by FUNCT_1:def_3;
hence  H . a is Ordinal ; ::_thesis: verum
end;
thus A34: H is one-to-one ::_thesis: for b1, b2 being set holds
( ( not [b1,b2] in R or ( b1 in field R & b2 in field R & [(H . b1),(H . b2)] in RelIncl A ) ) & ( not b1 in field R or not b2 in field R or not [(H . b1),(H . b2)] in RelIncl A or [b1,b2] in R ) )
proof
let a be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not a in dom H or not b1 in dom H or not H . a = H . b1 or a = b1 )
let b be set ; ::_thesis: ( not a in dom H or not b in dom H or not H . a = H . b or a = b )
assume that
A35: a in dom H and
A36: b in dom H and
A37: H . a = H . b ; ::_thesis: a = 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  a = b by A1, A10, A35, A36, WELLORD1:47; ::_thesis: verum
end;
let a, b be set ; ::_thesis: ( ( not [a,b] in R or ( a in field R & b in field R & [(H . a),(H . b)] in RelIncl A ) ) & ( not a in field R or not b in field R or not [(H . a),(H . b)] in RelIncl A or [a,b] in R ) )
thus  ( [a,b] in R implies ( a in field R & b in field R & [(H . a),(H . b)] in RelIncl A ) ) ::_thesis: ( not a in field R or not b in field R or not [(H . a),(H . b)] in RelIncl A or [a,b] in R )
proof
set Z = R -Seg b;
set P = R |_2 (R -Seg b);
A39: ( A = field (RelIncl A) & R |_2 (R -Seg b) is well-ordering ) by A1, Def1, WELLORD1:25;
assume A40: [a,b] in R ; ::_thesis: ( a in field R & b in field R & [(H . a),(H . b)] in RelIncl A )
hence A41: ( a in field R & b in field R ) by RELAT_1:15; ::_thesis: [(H . a),(H . b)] in RelIncl A
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__::_thesis:_(_a_<>_b_implies_[A9,B9]_in_RelIncl_A_)
assume  a <> b ; ::_thesis: [A9,B9] in RelIncl A
then A46: a in R -Seg b by A40, WELLORD1:1;
then A47: (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, WELLORD1:27;
 R -Seg b c= field R by WELLORD1:9;
then A48: a in field (R |_2 (R -Seg b)) by A1, A46, WELLORD1:31;
 A9 c= A by A43, ORDINAL1:def_2;
then A49: (RelIncl A) |_2 A9 = RelIncl A9 by Th7;
 ( A9 = (RelIncl A) -Seg A9 & R -Seg a c= R -Seg b ) by A1, A40, A41, A43, Th9, WELLORD1:29;
then A50: (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -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, Th9, ORDINAL1:def_2;
then  R |_2 (R -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A42, Th7;
hence  [A9,B9] in RelIncl A by A43, A44, A39, A48, A50, WELLORD1:51; ::_thesis: verum
end;
hence  [(H . a),(H . b)] in RelIncl A by A43, Def1; ::_thesis: verum
end;
assume that
A51: a in field R and
A52: b in field R and
A53: [(H . a),(H . b)] in RelIncl A ; ::_thesis: [a,b] in R
assume A54: not [a,b] in R ; ::_thesis: contradiction
 R is_reflexive_in field R by A1, RELAT_2:def_9;
then A55: a <> b by A51, A54, RELAT_2:def_1;
 R is_connected_in field R by A1, RELAT_2:def_14;
then A56: [b,a] in R by A51, A52, A54, A55, RELAT_2:def_6;
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 Th7;
set Z = R -Seg a;
set P = R |_2 (R -Seg a);
A64: A9 in A by A10, A51, FUNCT_1:def_3;
then  ( A9 = (RelIncl A) -Seg A9 & A9 c= A ) by Th9, ORDINAL1:def_2;
then A65: R |_2 (R -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A60, Th7;
A66: b in R -Seg a by A54, A56, WELLORD1:1;
then A67: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, WELLORD1:27;
 B9 = (RelIncl A) -Seg B9 by A62, Th9;
then A68: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A61, A63, A67, A57, WELLORD1:22;
 R -Seg a c= field R by WELLORD1:9;
then A69: b in field (R |_2 (R -Seg a)) by A1, A66, WELLORD1:31;
 R |_2 (R -Seg a) 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, RELAT_2:def_4;
hence  contradiction by A10, A34, A51, A52, A55, FUNCT_1:def_4; ::_thesis: verum
end;

theorem Th13: :: WELLORD2:13
for R being Relation st R is well-ordering holds
ex A being Ordinal st R, RelIncl A are_isomorphic
proof
let R be Relation; ::_thesis: ( R is well-ordering implies ex A being Ordinal st R, RelIncl A are_isomorphic )
assume A1: R is well-ordering ; ::_thesis: ex A being Ordinal st R, RelIncl A are_isomorphic
defpred S1[ set ] means  ex A being Ordinal st R |_2 (R -Seg $1), RelIncl A are_isomorphic ;
consider Z being set  such that
A2: for a being set holds
( a in Z iff ( a in field R & S1[a] ) ) from XBOOLE_0:sch_1();
now__::_thesis:_for_a_being_set_st_a_in_field_R_&_R_-Seg_a_c=_Z_holds_
a_in_Z
let a be set ; ::_thesis: ( a in field R & R -Seg a c= Z implies a in Z )
assume that
A3: a in field R and
A4: R -Seg a c= Z ; ::_thesis: a in Z
set P = R |_2 (R -Seg a);
now__::_thesis:_for_b_being_set_st_b_in_field_(R_|_2_(R_-Seg_a))_holds_
ex_A_being_Ordinal_st_(R_|_2_(R_-Seg_a))_|_2_((R_|_2_(R_-Seg_a))_-Seg_b),_RelIncl_A_are_isomorphic
let b be set ; ::_thesis: ( b in field (R |_2 (R -Seg a)) implies ex A being Ordinal st (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic )
assume A5: b in field (R |_2 (R -Seg a)) ; ::_thesis: ex A being Ordinal st (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic
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 being Ordinal such that
A9: R |_2 (R -Seg b), RelIncl A are_isomorphic by A2, A4, A6;
take A = A; ::_thesis: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic
 (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, A5, WELLORD1:12, WELLORD1:27;
hence  (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b), RelIncl A are_isomorphic by A9, A8, WELLORD1:22; ::_thesis: verum
end;
then  ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic by A1, Th12, WELLORD1:25;
hence  a in Z by A2, A3; ::_thesis: verum
end;
then  field R c= Z by A1, WELLORD1:33;
then  for a being set st a in field R holds
ex A being Ordinal st R |_2 (R -Seg a), RelIncl A are_isomorphic by A2;
hence  ex A being Ordinal st R, RelIncl A are_isomorphic by A1, Th12; ::_thesis: verum
end;

definition
let R be Relation;
assume A1: R is well-ordering ;
func order_type_of R ->  Ordinal means :Def2: :: WELLORD2:def 2
R, RelIncl it are_isomorphic ;
existence
 ex b1 being Ordinal st R, RelIncl b1 are_isomorphic by A1, Th13;
uniqueness
 for b1, b2 being Ordinal st R, RelIncl b1 are_isomorphic & R, RelIncl b2 are_isomorphic holds
b1 = b2 by Th11;
end;

:: deftheorem Def2 defines order_type_of WELLORD2:def_2_:_
 for R being Relation st R is well-ordering holds
for b2 being Ordinal holds
( b2 = order_type_of R iff R, RelIncl b2 are_isomorphic );

definition
let A be Ordinal;
let R be Relation;
predA is_order_type_of R means :: WELLORD2:def 3
A = order_type_of R;
end;

:: deftheorem  defines is_order_type_of WELLORD2:def_3_:_
 for A being Ordinal
for R being Relation holds
( A is_order_type_of R iff A = order_type_of R );

theorem :: WELLORD2:14
for X being set
for A being Ordinal st X c= A holds
order_type_of (RelIncl X) c= A
proof
let X be set ; ::_thesis: for A being Ordinal st X c= A holds
order_type_of (RelIncl X) c= A
let A be Ordinal; ::_thesis: ( X c= A implies order_type_of (RelIncl X) c= A )
assume A1: X c= A ; ::_thesis: order_type_of (RelIncl X) c= A
then A2: (RelIncl A) |_2 X = RelIncl X by Th7;
A3: RelIncl X is well-ordering by A1, Th8;
A4: now__::_thesis:_(_RelIncl_A,(RelIncl_A)_|_2_X_are_isomorphic_implies_order_type_of_(RelIncl_X)_c=_A_)
assume  RelIncl A,(RelIncl A) |_2 X are_isomorphic ; ::_thesis: order_type_of (RelIncl X) c= A
then  RelIncl X, RelIncl A are_isomorphic by A2, WELLORD1:40;
hence  order_type_of (RelIncl X) c= A by A3, Def2; ::_thesis: verum
end;
A5: now__::_thesis:_(_ex_a_being_set_st_
(_a_in_A_&_(RelIncl_A)_|_2_((RelIncl_A)_-Seg_a),(RelIncl_A)_|_2_X_are_isomorphic_)_implies_order_type_of_(RelIncl_X)_c=_A_)
given a being set  such that A6: a in A and
A7: (RelIncl A) |_2 ((RelIncl A) -Seg a),(RelIncl A) |_2 X are_isomorphic ; ::_thesis: order_type_of (RelIncl X) c= A
reconsider a = a as Ordinal by A6;
A8: (RelIncl A) -Seg a = a by A6, Th9;
A9: a c= A by A6, ORDINAL1:def_2;
then  (RelIncl A) |_2 a = RelIncl a by Th7;
then  RelIncl X, RelIncl a are_isomorphic by A2, A7, A8, WELLORD1:40;
hence  order_type_of (RelIncl X) c= A by A3, A9, Def2; ::_thesis: verum
end;
 field (RelIncl A) = A by Def1;
hence  order_type_of (RelIncl X) c= A by A1, A4, A5, WELLORD1:53; ::_thesis: verum
end;


definition
let X, Y be set ;
:: original: are_equipotent
redefine predX,Y are_equipotent  means :: WELLORD2:def 4
 ex f being Function st
( f is one-to-one & dom f = X & rng f = Y );
compatibility
 ( X,Y are_equipotent iff ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) )
proof
thus  ( X,Y are_equipotent implies ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) ) ::_thesis: ( ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) implies X,Y are_equipotent )
proof
assume  X,Y are_equipotent ; ::_thesis: ex f being Function st
( f is one-to-one & dom f = X & rng f = Y )
then consider Z being set  such that
A1: for x being set st x in X holds
ex y being set st
( y in Y & [x,y] in Z ) and
A2: for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) and
A3: for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) by TARSKI:def_6;
set F = Z /\ [:X,Y:];
 for x, y, z being set st [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] implies y = z )
assume  ( [x,y] in Z /\ [:X,Y:] & [x,z] in Z /\ [:X,Y:] ) ; ::_thesis: y = z
then  ( [x,y] in Z & [x,z] in Z ) by XBOOLE_0:def_4;
hence  y = z by A3; ::_thesis: verum
end;
then reconsider F = Z /\ [:X,Y:] as Function by FUNCT_1:def_1;
take f = F; ::_thesis: ( f is one-to-one & dom f = X & rng f = Y )
thus  f is one-to-one ::_thesis: ( dom f = X & rng f = Y )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A4: x in dom f and
A5: y in dom f and
A6: f . x = f . y ; ::_thesis: x = 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  x = y by A3, A6, A7; ::_thesis: verum
end;
thus  dom f c= X :: according to XBOOLE_0:def_10 ::_thesis: ( X c= dom f & rng f = Y )
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom f or x in X )
assume  x in dom f ; ::_thesis: x in X
then  [x,(f . x)] in f by FUNCT_1:1;
then  [x,(f . x)] in [:X,Y:] by XBOOLE_0:def_4;
hence  x in X by ZFMISC_1:87; ::_thesis: verum
end;
thus  X c= dom f ::_thesis: rng f = Y
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom f )
assume A8: x in X ; ::_thesis: x in dom f
then consider y being set  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  x in dom f by FUNCT_1:1; ::_thesis: verum
end;
thus  rng f c= Y :: according to XBOOLE_0:def_10 ::_thesis: Y c= rng f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in Y )
assume  y in rng f ; ::_thesis: y in Y
then consider x being set  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  y in Y by ZFMISC_1:87; ::_thesis: verum
end;
thus  Y c= rng f ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Y or y in rng f )
assume A12: y in Y ; ::_thesis: y in rng f
then consider x being set  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  y in rng f by FUNCT_1:def_3; ::_thesis: verum
end;
end;
 ( ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) implies ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in Y & [x,y] in Z ) ) & ( for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) ) )
proof
given f being Function such that A15: f is one-to-one and
A16: dom f = X and
A17: rng f = Y ; ::_thesis: ex Z being set st
( ( for x being set st x in X holds
ex y being set st
( y in Y & [x,y] in Z ) ) & ( for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) )
take Z = f; ::_thesis: ( ( for x being set st x in X holds
ex y being set st
( y in Y & [x,y] in Z ) ) & ( for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) )
thus  for x being set st x in X holds
ex y being set st
( y in Y & [x,y] in Z ) ::_thesis: ( ( for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) ) & ( for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u ) ) )
proof
let x be set ; ::_thesis: ( x in X implies ex y being set st
( y in Y & [x,y] in Z ) )
assume A18: x in X ; ::_thesis: ex y being set st
( y in Y & [x,y] in Z )
take  f . x ; ::_thesis: ( f . x in Y & [x,(f . x)] in Z )
thus  f . x in Y by A16, A17, A18, FUNCT_1:def_3; ::_thesis: [x,(f . x)] in Z
thus  [x,(f . x)] in Z by A16, A18, FUNCT_1:1; ::_thesis: verum
end;
thus  for y being set st y in Y holds
ex x being set st
( x in X & [x,y] in Z ) ::_thesis: for x, y, z, u being set st [x,y] in Z & [z,u] in Z holds
( x = z iff y = u )
proof
let y be set ; ::_thesis: ( y in Y implies ex x being set st
( x in X & [x,y] in Z ) )
assume A19: y in Y ; ::_thesis: ex x being set st
( x in X & [x,y] in Z )
take  (f ") . y ; ::_thesis: ( (f ") . y in X & [((f ") . y),y] in Z )
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; ::_thesis: [((f ") . y),y] in Z
 y = f . ((f ") . y) by A15, A17, A19, FUNCT_1:35;
hence  [((f ") . y),y] in Z by A22, A21, FUNCT_1:1; ::_thesis: verum
end;
let x, y, z, u be set ; ::_thesis: ( [x,y] in Z & [z,u] in Z implies ( x = z iff y = u ) )
assume A23: ( [x,y] in Z & [z,u] in Z ) ; ::_thesis: ( x = z iff y = u )
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  ( x = z iff y = u ) by A15, A24, FUNCT_1:def_4; ::_thesis: verum
end;
hence  ( ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) implies X,Y are_equipotent ) by TARSKI:def_6; ::_thesis: verum
end;
reflexivity
 for X being set ex f being Function st
( f is one-to-one & dom f = X & rng f = X )
proof
let X be set ; ::_thesis: ex f being Function st
( f is one-to-one & dom f = X & rng f = X )
take  id X ; ::_thesis: ( id X is one-to-one & dom (id X) = X & rng (id X) = X )
thus  ( id X is one-to-one & dom (id X) = X & rng (id X) = X ) ; ::_thesis: verum
end;
symmetry
 for X, Y being set st ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) holds
ex f being Function st
( f is one-to-one & dom f = Y & rng f = X )
proof
let X, Y be set ; ::_thesis: ( ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) implies ex f being Function st
( f is one-to-one & dom f = Y & rng f = X ) )
given f being Function such that A25: ( f is one-to-one & dom f = X & rng f = Y ) ; ::_thesis: ex f being Function st
( f is one-to-one & dom f = Y & rng f = X )
take  f " ; ::_thesis: ( f " is one-to-one & dom (f ") = Y & rng (f ") = X )
thus  ( f " is one-to-one & dom (f ") = Y & rng (f ") = X ) by A25, FUNCT_1:33; ::_thesis: verum
end;
end;

:: deftheorem  defines are_equipotent WELLORD2:def_4_:_
 for X, Y being set holds
( X,Y are_equipotent iff ex f being Function st
( f is one-to-one & dom f = X & rng f = Y ) );

theorem :: WELLORD2:15
for X, Y, Z being set st X,Y are_equipotent & Y,Z are_equipotent holds
X,Z are_equipotent
proof
let X, Y, Z be set ; ::_thesis: ( X,Y are_equipotent & Y,Z are_equipotent implies X,Z are_equipotent )
given f being Function such that A1: ( f is one-to-one & dom f = X & rng f = Y ) ; :: according to WELLORD2:def_4 ::_thesis: ( not Y,Z are_equipotent or X,Z are_equipotent )
given g being Function such that A2: ( g is one-to-one & dom g = Y & rng g = Z ) ; :: according to WELLORD2:def_4 ::_thesis: X,Z are_equipotent
take  g * f ; :: according to WELLORD2:def_4 ::_thesis: ( g * f is one-to-one & dom (g * f) = X & rng (g * f) = Z )
thus  ( g * f is one-to-one & dom (g * f) = X & rng (g * f) = Z ) by A1, A2, RELAT_1:27, RELAT_1:28; ::_thesis: verum
end;

theorem Th16: :: WELLORD2:16
for X being set
for R being Relation st R well_orders X holds
( field (R |_2 X) = X & R |_2 X is well-ordering )
proof
let X be set ; ::_thesis: for R being Relation st R well_orders X holds
( field (R |_2 X) = X & R |_2 X is well-ordering )
let R be Relation; ::_thesis: ( R well_orders X implies ( field (R |_2 X) = X & R |_2 X is well-ordering ) )
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 ; :: according to WELLORD1:def_5 ::_thesis: ( field (R |_2 X) = X & R |_2 X is well-ordering )
A6: R |_2 X is_antisymmetric_in X
proof
let x be set ; :: according to RELAT_2:def_4 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in R |_2 X or not [b1,x] in R |_2 X or x = b1 )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in R |_2 X or not [y,x] in R |_2 X or x = y )
assume that
A7: ( x in X & y in X ) and
A8: ( [x,y] in R |_2 X & [y,x] in R |_2 X ) ; ::_thesis: x = y
 ( [x,y] in R & [y,x] in R ) by A8, XBOOLE_0:def_4;
hence  x = y by A3, A7, RELAT_2:def_4; ::_thesis: verum
end;
A9: R |_2 X is_well_founded_in X
proof
let Y be set ; :: according to WELLORD1:def_3 ::_thesis: ( not Y c= X or Y = {} or ex b1 being set st
( b1 in Y & (R |_2 X) -Seg b1 misses Y ) )
assume  ( Y c= X & Y <> {} ) ; ::_thesis: ex b1 being set st
( b1 in Y & (R |_2 X) -Seg b1 misses Y )
then consider a being set  such that
A10: a in Y and
A11: R -Seg a misses Y by A5, WELLORD1:def_3;
take  a ; ::_thesis: ( a in Y & (R |_2 X) -Seg a misses Y )
thus  a in Y by A10; ::_thesis: (R |_2 X) -Seg a misses Y
assume  not (R |_2 X) -Seg a misses Y ; ::_thesis: contradiction
then consider x being set  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; ::_thesis: verum
end;
A15: R |_2 X is_transitive_in X
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in R |_2 X or not [b1,b2] in R |_2 X or [x,b2] in R |_2 X )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in R |_2 X or not [y,z] in R |_2 X or [x,z] in R |_2 X )
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 ) ; ::_thesis: [x,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, RELAT_2:def_8;
 [x,z] in [:X,X:] by A16, A18, ZFMISC_1:87;
hence  [x,z] in R |_2 X by A20, XBOOLE_0:def_4; ::_thesis: verum
end;
A21: R |_2 X is_connected_in X
proof
let x be set ; :: according to RELAT_2:def_6 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or x = b1 or [x,b1] in R |_2 X or [b1,x] in R |_2 X )
let y be set ; ::_thesis: ( not x in X or not y in X or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume that
A22: ( x in X & y in X ) and
A23: x <> y ; ::_thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X )
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, RELAT_2:def_6;
hence  ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by A24, XBOOLE_0:def_4; ::_thesis: verum
end;
thus A25: field (R |_2 X) = X ::_thesis: R |_2 X is well-ordering
proof
thus  field (R |_2 X) c= X by WELLORD1:13; :: according to XBOOLE_0:def_10 ::_thesis: X c= field (R |_2 X)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in field (R |_2 X) )
assume  x in X ; ::_thesis: x in field (R |_2 X)
then  ( [x,x] in R & [x,x] in [:X,X:] ) by A1, RELAT_2:def_1, ZFMISC_1:87;
then  [x,x] in R |_2 X by XBOOLE_0:def_4;
hence  x in field (R |_2 X) by RELAT_1:15; ::_thesis: verum
end;
 R |_2 X is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in R |_2 X )
assume  x in X ; ::_thesis: [x,x] in R |_2 X
then  ( [x,x] in R & [x,x] in [:X,X:] ) by A1, RELAT_2:def_1, ZFMISC_1:87;
hence  [x,x] in R |_2 X by XBOOLE_0:def_4; ::_thesis: verum
end;
then  R |_2 X well_orders X by A15, A6, A21, A9, WELLORD1:def_5;
hence  R |_2 X is well-ordering by A25, WELLORD1:4; ::_thesis: verum
end;

Lm1:  for X being set
for R being Relation st R is well-ordering & X, field R are_equipotent holds
ex R being Relation st R well_orders X
proof
let X be set ; ::_thesis: for R being Relation st R is well-ordering & X, field R are_equipotent holds
ex R being Relation st R well_orders X
let R be Relation; ::_thesis: ( R is well-ordering & X, field R are_equipotent implies ex R being Relation st R well_orders X )
assume A1: R is well-ordering ; ::_thesis: ( not X, field R are_equipotent or ex R being Relation st R well_orders X )
given f being Function such that A2: f is one-to-one and
A3: dom f = X and
A4: rng f = field R ; :: according to WELLORD2:def_4 ::_thesis: ex R being Relation st R well_orders X
defpred S1[ set , set ] means [(f . $1),(f . $2)] in R;
consider Q being Relation such that
A5: for x, y being set holds
( [x,y] in Q iff ( x in X & y in X & S1[x,y] ) ) from RELAT_1:sch_1();
take  Q ; ::_thesis: Q well_orders X
A6: R is_reflexive_in field R by A1, RELAT_2:def_9;
A7: field Q = X
proof
thus  field Q c= X :: according to XBOOLE_0:def_10 ::_thesis: X c= field Q
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in field Q or x in X )
assume that
A8: x in field Q and
A9: not x in X ; ::_thesis: contradiction
 for y being set holds not [y,x] in Q by A5, A9;
then A10: not x in rng Q by XTUPLE_0:def_13;
 for y being set 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; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in field Q )
assume A11: x in X ; ::_thesis: x in field Q
then  f . x in rng f by A3, FUNCT_1:def_3;
then  [(f . x),(f . x)] in R by A6, A4, RELAT_2:def_1;
then  [x,x] in Q by A5, A11;
hence  x in field Q by RELAT_1:15; ::_thesis: verum
end;
 f is_isomorphism_of Q,R
proof
thus  ( dom f = field Q & rng f = field R & f is one-to-one ) by A2, A3, A4, A7; :: according to WELLORD1:def_7 ::_thesis: for b1, b2 being set holds
( ( not [b1,b2] in Q or ( b1 in field Q & b2 in field Q & [(f . b1),(f . b2)] in R ) ) & ( not b1 in field Q or not b2 in field Q or not [(f . b1),(f . b2)] in R or [b1,b2] in Q ) )
let x, y be set ; ::_thesis: ( ( not [x,y] in Q or ( x in field Q & y in field Q & [(f . x),(f . y)] in R ) ) & ( not x in field Q or not y in field Q or not [(f . x),(f . y)] in R or [x,y] in Q ) )
thus  ( [x,y] in Q implies ( x in field Q & y in field Q & [(f . x),(f . y)] in R ) ) by A5, A7; ::_thesis: ( not x in field Q or not y in field Q or not [(f . x),(f . y)] in R or [x,y] in Q )
assume  ( x in field Q & y in field Q & [(f . x),(f . y)] in R ) ; ::_thesis: [x,y] in Q
hence  [x,y] in Q by A5, A7; ::_thesis: verum
end;
then  f " is_isomorphism_of R,Q by WELLORD1:39;
then  Q is well-ordering by A1, WELLORD1:44;
hence  Q well_orders X by A7, WELLORD1:4; ::_thesis: verum
end;

theorem Th17: :: WELLORD2:17
for X being set ex R being Relation st R well_orders X
proof
deffunc H1( set ) ->  set = {$1};
defpred S1[ set ] means $1 is Ordinal;
let X be set ; ::_thesis: ex R being Relation st R well_orders X
consider Class being set  such that
A1: X in Class and
A2: for Y, Z being set st Y in Class & Z c= Y holds
Z in Class and
 for Y being set st Y in Class holds
bool Y in Class and
A3: for Y being set holds
( not Y c= Class or Y,Class are_equipotent or Y in Class ) by ZFMISC_1:112;
consider ON being set  such that
A4: for x being set holds
( x in ON iff ( x in Class & S1[x] ) ) from XBOOLE_0:sch_1();
 for Y being set st Y in ON holds
( Y is Ordinal & Y c= ON )
proof
let Y be set ; ::_thesis: ( Y in ON implies ( Y is Ordinal & Y c= ON ) )
assume A5: Y in ON ; ::_thesis: ( Y is Ordinal & Y c= ON )
hence  Y is Ordinal by A4; ::_thesis: Y c= ON
reconsider A = Y as Ordinal by A4, A5;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Y or x in ON )
assume A6: x in Y ; ::_thesis: x in ON
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  x in ON by A4; ::_thesis: verum
end;
then reconsider ON = ON as Ordinal by ORDINAL1:19;
A8: ON c= Class
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ON or x in Class )
thus  ( not x in ON or x in Class ) by A4; ::_thesis: verum
end;
A9: ON,Class are_equipotent
proof
assume  not ON,Class are_equipotent ; ::_thesis: contradiction
then  ON in Class by A3, A8;
then  ON in ON by A4;
hence  contradiction ; ::_thesis: verum
end;
 field (RelIncl ON) = ON by Def1;
then consider R being Relation such that
A10: R well_orders Class by A9, Lm1;
consider f being Function such that
A11: ( dom f = X & ( for x being set st x in X holds
f . x = H1(x) ) ) from FUNCT_1:sch_3();
A12: rng f c= Class
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng f or x in Class )
assume  x in rng f ; ::_thesis: x in Class
then consider y being set  such that
A13: y in dom f and
A14: x = f . y by FUNCT_1:def_3;
A15: {y} c= X
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in {y} or z in X )
assume  z in {y} ; ::_thesis: z in X
hence  z in X by A11, A13, TARSKI:def_1; ::_thesis: verum
end;
 f . y = {y} by A11, A13;
hence  x in Class by A1, A2, A14, A15; ::_thesis: verum
end;
A16: X, rng f are_equipotent
proof
take  f ; :: according to WELLORD2:def_4 ::_thesis: ( f is one-to-one & dom f = X & rng f = rng f )
thus  f is one-to-one ::_thesis: ( dom f = X & rng f = rng f )
proof
let x be set ; :: according to FUNCT_1:def_4 ::_thesis: for b1 being set holds
( not x in dom f or not b1 in dom f or not f . x = f . b1 or x = b1 )
let y be set ; ::_thesis: ( not x in dom f or not y in dom f or not f . x = f . y or x = y )
assume that
A17: ( x in dom f & y in dom f ) and
A18: f . x = f . y ; ::_thesis: x = y
 ( f . x = {x} & f . y = {y} ) by A11, A17;
hence  x = y by A18, ZFMISC_1:3; ::_thesis: verum
end;
thus  ( dom f = X & rng f = rng f ) by A11; ::_thesis: verum
end;
set Q = R |_2 Class;
 field (R |_2 Class) = Class by A10, Th16;
then A19: field ((R |_2 Class) |_2 (rng f)) = rng f by A10, A12, Th16, WELLORD1:31;
 R |_2 Class is well-ordering by A10, Th16;
hence  ex R being Relation st R well_orders X by A16, A19, Lm1, WELLORD1:25; ::_thesis: verum
end;

theorem :: WELLORD2:18
for M being non empty set st ( for X being set st X in M holds
X <> {} ) & ( for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y ) holds
ex Choice being set st
for X being set st X in M holds
ex x being set st Choice /\ X = {x}
proof
let M be non empty set ; ::_thesis: ( ( for X being set st X in M holds
X <> {} ) & ( for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y ) implies ex Choice being set st
for X being set st X in M holds
ex x being set st Choice /\ X = {x} )
assume that
A1: for X being set st X in M holds
X <> {} and
A2: for X, Y being set st X in M & Y in M & X <> Y holds
X misses Y ; ::_thesis: ex Choice being set st
for X being set st X in M holds
ex x being set st Choice /\ X = {x}
consider R being Relation such that
A3: R well_orders union M by Th17;
A4: R is_reflexive_in union M by A3, WELLORD1:def_5;
A5: R is_connected_in union M by A3, WELLORD1:def_5;
defpred S1[ set , set ] means ( $2 in $1 & ( for z being set st z in $1 holds
[$2,z] in R ) );
A6: R is_antisymmetric_in union M by A3, WELLORD1:def_5;
A7: for x, y, z being set st x in M & S1[x,y] & S1[x,z] holds
y = z
proof
let x, y, z be set ; ::_thesis: ( x in M & S1[x,y] & S1[x,z] implies y = z )
assume A8: x in M ; ::_thesis: ( not S1[x,y] or not S1[x,z] or y = z )
assume that
A9: y in x and
A10: for u being set st u in x holds
[y,u] in R ; ::_thesis: ( not S1[x,z] or y = z )
A11: y in union M by A8, A9, TARSKI:def_4;
assume that
A12: z in x and
A13: for u being set st u in x holds
[z,u] in R ; ::_thesis: y = z
A14: z in union M by A8, A12, TARSKI:def_4;
 ( [y,z] in R & [z,y] in R ) by A9, A10, A12, A13;
hence  y = z by A6, A11, A14, RELAT_2:def_4; ::_thesis: verum
end;
A15: R is_well_founded_in union M by A3, WELLORD1:def_5;
A16: for x being set st x in M holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in M implies ex y being set st S1[x,y] )
assume A17: x in M ; ::_thesis: ex y being set st S1[x,y]
then A18: x c= union M by ZFMISC_1:74;
 x <> {} by A1, A17;
then consider y being set  such that
A19: y in x and
A20: R -Seg y misses x by A15, A18, WELLORD1:def_3;
take  y ; ::_thesis: S1[x,y]
thus  y in x by A19; ::_thesis: for z being set st z in x holds
[y,z] in R
let z be set ; ::_thesis: ( z in x implies [y,z] in R )
assume A21: z in x ; ::_thesis: [y,z] in R
then A22: not z in R -Seg y by A20, XBOOLE_0:3;
 ( not y <> z or [y,z] in R or [z,y] in R ) by A5, A18, A19, A21, RELAT_2:def_6;
hence  [y,z] in R by A4, A18, A21, A22, RELAT_2:def_1, WELLORD1:1; ::_thesis: verum
end;
consider f being Function such that
A23: ( dom f = M & ( for x being set st x in M holds
S1[x,f . x] ) ) from FUNCT_1:sch_2(A7, A16);
take Choice = rng f; ::_thesis: for X being set st X in M holds
ex x being set st Choice /\ X = {x}
let X be set ; ::_thesis: ( X in M implies ex x being set st Choice /\ X = {x} )
assume A24: X in M ; ::_thesis: ex x being set st Choice /\ X = {x}
take x = f . X; ::_thesis: Choice /\ X = {x}
thus  Choice /\ X c= {x} :: according to XBOOLE_0:def_10 ::_thesis: {x} c= Choice /\ X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in Choice /\ X or y in {x} )
assume A25: y in Choice /\ X ; ::_thesis: y in {x}
then A26: y in X by XBOOLE_0:def_4;
 y in Choice by A25, XBOOLE_0:def_4;
then consider z being set  such that
A27: z in dom f and
A28: y = f . z by FUNCT_1:def_3;
assume  not y in {x} ; ::_thesis: contradiction
then  X <> z by A28, TARSKI:def_1;
then  X misses z by A2, A23, A24, A27;
then A29: X /\ z = {} by XBOOLE_0:def_7;
 f . z in z by A23, A27;
hence  contradiction by A26, A28, A29, XBOOLE_0:def_4; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x} or y in Choice /\ X )
assume  y in {x} ; ::_thesis: y in Choice /\ X
then A30: y = x by TARSKI:def_1;
then A31: y in X by A24, A23;
 y in Choice by A23, A24, A30, FUNCT_1:def_3;
hence  y in Choice /\ X by A31, XBOOLE_0:def_4; ::_thesis: verum
end;

begin

theorem :: WELLORD2:19
for X being set holds RelIncl X is_reflexive_in X
proof
let X be set ; ::_thesis: RelIncl X is_reflexive_in X
 ( RelIncl X is reflexive & field (RelIncl X) = X ) by Def1;
hence  RelIncl X is_reflexive_in X by RELAT_2:def_9; ::_thesis: verum
end;

theorem :: WELLORD2:20
for X being set holds RelIncl X is_transitive_in X
proof
let X be set ; ::_thesis: RelIncl X is_transitive_in X
 ( RelIncl X is transitive & field (RelIncl X) = X ) by Def1;
hence  RelIncl X is_transitive_in X by RELAT_2:def_16; ::_thesis: verum
end;

theorem :: WELLORD2:21
for X being set holds RelIncl X is_antisymmetric_in X
proof
let X be set ; ::_thesis: RelIncl X is_antisymmetric_in X
 ( RelIncl X is antisymmetric & field (RelIncl X) = X ) by Def1;
hence  RelIncl X is_antisymmetric_in X by RELAT_2:def_12; ::_thesis: verum
end;

registration
cluster RelIncl {} ->  empty ;
coherence
 RelIncl {} is empty
proof
 for Y, Z being set st Y in {} & Z in {} holds
( [Y,Z] in {} iff Y c= Z ) ;
hence  RelIncl {} is empty by Def1, RELAT_1:40; ::_thesis: verum
end;
end;

registration
let X be non empty set ;
cluster RelIncl X ->  non empty ;
coherence
 not RelIncl X is empty
proof
set a = the Element of X;
 [ the Element of X, the Element of X] in RelIncl X by Def1;
hence  not RelIncl X is empty ; ::_thesis: verum
end;
end;

theorem :: WELLORD2:22
for x being set holds RelIncl {x} = {[x,x]}
proof
let x be set ; ::_thesis: RelIncl {x} = {[x,x]}
A1: for Y, Z being set st Y in {x} & Z in {x} holds
( [Y,Z] in {[x,x]} iff Y c= Z )
proof
let Y, Z be set ; ::_thesis: ( Y in {x} & Z in {x} implies ( [Y,Z] in {[x,x]} iff Y c= Z ) )
assume that
A2: Y in {x} and
A3: Z in {x} ; ::_thesis: ( [Y,Z] in {[x,x]} iff Y c= Z )
A4: Y = x by A2, TARSKI:def_1;
hence  ( [Y,Z] in {[x,x]} implies Y c= Z ) by A3, TARSKI:def_1; ::_thesis: ( Y c= Z implies [Y,Z] in {[x,x]} )
 Z = x by A3, TARSKI:def_1;
hence  ( Y c= Z implies [Y,Z] in {[x,x]} ) by A4, TARSKI:def_1; ::_thesis: verum
end;
 field {[x,x]} = {x} by RELAT_1:173;
hence  RelIncl {x} = {[x,x]} by A1, Def1; ::_thesis: verum
end;

theorem :: WELLORD2:23
for X being set holds RelIncl X c= [:X,X:]
proof
let X be set ; ::_thesis: RelIncl X c= [:X,X:]
set R = RelIncl X;
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in RelIncl X or [a,b] in [:X,X:] )
assume A1: [a,b] in RelIncl X ; ::_thesis: [a,b] in [:X,X:]
then  b in field (RelIncl X) by RELAT_1:15;
then A2: b in X by Def1;
 a in field (RelIncl X) by A1, RELAT_1:15;
then  a in X by Def1;
hence  [a,b] in [:X,X:] by A2, ZFMISC_1:87; ::_thesis: verum
end;