:: The Well Ordering Relations
:: by Grzegorz Bancerek
::
:: Received April 4, 1989
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

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

proof end;

Lm2: for R being Relation holds
( R is transitive iff for x, y, z being set 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 set 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 set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R )

proof end;

definition

let R be Relation;
let a be set ;
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 set holds R -Seg a = (Coim (R,a)) \ {a};

theorem Th1: :: WELLORD1:1

for x, a being set
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 set
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 set st
( a in Y & R -Seg a misses Y );
let X be set ;
pred R is_well_founded_in X means :Def3: :: WELLORD1:def 3
for Y being set st Y c= X & Y <> {} holds
ex a being set 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 set st
( a in Y & R -Seg a misses Y ) );

:: deftheorem Def3 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 set st
( a in Y & R -Seg a misses Y ) );

theorem :: WELLORD1:3

canceled;

theorem :: WELLORD1:4

canceled;

theorem Th5: :: WELLORD1:5

for R being Relation holds
( R is well_founded iff R is_well_founded_in field R )

proof end;

definition

let R be Relation;
attr R is well-ordering means :Def4: :: 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 :Def5: :: 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 Def4 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 Def5 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 ) );

theorem :: WELLORD1:6

canceled;

theorem :: WELLORD1:7

canceled;

theorem :: WELLORD1:8

for R being Relation holds
( R well_orders field R iff R is well-ordering )

proof end;

theorem :: WELLORD1:9

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 set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )

proof end;

theorem Th10: :: WELLORD1:10

for R being Relation st R is well-ordering holds
for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & ( for b being set st b in Y holds
[a,b] in R ) )

proof end;

theorem :: WELLORD1:11

for R being Relation st R is well-ordering & field R <> {} holds
ex a being set st
( a in field R & ( for b being set st b in field R holds
[a,b] in R ) ) by Th10;

theorem :: WELLORD1:12

for R being Relation st R is well-ordering holds
for a being set holds
( not a in field R or for b being set st b in field R holds
[b,a] in R or ex b being set st
( b in field R & [a,b] in R & ( for c being set st c in field R & [a,c] in R & not c = a holds
[b,c] in R ) ) )

proof end;

theorem Th13: :: WELLORD1:13

for a being set
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 :: WELLORD1:14

canceled;

theorem :: WELLORD1:15

canceled;

theorem :: WELLORD1:16

canceled;

theorem Th17: :: WELLORD1:17

for X being set
for R being Relation holds R |_2 X = (X | R) | X

proof end;

theorem Th18: :: WELLORD1:18

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 Th19: :: WELLORD1:19

for x, 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 Th20: :: WELLORD1:20

for X being set
for R being Relation holds
( field (R |_2 X) c= field R & field (R |_2 X) c= X )

proof end;

theorem Th21: :: WELLORD1:21

for X, a being set
for R being Relation holds (R |_2 X) -Seg a c= R -Seg a

proof end;

theorem Th22: :: WELLORD1:22

for X being set
for R being Relation st R is reflexive holds
R |_2 X is reflexive

proof end;

theorem Th23: :: WELLORD1:23

for Y being set
for R being Relation st R is connected holds
R |_2 Y is connected

proof end;

theorem Th24: :: WELLORD1:24

for Y being set
for R being Relation st R is transitive holds
R |_2 Y is transitive

proof end;

theorem Th25: :: WELLORD1:25

for Y being set
for R being Relation st R is antisymmetric holds
R |_2 Y is antisymmetric

proof end;

theorem Th26: :: WELLORD1:26

for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y)

proof end;

theorem :: WELLORD1:27

for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = (R |_2 Y) |_2 X

proof end;

theorem :: WELLORD1:28

for Y being set
for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y

proof end;

theorem Th29: :: WELLORD1:29

for Z, Y being set
for R being Relation st Z c= Y holds
(R |_2 Y) |_2 Z = R |_2 Z

proof end;

theorem Th30: :: WELLORD1:30

for R being Relation holds R |_2 (field R) = R

proof end;

theorem Th31: :: WELLORD1:31

for X being set
for R being Relation st R is well_founded holds
R |_2 X is well_founded

proof end;

theorem Th32: :: WELLORD1:32

for Y being set
for R being Relation st R is well-ordering holds
R |_2 Y is well-ordering

proof end;

theorem Th33: :: WELLORD1:33

for a, b being set
for R being Relation st R is well-ordering holds
R -Seg a,R -Seg b are_c=-comparable

