:: ORDINAL1 semantic presentation

theorem Th1: :: ORDINAL1:1

canceled;

theorem Th2: :: ORDINAL1:2

canceled;

theorem Th3: :: ORDINAL1:3

for b₁, b₂, b₃ being set holds
( not b₁ in b₂ or not b₂ in b₃ or not b₃ in b₁ )

proof end;

theorem Th4: :: ORDINAL1:4

for b₁, b₂, b₃, b₄ being set holds
( not b₁ in b₂ or not b₂ in b₃ or not b₃ in b₄ or not b₄ in b₁ )

proof end;

theorem Th5: :: ORDINAL1:5

for b₁, b₂, b₃, b₄, b₅ being set holds
( not b₁ in b₂ or not b₂ in b₃ or not b₃ in b₄ or not b₄ in b₅ or not b₅ in b₁ )

proof end;

theorem Th6: :: ORDINAL1:6

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds
( not b₁ in b₂ or not b₂ in b₃ or not b₃ in b₄ or not b₄ in b₅ or not b₅ in b₆ or not b₆ in b₁ )

proof end;

theorem Th7: :: ORDINAL1:7

for b₁, b₂ being set st b₁ in b₂ holds
not b₂ c= b₁

proof end;

definition

let c₁ be set ;
func succ c₁ -> set equals :: ORDINAL1:def 1
a₁ \/ {a₁};
coherence ;

end;

:: deftheorem Def1 defines succ ORDINAL1:def 1 :

registration

let c₁ be set ;
cluster succ a₁ -> non empty ;
coherence

proof end;

end;

theorem Th8: :: ORDINAL1:8

canceled;

theorem Th9: :: ORDINAL1:9

canceled;

theorem Th10: :: ORDINAL1:10

for b₁ being set holds b₁ in succ b₁

proof end;

theorem Th11: :: ORDINAL1:11

canceled;

theorem Th12: :: ORDINAL1:12

for b₁, b₂ being set st succ b₁ = succ b₂ holds
b₁ = b₂

proof end;

theorem Th13: :: ORDINAL1:13

for b₁, b₂ being set holds
( b₁ in succ b₂ iff ( b₁ in b₂ or b₁ = b₂ ) )

proof end;

theorem Th14: :: ORDINAL1:14

for b₁ being set holds b₁ <> succ b₁

proof end;

definition

let c₁ be set ;
attr a₁ is epsilon-transitive means :Def2: :: ORDINAL1:def 2
for b₁ being set st b₁ in a₁ holds
b₁ c= a₁;
attr a₁ is epsilon-connected means :Def3: :: ORDINAL1:def 3
for b₁, b₂ being set st b₁ in a₁ & b₂ in a₁ & not b₁ in b₂ & not b₁ = b₂ holds
b₂ in b₁;

end;

:: deftheorem Def2 defines epsilon-transitive ORDINAL1:def 2 :

:: deftheorem Def3 defines epsilon-connected ORDINAL1:def 3 :

Lemma7: ( {} is epsilon-transitive & {} is epsilon-connected )

proof end;

definition

let c₁ be set ;
attr a₁ is ordinal means :Def4: :: ORDINAL1:def 4
( a₁ is epsilon-transitive & a₁ is epsilon-connected );

end;

:: deftheorem Def4 defines ordinal ORDINAL1:def 4 :

registration

cluster ordinal -> epsilon-transitive epsilon-connected number ;
coherence by Def4;
cluster epsilon-transitive epsilon-connected -> ordinal number ;
coherence by Def4;

end;

notation

synonym number for set ;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal number ;
existence

proof end;

end;

definition

mode Ordinal is ordinal number ;

end;

theorem Th15: :: ORDINAL1:15

canceled;

theorem Th16: :: ORDINAL1:16

canceled;

theorem Th17: :: ORDINAL1:17

canceled;

theorem Th18: :: ORDINAL1:18

canceled;

theorem Th19: :: ORDINAL1:19

for b₁, b₂ being Ordinal
for b₃ being epsilon-transitive set st b₃ in b₁ & b₁ in b₂ holds
b₃ in b₂

proof end;

theorem Th20: :: ORDINAL1:20

canceled;

theorem Th21: :: ORDINAL1:21

for b₁ being epsilon-transitive set
for b₂ being Ordinal st b₁ c< b₂ holds
b₁ in b₂

proof end;

theorem Th22: :: ORDINAL1:22

for b₁ being epsilon-transitive set
for b₂, b₃ being Ordinal st b₁ c= b₂ & b₂ in b₃ holds
b₁ in b₃

proof end;

theorem Th23: :: ORDINAL1:23

for b₁ being set
for b₂ being Ordinal st b₁ in b₂ holds
b₁ is Ordinal

