Loading [MathJax]/extensions/tex2jax.js

:: The Ordinal Numbers. Transfinite Induction and Defining by Transfinite Induction
:: by Grzegorz Bancerek
::
:: Received March 20, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem :: ORDINAL1:1

canceled;

theorem :: ORDINAL1:2

canceled;

theorem :: ORDINAL1:3

canceled;

theorem :: ORDINAL1:4

canceled;

::$CT 4

theorem Th1: :: ORDINAL1:5

for X, Y being set st Y in X holds
not X c= Y

proof end;

definition

let X be set ;

func succ X -> set equals :: ORDINAL1:def 1
X \/ {X};

coherence
X \/ {X} is set ;

end;

:: deftheorem defines succ ORDINAL1:def 1 :
for X being set holds succ X = X \/ {X};

registration

let X be set ;

cluster succ X -> non empty ;

coherence
not succ X is empty ;

end;

theorem Th2: :: ORDINAL1:6

for X being set holds X in succ X

proof end;

theorem :: ORDINAL1:7

for X, Y being set st succ X = succ Y holds
X = Y

proof end;

theorem Th4: :: ORDINAL1:8

for X being set
for x being object holds
( x in succ X iff ( x in X or x = X ) )

proof end;

theorem Th5: :: ORDINAL1:9

for X being set holds X <> succ X

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;

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

::
:: 4. Definition of ordinal numbers - Ordinal
::

registration

cluster epsilon-transitive epsilon-connected for number ;

existence
ex b₁ being set st
( b₁ is epsilon-transitive & b₁ is epsilon-connected ) by Lm1;

end;

definition

let IT be object ;

attr IT is ordinal means :: ORDINAL1:def 4
IT is epsilon-transitive epsilon-connected set ;

end;

:: deftheorem defines ordinal ORDINAL1:def 4 :
for IT being object holds
( IT is ordinal iff IT is epsilon-transitive epsilon-connected set );

registration

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

coherence
for b₁ being set st b₁ is ordinal holds
( b₁ is epsilon-transitive & b₁ is epsilon-connected ) ;

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

coherence
for b₁ being set st b₁ is epsilon-transitive & b₁ is epsilon-connected holds
b₁ is ordinal ;

end;

notation

synonym Number for object ;
synonym number for set ;

end;

registration

cluster ordinal for number ;

existence
ex b₁ being number st b₁ is ordinal by Lm1;

end;

registration

cluster ordinal for Number ;

existence
ex b₁ being Number st b₁ is ordinal by Lm1;

end;

definition

mode Ordinal is ordinal number ;

end;

theorem Th6: :: ORDINAL1:10

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

proof end;

theorem Th7: :: ORDINAL1:11

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

proof end;

theorem :: ORDINAL1:12

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 Th9: :: ORDINAL1:13

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

proof end;

theorem Th10: :: ORDINAL1:14

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

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

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

proof end;

theorem Th12: :: ORDINAL1:16

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

proof end;

registration

cluster empty -> ordinal for number ;

coherence
for b₁ being number st b₁ is empty holds
b₁ is ordinal by Lm1;

end;

theorem Th13: :: ORDINAL1:17

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

proof end;

theorem Th14: :: ORDINAL1:18

for x being set st x is ordinal holds
( union x is epsilon-transitive & union x is epsilon-connected )

proof end;

registration

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

existence
not for b₁ being Ordinal holds b₁ is empty

proof end;

end;

registration

let A be Ordinal;

cluster succ A -> non empty ordinal ;

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

cluster union A -> ordinal ;

coherence
union A is ordinal by Th14;

end;

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 )

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

proof end;

theorem Th17: :: ORDINAL1:21

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

proof end;

theorem Th18: :: ORDINAL1:22

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

proof end;

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

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;

:: Transfinite induction

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;

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

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

proof end;

theorem Th21: :: ORDINAL1:25

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

proof end;

theorem Th22: :: ORDINAL1:26

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

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

proof end;

::
:: 8. Limit ordinals
::

definition

let A be set ;

attr A is limit_ordinal means :: ORDINAL1:def 6
A = union A;

end;

:: deftheorem defines limit_ordinal ORDINAL1:def 6 :
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 )

proof end;

theorem :: ORDINAL1:29

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

proof end;

::
:: 9. Transfinite sequences
::

definition

let IT be set ;

attr IT is Sequence-like means :Def7: :: ORDINAL1:def 7
( proj1 IT is epsilon-transitive & proj1 IT is epsilon-connected );

end;

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

registration

cluster empty -> Sequence-like for number ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is Sequence-like ;

end;

definition

mode Sequence is Sequence-like Function;

end;

registration

let Z be set ;

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

existence
ex b₁ being Sequence st b₁ is Z -valued

proof end;

end;

definition

let Z be set ;
mode Sequence of Z is Z -valued Sequence;

