:: by Grzegorz Bancerek

::

:: Received March 20, 1989

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

begin

definition
end;

definition

let X be set ;

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

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

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

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 ;

end;
attr IT is ordinal means :Def4: :: ORDINAL1:def 4

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

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

for IT being set holds

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

registration

coherence

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

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

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

( b

coherence

for b

b

registration
end;

definition

let A, B be Ordinal;

( 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 redefine pred A c= B means :: ORDINAL1:def 5

for C being Ordinal st C in A holds

C in B;

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

for A, B being Ordinal holds

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

C in B );

registration

let A be Ordinal;

coherence

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

coherence

union A is ordinal by Th18;

end;
coherence

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

coherence

union A is ordinal by Th18;

theorem Th20: :: ORDINAL1:20

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;

::

:: 6. Transfinite induction and principle of minimum of ordinals

::

:: 6. Transfinite induction and principle of minimum of ordinals

::

::

:: 7. Properties of sets of ordinals

::

:: 7. Properties of sets of ordinals

::

theorem Th24: :: ORDINAL1:24

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 :: ORDINAL1:27

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;

::

:: 8. Limit ordinals

::

:: 8. Limit ordinals

::

:: deftheorem Def6 defines limit_ordinal ORDINAL1:def 6 :

for A being set holds

( A is limit_ordinal iff A = union A );

for A being set holds

( A is limit_ordinal iff A = union A );

theorem Th28: :: ORDINAL1:28

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;

::

:: 9. Transfinite sequences

::

:: 9. Transfinite sequences

::

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

for IT being set holds

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

registration
end;

registration
end;

theorem :: ORDINAL1:31

registration
end;

registration

let L be T-Sequence;

let A be Ordinal;

coherence

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

end;
let A be Ordinal;

coherence

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

proof end;

theorem :: ORDINAL1:33

definition

let IT be set ;

end;
attr IT is c=-linear means :Def8: :: ORDINAL1:def 8

for x, y being set st x in IT & y in IT holds

x,y are_c=-comparable ;

for x, y being set st x in IT & y in IT holds

x,y are_c=-comparable ;

:: deftheorem Def8 defines c=-linear ORDINAL1:def 8 :

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

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:34

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;

::

:: 10. Schemes of definability by transfinite induction

::

:: 10. Schemes of definability by transfinite induction

::

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;

begin

:: moved from ORDINAL2, 2006.06.22, A.T.

definition

let X be set ;

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}

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 :Def9: :: ORDINAL1:def 9

for x being set holds

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

existence for x being set holds

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

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 10

for x being set holds

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

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

existence for x being set holds

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

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

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 Def9 defines On ORDINAL1:def 9 :

for X, b_{2} being set holds

( b_{2} = On X iff for x being set holds

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

for X, b

( b

( x in b

:: deftheorem defines Lim ORDINAL1:def 10 :

for X, b_{2} being set holds

( b_{2} = Lim X iff for x being set holds

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

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

for X, b

( b

( x in b

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

definition

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;

func omega -> set means :Def11: :: ORDINAL1:def 11

( {} 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 ( {} in it & it is limit_ordinal & it is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds

it c= A ) );

ex b

( {} in b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def11 defines omega ORDINAL1:def 11 :

for b_{1} being set holds

( b_{1} = omega iff ( {} 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

( b

b

registration
end;

:: deftheorem Def12 defines natural ORDINAL1:def 12 :

for A being set holds

( A is natural iff A in omega );

for A being set holds

( A is natural iff A in omega );

registration
end;

registration

natural number
ex b_{1} being number st

for b_{2} being natural number holds b_{2} in b_{1}

end;
for b

proof end;

:: from ARYTM_3, 2006.05.26

registration
end;

:: missing, 2006.06.25, A.T.

registration
end;

:: from ZF_REFLE, 2007,03.13, A.T.

:: from CARD_4, 2007.08.06, A.T.

:: from ARYTM_3, 2007.09.16, A.T.

registration

coherence

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

b_{1} is natural

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

end;
for b

b

proof end;

coherence for b

registration
end;

:: from ARYTM_3, 2007.10.23, A.T.

registration
end;

:: from DILWORTH, 2011.07.31,A.T.

registration
end;

registration
end;

:: 4. Definition of ordinal numbers - Ordinal

::