:: by Grzegorz Bancerek

::

:: Received March 20, 1989

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

::$CT 4

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 )

;

::

:: 4. Definition of ordinal numbers - Ordinal

::

:: 4. Definition of ordinal numbers - Ordinal

::

registration

existence

ex b_{1} being set st

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

end;
ex b

( b

:: deftheorem defines ordinal ORDINAL1:def 4 :

for IT being object holds

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

for IT being object holds

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

registration

coherence

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

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

coherence

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

b_{1} is ordinal
;

end;
for b

( b

coherence

for b

b

registration
end;

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

theorem Th14: :: ORDINAL1:18

for x being set st x is ordinal holds

( union x is epsilon-transitive & union x is epsilon-connected )

( union x is epsilon-transitive & union x is epsilon-connected )

proof end;

registration

let A be Ordinal;

coherence

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

coherence

union A is ordinal by Th14;

end;
coherence

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

coherence

union A is ordinal by Th14;

theorem Th15: :: ORDINAL1:19

for X being set st ( for x being set st x in X holds

( x is Ordinal & x c= X ) ) holds

( X is epsilon-transitive & X is epsilon-connected )

( x is Ordinal & x c= X ) ) holds

( X is epsilon-transitive & X is epsilon-connected )

proof end;

theorem Th16: :: 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;

::

:: 7. Properties of sets of ordinals

::

:: 7. Properties of sets of ordinals

::

theorem Th19: :: ORDINAL1:23

for X being set st ( for a being object st a in X holds

a is Ordinal ) holds

( union X is epsilon-transitive & union X is epsilon-connected )

a is Ordinal ) holds

( union X is epsilon-transitive & union X is epsilon-connected )

proof end;

theorem Th20: :: ORDINAL1:24

for X being set st ( for a being object 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 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 Th24: :: 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

let IT be set ;

end;
attr IT is Sequence-like means :Def7: :: ORDINAL1:def 7

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

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

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

for IT being set holds

( IT is Sequence-like iff ( proj1 IT is epsilon-transitive & proj1 IT is epsilon-connected ) );

for IT being set holds

( IT is Sequence-like iff ( proj1 IT is epsilon-transitive & proj1 IT is epsilon-connected ) );

theorem :: ORDINAL1:31

registration
end;

registration

let L be Sequence;

let A be Ordinal;

coherence

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

end;
let A be Ordinal;

coherence

( L | A is rng L -valued & L | A is 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 object st a in X holds

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

union X is Sequence

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

union X is Sequence

proof end;

scheme :: ORDINAL1:sch 3

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

provided

TSUniq{ F

provided

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

for L being 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 Sequence st B in F_{1}() & L = F_{4}() | B holds

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

for L being Sequence st B in F

F

A2: ( dom F

for L being Sequence st B in F

F

proof end;

scheme :: ORDINAL1:sch 5

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

provided

FuncTS{ F

provided

A1:
for A being Ordinal

for a being object holds

( a = F_{2}(A) iff ex L being 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 object holds

( a = F

( a = F

L . B = F

A2: for A being Ordinal st A in dom F

F

proof end;

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

definition

let X be set ;

ex b_{1} being set st

for x being object holds

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

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

( x in b_{1} iff ( x in X & x is Ordinal ) ) ) & ( for x being object 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 object 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 object holds

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

( x = A & A is limit_ordinal ) ) ) ) & ( for x being object 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 object holds

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

existence for x being object holds

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

ex b

for x being object 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 object holds

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

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

existence for x being object holds

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

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

ex b

for x being object 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 object 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 object 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 object 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

:: 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 object holds

( A is natural iff A in omega );

for A being object holds

( A is natural iff A in omega );

registration

existence

ex b_{1} being Number st b_{1} is natural

ex b_{1} being set st b_{1} is natural

end;
ex b

proof end;

existence ex b

proof end;

:: from ARYTM_3, 2006.05.26

registration
end;

:: missing, 2006.06.25, 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
by Def11;

coherence

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

end;
for b

b

coherence

for b

registration
end;

:: from ARYTM_3, 2007.10.23, A.T.

registration
end;

:: from DILWORTH, 2011.07.31,A.T.

registration
end;

::$CT

:: deftheorem Def14 defines zero ORDINAL1:def 14 :

for x being Number holds

( x is zero iff x = 0 );

for x being Number holds

( x is zero iff x = 0 );

registration

coherence

0 is zero ;

existence

ex b_{1} being Number st b_{1} is zero

ex b_{1} being set st b_{1} is zero

end;
0 is zero ;

existence

ex b

proof end;

existence ex b

proof end;

registration
end;

registration

coherence

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

b_{1} is trivial
;

coherence

for b_{1} being set st not b_{1} is trivial holds

not b_{1} is zero
;

end;
for b

b

coherence

for b

not b

definition
end;

:: deftheorem Def15 defines non-zero ORDINAL1:def 15 :

for R being Relation holds

( R is non-zero iff not 0 in rng R );

for R being Relation holds

( R is non-zero iff not 0 in rng R );

:: deftheorem Def16 defines with_zero ORDINAL1:def 16 :

for X being set holds

( X is with_zero iff 0 in X );

for X being set holds

( X is with_zero iff 0 in X );

registration
end;

registration

let X be non empty without_zero set ;

coherence

for b_{1} being Element of X holds not b_{1} is zero
by Def16;

end;
coherence

for b

registration

existence

ex b_{1} being Relation st b_{1} is non-zero

not for b_{1} being Relation holds b_{1} is non-zero

end;
ex b

proof end;

existence not for b

proof end;

registration
end;

:: to be removed

registration

coherence

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

b_{1} is with_non-empty_elements

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

not b_{1} is with_non-empty_elements

for b_{1} being set st b_{1} is with_non-empty_elements holds

b_{1} is without_zero
;

coherence

for b_{1} being set st not b_{1} is with_non-empty_elements holds

b_{1} is with_zero
;

end;
for b

b

proof end;

coherence for b

not b

proof end;

coherence for b

b

coherence

for b

b

definition
end;

registration
end;