let R be Relation; :: thesis: ( R is well-ordering & ( for a being object 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 object 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[ object , object ] means for A being Ordinal holds
( A = $2 iff R |_2 (R -Seg $1), RelIncl A are_isomorphic );
assume A2: for a being object 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 object st a in field R holds
ex b being object st S1[a,b]
proof
let a be object ; :: thesis: ( a in field R implies ex b being object st S1[a,b] )
assume a in field R ; :: thesis: ex b being object 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, Th5; :: thesis: verum
end;
A5: for b, c, d being object st b in field R & S1[b,c] & S1[b,d] holds
c = d
proof
let b, c, d be object ; :: 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 object st b in field R holds
S1[b,H . b] ) ) from FUNCT_1:sch 2(A5, A3);
 for a being object st a in rng H holds
a is Ordinal
proof
let b be object ; :: thesis: ( b in rng H implies b is Ordinal )
assume b in rng H ; :: thesis: b is Ordinal
then consider c being object 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 object st b in rng H holds
for c being object st [c,b] in RelIncl C holds
c in rng H
let b be object ; :: thesis: ( b in rng H implies for c being object st [c,b] in RelIncl C holds
c in rng H )
assume A15: b in rng H ; :: thesis: for c being object st [c,b] in RelIncl C holds
c in rng H
then consider b9 being 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 (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 object ; :: 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 Th1;
assume c <> b ; :: thesis: c in rng H
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,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 object 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 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 ; :: 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 object 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 object 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 object st a in dom H holds
H . a is Ordinal
proof
let a be object ; :: 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 object 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, b be object ; :: according to FUNCT_1:def 4 :: 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 object ; :: 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 Th1;
( A9 = (RelIncl A) -Seg A9 & R -Seg a c= R -Seg b ) by A1, A40, A41, A43, Th3, 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, Th3, ORDINAL1:def 2;
then R |_2 (R -Seg b),(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; :: 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;
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 (R -Seg a);
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: R |_2 (R -Seg a),(RelIncl A) |_2 ((RelIncl A) -Seg A9) are_isomorphic by A60, Th1;
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, Th3;
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;
hence contradiction by A10, A34, A51, A52, A55; :: thesis: verum