:: WELLORD2 semantic presentation

definition

let c₁ be set ;
func RelIncl c₁ -> Relation means :Def1: :: WELLORD2:def 1
( field a₂ = a₁ & ( for b₁, b₂ being set st b₁ in a₁ & b₂ in a₁ holds
( [b₁,b₂] in a₂ iff b₁ c= b₂ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines RelIncl WELLORD2:def 1 :

theorem Th1: :: WELLORD2:1

canceled;

theorem Th2: :: WELLORD2:2

for b₁ being set holds RelIncl b₁ is reflexive

proof end;

theorem Th3: :: WELLORD2:3

for b₁ being set holds RelIncl b₁ is transitive

proof end;

theorem Th4: :: WELLORD2:4

for b₁ being Ordinal holds RelIncl b₁ is connected

proof end;

theorem Th5: :: WELLORD2:5

for b₁ being set holds RelIncl b₁ is antisymmetric

proof end;

theorem Th6: :: WELLORD2:6

for b₁ being Ordinal holds RelIncl b₁ is well_founded

proof end;

theorem Th7: :: WELLORD2:7

for b₁ being Ordinal holds RelIncl b₁ is well-ordering

proof end;

theorem Th8: :: WELLORD2:8

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

proof end;

theorem Th9: :: WELLORD2:9

for b₁ being Ordinal
for b₂ being set st b₂ c= b₁ holds
RelIncl b₂ is well-ordering

proof end;

theorem Th10: :: WELLORD2:10

for b₁, b₂ being Ordinal st b₁ in b₂ holds
b₁ = (RelIncl b₂) -Seg b₁

proof end;

theorem Th11: :: WELLORD2:11

for b₁, b₂ being Ordinal st RelIncl b₁, RelIncl b₂ are_isomorphic holds
b₁ = b₂

proof end;

theorem Th12: :: WELLORD2:12

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

proof end;

theorem Th13: :: WELLORD2:13

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

proof end;

theorem Th14: :: WELLORD2:14

for b₁ being Relation st b₁ is well-ordering holds
ex b₂ being Ordinal st b₁, RelIncl b₂ are_isomorphic

proof end;

definition

let c₁ be Relation;
assume E15: c₁ is well-ordering ;
func order_type_of c₁ -> Ordinal means :Def2: :: WELLORD2:def 2
a₁, RelIncl a₂ are_isomorphic ;
existence by E15, Th14;
uniqueness by Th12;

end;

:: deftheorem Def2 defines order_type_of WELLORD2:def 2 :

definition

let c₁ be Ordinal;
let c₂ be Relation;
pred c₁ is_order_type_of c₂ means :: WELLORD2:def 3
a₁ = order_type_of a₂;

end;

:: deftheorem Def3 defines is_order_type_of WELLORD2:def 3 :

theorem Th15: :: WELLORD2:15

canceled;

theorem Th16: :: WELLORD2:16

canceled;

theorem Th17: :: WELLORD2:17

for b₁ being set
for b₂ being Ordinal st b₁ c= b₂ holds
order_type_of (RelIncl b₁) c= b₂

proof end;

definition

let c₁, c₂ be set ;
redefine pred are_equipotent as c₁,c₂ are_equipotent means :: WELLORD2:def 4
ex b₁ being Function st
( b₁ is one-to-one & dom b₁ = a₁ & rng b₁ = a₂ );
compatibility

proof end;

reflexivity

proof end;

symmetry

proof end;

end;

:: deftheorem Def4 defines are_equipotent WELLORD2:def 4 :

theorem Th18: :: WELLORD2:18

canceled;

theorem Th19: :: WELLORD2:19

canceled;

theorem Th20: :: WELLORD2:20

canceled;

theorem Th21: :: WELLORD2:21

canceled;

theorem Th22: :: WELLORD2:22

for b₁, b₂, b₃ being set st b₁,b₂ are_equipotent & b₂,b₃ are_equipotent holds
b₁,b₃ are_equipotent

proof end;

theorem Th23: :: WELLORD2:23

canceled;

theorem Th24: :: WELLORD2:24

canceled;

theorem Th25: :: WELLORD2:25

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

proof end;

Lemma17: for b₁ being set
for b₂ being Relation st b₂ is well-ordering & b₁, field b₂ are_equipotent holds
ex b₃ being Relation st b₃ well_orders b₁

proof end;

theorem Th26: :: WELLORD2:26

for b₁ being set ex b₂ being Relation st b₂ well_orders b₁

proof end;

theorem Th27: :: WELLORD2:27

for b₁ being non empty set st ( for b₂ being set st b₂ in b₁ holds
b₂ <> {} ) & ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ & b₂ <> b₃ holds
b₂ misses b₃ ) holds
ex b₂ being set st
for b₃ being set st b₃ in b₁ holds
ex b₄ being set st b₂ /\ b₃ = {b₄}

proof end;

theorem Th28: :: WELLORD2:28

for b₁ being non empty set st ( for b₂ being set st b₂ in b₁ holds
b₂ <> {} ) holds
ex b₂ being Function st
( dom b₂ = b₁ & ( for b₃ being set st b₃ in b₁ holds
b₂ . b₃ in b₃ ) )

proof end;

scheme :: WELLORD2:sch 1
s1{ F₁() -> set , F₂() -> set , P₁[ set , set ] } :

ex b₁ being Function st
( dom b₁ = F₁() & rng b₁ c= F₂() & ( for b₂ being set st b₂ in F₁() holds
P₁[b₂,b₁ . b₂] ) )

provided

E20: for b₁ being set st b₁ in F₁() holds
ex b₂ being set st
( b₂ in F₂() & P₁[b₁,b₂] )

proof end;

scheme :: WELLORD2:sch 2
s2{ F₁() -> set , F₂() -> set , F₃() -> set , P₁[ set , set , set ] } :

ex b₁, b₂ being Function st
( dom b₁ = F₁() & dom b₂ = F₁() & ( for b₃ being set st b₃ in F₁() holds
P₁[b₃,b₁ . b₃,b₂ . b₃] ) )

provided

E20: for b₁ being set st b₁ in F₁() holds
ex b₂, b₃ being set st
( b₂ in F₂() & b₃ in F₃() & P₁[b₁,b₂,b₃] )

proof end;