end;

theorem :: ORDINAL1:30

for Z being set holds {} is Sequence of Z

proof end;

theorem :: ORDINAL1:31

for F being Function st dom F is Ordinal holds
F is Sequence of rng F by Def7, RELAT_1:def 19;

registration

let L be Sequence;

cluster proj1 L -> ordinal ;

coherence
dom L is ordinal by Def7;

end;

theorem :: ORDINAL1:32

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

proof end;

registration

let L be Sequence;
let A be Ordinal;

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

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

proof end;

end;

theorem :: ORDINAL1:33

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

definition

let IT be set ;

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 ;

end;

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

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

proof end;

::
:: 10. Schemes of definability by transfinite induction
::

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

F₃() = F₄()

provided

A1: ( dom F₃() = F₁() & ( for B being Ordinal
for L being 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 Sequence st B in F₁() & L = F₄() | B holds
F₄() . B = F₂(L) ) )

proof end;

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

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

proof end;

scheme :: ORDINAL1:sch 5
FuncTS{ F₁() -> Sequence, F₂( Ordinal) -> set , F₃( 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 object holds
( a = F₂(A) iff ex L being 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:35

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

proof end;

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

definition

let X be set ;

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
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in X & x is Ordinal ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in X & x is Ordinal ) ) ) & ( for x being object holds
( x in b₂ iff ( x in X & x is Ordinal ) ) ) holds
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
ex b₁ being set st
for x being object holds
( x in b₁ iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) & ( for x being object holds
( x in b₂ iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines On ORDINAL1:def 9 :
for X, b₂ being set holds
( b₂ = On X iff for x being object holds
( x in b₂ iff ( x in X & x is Ordinal ) ) );

:: deftheorem defines Lim ORDINAL1:def 10 :
for X, b₂ being set holds
( b₂ = Lim X iff for x being object holds
( x in b₂ iff ( x in X & ex A being Ordinal st
( x = A & A is limit_ordinal ) ) ) );

:: Generalized Axiom of Infinity

theorem Th32: :: ORDINAL1:36

for D being Ordinal ex A being Ordinal st
( D in A & A is limit_ordinal )

proof end;

definition

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
ex b₁ being set st
( {} in b₁ & b₁ is limit_ordinal & b₁ is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b₁ c= A ) )

proof end;

uniqueness
for b₁, b₂ being set st {} in b₁ & b₁ is limit_ordinal & b₁ is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b₁ c= A ) & {} in b₂ & b₂ is limit_ordinal & b₂ is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b₂ c= A ) holds
b₁ = b₂ ;

end;

:: deftheorem Def11 defines omega ORDINAL1:def 11 :
for b₁ being set holds
( b₁ = omega iff ( {} in b₁ & b₁ is limit_ordinal & b₁ is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
b₁ c= A ) ) );

registration

cluster omega -> non empty ordinal ;

coherence
( not omega is empty & omega is ordinal ) by Def11;

end;

definition

let A be object ;

attr A is natural means :Def12: :: ORDINAL1:def 12
A in omega ;

end;

:: deftheorem Def12 defines natural ORDINAL1:def 12 :
for A being object holds
( A is natural iff A in omega );

registration

cluster natural for Number ;

existence
ex b₁ being Number st b₁ is natural

proof end;

cluster natural for number ;

existence
ex b₁ being set st b₁ is natural

proof end;

end;

definition

mode Nat is natural number ;

end;

registration

Nat ex b₁ being number st
for b₂ being Nat holds b₂ in b₁

proof end;

end;

:: from ARYTM_3, 2006.05.26

registration

let A be Ordinal;

cluster -> ordinal for Element of A;

coherence
for b₁ being Element of A holds b₁ is ordinal

proof end;

end;

:: missing, 2006.06.25, A.T.

registration

cluster natural -> ordinal for number ;

coherence
for b₁ being number st b₁ is natural holds
b₁ is ordinal ;

end;

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

scheme :: ORDINAL1:sch 6
ALFA{ F₁() -> non empty set , P₁[ object , object ] } :

ex F being Function st
( dom F = F₁() & ( for d being Element of F₁() ex A being Ordinal st
( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) ) ) )

provided

A1: for d being Element of F₁() ex A being Ordinal st P₁[d,A]

proof end;

:: from CARD_4, 2007.08.06, A.T.

theorem :: ORDINAL1:37

for X being set holds (succ X) \ {X} = X

proof end;

:: from ARYTM_3, 2007.09.16, A.T.

registration

cluster empty -> natural for number ;

coherence
for b₁ being number st b₁ is empty holds
b₁ is natural by Def11;

cluster -> natural for Element of omega ;

coherence
for b₁ being Element of omega holds b₁ is natural ;

end;

registration

cluster non empty natural for number ;

existence
ex b₁ being number st
( not b₁ is empty & b₁ is natural )