proof end;

theorem Th24: :: ORDINAL1:24

for b₁, b₂ being Ordinal holds
( b₁ in b₂ or b₁ = b₂ or b₂ in b₁ )

proof end;

definition

let c₁, c₂ be Ordinal;
redefine pred c= as c₁ c= c₂;
connectedness

proof end;

end;

theorem Th25: :: ORDINAL1:25

for b₁, b₂ being Ordinal holds b₁,b₂ are_c=-comparable

proof end;

theorem Th26: :: ORDINAL1:26

for b₁, b₂ being Ordinal holds
( b₁ c= b₂ or b₂ in b₁ )

proof end;

theorem Th27: :: ORDINAL1:27

{} is Ordinal by Def4, Lemma7;

registration

cluster empty number ;
existence by Th27;

end;

registration

cluster empty -> epsilon-transitive epsilon-connected ordinal number ;
coherence by Def4, Lemma7;

end;

registration

cluster {} -> epsilon-transitive epsilon-connected ordinal ;
coherence ;

end;

theorem Th28: :: ORDINAL1:28

canceled;

theorem Th29: :: ORDINAL1:29

for b₁ being set st b₁ is Ordinal holds
succ b₁ is Ordinal

proof end;

theorem Th30: :: ORDINAL1:30

for b₁ being set st b₁ is ordinal holds
union b₁ is ordinal

proof end;

registration

cluster non empty number ;
existence

proof end;

end;

registration

let c₁ be Ordinal;
cluster succ a₁ -> non empty epsilon-transitive epsilon-connected ordinal ;
coherence by Th29;
cluster union a₁ -> epsilon-transitive epsilon-connected ordinal ;
coherence by Th30;

end;

theorem Th31: :: ORDINAL1:31

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
( b₂ is Ordinal & b₂ c= b₁ ) ) holds
b₁ is ordinal

proof end;

theorem Th32: :: ORDINAL1:32

for b₁ being set
for b₂ being Ordinal st b₁ c= b₂ & b₁ <> {} holds
ex b₃ being Ordinal st
( b₃ in b₁ & ( for b₄ being Ordinal st b₄ in b₁ holds
b₃ c= b₄ ) )

proof end;

theorem Th33: :: ORDINAL1:33

for b₁, b₂ being Ordinal holds
( b₁ in b₂ iff succ b₁ c= b₂ )

proof end;

theorem Th34: :: ORDINAL1:34

for b₁, b₂ being Ordinal holds
( b₁ in succ b₂ iff b₁ c= b₂ )

proof end;

scheme :: ORDINAL1:sch 1
s1{ P₁[ Ordinal] } :

ex b₁ being Ordinal st
( P₁[b₁] & ( for b₂ being Ordinal st P₁[b₂] holds
b₁ c= b₂ ) )

provided

E20: ex b₁ being Ordinal st P₁[b₁]

proof end;

scheme :: ORDINAL1:sch 2
s2{ P₁[ Ordinal] } :

for b₁ being Ordinal holds P₁[b₁]

provided

E20: for b₁ being Ordinal st ( for b₂ being Ordinal st b₂ in b₁ holds
P₁[b₂] ) holds
P₁[b₁]

proof end;

theorem Th35: :: ORDINAL1:35

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is Ordinal ) holds
union b₁ is ordinal

proof end;

theorem Th36: :: ORDINAL1:36

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is Ordinal ) holds
ex b₂ being Ordinal st b₁ c= b₂

proof end;

theorem Th37: :: ORDINAL1:37

for b₁ being set holds
not for b₂ being set holds
( b₂ in b₁ iff b₂ is Ordinal )

proof end;

theorem Th38: :: ORDINAL1:38

for b₁ being set holds
not for b₂ being Ordinal holds b₂ in b₁

proof end;

theorem Th39: :: ORDINAL1:39

for b₁ being set ex b₂ being Ordinal st
( not b₂ in b₁ & ( for b₃ being Ordinal st not b₃ in b₁ holds
b₂ c= b₃ ) )

proof end;

definition

let c₁ be set ;
canceled;
attr a₁ is being_limit_ordinal means :Def6: :: ORDINAL1:def 6
a₁ = union a₁;

end;

:: deftheorem Def5 ORDINAL1:def 5 :

:: deftheorem Def6 defines being_limit_ordinal ORDINAL1:def 6 :

notation

let c₁ be set ;
synonym c₁ is_limit_ordinal for being_limit_ordinal c₁;

end;

theorem Th40: :: ORDINAL1:40

canceled;

theorem Th41: :: ORDINAL1:41

for b₁ being Ordinal holds
( b₁ is_limit_ordinal iff for b₂ being Ordinal st b₂ in b₁ holds
succ b₂ in b₁ )

