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


begin

theorem :: ORDINAL1:1
canceled;

theorem :: ORDINAL1:2
canceled;

theorem :: ORDINAL1:3
canceled;

theorem :: ORDINAL1:4
canceled;

theorem Th5: :: ORDINAL1:5
for Y, X being set st Y in X holds
not X c= Y
proofend;

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 Th6: :: ORDINAL1:6
for X being set holds X in succ X
proofend;

theorem :: ORDINAL1:7
for X, Y being set st succ X = succ Y holds
X = Y
proofend;

theorem Th8: :: ORDINAL1:8
for x, X being set holds
( x in succ X iff ( x in X or x = X ) )
proofend;

theorem Th9: :: ORDINAL1:9
for X being set holds X <> succ X
proofend;

definition
let X be set ;
attrX is epsilon-transitive  means :Def2: :: ORDINAL1:def 2
 for x being set st x in X holds
x c= X;
attrX is epsilon-connected  means :Def3: :: ORDINAL1:def 3
 for x, y being set st x in X &amp; y in X &amp; not x in y &amp; 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 &amp; y in X &amp; not x in y &amp; not x = y holds
y in x );

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

::
:: 4. Definition of ordinal numbers - Ordinal
::
definition
let IT be set ;
attrIT is ordinal  means :Def4: :: ORDINAL1:def 4
( IT is epsilon-transitive &amp; IT is epsilon-connected );
end;

:: deftheorem Def4 defines ordinal ORDINAL1:def_4_:_
 for IT being set holds
( IT is ordinal iff ( IT is epsilon-transitive &amp; IT is epsilon-connected ) );

registration
cluster ordinal  ->  epsilon-transitive epsilon-connected for number ;
coherence
 for b1 being set st b1 is ordinal holds
( b1 is epsilon-transitive &amp; b1 is epsilon-connected ) by Def4;
cluster epsilon-transitive epsilon-connected  ->  ordinal for number ;
coherence
 for b1 being set st b1 is epsilon-transitive &amp; b1 is epsilon-connected holds
b1 is ordinal by Def4;
end;

notation
synonym  number for  set ;
end;

registration
cluster ordinal for number ;
existence
 ex b1 being number st b1 is ordinal by Lm1;
end;

definition
mode Ordinal is ordinal number ;
end;

theorem Th10: :: ORDINAL1:10
for A, B being set
for C being epsilon-transitive set st A in B &amp; B in C holds
A in C
proofend;

theorem Th11: :: ORDINAL1:11
for x being epsilon-transitive set
for A being Ordinal st x c< A holds
x in A
proofend;

theorem :: ORDINAL1:12
for A being epsilon-transitive set
for B, C being Ordinal st A c= B &amp; B in C holds
A in C
proofend;

theorem Th13: :: ORDINAL1:13
for a being set
for A being Ordinal st a in A holds
a is Ordinal
proofend;

theorem Th14: :: ORDINAL1:14
for A, B being Ordinal holds
( A in B or A = B or B in A )
proofend;

definition
let A, B be Ordinal;
:: original:c=
redefine predA 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 )
proofend;
connectedness
 for A, B being Ordinal st ex C being Ordinal st
( C in A &amp; not C in B ) holds
for C being Ordinal st C in B holds
C in A
proofend;
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
proofend;

theorem Th16: :: ORDINAL1:16
for A, B being Ordinal holds
( A c= B or B in A )
proofend;

registration
cluster empty  ->  ordinal for number ;
coherence
 for b1 being number st b1 is empty holds
b1 is ordinal by Lm1;
end;

theorem Th17: :: ORDINAL1:17
for x being set st x is Ordinal holds
succ x is Ordinal
proofend;

theorem Th18: :: ORDINAL1:18
for x being set st x is ordinal holds
union x is ordinal
proofend;

registration
cluster non empty epsilon-transitive epsilon-connected ordinal for number ;
existence
 not for b1 being Ordinal holds b1 is empty
proofend;
end;

registration
let A be Ordinal;
cluster succ A ->  non empty ordinal ;
coherence
 ( not succ A is empty &amp; succ A is ordinal ) by Th17;
cluster union A ->  ordinal ;
coherence
 union A is ordinal by Th18;
end;

theorem Th19: :: ORDINAL1:19
for X being set st ( for x being set st x in X holds
( x is Ordinal &amp; x c= X ) ) holds
X is ordinal
proofend;

theorem Th20: :: ORDINAL1:20
for X being set
for A being Ordinal st X c= A &amp; X <> {} holds
ex C being Ordinal st
( C in X &amp; ( for B being Ordinal st B in X holds
C c= B ) )
proofend;

theorem Th21: :: ORDINAL1:21
for A, B being Ordinal holds
( A in B iff succ A c= B )
proofend;

theorem Th22: :: ORDINAL1:22
for A, C being Ordinal holds
( A in succ C iff A c= C )
proofend;

scheme :: ORDINAL1:sch 1
OrdinalMin{ P1[ Ordinal] } :
 ex A being Ordinal st
( P1[A] &amp; ( for B being Ordinal st P1[B] holds
A c= B ) )
provided
A1: ex A being Ordinal st P1[A]
proofend;

