:: by Grzegorz Bancerek

::

:: Received March 20, 1989

:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem :: ORDINAL1:1

canceled;

theorem :: ORDINAL1:2

canceled;

theorem Th3: :: ORDINAL1:3

proof end;

theorem :: ORDINAL1:4

proof end;

theorem :: ORDINAL1:5

for X1, X2, X3, X4, X5 being set holds

( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X1 )

( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X1 )

proof end;

theorem :: ORDINAL1:6

for X1, X2, X3, X4, X5, X6 being set holds

( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X6 or not X6 in X1 )

( not X1 in X2 or not X2 in X3 or not X3 in X4 or not X4 in X5 or not X5 in X6 or not X6 in X1 )

proof end;

theorem Th7: :: ORDINAL1:7

proof end;

definition
end;

:: deftheorem defines succ ORDINAL1:def 1 :

for X being set holds succ X = X \/ {X};

theorem :: ORDINAL1:8

canceled;

theorem :: ORDINAL1:9

canceled;

theorem Th10: :: ORDINAL1:10

proof end;

theorem :: ORDINAL1:11

canceled;

theorem :: ORDINAL1:12

proof end;

theorem Th13: :: ORDINAL1:13

proof end;

theorem Th14: :: ORDINAL1:14

proof end;

definition

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;
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;

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

for X being set holds

( X is epsilon-transitive iff for x being set st x in X holds

x c= X );

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

for X being set holds

( X is epsilon-connected iff for x, y being set st x in X & y in X & not x in y & not x = y holds

y in x );

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;
attr IT is ordinal means :Def4: :: ORDINAL1:def 4

( IT is epsilon-transitive & IT is epsilon-connected );

:: deftheorem Def4 defines ordinal ORDINAL1:def 4 :

for IT being set holds

( IT is ordinal iff ( IT is epsilon-transitive & IT is epsilon-connected ) );

registration

cluster ordinal -> epsilon-transitive epsilon-connected number ;

coherence

for b_{1} being set st b_{1} is ordinal holds

( b_{1} is epsilon-transitive & b_{1} is epsilon-connected )
by Def4;

cluster epsilon-transitive epsilon-connected -> ordinal number ;

coherence

for b_{1} being set st b_{1} is epsilon-transitive & b_{1} is epsilon-connected holds

b_{1} is ordinal
by Def4;

end;
coherence

for b

( b

cluster epsilon-transitive epsilon-connected -> ordinal number ;

coherence

for b

b

registration
end;

theorem :: ORDINAL1:15

canceled;

theorem :: ORDINAL1:16

canceled;

theorem :: ORDINAL1:17

canceled;

theorem :: ORDINAL1:18

canceled;

theorem Th19: :: ORDINAL1:19

proof end;

theorem :: ORDINAL1:20

canceled;

theorem Th21: :: ORDINAL1:21

proof end;

theorem :: ORDINAL1:22

proof end;

theorem Th23: :: ORDINAL1:23

proof end;

theorem Th24: :: ORDINAL1:24

proof end;

definition

let A, B be Ordinal;

:: original: c=

redefine pred A c= B means :: ORDINAL1:def 5

for C being Ordinal st C in A holds

C in B;

compatibility

( A c= B iff for C being Ordinal st C in A holds

C in B )

for A, B being Ordinal st ex C being Ordinal st

( C in A & not C in B ) holds

for C being Ordinal st C in B holds

C in A

end;
:: original: c=

redefine pred A c= B means :: ORDINAL1:def 5

for C being Ordinal st C in A holds

C in B;

compatibility

( A c= B iff for C being Ordinal st C in A holds

C in B )

proof end;

connectedness for A, B being Ordinal st ex C being Ordinal st

( C in A & not C in B ) holds

for C being Ordinal st C in B holds

C in A

proof end;

:: deftheorem defines c= ORDINAL1:def 5 :

for A, B being Ordinal holds

( A c= B iff for C being Ordinal st C in A holds

C in B );

theorem :: ORDINAL1:25

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

proof end;

theorem Th26: :: ORDINAL1:26

proof end;

registration

cluster empty -> ordinal number ;

coherence

for b_{1} being number st b_{1} is empty holds

b_{1} is ordinal
by Lm1;

end;
coherence

for b

b

theorem :: ORDINAL1:27

canceled;

theorem :: ORDINAL1:28

canceled;

theorem Th29: :: ORDINAL1:29

proof end;

theorem Th30: :: ORDINAL1:30

proof end;

registration

cluster non empty epsilon-transitive epsilon-connected ordinal number ;

existence

not for b_{1} being Ordinal holds b_{1} is empty

end;
existence

not for b

proof end;

registration

let A be Ordinal;

cluster succ A -> non empty ordinal ;

coherence

( not succ A is empty & succ A is ordinal ) by Th29;

cluster union A -> ordinal ;

coherence

union A is ordinal by Th30;

end;
cluster succ A -> non empty ordinal ;

coherence

( not succ A is empty & succ A is ordinal ) by Th29;

cluster union A -> ordinal ;

coherence

union A is ordinal by Th30;

theorem Th31: :: ORDINAL1:31

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 ) )

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

