:: The Well Ordering Relations
:: by Grzegorz Bancerek
::
:: Copyright (c) 1990-2021 Association of Mizar Users

Lm1: for R being Relation holds
( R is reflexive iff for x being object st x in field R holds
[x,x] in R )

by ;

Lm2: for R being Relation holds
( R is transitive iff for x, y, z being object st [x,y] in R & [y,z] in R holds
[x,z] in R )

proof end;

Lm3: for R being Relation holds
( R is antisymmetric iff for x, y being object st [x,y] in R & [y,x] in R holds
x = y )

proof end;

Lm4: for R being Relation holds
( R is connected iff for x, y being object st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R )

by ;

definition
let R be Relation;
let a be object ;
func R -Seg a -> set equals :: WELLORD1:def 1
(Coim (R,a)) \ {a};
coherence
(Coim (R,a)) \ {a} is set
;
end;

:: deftheorem defines -Seg WELLORD1:def 1 :
for R being Relation
for a being object holds R -Seg a = (Coim (R,a)) \ {a};

theorem Th1: :: WELLORD1:1
for a, x being object
for R being Relation holds
( x in R -Seg a iff ( x <> a & [x,a] in R ) )
proof end;

theorem Th2: :: WELLORD1:2
for x being object
for R being Relation holds
( x in field R or R -Seg x = {} )
proof end;

definition
let R be Relation;
attr R is well_founded means :Def2: :: WELLORD1:def 2
for Y being set st Y c= field R & Y <> {} holds
ex a being object st
( a in Y & R -Seg a misses Y );
let X be set ;
pred R is_well_founded_in X means :: WELLORD1:def 3
for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & R -Seg a misses Y );
end;

:: deftheorem Def2 defines well_founded WELLORD1:def 2 :
for R being Relation holds
( R is well_founded iff for Y being set st Y c= field R & Y <> {} holds
ex a being object st
( a in Y & R -Seg a misses Y ) );

:: deftheorem defines is_well_founded_in WELLORD1:def 3 :
for R being Relation
for X being set holds
( R is_well_founded_in X iff for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & R -Seg a misses Y ) );

theorem :: WELLORD1:3
for R being Relation holds
( R is well_founded iff R is_well_founded_in field R ) ;

definition
let R be Relation;
attr R is well-ordering means :: WELLORD1:def 4
( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded );
let X be set ;
end;

:: deftheorem defines well-ordering WELLORD1:def 4 :
for R being Relation holds
( R is well-ordering iff ( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded ) );

:: deftheorem defines well_orders WELLORD1:def 5 :
for R being Relation
for X being set holds
( R well_orders X iff ( R is_reflexive_in X & R is_transitive_in X & R is_antisymmetric_in X & R is_connected_in X & R is_well_founded_in X ) );

registration
coherence
for b1 being Relation st b1 is well-ordering holds
( b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded )
;
coherence
for b1 being Relation st b1 is reflexive & b1 is transitive & b1 is antisymmetric & b1 is connected & b1 is well_founded holds
b1 is well-ordering
;
end;

theorem :: WELLORD1:4
for R being Relation holds
( R well_orders field R iff R is well-ordering )
proof end;

theorem :: WELLORD1:5
for X being set
for R being Relation st R well_orders X holds
for Y being set st Y c= X & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )
proof end;

theorem Th6: :: WELLORD1:6
for R being Relation st R is well-ordering holds
for Y being set st Y c= field R & Y <> {} holds
ex a being object st
( a in Y & ( for b being object st b in Y holds
[a,b] in R ) )
proof end;

theorem :: WELLORD1:7
for R being Relation st R is well-ordering & field R <> {} holds
ex a being object st
( a in field R & ( for b being object st b in field R holds
[a,b] in R ) ) by Th6;