proof end;

end;

:: from ARYTM_3, 2007.10.23, A.T.

registration

let a be natural Ordinal;

cluster succ a -> natural ;

coherence
succ a is natural

proof end;

end;

:: from DILWORTH, 2011.07.31,A.T.

registration

cluster empty -> c=-linear for number ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is c=-linear ;

end;

registration

let X be c=-linear set ;

cluster -> c=-linear for Element of bool X;

coherence
for b₁ being Subset of X holds b₁ is c=-linear by Def8;

end;

theorem :: ORDINAL1:38

canceled;

::$CT

definition

::$CT

func 0 -> number equals :: ORDINAL1:def 13
{} ;

coherence
{} is number ;

end;

:: deftheorem defines 0 ORDINAL1:def 13 :
0 = {} ;

registration

cluster 0 -> natural ;

coherence
0 is natural ;

end;

definition

let x be Number ;

attr x is zero means :Def14: :: ORDINAL1:def 14
x = 0 ;

end;

:: deftheorem Def14 defines zero ORDINAL1:def 14 :
for x being Number holds
( x is zero iff x = 0 );

registration

cluster 0 -> zero ;

coherence
0 is zero ;

cluster zero for Number ;

existence
ex b₁ being Number st b₁ is zero

proof end;

cluster zero for number ;

existence
ex b₁ being set st b₁ is zero

proof end;

end;

registration

cluster zero -> natural for Number ;

coherence
for b₁ being Number st b₁ is zero holds
b₁ is natural ;

end;

registration

cluster non zero for Number ;

existence
not for b₁ being Number holds b₁ is zero

proof end;

end;

registration

cluster zero -> trivial for number ;

coherence
for b₁ being set st b₁ is zero holds
b₁ is trivial ;

cluster non trivial -> non zero for number ;

coherence
for b₁ being set st not b₁ is trivial holds
not b₁ is zero ;

end;

definition

let R be Relation;

attr R is non-zero means :Def15: :: ORDINAL1:def 15
not 0 in rng R;

end;

:: deftheorem Def15 defines non-zero ORDINAL1:def 15 :
for R being Relation holds
( R is non-zero iff not 0 in rng R );

definition

let X be set ;

attr X is with_zero means :Def16: :: ORDINAL1:def 16
0 in X;

end;

:: deftheorem Def16 defines with_zero ORDINAL1:def 16 :
for X being set holds
( X is with_zero iff 0 in X );

notation

let X be set ;
antonym without_zero X for with_zero ;

end;

registration

cluster empty -> without_zero for number ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is without_zero ;

end;

registration

cluster empty Relation-like -> non-zero for number ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is non-zero ;

end;

registration

cluster non empty without_zero for number ;

existence
ex b₁ being set st
( b₁ is without_zero & not b₁ is empty )

proof end;

end;

registration

let X be non empty without_zero set ;

cluster -> non zero for Element of X;

coherence
for b₁ being Element of X holds not b₁ is zero by Def16;

end;

registration

cluster Relation-like non-zero for number ;

existence
ex b₁ being Relation st b₁ is non-zero

proof end;

cluster Relation-like non non-zero for number ;

existence
not for b₁ being Relation holds b₁ is non-zero

proof end;

end;

registration

let R be non-zero Relation;

cluster proj2 R -> without_zero ;

coherence
not rng R is with_zero by Def15;

end;

registration

let R be non non-zero Relation;

cluster proj2 R -> with_zero ;

coherence
rng R is with_zero by Def15;

end;

registration

let R be non-zero Relation;
let S be Relation;

cluster S * R -> non-zero ;

coherence
S * R is non-zero

proof end;

end;

:: to be removed

registration

cluster without_zero -> with_non-empty_elements for number ;

coherence
for b₁ being set st b₁ is without_zero holds
b₁ is with_non-empty_elements

proof end;

cluster with_zero -> non with_non-empty_elements for number ;

coherence
for b₁ being set st b₁ is with_zero holds
not b₁ is with_non-empty_elements

proof end;

cluster with_non-empty_elements -> without_zero for number ;

coherence
for b₁ being set st b₁ is with_non-empty_elements holds
b₁ is without_zero ;

cluster non with_non-empty_elements -> with_zero for number ;

coherence
for b₁ being set st not b₁ is with_non-empty_elements holds
b₁ is with_zero ;

end;

definition

let o be object ;

func Segm o -> set equals :: ORDINAL1:def 17
o;

coherence
o is set by TARSKI:1;

end;

:: deftheorem defines Segm ORDINAL1:def 17 :
for o being object holds Segm o = o;

registration

let n be Ordinal;

cluster Segm n -> ordinal ;

coherence
Segm n is ordinal ;

end;

registration

let n be zero Ordinal;

cluster Segm n -> empty ;

coherence
Segm n is empty by Def14;

end;