:: WELLORD1 semantic presentation

Lemma1: for b₁ being Relation holds
( b₁ is reflexive iff for b₂ being set st b₂ in field b₁ holds
[b₂,b₂] in b₁ )

proof end;

Lemma2: for b₁ being Relation holds
( b₁ is transitive iff for b₂, b₃, b₄ being set st [b₂,b₃] in b₁ & [b₃,b₄] in b₁ holds
[b₂,b₄] in b₁ )

proof end;

Lemma3: for b₁ being Relation holds
( b₁ is antisymmetric iff for b₂, b₃ being set st [b₂,b₃] in b₁ & [b₃,b₂] in b₁ holds
b₂ = b₃ )

proof end;

Lemma4: for b₁ being Relation holds
( b₁ is connected iff for b₂, b₃ being set st b₂ in field b₁ & b₃ in field b₁ & b₂ <> b₃ & not [b₂,b₃] in b₁ holds
[b₃,b₂] in b₁ )

proof end;

definition

let c₁ be Relation;
let c₂ be set ;
defpred S₁[ set ] means ( a₁ <> c₂ & [a₁,c₂] in c₁ );
func c₁ -Seg c₂ -> set means :Def1: :: WELLORD1:def 1
for b₁ being set holds
( b₁ in a₃ iff ( b₁ <> a₂ & [b₁,a₂] in a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines -Seg WELLORD1:def 1 :

theorem Th1: :: WELLORD1:1

canceled;

theorem Th2: :: WELLORD1:2

for b₁ being set
for b₂ being Relation holds
( b₁ in field b₂ or b₂ -Seg b₁ = {} )

proof end;

definition

let c₁ be Relation;
attr a₁ is well_founded means :Def2: :: WELLORD1:def 2
for b₁ being set st b₁ c= field a₁ & b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & a₁ -Seg b₂ misses b₁ );
let c₂ be set ;
pred c₁ is_well_founded_in c₂ means :Def3: :: WELLORD1:def 3
for b₁ being set st b₁ c= a₂ & b₁ <> {} holds
ex b₂ being set st
( b₂ in b₁ & a₁ -Seg b₂ misses b₁ );

end;

:: deftheorem Def2 defines well_founded WELLORD1:def 2 :

:: deftheorem Def3 defines is_well_founded_in WELLORD1:def 3 :

theorem Th3: :: WELLORD1:3

canceled;

theorem Th4: :: WELLORD1:4

canceled;

theorem Th5: :: WELLORD1:5

for b₁ being Relation holds
( b₁ is well_founded iff b₁ is_well_founded_in field b₁ )

proof end;

definition

let c₁ be Relation;
attr a₁ is well-ordering means :Def4: :: WELLORD1:def 4
( a₁ is reflexive & a₁ is transitive & a₁ is antisymmetric & a₁ is connected & a₁ is well_founded );
let c₂ be set ;
pred c₁ well_orders c₂ means :Def5: :: WELLORD1:def 5
( a₁ is_reflexive_in a₂ & a₁ is_transitive_in a₂ & a₁ is_antisymmetric_in a₂ & a₁ is_connected_in a₂ & a₁ is_well_founded_in a₂ );

end;

:: deftheorem Def4 defines well-ordering WELLORD1:def 4 :

:: deftheorem Def5 defines well_orders WELLORD1:def 5 :

theorem Th6: :: WELLORD1:6

canceled;

theorem Th7: :: WELLORD1:7

canceled;

theorem Th8: :: WELLORD1:8

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

proof end;

theorem Th9: :: WELLORD1:9

for b₁ being set
for b₂ being Relation st b₂ well_orders b₁ holds
for b₃ being set st b₃ c= b₁ & b₃ <> {} holds
ex b₄ being set st
( b₄ in b₃ & ( for b₅ being set st b₅ in b₃ holds
[b₄,b₅] in b₂ ) )

proof end;

theorem Th10: :: WELLORD1:10

for b₁ being Relation st b₁ is well-ordering holds
for b₂ being set st b₂ c= field b₁ & b₂ <> {} holds
ex b₃ being set st
( b₃ in b₂ & ( for b₄ being set st b₄ in b₂ holds
[b₃,b₄] in b₁ ) )

proof end;

theorem Th11: :: WELLORD1:11

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

theorem Th12: :: WELLORD1:12

for b₁ being Relation st b₁ is well-ordering & field b₁ <> {} holds
for b₂ being set holds
( not b₂ in field b₁ or for b₃ being set st b₃ in field b₁ holds
[b₃,b₂] in b₁ or ex b₃ being set st
( b₃ in field b₁ & [b₂,b₃] in b₁ & ( for b₄ being set st b₄ in field b₁ & [b₂,b₄] in b₁ & not b₄ = b₂ holds
[b₃,b₄] in b₁ ) ) )

proof end;

theorem Th13: :: WELLORD1:13

for b₁ being set
for b₂ being Relation holds b₂ -Seg b₁ c= field b₂

proof end;

definition

let c₁ be Relation;
let c₂ be set ;
func c₁ |_2 c₂ -> Relation equals :: WELLORD1:def 6
a₁ /\ [:a₂,a₂:];
coherence by RELAT_1:9;

end;

:: deftheorem Def6 defines |_2 WELLORD1:def 6 :

theorem Th14: :: WELLORD1:14

canceled;

theorem Th15: :: WELLORD1:15

for b₁ being set
for b₂ being Relation holds
( b₂ |_2 b₁ c= b₂ & b₂ |_2 b₁ c= [:b₁,b₁:] ) by XBOOLE_1:17;

theorem Th16: :: WELLORD1:16

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in b₃ |_2 b₂ iff ( b₁ in b₃ & b₁ in [:b₂,b₂:] ) ) by XBOOLE_0:def 3;

