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, Th12; :: 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 5;
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:36;
A14: now
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 5;
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
A21: C = field (RelIncl C) by Def1;
then A22: c in C by A19, RELAT_1:30;
then reconsider B = c as Ordinal ;
b in C by A19, A21, RELAT_1:30;
then A23: B c= A by A20, A19, A22, Def1;
then A24: (RelIncl A) |_2 B = RelIncl B by Th8;
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 Th10, ORDINAL1:21;
A27: A = field (RelIncl A) by Def1;
A28: RelIncl A is well-ordering by Th7;
RelIncl A,R |_2 (R -Seg b9) are_isomorphic by A18, WELLORD1:50;
then canonical_isomorphism_of (RelIncl A),(R |_2 (R -Seg b9)) is_isomorphism_of RelIncl A,R |_2 (R -Seg b9) by A28, WELLORD1:def 9;
then consider d being set such that
A29: d in field (R |_2 (R -Seg b9)) and
A30: (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, A28, ORDINAL1:21, WELLORD1:61;
A31: d in field R by A29, WELLORD1:19;
A32: (R |_2 (R -Seg b9)) -Seg d = R -Seg d by A1, A29, WELLORD1:19, WELLORD1:35;
d in R -Seg b9 by A29, WELLORD1:19;
then [d,b9] in R by WELLORD1:def 1;
then R -Seg d c= R -Seg b9 by A1, A10, A16, A31, WELLORD1:37;
then RelIncl B,R |_2 (R -Seg d) are_isomorphic by A30, A26, A24, A32, WELLORD1:29;
then R |_2 (R -Seg d), RelIncl B are_isomorphic by WELLORD1:50;
then B = H . d by A10, A31;
hence c in rng H by A10, A31, FUNCT_1:def 5; :: thesis: verum
end;
hence c in rng H by A15; :: thesis: verum
end;
A33: ( ex a being set st
( a in C & rng H = (RelIncl C) -Seg a ) implies rng H is Ordinal ) by Th10;
( C = field (RelIncl C) & RelIncl C is well-ordering ) by Def1, Th7;
then reconsider A = rng H as Ordinal by A13, A14, A33, WELLORD1:36;
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: ( proj2 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 ) ) ) )
A34: 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 5;
hence H . a is Ordinal ; :: thesis: verum
end;
thus A35: 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 8 :: thesis: for b1 being set holds
( not a in proj1 H or not b1 in proj1 H or not H . a = H . b1 or a = b1 )
let b be set ; :: thesis: ( not a in proj1 H or not b in proj1 H or not H . a = H . b or a = b )
assume that
A36: a in dom H and
A37: b in dom H and
A38: H . a = H . b ; :: thesis: a = b
reconsider B = H . a as Ordinal by A34, A36;
R |_2 (R -Seg b), RelIncl B are_isomorphic by A10, A37, A38;
then A39: RelIncl B,R |_2 (R -Seg b) are_isomorphic by WELLORD1:50;
R |_2 (R -Seg a), RelIncl B are_isomorphic by A10, A36;
then R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic by A39, WELLORD1:52;
hence a = b by A1, A10, A36, A37, WELLORD1:58; :: 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);
A40: ( A = field (RelIncl A) & R |_2 (R -Seg b) is well-ordering ) by A1, Def1, WELLORD1:32;
assume A41: [a,b] in R ; :: thesis: ( a in field R & b in field R & [(H . a),(H . b)] in RelIncl A )
hence A42: ( a in field R & b in field R ) by RELAT_1:30; :: thesis: [(H . a),(H . b)] in RelIncl A
then reconsider A9 = H . a, B9 = H . b as Ordinal by A10, A34;
A43: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by A10, A42;
A44: A9 in A by A10, A42, FUNCT_1:def 5;
A45: B9 in A by A10, A42, FUNCT_1:def 5;
A46: R |_2 (R -Seg a), RelIncl A9 are_isomorphic by A10, A42;
now
assume a <> b ; :: thesis: [A9,B9] in RelIncl A
then A47: a in R -Seg b by A41, WELLORD1:def 1;
then A48: (R |_2 (R -Seg b)) -Seg a = R -Seg a by A1, WELLORD1:35;
R -Seg b c= field R by WELLORD1:13;
then A49: a in field (R |_2 (R -Seg b)) by A1, A47, WELLORD1:39;
A9 c= A by A44, ORDINAL1:def 2;
then A50: (RelIncl A) |_2 A9 = RelIncl A9 by Th8;
( A9 = (RelIncl A) -Seg A9 & R -Seg a c= R -Seg b ) by A1, A41, A42, A44, Th10, WELLORD1:37;
then A51: (R |_2 (R -Seg b)) |_2 ((R |_2 (R -Seg b)) -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A46, A50, A48, WELLORD1:29;
( B9 = (RelIncl A) -Seg B9 & B9 c= A ) by A45, Th10, ORDINAL1:def 2;
then A52: R |_2 (R -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A43, Th8;
RelIncl A is well-ordering by Th7;
hence [A9,B9] in RelIncl A by A44, A45, A40, A49, A52, A51, WELLORD1:62; :: thesis: verum
end;
hence [(H . a),(H . b)] in RelIncl A by A44, Def1; :: thesis: verum
end;
assume that
A53: a in field R and
A54: b in field R and
A55: [(H . a),(H . b)] in RelIncl A ; :: thesis: [a,b] in R
assume A56: not [a,b] in R ; :: thesis: contradiction
R is reflexive by A1, WELLORD1:def 4;
then R is_reflexive_in field R by RELAT_2:def 9;
then A57: a <> b by A53, A56, RELAT_2:def 1;
R is connected by A1, WELLORD1:def 4;
then R is_connected_in field R by RELAT_2:def 14;
then A58: [b,a] in R by A53, A54, A56, A57, RELAT_2:def 6;
then A59: R -Seg b c= R -Seg a by A1, A53, A54, WELLORD1:37;
RelIncl A is antisymmetric by Th5;
then A60: RelIncl A is_antisymmetric_in field (RelIncl A) by RELAT_2:def 12;
A61: A = field (RelIncl A) by Def1;
reconsider A9 = H . a, B9 = H . b as Ordinal by A10, A34, A53, A54;
A62: R |_2 (R -Seg a), RelIncl A9 are_isomorphic by A10, A53;
A63: R |_2 (R -Seg b), RelIncl B9 are_isomorphic by A10, A54;
A64: B9 in A by A10, A54, FUNCT_1:def 5;
then B9 c= A by ORDINAL1:def 2;
then A65: (RelIncl A) |_2 B9 = RelIncl B9 by Th8;
set Z = R -Seg a;
set P = R |_2 (R -Seg a);
A66: RelIncl A is well-ordering by Th7;
A67: A9 in A by A10, A53, FUNCT_1:def 5;
then ( A9 = (RelIncl A) -Seg A9 & A9 c= A ) by Th10, ORDINAL1:def 2;
then A68: R |_2 (R -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A62, Th8;
A69: b in R -Seg a by A56, A58, WELLORD1:def 1;
then A70: (R |_2 (R -Seg a)) -Seg b = R -Seg b by A1, WELLORD1:35;
B9 = (RelIncl A) -Seg B9 by A64, Th10;
then A71: (R |_2 (R -Seg a)) |_2 ((R |_2 (R -Seg a)) -Seg b),(RelIncl A) |_2 ((RelIncl A) -Seg B9) are_isomorphic by A63, A65, A70, A59, WELLORD1:29;
R -Seg a c= field R by WELLORD1:13;
then A72: b in field (R |_2 (R -Seg a)) by A1, A69, WELLORD1:39;
R |_2 (R -Seg a) is well-ordering by A1, WELLORD1:32;
then [B9,A9] in RelIncl A by A72, A66, A67, A64, A61, A68, A71, WELLORD1:62;
then H . a = H . b by A55, A60, A67, A64, A61, RELAT_2:def 4;
hence contradiction by A10, A35, A53, A54, A57, FUNCT_1:def 8; :: thesis: verum