proof end;

theorem Th42: :: ORDINAL1:42

for b₁ being Ordinal holds
( not b₁ is_limit_ordinal iff ex b₂ being Ordinal st b₁ = succ b₂ )

proof end;

definition

let c₁ be Function;
attr a₁ is T-Sequence-like means :Def7: :: ORDINAL1:def 7
dom a₁ is ordinal;

end;

:: deftheorem Def7 defines T-Sequence-like ORDINAL1:def 7 :

registration

cluster T-Sequence-like number ;
existence

proof end;

end;

definition

mode T-Sequence is T-Sequence-like Function;

end;

definition

let c₁ be set ;
mode T-Sequence of c₁ -> T-Sequence means :Def8: :: ORDINAL1:def 8
rng a₂ c= a₁;
existence

proof end;

end;

:: deftheorem Def8 defines T-Sequence ORDINAL1:def 8 :

theorem Th43: :: ORDINAL1:43

canceled;

theorem Th44: :: ORDINAL1:44

canceled;

theorem Th45: :: ORDINAL1:45

for b₁ being set holds {} is T-Sequence of b₁

proof end;

theorem Th46: :: ORDINAL1:46

for b₁ being Function st dom b₁ is Ordinal holds
b₁ is T-Sequence of rng b₁

proof end;

registration

let c₁ be T-Sequence;
cluster dom a₁ -> epsilon-transitive epsilon-connected ordinal ;
coherence by Def7;

end;

theorem Th47: :: ORDINAL1:47

for b₁, b₂ being set st b₁ c= b₂ holds
for b₃ being T-Sequence of b₁ holds b₃ is T-Sequence of b₂

proof end;

definition

let c₁ be T-Sequence;
let c₂ be Ordinal;
redefine func | as c₁ | c₂ -> T-Sequence of rng a₁;
coherence

proof end;

end;

theorem Th48: :: ORDINAL1:48

for b₁ being set
for b₂ being T-Sequence of b₁
for b₃ being Ordinal holds b₂ | b₃ is T-Sequence of b₁

proof end;

definition

let c₁ be set ;
attr a₁ is c=-linear means :Def9: :: ORDINAL1:def 9
for b₁, b₂ being set st b₁ in a₁ & b₂ in a₁ holds
b₁,b₂ are_c=-comparable ;

end;

:: deftheorem Def9 defines c=-linear ORDINAL1:def 9 :

theorem Th49: :: ORDINAL1:49

for b₁ being set st ( for b₂ being set st b₂ in b₁ holds
b₂ is T-Sequence ) & b₁ is c=-linear holds
union b₁ is T-Sequence

proof end;

scheme :: ORDINAL1:sch 3
s3{ F₁() -> Ordinal, F₂( T-Sequence) -> set , F₃() -> T-Sequence, F₄() -> T-Sequence } :

F₃() = F₄()

provided

E30: ( dom F₃() = F₁() & ( for b₁ being Ordinal
for b₂ being T-Sequence st b₁ in F₁() & b₂ = F₃() | b₁ holds
F₃() . b₁ = F₂(b₂) ) ) and
E31: ( dom F₄() = F₁() & ( for b₁ being Ordinal
for b₂ being T-Sequence st b₁ in F₁() & b₂ = F₄() | b₁ holds
F₄() . b₁ = F₂(b₂) ) )

proof end;

scheme :: ORDINAL1:sch 4
s4{ F₁() -> Ordinal, F₂( T-Sequence) -> set } :

ex b₁ being T-Sequence st
( dom b₁ = F₁() & ( for b₂ being Ordinal
for b₃ being T-Sequence st b₂ in F₁() & b₃ = b₁ | b₂ holds
b₁ . b₂ = F₂(b₃) ) )

proof end;

scheme :: ORDINAL1:sch 5
s5{ F₁() -> T-Sequence, F₂( Ordinal) -> set , F₃( T-Sequence) -> set } :

for b₁ being Ordinal st b₁ in dom F₁() holds
F₁() . b₁ = F₃((F₁() | b₁))

provided

E30: for b₁ being Ordinal
for b₂ being set holds
( b₂ = F₂(b₁) iff ex b₃ being T-Sequence st
( b₂ = F₃(b₃) & dom b₃ = b₁ & ( for b₄ being Ordinal st b₄ in b₁ holds
b₃ . b₄ = F₃((b₃ | b₄)) ) ) ) and
E31: for b₁ being Ordinal st b₁ in dom F₁() holds
F₁() . b₁ = F₂(b₁)

proof end;

theorem Th50: :: ORDINAL1:50

for b₁, b₂ being Ordinal holds
( b₁ c< b₂ or b₁ = b₂ or b₂ c< b₁ )

proof end;