proof end;

theorem Th34: :: ORDINAL1:34

proof end;

theorem Th35: :: ORDINAL1:35

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

a is Ordinal ) holds

ex A being Ordinal st X c= A

proof end;

theorem Th37: :: ORDINAL1:37

proof end;

theorem Th38: :: ORDINAL1:38

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 ) )

( not A in X & ( for B being Ordinal st not B in X holds

A c= B ) )

proof end;

:: deftheorem Def6 defines limit_ordinal ORDINAL1:def 6 :

for A being set holds

( A is limit_ordinal iff A = union A );

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 )

( A is limit_ordinal iff for C being Ordinal st C in A holds

succ C in A )

proof end;

theorem :: ORDINAL1:42

proof end;

definition
end;

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

for IT being set holds

( IT is T-Sequence-like iff proj1 IT is ordinal );

registration

cluster empty -> T-Sequence-like number ;

coherence

for b_{1} being set st b_{1} is empty holds

b_{1} is T-Sequence-like

end;
coherence

for b

b

proof end;

registration

let Z be set ;

cluster Relation-like Z -valued Function-like T-Sequence-like number ;

existence

ex b_{1} being T-Sequence st b_{1} is Z -valued

end;
cluster Relation-like Z -valued Function-like T-Sequence-like number ;

existence

ex b

proof end;

theorem :: ORDINAL1:43

canceled;

theorem :: ORDINAL1:44

canceled;

theorem :: ORDINAL1:45

proof end;

theorem :: ORDINAL1:46

registration
end;

theorem :: ORDINAL1:47

proof end;

registration

let L be T-Sequence;

let A be Ordinal;

cluster L | A -> rng L -valued T-Sequence-like ;

coherence

( L | A is rng L -valued & L | A is T-Sequence-like )

end;
let A be Ordinal;

cluster L | A -> rng L -valued T-Sequence-like ;

coherence

( L | A is rng L -valued & L | A is T-Sequence-like )

proof end;

theorem :: ORDINAL1:48

definition

canceled;

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;
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 ;

:: deftheorem ORDINAL1:def 8 :

canceled;

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

for IT being set holds

( IT is c=-linear iff for x, y being set st x in IT & y in IT holds

x,y are_c=-comparable );

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

a is T-Sequence ) & X is c=-linear holds

union X is T-Sequence

proof end;

scheme :: ORDINAL1:sch 3

TSUniq{ F_{1}() -> Ordinal, F_{2}( T-Sequence) -> set , F_{3}() -> T-Sequence, F_{4}() -> T-Sequence } :

provided

