:: WELLORD1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 ;
defpred S1[ set ] means ( $1 <> a & [$1,a] in R );
func R -Seg a -> set means :Def1: :: WELLORD1:def 1
for x being set holds
( x in it iff ( x <> a & [x,a] in R ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x <> a & [x,a] in R ) )
proof end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x <> a & [x,a] in R ) ) ) & ( for x being set holds
( x in b2 iff ( x <> a & [x,a] in R ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines -Seg WELLORD1:def 1 :
for R being Relation
for a, b3 being set holds
( b3 = R -Seg a iff for x being set holds
( x in b3 iff ( x <> a & [x,a] in R ) ) );

theorem :: WELLORD1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th2: :: WELLORD1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WELLORD1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th5: :: WELLORD1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WELLORD1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WELLORD1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds
( R well_orders field R iff R is well-ordering )
proof end;

theorem :: WELLORD1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation st R is well-ordering & field R <> {} 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
by RELAT_1:9;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: WELLORD1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation holds
( R |_2 X c= R & R |_2 X c= [:X,X:] ) by XBOOLE_1:17;

theorem Th16: :: WELLORD1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, X being set
for R being Relation holds
( x in R |_2 X iff ( x in R & x in [:X,X:] ) ) by XBOOLE_0:def 3;

theorem Th17: :: WELLORD1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation holds R |_2 X = (X | R) | X
proof end;

theorem Th18: :: WELLORD1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for R being Relation st R is reflexive holds
R |_2 X is reflexive
proof end;

theorem Th23: :: WELLORD1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for R being Relation st R is connected holds
R |_2 Y is connected
proof end;

theorem Th24: :: WELLORD1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for R being Relation st R is transitive holds
R |_2 Y is transitive
proof end;

theorem Th25: :: WELLORD1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for R being Relation st R is antisymmetric holds
R |_2 Y is antisymmetric
proof end;

theorem Th26: :: WELLORD1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for R being Relation holds (R |_2 X) |_2 Y = R |_2 (X /\ Y)
proof end;

theorem :: WELLORD1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for R being Relation holds (R |_2 Y) |_2 Y = R |_2 Y
proof end;

theorem Th29: :: WELLORD1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds R |_2 (field R) = R
proof end;

theorem Th31: :: WELLORD1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th35: :: WELLORD1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set
for R being Relation st R is well-ordering & a in field R & b in R -Seg a holds
(R |_2 (R -Seg a)) -Seg b = R -Seg b
proof end;

theorem Th36: :: WELLORD1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th45: :: WELLORD1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th47: :: WELLORD1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds id (field R) is_isomorphism_of R,R
proof end;

theorem :: WELLORD1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R being Relation holds R,R are_isomorphic
proof end;

theorem Th49: :: WELLORD1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for R, S being Relation st R,S are_isomorphic holds
S,R are_isomorphic
proof end;

theorem Th51: :: WELLORD1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 A1: ( R is well-ordering & 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 A1, Def8;
uniqueness
for b1, b2 being Function st b1 is_isomorphism_of R,S & b2 is_isomorphism_of R,S holds
b1 = b2
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 b3 being Function holds
( b3 = canonical_isomorphism_of R,S iff b3 is_isomorphism_of R,S );

theorem :: WELLORD1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th57: :: WELLORD1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & F .: (R -Seg a) = S -Seg b )
proof end;

theorem Th61: :: WELLORD1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;