scheme :: ORDINAL1:sch 2
TransfiniteInd{ P1[ Ordinal] } :
 for A being Ordinal holds P1[A]
provided
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
P1[C] ) holds
P1[A]
proofend;

::
:: 7. Properties of sets of ordinals
::
theorem Th23: :: ORDINAL1:23
for X being set st ( for a being set st a in X holds
a is Ordinal ) holds
union X is ordinal
proofend;

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

theorem Th25: :: ORDINAL1:25
for X being set holds
not for x being set holds
( x in X iff x is Ordinal )
proofend;

theorem Th26: :: ORDINAL1:26
for X being set holds
not for A being Ordinal holds A in X
proofend;

theorem :: ORDINAL1:27
for X being set ex A being Ordinal st
( not A in X &amp; ( for B being Ordinal st not B in X holds
A c= B ) )
proofend;

::
:: 8. Limit ordinals
::
definition
let A be set ;
attrA is limit_ordinal  means :Def6: :: ORDINAL1:def 6
A = union A;
end;

:: deftheorem Def6 defines limit_ordinal ORDINAL1:def_6_:_
 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 )
proofend;

theorem :: ORDINAL1:29
for A being Ordinal holds
( not A is limit_ordinal iff ex B being Ordinal st A = succ B )
proofend;

::
:: 9. Transfinite sequences
::
definition
let IT be set ;
attrIT is T-Sequence-like  means :Def7: :: ORDINAL1:def 7
 proj1 IT is ordinal ;
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 for number ;
coherence
 for b1 being set st b1 is empty holds
b1 is T-Sequence-like
proofend;
end;

definition
mode T-Sequence is T-Sequence-like Function;
end;

registration
let Z be set ;
cluster Relation-like Z -valued Function-like T-Sequence-like for number ;
existence
 ex b1 being T-Sequence st b1 is Z -valued
proofend;
end;

definition
let Z be set ;
mode T-Sequence of Z is Z -valued T-Sequence;
end;

theorem :: ORDINAL1:30
for Z being set holds {} is T-Sequence of Z
proofend;

theorem :: ORDINAL1:31
for F being Function st dom F is Ordinal holds
F is T-Sequence of rng F by Def7, RELAT_1:def_19;

registration
let L be T-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 T-Sequence of X holds L is T-Sequence of Y
proofend;

registration
let L be T-Sequence;
let A be Ordinal;
clusterL | A ->  rng L -valued T-Sequence-like ;
coherence
 ( L | A is rng L -valued &amp; L | A is T-Sequence-like )
proofend;
end;

theorem :: ORDINAL1:33
for X being set
for L being T-Sequence of X
for A being Ordinal holds L | A is T-Sequence of X ;

definition
let IT be set ;
attrIT is c=-linear  means :Def8: :: ORDINAL1:def 8
 for x, y being set st x in IT &amp; 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 &amp; 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 ) &amp; X is c=-linear holds
union X is T-Sequence
proofend;

scheme :: ORDINAL1:sch 3
TSUniq{ F1() ->  Ordinal, F2( T-Sequence) ->  set , F3() ->  T-Sequence, F4() ->  T-Sequence } :
 F3() = F4()
provided
A1: ( dom F3() = F1() &amp; ( for B being Ordinal
for L being T-Sequence st B in F1() &amp; L = F3() | B holds
F3() . B = F2(L) ) ) and
A2: ( dom F4() = F1() &amp; ( for B being Ordinal
for L being T-Sequence st B in F1() &amp; L = F4() | B holds
F4() . B = F2(L) ) )
proofend;

scheme :: ORDINAL1:sch 4
TSExist{ F1() ->  Ordinal, F2( T-Sequence) ->  set } :
 ex L being T-Sequence st
( dom L = F1() &amp; ( for B being Ordinal
for L1 being T-Sequence st B in F1() &amp; L1 = L | B holds
L . B = F2(L1) ) )
proofend;

scheme :: ORDINAL1:sch 5
FuncTS{ F1() ->  T-Sequence, F2( Ordinal) ->  set , F3( T-Sequence) ->  set } :
 for B being Ordinal st B in dom F1() holds
F1() . B = F3((F1() | B))
provided
A1: for A being Ordinal
for a being set holds
( a = F2(A) iff ex L being T-Sequence st
( a = F3(L) &amp; dom L = A &amp; ( for B being Ordinal st B in A holds
L . B = F3((L | B)) ) ) ) and
A2: for A being Ordinal st A in dom F1() holds
F1() . A = F2(A)
proofend;

theorem :: ORDINAL1:35
for A, B being Ordinal holds
( A c< B or A = B or B c< A )
proofend;

begin

:: 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 set holds
( x in it iff ( x in X &amp; x is Ordinal ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x in X &amp; x is Ordinal ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X &amp; x is Ordinal ) ) ) &amp; ( for x being set holds
( x in b2 iff ( x in X &amp; x is Ordinal ) ) ) holds
b1 = b2
proofend;
func Lim X ->  set  means :: ORDINAL1:def 10
 for x being set holds
