:: The Well Ordering Relations
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: 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 RELAT_2:def 1, RELAT_2:def 9;

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 RELAT_2:def 6, RELAT_2:def 14;

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 ;

pred R well_orders X means :: WELLORD1:def 5
( 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 );

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

cluster Relation-like well-ordering -> reflexive antisymmetric connected transitive well_founded for set ;

coherence
for b₁ being Relation st b₁ is well-ordering holds
( b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric & b₁ is connected & b₁ is well_founded ) ;

cluster Relation-like reflexive antisymmetric connected transitive well_founded -> well-ordering for set ;

coherence
for b₁ being Relation st b₁ is reflexive & b₁ is transitive & b₁ is antisymmetric & b₁ is connected & b₁ is well_founded holds
b₁ 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 (field R) = 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 Th15, Th16, Th17, Th18, Th24;

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 (field R) 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 b₁ being Function st b₁ is_isomorphism_of R,S by A2;
uniqueness
for b₁, b₂ being Function st b₁ is_isomorphism_of R,S & b₂ is_isomorphism_of R,S holds
b₁ = b₂ by A1, Th45;

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 b₃ being Function holds
( b₃ = canonical_isomorphism_of (R,S) iff b₃ 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;