:: The Ordinal Numbers. Transfinite Induction and Defining by Transfinite Induction
:: by Grzegorz Bancerek
::
:: 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: ; :: :: 4. Definition of ordinal numbers - Ordinal :: registration existence ex b1 being set st ( b1 is epsilon-transitive & b1 is epsilon-connected ) by Lm1; end; definition let IT be object ; end; :: deftheorem defines ordinal ORDINAL1:def 4 : for IT being object holds ( IT is ordinal iff IT is epsilon-transitive epsilon-connected set ); registration coherence for b1 being set st b1 is ordinal holds ( b1 is epsilon-transitive & b1 is epsilon-connected ) ; coherence for b1 being set st b1 is epsilon-transitive & b1 is epsilon-connected holds b1 is ordinal ; end; notation end; registration existence ex b1 being number st b1 is ordinal by Lm1; end; registration existence ex b1 being Number st b1 is ordinal by Lm1; end; definition 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 coherence for b1 being number st b1 is empty holds b1 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 existence not for b1 being Ordinal holds b1 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; 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{ P1[ Ordinal] } : ex A being Ordinal st ( P1[A] & ( for B being Ordinal st P1[B] holds A c= B ) ) provided A1: ex A being Ordinal st P1[A] proof end; :: Transfinite induction 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] 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 coherence for b1 being set st b1 is empty holds b1 is Sequence-like ; end; definition end; registration let Z be set ; existence ex b1 being Sequence st b1 is Z -valued proof end; end; definition 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 ; registration let L be Sequence; 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; 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{ F1() -> Ordinal, F2( Sequence) -> set , F3() -> Sequence, F4() -> Sequence } : F3() = F4() provided A1: ( dom F3() = F1() & ( for B being Ordinal for L being Sequence st B in F1() & L = F3() | B holds F3() . B = F2(L) ) ) and A2: ( dom F4() = F1() & ( for B being Ordinal for L being Sequence st B in F1() & L = F4() | B holds F4() . B = F2(L) ) ) proof end; scheme :: ORDINAL1:sch 4 TSExist{ F1() -> Ordinal, F2( Sequence) -> set } : ex L being Sequence st ( dom L = F1() & ( for B being Ordinal for L1 being Sequence st B in F1() & L1 = L | B holds L . B = F2(L1) ) ) proof end; scheme :: ORDINAL1:sch 5 FuncTS{ F1() -> Sequence, F2( Ordinal) -> set , F3( 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 object holds ( a = F2(A) iff ex L being Sequence st ( a = F3(L) & dom L = A & ( 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) 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 b1 being set st for x being object holds ( x in b1 iff ( x in X & x is Ordinal ) ) proof end; uniqueness for b1, b2 being set st ( for x being object holds ( x in b1 iff ( x in X & x is Ordinal ) ) ) & ( for x being object holds ( x in b2 iff ( x in X & x is Ordinal ) ) ) holds b1 = b2 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 b1 being set st for x being object holds ( x in b1 iff ( x in X & ex A being Ordinal st ( x = A & A is limit_ordinal ) ) ) proof end; uniqueness for b1, b2 being set st ( for x being object holds ( x in b1 iff ( x in X & ex A being Ordinal st ( x = A & A is limit_ordinal ) ) ) ) & ( for x being object holds ( x in b2 iff ( x in X & ex A being Ordinal st ( x = A & A is limit_ordinal ) ) ) ) holds b1 = b2 proof end; end; :: deftheorem Def9 defines On ORDINAL1:def 9 : for X, b2 being set holds ( b2 = On X iff for x being object holds ( x in b2 iff ( x in X & x is Ordinal ) ) ); :: deftheorem defines Lim ORDINAL1:def 10 : for X, b2 being set holds ( b2 = Lim X iff for x being object holds ( x in b2 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 b1 being set st ( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds b1 c= A ) ) proof end; uniqueness for b1, b2 being set st {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds b1 c= A ) & {} in b2 & b2 is limit_ordinal & b2 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds b2 c= A ) holds b1 = b2 ; end; :: deftheorem Def11 defines omega ORDINAL1:def 11 : for b1 being set holds ( b1 = omega iff ( {} in b1 & b1 is limit_ordinal & b1 is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds b1 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 existence ex b1 being Number st b1 is natural proof end; existence ex b1 being set st b1 is natural proof end; end; definition end; registration Nat ex b1 being number st for b2 being Nat holds b2 in b1 proof end; 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 proof end; end; :: missing, 2006.06.25, A.T. registration coherence for b1 being number st b1 is natural holds b1 is ordinal ; end; :: from ZF_REFLE, 2007,03.13, A.T. scheme :: ORDINAL1:sch 6 ALFA{ F1() -> non empty set , P1[ object , object ] } : ex F being Function st ( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st ( A = F . d & P1[d,A] & ( 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] 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 coherence for b1 being number st b1 is empty holds b1 is natural by Def11; cluster -> natural for Element of omega ; coherence for b1 being Element of omega holds b1 is natural ; end; registration cluster non empty natural for number ; existence ex b1 being number st ( not b1 is empty & b1 is natural ) proof end; end; :: from ARYTM_3, 2007.10.23, A.T. registration let a be natural Ordinal; coherence succ a is natural proof end; end; :: from DILWORTH, 2011.07.31,A.T. registration coherence for b1 being set st b1 is empty holds b1 is c=-linear ; 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 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
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
;
existence
ex b1 being Number st b1 is zero
proof end;
existence
ex b1 being set st b1 is zero
proof end;
end;

registration
cluster zero -> natural for Number ;
coherence
for b1 being Number st b1 is zero holds
b1 is natural
;
end;

registration
cluster non zero for Number ;
existence
not for b1 being Number holds b1 is zero
proof end;
end;

registration
cluster zero -> trivial for number ;
coherence
for b1 being set st b1 is zero holds
b1 is trivial
;
cluster non trivial -> non zero for number ;
coherence
for b1 being set st not b1 is trivial holds
not b1 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
coherence
for b1 being set st b1 is empty holds
b1 is without_zero
;
end;

registration
coherence
for b1 being Relation st b1 is empty holds
b1 is non-zero
;
end;

registration
existence
ex b1 being set st
( b1 is without_zero & not b1 is empty )
proof end;
end;

registration
let X be non empty without_zero set ;
cluster -> non zero for Element of X;
coherence
for b1 being Element of X holds not b1 is zero
by Def16;
end;

registration
existence
ex b1 being Relation st b1 is non-zero
proof end;
existence
not for b1 being Relation holds b1 is non-zero
proof end;
end;

registration
let R be non-zero Relation;
coherence
not rng R is with_zero
by Def15;
end;

registration
let R be non non-zero Relation;
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
coherence
for b1 being set st b1 is without_zero holds
b1 is with_non-empty_elements
proof end;
coherence
for b1 being set st b1 is with_zero holds
not b1 is with_non-empty_elements
proof end;
coherence
for b1 being set st b1 is with_non-empty_elements holds
b1 is without_zero
;
coherence
for b1 being set st not b1 is with_non-empty_elements holds
b1 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;
coherence
Segm n is ordinal
;
end;

registration
let n be zero Ordinal;
cluster Segm n -> empty ;
coherence
Segm n is empty
by Def14;
end;