( x in it iff ( x in X &amp; ex A being Ordinal st
( x = A &amp; A is limit_ordinal ) ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ( x in X &amp; ex A being Ordinal st
( x = A &amp; A is limit_ordinal ) ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x in X &amp; ex A being Ordinal st
( x = A &amp; A is limit_ordinal ) ) ) ) &amp; ( for x being set holds
( x in b2 iff ( x in X &amp; ex A being Ordinal st
( x = A &amp; A is limit_ordinal ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines On ORDINAL1:def_9_:_
 for X, b2 being set holds
( b2 = On X iff for x being set holds
( x in b2 iff ( x in X &amp; x is Ordinal ) ) );

:: deftheorem  defines Lim ORDINAL1:def_10_:_
 for X, b2 being set holds
( b2 = Lim X iff for x being set holds
( x in b2 iff ( x in X &amp; ex A being Ordinal st
( x = A &amp; A is limit_ordinal ) ) ) );

:: [WP: ] Generalized_Axiom_of_Infinity
theorem Th36: :: ORDINAL1:36
for D being Ordinal ex A being Ordinal st
( D in A &amp; A is limit_ordinal )
proofend;

definition
func omega  ->  set  means :Def11: :: ORDINAL1:def 11
( {} in it &amp; it is limit_ordinal &amp; it is ordinal &amp; ( for A being Ordinal st {} in A &amp; A is limit_ordinal holds
it c= A ) );
existence
 ex b1 being set st
( {} in b1 &amp; b1 is limit_ordinal &amp; b1 is ordinal &amp; ( for A being Ordinal st {} in A &amp; A is limit_ordinal holds
b1 c= A ) )
proofend;
uniqueness
 for b1, b2 being set st {} in b1 &amp; b1 is limit_ordinal &amp; b1 is ordinal &amp; ( for A being Ordinal st {} in A &amp; A is limit_ordinal holds
b1 c= A ) &amp; {} in b2 &amp; b2 is limit_ordinal &amp; b2 is ordinal &amp; ( for A being Ordinal st {} in A &amp; A is limit_ordinal holds
b2 c= A ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines omega ORDINAL1:def_11_:_
 for b1 being set holds
( b1 = omega iff ( {} in b1 &amp; b1 is limit_ordinal &amp; b1 is ordinal &amp; ( for A being Ordinal st {} in A &amp; A is limit_ordinal holds
b1 c= A ) ) );

registration
cluster omega  ->  non empty ordinal ;
coherence
 ( not omega is empty &amp; omega is ordinal ) by Def11;
end;

definition
let A be set ;
attrA is natural  means :Def12: :: ORDINAL1:def 12
A in omega ;
end;

:: deftheorem Def12 defines natural ORDINAL1:def_12_:_
 for A being set holds
( A is natural iff A in omega );

registration
cluster natural for number ;
existence
 ex b1 being number st b1 is natural
proofend;
end;

definition
mode Nat is natural number ;
end;

registration
natural number  ex b1 being number st
for b2 being natural number holds b2 in b1
proofend;
end;

:: from ARYTM_3, 2006.05.26
registration
let A be Ordinal;
cluster  ->  ordinal for Element of A;
coherence
 for b1 being Element of A holds b1 is ordinal
proofend;
end;

:: missing, 2006.06.25, A.T.
registration
cluster natural  ->  ordinal for number ;
coherence
 for b1 being number st b1 is natural holds
b1 is ordinal
proofend;
end;

scheme :: ORDINAL1:sch 6
ALFA{ F1() ->  non empty set , P1[ set , set ] } :
 ex F being Function st
( dom F = F1() &amp; ( for d being Element of F1() ex A being Ordinal st
( A = F . d &amp; P1[d,A] &amp; ( for B being Ordinal st P1[d,B] holds
A c= B ) ) ) )
provided
A1: for d being Element of F1() ex A being Ordinal st P1[d,A]
proofend;

:: from CARD_4, 2007.08.06, A.T.
theorem :: ORDINAL1:37
for X being set holds (succ X) \ {X} = X
proofend;

:: from ARYTM_3, 2007.09.16, A.T.
registration
cluster empty  ->  natural for number ;
coherence
 for b1 being number st b1 is empty holds
b1 is natural
proofend;
cluster  ->  natural for Element of omega ;
coherence
 for b1 being Element of omega holds b1 is natural by Def12;
end;

registration
cluster non empty natural for number ;
existence
 ex b1 being number st
( not b1 is empty &amp; b1 is natural )
proofend;
end;

:: from ARYTM_3, 2007.10.23, A.T.
registration
let a be natural Ordinal;
cluster succ a ->  natural ;
coherence
 succ a is natural
proofend;
end;

:: from DILWORTH, 2011.07.31,A.T.
registration
cluster empty  ->  c=-linear for number ;
coherence
 for b1 being set st b1 is empty holds
b1 is c=-linear
proofend;
end;

registration
let X be c=-linear set ;
cluster  ->  c=-linear for Element of bool X;
coherence
 for b1 being Subset of X holds b1 is c=-linear
proofend;
end;