theorem Th17: :: WELLORD1:17

for b₁ being set
for b₂ being Relation holds b₂ |_2 b₁ = (b₁ | b₂) | b₁

proof end;

theorem Th18: :: WELLORD1:18

for b₁ being set
for b₂ being Relation holds b₂ |_2 b₁ = b₁ | (b₂ | b₁)

proof end;

Lemma17: for b₁ being set
for b₂ being Relation holds dom (b₁ | b₂) c= dom b₂

proof end;

theorem Th19: :: WELLORD1:19

for b₁, b₂ being set
for b₃ being Relation st b₁ in field (b₃ |_2 b₂) holds
( b₁ in field b₃ & b₁ in b₂ )

proof end;

theorem Th20: :: WELLORD1:20

for b₁ being set
for b₂ being Relation holds
( field (b₂ |_2 b₁) c= field b₂ & field (b₂ |_2 b₁) c= b₁ )

proof end;

theorem Th21: :: WELLORD1:21

for b₁, b₂ being set
for b₃ being Relation holds (b₃ |_2 b₁) -Seg b₂ c= b₃ -Seg b₂

proof end;

theorem Th22: :: WELLORD1:22

for b₁ being set
for b₂ being Relation st b₂ is reflexive holds
b₂ |_2 b₁ is reflexive

proof end;

theorem Th23: :: WELLORD1:23

for b₁ being set
for b₂ being Relation st b₂ is connected holds
b₂ |_2 b₁ is connected

proof end;

theorem Th24: :: WELLORD1:24

for b₁ being set
for b₂ being Relation st b₂ is transitive holds
b₂ |_2 b₁ is transitive

proof end;

theorem Th25: :: WELLORD1:25

for b₁ being set
for b₂ being Relation st b₂ is antisymmetric holds
b₂ |_2 b₁ is antisymmetric

proof end;

theorem Th26: :: WELLORD1:26

for b₁, b₂ being set
for b₃ being Relation holds (b₃ |_2 b₁) |_2 b₂ = b₃ |_2 (b₁ /\ b₂)

proof end;

theorem Th27: :: WELLORD1:27