theorem :: WELLORD1:8
for R being Relation st R is well-ordering holds
for a being object holds
( not a in field R or for b being object st b in field R holds
[b,a] in R or ex b being object st
( b in field R & [a,b] in R & ( for c being object st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )
proof end;

theorem Th9: :: WELLORD1:9
for a being object
for R being Relation holds R -Seg a c= field R
proof end;

definition
let R be Relation;
let Y be set ;
func R |_2 Y -> Relation equals :: WELLORD1:def 6
R /\ [:Y,Y:];
coherence
R /\ [:Y,Y:] is Relation
;
end;

:: deftheorem defines |_2 WELLORD1:def 6 :
for R being Relation
for Y being set holds R |_2 Y = R /\ [:Y,Y:];

theorem Th10: :: WELLORD1:10
for X being set
for R being Relation holds R |_2 X = (X | R) | X
proof end;

theorem Th11: :: WELLORD1:11
for X being set
for R being Relation holds R |_2 X = X | (R | X)
proof end;

Lm5: for X being set
for R being Relation holds dom (X |` R) c= dom R

proof end;

theorem Th12: :: WELLORD1:12
for x being object
for X being set
for R being Relation st x in field (R |_2 X) holds
( x in field R & x in X )
proof end;

theorem Th13: :: WELLORD1:13
for X being set
for R being Relation holds
( field (R |_2 X) c= field R & field (R |_2 X) c= X ) by Th12;

theorem Th14: :: WELLORD1:14
for a being object
for X being set
for R being Relation holds (R |_2 X) -Seg a c= R -Seg a
proof end;

theorem Th15: :: WELLORD1:15
for X being set
for R being Relation st R is reflexive holds
R |_2 X is reflexive
proof end;

theorem Th16: :: WELLORD1:16
for Y being set
for R being Relation st R is connected holds
R |_2 Y is connected
proof end;

theorem Th17: :: WELLORD1:17
for Y being set
for R being Relation st R is transitive holds
R |_2 Y is transitive
proof end;

theorem Th18: :: WELLORD1:18
for Y being set
for R being Relation st R is antisymmetric holds
R |_2 Y is antisymmetric
proof end;

theorem Th19: :: WELLORD1:19
for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y)
proof end;

theorem :: WELLORD1:20
for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = (R |_2 Y) |_2 X
proof end;

theorem :: WELLORD1:21
for Y being set
for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y
proof end;

theorem Th22: :: WELLORD1:22
for Y, Z being set
for R being Relation st Z c= Y holds
(R |_2 Y) |_2 Z = R |_2 Z
proof end;

theorem Th23: :: WELLORD1:23
for R being Relation holds R |_2 () = R
proof end;

theorem Th24: :: WELLORD1:24
for X being set
for R being Relation st R is well_founded holds
R |_2 X is well_founded
proof end;

theorem Th25: :: WELLORD1:25
for Y being set
for R being Relation st R is well-ordering holds
R |_2 Y is well-ordering by ;

theorem Th26: :: WELLORD1:26
for a, b being object
for R being Relation st R is well-ordering holds
R -Seg a,R -Seg b are_c=-comparable
proof end;

theorem Th27: :: WELLORD1:27
for a, b being object
for R being Relation st R is well-ordering & b in R -Seg a holds
(R |_2 (R -Seg a)) -Seg b = R -Seg b
proof end;

theorem Th28: :: WELLORD1:28
for Y being set
for R being Relation st R is well-ordering & Y c= field R holds
( ( Y = field R or ex a being object st
( a in field R & Y = R -Seg a ) ) iff for a being object st a in Y holds
for b being object st [b,a] in R holds
b in Y )
proof end;

theorem Th29: :: WELLORD1:29
for a, b being object
for R being Relation st R is well-ordering & a in field R & b in field R holds
( [a,b] in R iff R -Seg a c= R -Seg b )
proof end;

theorem Th30: :: WELLORD1:30
for a, b being object
for R being Relation st R is well-ordering & a in field R & b in field R holds
( R -Seg a c= R -Seg b iff ( a = b or a in R -Seg b ) )
proof end;

theorem Th31: :: WELLORD1:31
for X being set
for R being Relation st R is well-ordering & X c= field R holds
field (R |_2 X) = X
proof end;

theorem Th32: :: WELLORD1:32
for a being object
for R being Relation st R is well-ordering holds
field (R |_2 (R -Seg a)) = R -Seg a
proof end;

theorem Th33: :: WELLORD1:33
for R being Relation st R is well-ordering holds
for Z being set st ( for a being object st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z
proof end;

theorem Th34: :: WELLORD1:34
for a, b being object
for R being Relation st R is well-ordering & a in field R & b in field R & ( for c being object st c in R -Seg a holds
( [c,b] in R & c <> b ) ) holds
[a,b] in R
proof end;

theorem Th35: :: WELLORD1:35
for R being Relation
for F being Function st R is well-ordering & dom F = field R & rng F c= field R & ( for a, b being object st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds
for a being object st a in field R holds
[a,(F . a)] in R
proof end;

definition
let R, S be Relation;
let F be Function;
pred F is_isomorphism_of R,S means :: WELLORD1:def 7
( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being object holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) );
end;

:: deftheorem defines is_isomorphism_of WELLORD1:def 7 :
for R, S being Relation
for F being Function holds
( F is_isomorphism_of R,S iff ( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being object holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) );

theorem Th36: :: WELLORD1:36
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
for a, b being object st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in S & F . a <> F . b )
proof end;

definition
let R, S be Relation;
pred R,S are_isomorphic means :: WELLORD1:def 8
ex F being Function st F is_isomorphism_of R,S;
end;

:: deftheorem defines are_isomorphic WELLORD1:def 8 :
for R, S being Relation holds
( R,S are_isomorphic iff ex F being Function st F is_isomorphism_of R,S );

theorem Th37: :: WELLORD1:37
for R being Relation holds id () is_isomorphism_of R,R
proof end;

theorem :: WELLORD1:38
for R being Relation holds R,R are_isomorphic
proof end;

theorem Th39: :: WELLORD1:39
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
F " is_isomorphism_of S,R
proof end;

theorem Th40: :: WELLORD1:40
for R, S being Relation st R,S are_isomorphic holds
S,R are_isomorphic
proof end;

theorem Th41: :: WELLORD1:41
for R, S, T being Relation
for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of S,T holds
G * F is_isomorphism_of R,T
proof end;

theorem Th42: :: WELLORD1:42
for R, S, T being Relation st R,S are_isomorphic & S,T are_isomorphic holds
R,T are_isomorphic
proof end;

theorem Th43: :: WELLORD1:43
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
( ( R is reflexive implies S is reflexive ) & ( R is transitive implies S is transitive ) & ( R is connected implies S is connected ) & ( R is antisymmetric implies S is antisymmetric ) & ( R is well_founded implies S is well_founded ) )
proof end;

theorem Th44: :: WELLORD1:44
for R, S being Relation
for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
S is well-ordering by Th43;

theorem Th45: :: WELLORD1:45
for R, S being Relation st R is well-ordering holds
for F, G being Function st F is_isomorphism_of R,S & G is_isomorphism_of R,S holds
F = G
proof end;

definition
let R, S be Relation;
assume that
A1: R is well-ordering and
A2: R,S are_isomorphic ;
func canonical_isomorphism_of (R,S) -> Function means :Def9: :: WELLORD1:def 9
it is_isomorphism_of R,S;
existence
ex b1 being Function st b1 is_isomorphism_of R,S
by A2;
uniqueness
for b1, b2 being Function st b1 is_isomorphism_of R,S & b2 is_isomorphism_of R,S holds
b1 = b2
by ;
end;

:: deftheorem Def9 defines canonical_isomorphism_of WELLORD1:def 9 :
for R, S being Relation st R is well-ordering & R,S are_isomorphic holds
for b3 being Function holds
( b3 = canonical_isomorphism_of (R,S) iff b3 is_isomorphism_of R,S );

theorem Th46: :: WELLORD1:46
for R being Relation st R is well-ordering holds
for a being object st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic
proof end;

theorem Th47: :: WELLORD1:47
for a, b being object
for R being Relation st R is well-ordering & a in field R & b in field R & a <> b holds
not R |_2 (R -Seg a),R |_2 (R -Seg b) are_isomorphic
proof end;

theorem Th48: :: WELLORD1:48
for Z being set
for R, S being Relation
for F being Function st R is well-ordering & Z c= field R & F is_isomorphism_of R,S holds
( F | Z is_isomorphism_of R |_2 Z,S |_2 (F .: Z) & R |_2 Z,S |_2 (F .: Z) are_isomorphic )
proof end;

theorem Th49: :: WELLORD1:49
for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
for a being object st a in field R holds
ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b )
proof end;

theorem Th50: :: WELLORD1:50
for R, S being Relation
for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
for a being object st a in field R holds
ex b being object st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )
proof end;

theorem Th51: :: WELLORD1:51
for a, b, c being object
for R, S being Relation st R is well-ordering & S is well-ordering & a in field R & b in field S & c in field S & R,S |_2 (S -Seg b) are_isomorphic & R |_2 (R -Seg a),S |_2 (S -Seg c) are_isomorphic holds
( S -Seg c c= S -Seg b & [c,b] in S )
proof end;

theorem Th52: :: WELLORD1:52
for R, S being Relation st R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being object holds
( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) holds
ex a being object st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic )
proof end;

theorem :: WELLORD1:53
for Y being set
for R being Relation st Y c= field R & R is well-ordering & not R,R |_2 Y are_isomorphic holds
ex a being object st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic )
proof end;

:: from AMISTD_3, 2010.01.10, A.T.
theorem :: WELLORD1:54
for R, S being Relation st R,S are_isomorphic & R is well-ordering holds
S is well-ordering by Th44;