:: by Grzegorz Bancerek

::

:: Received April 4, 1989

:: Copyright (c) 1990-2012 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;

:: deftheorem defines -Seg WELLORD1:def 1 :

for R being Relation

for a being set holds R -Seg a = (Coim (R,a)) \ {a};

for R being Relation

for a being set holds R -Seg a = (Coim (R,a)) \ {a};

definition

let R be Relation;

end;
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 ;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 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 ) );

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 ) );

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 ) );

definition

let R be Relation;

end;
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 ;( R is reflexive & R is transitive & R is antisymmetric & R is connected & R is well_founded );

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 );

( 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 );

:: 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 ) );

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 ) );

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

for b_{1} being Relation st b_{1} is well-ordering holds

( b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is connected & b_{1} is well_founded )
by Def4;

for b_{1} being Relation st b_{1} is reflexive & b_{1} is transitive & b_{1} is antisymmetric & b_{1} is connected & b_{1} is well_founded holds

b_{1} is well-ordering
by Def4;

end;

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

coherence for b

( b

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

coherence for b

b

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 set st

( a in Y & ( for b being set st b in Y holds

[a,b] in R ) )

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 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 set st

( a in Y & ( for b being set st b in Y holds

[a,b] in R ) )

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

theorem :: WELLORD1:8

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 ) ) )

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;

:: deftheorem defines |_2 WELLORD1:def 6 :

for R being Relation

for Y being set holds R |_2 Y = R /\ [:Y,Y:];

for R being Relation

for Y being set holds R |_2 Y = R /\ [:Y,Y:];

Lm5: for X being set

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

proof end;

theorem Th26: :: WELLORD1:26

for a, b being set

for R being Relation st R is well-ordering holds

R -Seg a,R -Seg b are_c=-comparable

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 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

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 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 )

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 Th29: :: WELLORD1:29

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 )

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 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 ) )

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 Th32: :: WELLORD1:32

for a being set

for R being Relation st R is well-ordering holds

field (R |_2 (R -Seg a)) = R -Seg a

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 set st a in field R & R -Seg a c= Z holds

a in Z ) holds

field R c= Z

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 Th34: :: WELLORD1:34

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

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 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 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

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;

:: 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 ) ) ) ) );

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 Th36: :: WELLORD1:36

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 )

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;

end;
pred R,S are_isomorphic means :Def8: :: WELLORD1:def 8

ex F being Function st F is_isomorphism_of R,S;

ex F being Function st F is_isomorphism_of R,S;

:: 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 );

for R, S being Relation holds

( R,S are_isomorphic iff ex F being Function st F is_isomorphism_of R,S );

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

for F being Function st F is_isomorphism_of R,S holds

F " is_isomorphism_of S,R

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

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 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 ) )

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

for F being Function st R is well-ordering & F is_isomorphism_of R,S holds

S is well-ordering

proof end;

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

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 ;

ex b_{1} being Function st b_{1} is_isomorphism_of R,S
by A2, Def8;

uniqueness

for b_{1}, b_{2} being Function st b_{1} is_isomorphism_of R,S & b_{2} is_isomorphism_of R,S holds

b_{1} = b_{2}
by A1, Th45;

end;
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 it is_isomorphism_of R,S;

ex b

uniqueness

for b

b

:: 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_{3} being Function holds

( b_{3} = canonical_isomorphism_of (R,S) iff b_{3} is_isomorphism_of R,S );

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

for b

( b

theorem Th46: :: WELLORD1:46

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

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

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 )

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 set st a in field R holds

ex b being set st

( b in field S & F .: (R -Seg a) = S -Seg b )

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 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 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 )

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 Th51: :: WELLORD1:51

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 )

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 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 )

( 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: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 set st

( a in field R & R |_2 (R -Seg a),R |_2 Y are_isomorphic )

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;

:: from AMISTD_3, 2010.01.10, A.T.