for b₁, b₂ being set
for b₃ being Relation holds (b₃ |_2 b₁) |_2 b₂ = (b₃ |_2 b₂) |_2 b₁

proof end;

theorem Th28: :: WELLORD1:28

for b₁ being set
for b₂ being Relation holds (b₂ |_2 b₁) |_2 b₁ = b₂ |_2 b₁

proof end;

theorem Th29: :: WELLORD1:29

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
(b₃ |_2 b₂) |_2 b₁ = b₃ |_2 b₁

proof end;

theorem Th30: :: WELLORD1:30

for b₁ being Relation holds b₁ |_2 (field b₁) = b₁

proof end;

theorem Th31: :: WELLORD1:31

for b₁ being set
for b₂ being Relation st b₂ is well_founded holds
b₂ |_2 b₁ is well_founded

proof end;

theorem Th32: :: WELLORD1:32

for b₁ being set
for b₂ being Relation st b₂ is well-ordering holds
b₂ |_2 b₁ is well-ordering

proof end;

theorem Th33: :: WELLORD1:33

for b₁, b₂ being set
for b₃ being Relation st b₃ is well-ordering holds
b₃ -Seg b₁,b₃ -Seg b₂ are_c=-comparable

proof end;

theorem Th34: :: WELLORD1:34

canceled;

theorem Th35: :: WELLORD1:35

for b₁, b₂ being set
for b₃ being Relation st b₃ is well-ordering & b₁ in field b₃ & b₂ in b₃ -Seg b₁ holds
(b₃ |_2 (b₃ -Seg b₁)) -Seg b₂ = b₃ -Seg b₂

proof end;

theorem Th36: :: WELLORD1:36

for b₁ being set
for b₂ being Relation st b₂ is well-ordering & b₁ c= field b₂ holds
( ( b₁ = field b₂ or ex b₃ being set st
( b₃ in field b₂ & b₁ = b₂ -Seg b₃ ) ) iff for b₃ being set st b₃ in b₁ holds
for b₄ being set st [b₄,b₃] in b₂ holds
b₄ in b₁ )

proof end;

theorem Th37: :: WELLORD1:37

for b₁, b₂ being set
for b₃ being Relation st b₃ is well-ordering & b₁ in field b₃ & b₂ in field b₃ holds
( [b₁,b₂] in b₃ iff b₃ -Seg b₁ c= b₃ -Seg b₂ )

proof end;

theorem Th38: :: WELLORD1:38

for b₁, b₂ being set
for b₃ being Relation st b₃ is well-ordering & b₁ in field b₃ & b₂ in field b₃ holds
( b₃ -Seg b₁ c= b₃ -Seg b₂ iff ( b₁ = b₂ or b₁ in b₃ -Seg b₂ ) )

proof end;

theorem Th39: :: WELLORD1:39

for b₁ being set
for b₂ being Relation st b₂ is well-ordering & b₁ c= field b₂ holds
field (b₂ |_2 b₁) = b₁

proof end;

theorem Th40: :: WELLORD1:40

for b₁ being set
for b₂ being Relation st b₂ is well-ordering holds
field (b₂ |_2 (b₂ -Seg b₁)) = b₂ -Seg b₁

proof end;

theorem Th41: :: WELLORD1:41

for b₁ being Relation st b₁ is well-ordering holds
for b₂ being set st ( for b₃ being set st b₃ in field b₁ & b₁ -Seg b₃ c= b₂ holds
b₃ in b₂ ) holds
field b₁ c= b₂

proof end;

theorem Th42: :: WELLORD1:42

for b₁, b₂ being set
for b₃ being Relation st b₃ is well-ordering & b₁ in field b₃ & b₂ in field b₃ & ( for b₄ being set st b₄ in b₃ -Seg b₁ holds
( [b₄,b₂] in b₃ & b₄ <> b₂ ) ) holds
[b₁,b₂] in b₃

proof end;

theorem Th43: :: WELLORD1:43