proof end;

theorem :: WELLORD1:34

canceled;

theorem Th35: :: WELLORD1:35

for b, a being set
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 Th36: :: WELLORD1:36

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 set st
( a in field R & Y = R -Seg a ) ) iff for a being set st a in Y holds
for b being set st [b,a] in R holds
b in Y )

proof end;

theorem Th37: :: WELLORD1:37

for a, b being set
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 Th38: :: WELLORD1:38

for a, b being set
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 Th39: :: WELLORD1:39

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 Th40: :: WELLORD1:40

for a being set
for R being Relation st R is well-ordering holds
field (R |_2 (R -Seg a)) = R -Seg a

proof end;

theorem Th41: :: WELLORD1:41

for R being Relation st R is well-ordering holds
for Z being set st ( for a being set st a in field R & R -Seg a c= Z holds
a in Z ) holds
field R c= Z

proof end;

theorem Th42: :: WELLORD1:42

for a, b being set
for R being Relation st R is well-ordering & a in field R & b in field R & ( for c being set st c in R -Seg a holds
( [c,b] in R & c <> b ) ) holds
[a,b] in R

proof end;

theorem Th43: :: WELLORD1:43

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 set st [a,b] in R & a <> b holds
( [(F . a),(F . b)] in R & F . a <> F . b ) ) holds
for a being set 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 :Def7: :: WELLORD1:def 7
( dom F = field R & rng F = field S & F is one-to-one & ( for a, b being set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) );

end;

:: deftheorem Def7 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 set holds
( [a,b] in R iff ( a in field R & b in field R & [(F . a),(F . b)] in S ) ) ) ) );

theorem :: WELLORD1:44

canceled;

theorem Th45: :: WELLORD1:45

for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
for a, b being set 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 :Def8: :: WELLORD1:def 8
ex F being Function st F is_isomorphism_of R,S;

end;

:: deftheorem Def8 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 :: WELLORD1:46

canceled;

theorem Th47: :: WELLORD1:47

for R being Relation holds id (field R) is_isomorphism_of R,R

proof end;

theorem :: WELLORD1:48

for R being Relation holds R,R 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
F " is_isomorphism_of S,R

proof end;

theorem Th50: :: WELLORD1:50

for R, S being Relation st R,S are_isomorphic holds
S,R are_isomorphic

proof end;

theorem Th51: :: WELLORD1:51

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 Th52: :: WELLORD1:52

for R, S, T being Relation st R,S are_isomorphic & S,T are_isomorphic holds
R,T are_isomorphic

proof end;

theorem Th53: :: WELLORD1:53

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 Th54: :: WELLORD1:54

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

proof end;

theorem Th55: :: WELLORD1:55

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, Def8;
uniqueness
for b₁, b₂ being Function st b₁ is_isomorphism_of R,S & b₂ is_isomorphism_of R,S holds
b₁ = b₂ by A1, Th55;

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 :: WELLORD1:56

canceled;

theorem Th57: :: WELLORD1:57

for R being Relation st R is well-ordering holds
for a being set st a in field R holds
not R,R |_2 (R -Seg a) are_isomorphic

proof end;

theorem Th58: :: WELLORD1:58

for a, b being set
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 Th59: :: WELLORD1:59

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 Th60: :: WELLORD1:60

for R, S being Relation
for F being Function st F is_isomorphism_of R,S holds
for a being set st a in field R holds
ex b being set st
( b in field S & F .: (R -Seg a) = S -Seg b )

proof end;

theorem Th61: :: WELLORD1:61

for R, S being Relation
for F being Function st R is well-ordering & F is_isomorphism_of R,S holds
for a being set st a in field R holds
ex b being set st
( b in field S & R |_2 (R -Seg a),S |_2 (S -Seg b) are_isomorphic )

proof end;

theorem Th62: :: WELLORD1:62

for a, b, c being set
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 Th63: :: WELLORD1:63

for R, S being Relation st R is well-ordering & S is well-ordering & not R,S are_isomorphic & ( for a being set holds
( not a in field R or not R |_2 (R -Seg a),S are_isomorphic ) ) holds
ex a being set st
( a in field S & R,S |_2 (S -Seg a) are_isomorphic )

proof end;

theorem :: WELLORD1:64

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 set st
( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic )

proof end;

theorem :: WELLORD1:65

for R, S being Relation st R,S are_isomorphic & R is well-ordering holds
S is well-ordering

proof end;