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

end;

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

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

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

proof end;

definition

let IT be set ;
attr IT is ordinal means :Def4: :: ORDINAL1:def 4
( IT is epsilon-transitive & IT 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 :: ORDINAL1:15

canceled;

theorem :: ORDINAL1:16

canceled;

theorem :: ORDINAL1:17

canceled;

theorem :: ORDINAL1:18

canceled;

theorem Th19: :: ORDINAL1:19

for B, C being Ordinal
for A being epsilon-transitive set st A in B & B in C holds
A in C

proof end;

theorem :: ORDINAL1:20

canceled;

theorem Th21: :: ORDINAL1:21

for x being epsilon-transitive set
for A being Ordinal st x c< A holds
x in A

proof end;

theorem :: ORDINAL1:22

for A being epsilon-transitive set
for B, C being Ordinal st A c= B & B in C holds
A in C

proof end;

theorem Th23: :: ORDINAL1:23

for a being set
for A being Ordinal st a in A holds
a is Ordinal

proof end;

theorem Th24: :: ORDINAL1:24

for A, B being Ordinal holds
( A in B or A = B or B in A )

proof end;

definition

let A, B be Ordinal;
:: original: c=
redefine pred A c= B;
connectedness

proof end;

end;

theorem :: ORDINAL1:25

for A, B being Ordinal holds A,B are_c=-comparable

proof end;

theorem Th26: :: ORDINAL1:26

for A, B being Ordinal holds
( A c= B or B in A )

proof end;

theorem Th27: :: ORDINAL1:27

{} is Ordinal by Def4, Lm1;

registration

cluster empty number ;
existence by Th27;

end;

registration

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

end;

registration

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

end;

theorem :: ORDINAL1:28

canceled;

theorem Th29: :: ORDINAL1:29

for x being set st x is Ordinal holds
succ x is Ordinal

proof end;

theorem Th30: :: ORDINAL1:30

for x being set st x is ordinal holds
union x is ordinal

proof end;

registration

cluster non empty number ;
existence

proof end;

end;

registration

let A 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 :: ORDINAL1:31

for X being set st ( for x being set st x in X holds
( x is Ordinal & x c= X ) ) holds
X is ordinal

proof end;

theorem Th32: :: ORDINAL1:32

for X being set
for A being Ordinal st X c= A & X <> {} holds
ex C being Ordinal st
( C in X & ( for B being Ordinal st B in X holds
C c= B ) )

proof end;

theorem Th33: :: ORDINAL1:33

for A, B being Ordinal holds
( A in B iff succ A c= B )

proof end;

theorem Th34: :: ORDINAL1:34

for A, C being Ordinal holds
( A in succ C iff A c= C )

proof end;

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

ex A being Ordinal st
( P₁[A] & ( for B being Ordinal st P₁[B] holds
A c= B ) )

provided

A1: ex A being Ordinal st P₁[A]

proof end;

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

for A being Ordinal holds P₁[A]

provided

A1: for A being Ordinal st ( for C being Ordinal st C in A holds
P₁[C] ) holds
P₁[A]

proof end;

theorem Th35: :: ORDINAL1:35

for X being set st ( for a being set st a in X holds
a is Ordinal ) holds
union X is ordinal

proof end;

theorem Th36: :: ORDINAL1:36

for X being set st ( for a being set st a in X holds
a is Ordinal ) holds
ex A being Ordinal st X c= A

proof end;

theorem Th37: :: ORDINAL1:37

for X being set holds
not for x being set holds
( x in X iff x is Ordinal )

proof end;

theorem Th38: :: ORDINAL1:38

for X being set holds
not for A being Ordinal holds A in X

proof end;

theorem :: ORDINAL1:39

for X being set ex A being Ordinal st
( not A in X & ( for B being Ordinal st not B in X holds
A c= B ) )

proof end;

definition

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

end;

:: deftheorem ORDINAL1:def 5 :

:: deftheorem Def6 defines being_limit_ordinal ORDINAL1:def 6 :

notation

let A be set ;
synonym A is_limit_ordinal for being_limit_ordinal A;

end;

theorem :: ORDINAL1:40

canceled;

theorem Th41: :: ORDINAL1:41

for A being Ordinal holds
( A is_limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )

proof end;

theorem :: ORDINAL1:42

for A being Ordinal holds
( not A is_limit_ordinal iff ex B being Ordinal st A = succ B )

proof end;

definition

let IT be Function;
attr IT is T-Sequence-like means :Def7: :: ORDINAL1:def 7
dom IT 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 Z be set ;
mode T-Sequence of Z -> T-Sequence means :Def8: :: ORDINAL1:def 8
rng it c= Z;
existence

proof end;

end;

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

theorem :: ORDINAL1:43

canceled;

theorem :: ORDINAL1:44

canceled;

theorem :: ORDINAL1:45

for Z being set holds {} is T-Sequence of Z

proof end;

theorem :: ORDINAL1:46

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

proof end;

registration

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

end;

theorem Th47: :: ORDINAL1:47

for X, Y being set st X c= Y holds
for L being T-Sequence of X holds L is T-Sequence of Y

proof end;

definition

let L be T-Sequence;
let A be Ordinal;
:: original: |
redefine func L | A -> T-Sequence of rng L;
coherence

proof end;

end;

theorem :: ORDINAL1:48

for X being set
for L being T-Sequence of X
for A being Ordinal holds L | A is T-Sequence of X

proof end;

definition

let IT be set ;
attr IT is c=-linear means :Def9: :: ORDINAL1:def 9
for x, y being set st x in IT & y in IT holds
x,y are_c=-comparable ;

end;

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

theorem :: ORDINAL1:49

for X being set st ( for a being set st a in X holds
a is T-Sequence ) & X is c=-linear holds
union X is T-Sequence

proof end;

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

F₃() = F₄()

provided

A1: ( dom F₃() = F₁() & ( for B being Ordinal
for L being T-Sequence st B in F₁() & L = F₃() | B holds
F₃() . B = F₂(L) ) ) and
A2: ( dom F₄() = F₁() & ( for B being Ordinal
for L being T-Sequence st B in F₁() & L = F₄() | B holds
F₄() . B = F₂(L) ) )

proof end;

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

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

proof end;

scheme :: ORDINAL1:sch 5
FuncTS{ 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

A1: for A being Ordinal
for a being set holds
( a = F₂(A) iff ex L being T-Sequence st
( a = F₃(L) & dom L = A & ( for B being Ordinal st B in A holds
L . B = F₃((L | B)) ) ) ) and
A2: for A being Ordinal st A in dom F₁() holds
F₁() . A = F₂(A)

proof end;

theorem :: ORDINAL1:50

for A, B being Ordinal holds
( A c< B or A = B or B c< A )

proof end;