for b₁ being Relation
for b₂ being Function st b₁ is well-ordering & dom b₂ = field b₁ & rng b₂ c= field b₁ & ( for b₃, b₄ being set st [b₃,b₄] in b₁ & b₃ <> b₄ holds
( [(b₂ . b₃),(b₂ . b₄)] in b₁ & b₂ . b₃ <> b₂ . b₄ ) ) holds
for b₃ being set st b₃ in field b₁ holds
[b₃,(b₂ . b₃)] in b₁

proof end;

definition

let c₁, c₂ be Relation;
let c₃ be Function;
pred c₃ is_isomorphism_of c₁,c₂ means :Def7: :: WELLORD1:def 7
( dom a₃ = field a₁ & rng a₃ = field a₂ & a₃ is one-to-one & ( for b₁, b₂ being set holds
( [b₁,b₂] in a₁ iff ( b₁ in field a₁ & b₂ in field a₁ & [(a₃ . b₁),(a₃ . b₂)] in a₂ ) ) ) );

end;

:: deftheorem Def7 defines is_isomorphism_of WELLORD1:def 7 :

theorem Th44: :: WELLORD1:44

canceled;

theorem Th45: :: WELLORD1:45

for b₁, b₂ being Relation
for b₃ being Function st b₃ is_isomorphism_of b₁,b₂ holds
for b₄, b₅ being set st [b₄,b₅] in b₁ & b₄ <> b₅ holds
( [(b₃ . b₄),(b₃ . b₅)] in b₂ & b₃ . b₄ <> b₃ . b₅ )

proof end;

definition

let c₁, c₂ be Relation;
pred c₁,c₂ are_isomorphic means :Def8: :: WELLORD1:def 8
ex b₁ being Function st b₁ is_isomorphism_of a₁,a₂;

end;

:: deftheorem Def8 defines are_isomorphic WELLORD1:def 8 :

theorem Th46: :: WELLORD1:46

canceled;

theorem Th47: :: WELLORD1:47

for b₁ being Relation holds id (field b₁) is_isomorphism_of b₁,b₁

proof end;

theorem Th48: :: WELLORD1:48

for b₁ being Relation holds b₁,b₁ are_isomorphic

proof end;

theorem Th49: :: WELLORD1:49

for b₁, b₂ being Relation
for b₃ being Function st b₃ is_isomorphism_of b₁,b₂ holds
b₃ " is_isomorphism_of b₂,b₁

proof end;

theorem Th50: :: WELLORD1:50

for b₁, b₂ being Relation st b₁,b₂ are_isomorphic holds
b₂,b₁ are_isomorphic

proof end;

theorem Th51: :: WELLORD1:51

for b₁, b₂, b₃ being Relation
for b₄, b₅ being Function st b₄ is_isomorphism_of b₁,b₂ & b₅ is_isomorphism_of b₂,b₃ holds
b₅ * b₄ is_isomorphism_of b₁,b₃

proof end;

theorem Th52: :: WELLORD1:52

for b₁, b₂, b₃ being Relation st b₁,b₂ are_isomorphic & b₂,b₃ are_isomorphic holds
b₁,b₃ are_isomorphic

proof end;

theorem Th53: :: WELLORD1:53

for b₁, b₂ being Relation
for b₃ being Function st b₃ is_isomorphism_of b₁,b₂ holds
( ( b₁ is reflexive implies b₂ is reflexive ) & ( b₁ is transitive implies b₂ is transitive ) & ( b₁ is connected implies b₂ is connected ) & ( b₁ is antisymmetric implies b₂ is antisymmetric ) & ( b₁ is well_founded implies b₂ is well_founded ) )

proof end;

theorem Th54: :: WELLORD1:54

for b₁, b₂ being Relation
for b₃ being Function st b₁ is well-ordering & b₃ is_isomorphism_of b₁,b₂ holds
b₂ is well-ordering

proof end;

theorem Th55: :: WELLORD1:55