TSUniq{ F

provided

A1:
( dom F_{3}() = F_{1}() & ( for B being Ordinal

for L being T-Sequence st B in F_{1}() & L = F_{3}() | B holds

F_{3}() . B = F_{2}(L) ) )
and

A2: ( dom F_{4}() = F_{1}() & ( for B being Ordinal

for L being T-Sequence st B in F_{1}() & L = F_{4}() | B holds

F_{4}() . B = F_{2}(L) ) )

for L being T-Sequence st B in F

F

A2: ( dom F

for L being T-Sequence st B in F

F

proof end;

scheme :: ORDINAL1:sch 4

TSExist{ F_{1}() -> Ordinal, F_{2}( T-Sequence) -> set } :

TSExist{ F

ex L being T-Sequence st

( dom L = F_{1}() & ( for B being Ordinal

for L1 being T-Sequence st B in F_{1}() & L1 = L | B holds

L . B = F_{2}(L1) ) )

( dom L = F

for L1 being T-Sequence st B in F

L . B = F

proof end;

scheme :: ORDINAL1:sch 5

FuncTS{ F_{1}() -> T-Sequence, F_{2}( Ordinal) -> set , F_{3}( T-Sequence) -> set } :

provided

FuncTS{ F

provided

A1:
for A being Ordinal

for a being set holds

( a = F_{2}(A) iff ex L being T-Sequence st

( a = F_{3}(L) & dom L = A & ( for B being Ordinal st B in A holds

L . B = F_{3}((L | B)) ) ) )
and

A2: for A being Ordinal st A in dom F_{1}() holds

F_{1}() . A = F_{2}(A)

for a being set holds

( a = F

( a = F

L . B = F

A2: for A being Ordinal st A in dom F

F

proof end;

theorem :: ORDINAL1:50

proof end;

begin

definition

let X be set ;

func On X -> set means :Def10: :: ORDINAL1:def 10

for x being set holds

( x in it iff ( x in X & x is Ordinal ) );

existence

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X & x is Ordinal ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X & x is Ordinal ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & x is Ordinal ) ) ) holds

b_{1} = b_{2}

for x being set holds

( x in it iff ( x in X & ex A being Ordinal st

( x = A & A is limit_ordinal ) ) );

existence

ex b_{1} being set st

for x being set holds

( x in b_{1} iff ( x in X & ex A being Ordinal st

( x = A & A is limit_ordinal ) ) )

for b_{1}, b_{2} being set st ( for x being set holds

( x in b_{1} iff ( x in X & ex A being Ordinal st

( x = A & A is limit_ordinal ) ) ) ) & ( for x being set holds

( x in b_{2} iff ( x in X & ex A being Ordinal st

( x = A & A is limit_ordinal ) ) ) ) holds

b_{1} = b_{2}

end;
func On X -> set means :Def10: :: ORDINAL1:def 10

for x being set holds

( x in it iff ( x in X & x is Ordinal ) );

existence

ex b

for x being set holds

( x in b

proof end;

uniqueness for b

( x in b

( x in b

b

proof end;

func Lim X -> set means :: ORDINAL1:def 11for x being set holds

( x in it iff ( x in X & ex A being Ordinal st

( x = A & A is limit_ordinal ) ) );

existence

ex b

for x being set holds

( x in b

( x = A & A is limit_ordinal ) ) )

proof end;

uniqueness for b

( x in b

( x = A & A is limit_ordinal ) ) ) ) & ( for x being set holds

( x in b

( x = A & A is limit_ordinal ) ) ) ) holds

b

proof end;

:: deftheorem Def10 defines On ORDINAL1:def 10 :

for X, b

( b

( x in b

:: deftheorem defines Lim ORDINAL1:def 11 :

for X, b

( b

( x in b

( x = A & A is limit_ordinal ) ) ) );

theorem Th51: :: ORDINAL1:51

proof end;

definition

func omega -> set means :Def12: :: ORDINAL1:def 12

( {} in it & it is limit_ordinal & it is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds

it c= A ) );

existence

ex b_{1} being set st

( {} in b_{1} & b_{1} is limit_ordinal & b_{1} is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds

b_{1} c= A ) )

for b_{1}, b_{2} being set st {} in b_{1} & b_{1} is limit_ordinal & b_{1} is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds

b_{1} c= A ) & {} in b_{2} & b_{2} is limit_ordinal & b_{2} is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds

b_{2} c= A ) holds

b_{1} = b_{2}

end;
( {} in it & it is limit_ordinal & it is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds

it c= A ) );

existence

ex b

( {} in b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines omega ORDINAL1:def 12 :

for b

( b

b

registration
end;

:: deftheorem Def13 defines natural ORDINAL1:def 13 :

for A being set holds

( A is natural iff A in omega );

registration
end;

registration

let A be Ordinal;

cluster -> ordinal Element of A;

coherence

for b_{1} being Element of A holds b_{1} is ordinal

end;
cluster -> ordinal Element of A;

coherence

for b

proof end;

registration

cluster natural -> ordinal number ;

coherence

for b_{1} being number st b_{1} is natural holds

b_{1} is ordinal

end;
coherence

for b

b

proof end;

scheme :: ORDINAL1:sch 6

ALFA{ F_{1}() -> non empty set , P_{1}[ set , set ] } :

ALFA{ F

ex F being Function st

( dom F = F_{1}() & ( for d being Element of F_{1}() ex A being Ordinal st

( A = F . d & P_{1}[d,A] & ( for B being Ordinal st P_{1}[d,B] holds

A c= B ) ) ) )

provided
( dom F = F

( A = F . d & P

A c= B ) ) ) )

proof end;

theorem :: ORDINAL1:52

proof end;

registration

cluster empty -> natural number ;

coherence

for b_{1} being number st b_{1} is empty holds

b_{1} is natural

coherence

for b_{1} being Element of omega holds b_{1} is natural
by Def13;

end;
coherence

for b

b

proof end;

cluster -> natural Element of omega ;coherence

for b

registration

cluster non empty natural number ;

existence

ex b_{1} being number st

( not b_{1} is empty & b_{1} is natural )

end;
existence

ex b

( not b

proof end;

registration
end;