for b₁, b₂ being Relation st b₁ is well-ordering holds
for b₃, b₄ being Function st b₃ is_isomorphism_of b₁,b₂ & b₄ is_isomorphism_of b₁,b₂ holds
b₃ = b₄

proof end;

definition

let c₁, c₂ be Relation;
assume E51: ( c₁ is well-ordering & c₁,c₂ are_isomorphic ) ;
func canonical_isomorphism_of c₁,c₂ -> Function means :Def9: :: WELLORD1:def 9
a₃ is_isomorphism_of a₁,a₂;
existence by E51, Def8;
uniqueness by E51, Th55;

end;

:: deftheorem Def9 defines canonical_isomorphism_of WELLORD1:def 9 :

theorem Th56: :: WELLORD1:56

canceled;

theorem Th57: :: WELLORD1:57

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

proof end;

theorem Th58: :: WELLORD1:58

for b₁, b₂ being set
for b₃ being Relation st b₃ is well-ordering & b₁ in field b₃ & b₂ in field b₃ & b₁ <> b₂ holds
not b₃ |_2 (b₃ -Seg b₁),b₃ |_2 (b₃ -Seg b₂) are_isomorphic

proof end;

theorem Th59: :: WELLORD1:59

for b₁ being set
for b₂, b₃ being Relation
for b₄ being Function st b₂ is well-ordering & b₁ c= field b₂ & b₄ is_isomorphism_of b₂,b₃ holds
( b₄ | b₁ is_isomorphism_of b₂ |_2 b₁,b₃ |_2 (b₄ .: b₁) & b₂ |_2 b₁,b₃ |_2 (b₄ .: b₁) are_isomorphic )

proof end;

theorem Th60: :: WELLORD1:60

for b₁, b₂ being Relation
for b₃ being Function st b₁ is well-ordering & b₃ is_isomorphism_of b₁,b₂ holds
for b₄ being set st b₄ in field b₁ holds
ex b₅ being set st
( b₅ in field b₂ & b₃ .: (b₁ -Seg b₄) = b₂ -Seg b₅ )

proof end;

theorem Th61: :: WELLORD1:61

for b₁, b₂ being Relation
for b₃ being Function st b₁ is well-ordering & b₃ is_isomorphism_of b₁,b₂ holds
for b₄ being set st b₄ in field b₁ holds
ex b₅ being set st
( b₅ in field b₂ & b₁ |_2 (b₁ -Seg b₄),b₂ |_2 (b₂ -Seg b₅) are_isomorphic )

proof end;

theorem Th62: :: WELLORD1:62

for b₁, b₂, b₃ being set
for b₄, b₅ being Relation st b₄ is well-ordering & b₅ is well-ordering & b₁ in field b₄ & b₂ in field b₅ & b₃ in field b₅ & b₄,b₅ |_2 (b₅ -Seg b₂) are_isomorphic & b₄ |_2 (b₄ -Seg b₁),b₅ |_2 (b₅ -Seg b₃) are_isomorphic holds
( b₅ -Seg b₃ c= b₅ -Seg b₂ & [b₃,b₂] in b₅ )

proof end;

theorem Th63: :: WELLORD1:63

for b₁, b₂ being Relation st b₁ is well-ordering & b₂ is well-ordering & not b₁,b₂ are_isomorphic & ( for b₃ being set holds
( not b₃ in field b₁ or not b₁ |_2 (b₁ -Seg b₃),b₂ are_isomorphic ) ) holds
ex b₃ being set st
( b₃ in field b₂ & b₁,b₂ |_2 (b₂ -Seg b₃) are_isomorphic )

proof end;

theorem Th64: :: WELLORD1:64

for b₁ being set
for b₂ being Relation st b₁ c= field b₂ & b₂ is well-ordering & not b₂,b₂ |_2 b₁ are_isomorphic holds
ex b₃ being set st
( b₃ in field b₂ & b₂ |_2 (b₂ -Seg b₃),b₂ |_2 b₁ are_isomorphic )

proof end;