:: The Ordinal Numbers. Transfinite Induction and Defining by
:: Transfinite Induction
:: by Grzegorz Bancerek
::
:: Received March 20, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies TARSKI, XBOOLE_0, SUBSET_1, FUNCT_1, RELAT_1, ZFMISC_1, ORDINAL1,
CARD_1, XCMPLX_0, NAT_1, VALUED_0, QUANTAL1, FREEALG, SETFAM_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XTUPLE_0, SUBSET_1, SETFAM_1,
RELAT_1, FUNCT_1;
constructors TARSKI, ENUMSET1, SUBSET_1, FUNCT_1, XTUPLE_0, SETFAM_1;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SETFAM_1;
expansions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
theorems TARSKI, XBOOLE_0, FUNCT_1, ZFMISC_1, RELAT_1, XBOOLE_1, SUBSET_1,
XTUPLE_0, XREGULAR;
schemes XBOOLE_0, FUNCT_1;
begin
reserve X,Y,Z,X1,X2,X3,X4,X5,X6 for set, x,y for object;
::$CT 4
theorem Th1:
Y in X implies not X c= Y
proof
assume
A1: Y in X;
assume X c= Y;
then Y in Y by A1;
hence contradiction;
end;
definition
let X;
func succ X -> set equals
X \/ { X };
coherence;
end;
registration
let X;
cluster succ X -> non empty;
coherence;
end;
theorem Th2:
X in succ X
proof
X in { X } by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
theorem
succ X = succ Y implies X = Y
proof
assume that
A1: succ X = succ Y and
A2: X <> Y;
Y in X \/ { X } by A1,Th2;
then
A3: Y in X or Y in { X } by XBOOLE_0:def 3;
X in Y \/ { Y } by A1,Th2;
then X in Y or X in { Y } by XBOOLE_0:def 3;
hence contradiction by A2,A3,TARSKI:def 1;
end;
theorem Th4:
x in succ X iff x in X or x = X
proof
thus x in succ X implies x in X or x = X
proof
assume x in succ X;
then x in X or x in { X } by XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
assume x in X or x = X;
then x in X or x in { X } by TARSKI:def 1;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th5:
X <> succ X
proof
assume
A1: X = succ X;
X in succ X by Th2;
hence contradiction by A1;
end;
::
:: 3. epsilon-transitivity & epsilon-connectedness
::
reserve a,b,c for object, X,Y,Z,x,y,z for set;
definition
let X;
attr X is epsilon-transitive means
:Def2:
for x st x in X holds x c= X;
attr X is epsilon-connected means
:Def3:
for x,y st x in X & y in X holds x in y or x = y or y in x;
end;
Lm1: {} is epsilon-transitive epsilon-connected;
::
:: 4. Definition of ordinal numbers - Ordinal
::
registration
cluster epsilon-transitive epsilon-connected for set;
existence by Lm1;
end;
registration
let X be empty set;
cluster { X } -> epsilon-transitive;
coherence
proof
let x;
thus thesis by TARSKI:def 1;
end;
end;
registration
let X be non empty set;
cluster { X } -> non epsilon-transitive;
coherence
proof
take X;
thus X in {X} by TARSKI:def 1;
consider x being object such that
A1: x in X by XBOOLE_0:7;
reconsider x as set by TARSKI:1;
A2: x in X by A1;
assume X c= {X};
then x = X by A1,TARSKI:def 1;
hence contradiction by A2;
end;
end;
registration
let X be set;
cluster { X } -> epsilon-connected;
coherence
proof
let x,y;
assume x in {X} & y in {X};
then x = X & y = X by TARSKI:def 1;
hence thesis;
end;
end;
definition
let IT be set;
attr IT is ordinal means
IT is epsilon-transitive epsilon-connected;
end;
registration
cluster ordinal -> epsilon-transitive epsilon-connected for set;
coherence;
cluster epsilon-transitive epsilon-connected -> ordinal for set;
coherence;
end;
notation
synonym Number for object;
synonym number for set;
end;
registration
cluster ordinal for number;
existence by Lm1;
end;
definition
mode Ordinal is ordinal number;
end;
registration
cluster empty -> ordinal for number;
coherence by Lm1;
end;
registration
let X be non empty set;
cluster { X } -> non ordinal;
coherence;
end;
reserve A,B,C,D for Ordinal;
theorem Th6:
for A,B being set, C being epsilon-transitive set st A in B & B in C
holds A in C
proof
let A,B be set, C be epsilon-transitive set;
assume that
A1: A in B and
A2: B in C;
B c= C by A2,Def2;
hence thesis by A1;
end;
theorem Th7:
for x being epsilon-transitive set, A being Ordinal st x c< A holds x in A
proof
let x be epsilon-transitive set, A be Ordinal;
set a = the Element of A \ x;
assume
A1: x c< A;
A \ x <> {} by A1,XBOOLE_1:37,60;
then a in A \ x;
then consider y such that
A3: y in A \ x and
A4: not ex a being object st a in A \ x & a in y by TARSKI:3;
A5: not y in x by A3,XBOOLE_0:def 5;
now
let a be object;
assume a in x;
then consider z such that
A6: z = a and
A7: z in x;
z c= x by A7,Def2;
then not y in z by A3,XBOOLE_0:def 5;
hence a in y by A1,A3,A5,A6,A7,Def3;
end;
then
A8: x c= y;
A9: y c= A by A3,Def2;
now
let a be object;
assume
A10: a in y;
then not a in A \ x by A4;
hence a in x by A9,A10,XBOOLE_0:def 5;
end;
then
A11: y c= x;
y in A by A3;
hence thesis by A11,A8,XBOOLE_0:def 10;
end;
theorem
for A being epsilon-transitive set, B, C being Ordinal
st A c= B & B in C holds A in C
proof
let A be epsilon-transitive set, B, C be Ordinal;
assume that
A1: A c= B and
A2: B in C;
B c= C by A2,Def2;
then
A3: A c= C by A1;
A <> C by A1,A2,Th1;
then A c< C by A3;
hence thesis by Th7;
end;
theorem Th9:
a in A implies a is Ordinal
proof
assume
A1: a in A;
reconsider a as set by TARSKI:1;
A2: a c= A by Def2,A1;
now
let y;
assume
A3: y in a;
then
A4: y c= A by A2,Def2;
assume not y c= a;
then consider b be object such that
A5: b in y & not b in a;
b in y \ a by A5,XBOOLE_0:def 5;
then consider z such that
A6: z in y \ a and
not ex c being object st c in y \ a & c in z by TARSKI:3;
z in y by A6;
then z in a or z = a or a in z by A1,A4,Def3;
hence contradiction by A3,A6,XBOOLE_0:def 5,XREGULAR:7;
end;
then
A7: a is epsilon-transitive;
for y,z st y in a & z in a holds y in z or y = z or z in y by A2,Def3;
then a is epsilon-connected;
hence thesis by A7;
end;
theorem Th10:
A in B or A = B or B in A
proof
assume that
A1: not A in B and
A2: A <> B;
not A c< B by A1,Th7;
then not A c= B by A2;
then consider a be object such that
A3: a in A & not a in B;
a in A \ B by A3,XBOOLE_0:def 5;
then consider X such that
A4: X in A \ B and
A5: not ex a being object st a in A \ B & a in X by TARSKI:3;
A6: X c= A by A4,Def2;
now
let b be object;
assume
A7: b in X;
then not b in A \ B by A5;
hence b in B by A6,A7,XBOOLE_0:def 5;
end;
then X c= B;
then
A8: X c< B or X = B;
( not X in B)& X is Ordinal by A4,Th9,XBOOLE_0:def 5;
hence thesis by A4,A8,Th7;
end;
definition
let A,B;
redefine pred A c= B means :: redefines c= (TARSKI, definition)
for C st C in A holds C in B;
compatibility
proof
thus A c= B implies for C st C in A holds C in B;
assume
A1: for C st C in A holds C in B;
let x be object;
assume
A2: x in A;
then reconsider C = x as Ordinal by Th9;
C in B by A1,A2;
hence thesis;
end;
connectedness
proof
let A,B;
given C such that
A3: C in A & not C in B;
let D;
A in B or A = B or B in A by Th10;
hence thesis by A3,Th6;
end;
end;
theorem
A,B are_c=-comparable
proof
A c= B or B c= A;
hence thesis;
end;
theorem Th12:
A c= B or B in A
proof
A in B or A = B or B in A by Th10;
hence thesis by Def2;
end;
theorem Th13:
x is Ordinal implies succ x is Ordinal
proof
A1: now
let y;
A2: y in { x } implies y = x by TARSKI:def 1;
assume y in succ x;
hence y in x or y = x by A2,XBOOLE_0:def 3;
end;
assume
A3: x is Ordinal;
now
let y;
A4: y = x implies y c= succ x by XBOOLE_1:7;
A5: now
assume y in x;
then
A6: y c= x by A3,Def2;
x c= x \/ { x } by XBOOLE_1:7;
hence y c= succ x by A6;
end;
assume y in succ x;
hence y c= succ x by A1,A5,A4;
end;
then
A7: succ x is epsilon-transitive;
now
let y,z;
assume that
A8: y in succ x and
A9: z in succ x;
A10: z in x or z = x by A1,A9;
y in x or y = x by A1,A8;
hence y in z or y = z or z in y by A3,A10,Def3;
end;
then succ x is epsilon-connected;
hence thesis by A7;
end;
theorem Th14:
x is ordinal implies union x is epsilon-transitive epsilon-connected
proof
assume x is ordinal;
then reconsider A = x as Ordinal;
thus y in union x implies y c= union x
proof
assume y in union x;
then consider z such that
A1: y in z and
A2: z in x by TARSKI:def 4;
z in A by A2;
then reconsider z as Ordinal by Th9;
z c= A by A2,Def2;
hence thesis by A1,ZFMISC_1:74;
end;
let y,z;
assume that
A3: y in union x and
A4: z in union x;
consider X such that
A5: y in X and
A6: X in x by A3,TARSKI:def 4;
A7: X in A by A6;
consider Y such that
A8: z in Y and
A9: Y in x by A4,TARSKI:def 4;
reconsider X,Y as Ordinal by A9,A7,Th9;
z in Y by A8;
then
A10: z is Ordinal by Th9;
y in X by A5;
then y is Ordinal by Th9;
hence thesis by A10,Th10;
end;
registration
cluster non empty for Ordinal;
existence
proof
reconsider A = succ {} as Ordinal;
take A;
thus thesis;
end;
end;
registration
let A;
cluster succ A -> non empty ordinal;
coherence by Th13;
cluster union A -> ordinal;
coherence by Th14;
end;
theorem Th15:
(for x st x in X holds x is Ordinal & x c= X) implies
X is epsilon-transitive epsilon-connected
proof
assume
A1: for x st x in X holds x is Ordinal & x c= X;
thus X is epsilon-transitive
by A1;
let x,y;
assume x in X & y in X;
then x is Ordinal & y is Ordinal by A1;
hence thesis by Th10;
end;
theorem Th16:
X c= A & X <> {} implies ex C st C in X & for B st B in X holds C c= B
proof
set a = the Element of X;
assume that
A1: X c= A and
A2: X <> {};
a in X by A2;
then consider Y such that
A3: Y in X and
A4: not ex a being object st a in X & a in Y by TARSKI:3;
Y is Ordinal by A1,A3,Th9;
then consider C such that
A5: C = Y;
take C;
thus C in X by A3,A5;
let B;
assume B in X;
then not B in C by A4,A5;
then B = C or C in B by Th10;
hence thesis by Def2;
end;
theorem Th17:
A in B iff succ A c= B
proof
thus A in B implies succ A c= B
proof
assume
A1: A in B;
then for a be object holds a in { A } implies a in B by TARSKI:def 1;
then
A2: { A } c= B;
A c= B by A1,Def2;
hence thesis by A2,XBOOLE_1:8;
end;
assume
A3: succ A c= B;
A in succ A by Th2;
hence thesis by A3;
end;
theorem Th18:
A in succ C iff A c= C
proof
thus A in succ C implies A c= C
proof
assume A in succ C;
then A in C or A in { C } by XBOOLE_0:def 3;
hence thesis by Def2,TARSKI:def 1;
end;
assume
A1: A c= C;
assume not A in succ C;
then A = succ C or succ C in A by Th10;
then
A2: succ C c= C by A1,Def2;
C in succ C by Th2;
then C c= succ C by Def2;
then succ C = C by A2;
hence contradiction by Th5;
end;
::
:: 6. Transfinite induction and principle of minimum of ordinals
::
scheme
OrdinalMin { P[Ordinal] } : ex A st P[A] & for B st P[B] holds A c= B
provided
A1: ex A st P[A]
proof
consider A such that
A2: P[A] by A1;
defpred R[object] means ex B st $1 = B & P[B];
consider X such that
A3: for x being object holds x in X iff x in succ A & R[x]
from XBOOLE_0:sch 1;
for a be object holds a in X implies a in succ A by A3;
then
A4: X c= succ A;
A in succ A by Th2;
then X <> {} by A2,A3;
then consider C such that
A5: C in X and
A6: for B st B in X holds C c= B by A4,Th16;
C in succ A by A3,A5;
then
A7: C c= succ A by Def2;
take C;
ex B st C = B & P[B] by A3,A5;
hence P[C];
let B;
assume
A8: P[B];
assume
A9: not C c= B;
then B c< C;
then B in C by Th7;
then B in X by A3,A8,A7;
hence contradiction by A6,A9;
end;
::$N Transfinite induction
scheme
TransfiniteInd { P[Ordinal] } : for A holds P[A]
provided
A1: for A st for C st C in A holds P[C] holds P[A]
proof
defpred R[object] means ex B st $1 = B & P[B];
let A;
set Y = succ A;
consider Z such that
A2: for x being object holds x in Z iff x in Y & R[x] from XBOOLE_0:sch 1;
now
assume Y \ Z <> {};
then consider C such that
A3: C in Y \ Z and
A4: for B st B in Y \ Z holds C c= B by Th16;
now
let B such that
A5: B in C;
A6: C c= Y by A3,Def2;
now
assume not B in Z;
then B in Y \ Z by A5,A6,XBOOLE_0:def 5;
then
A7: C c= B by A4;
C <> B by A5;
then C c< B by A7;
hence contradiction by A5,Th7;
end;
then ex B9 being Ordinal st B = B9 & P[B9] by A2;
hence P[B];
end;
then
A8: P[C] by A1;
not C in Z by A3,XBOOLE_0:def 5;
hence contradiction by A2,A3,A8;
end;
then not A in Y or A in Z by XBOOLE_0:def 5;
then ex B st A = B & P[B] by A2,Th2;
hence thesis;
end;
::
:: 7. Properties of sets of ordinals
::
theorem Th19:
for X st for a st a in X holds a is Ordinal
holds union X is epsilon-transitive epsilon-connected
proof
let X such that
A1: for a st a in X holds a is Ordinal;
thus union X is epsilon-transitive
proof
let x;
assume x in union X;
then consider Y such that
A2: x in Y and
A3: Y in X by TARSKI:def 4;
Y is Ordinal by A1,A3;
then
A4: x c= Y by A2,Def2;
let a be object;
assume a in x;
hence thesis by A3,A4,TARSKI:def 4;
end;
let x,y;
assume that
A5: x in union X and
A6: y in union X;
consider Z such that
A7: y in Z and
A8: Z in X by A6,TARSKI:def 4;
Z is Ordinal by A1,A8;
then
A9: y is Ordinal by A7,Th9;
consider Y such that
A10: x in Y and
A11: Y in X by A5,TARSKI:def 4;
Y is Ordinal by A1,A11;
then x is Ordinal by A10,Th9;
hence thesis by A9,Th10;
end;
theorem Th20:
for X st for a st a in X holds a is Ordinal ex A st X c= A
proof
let X;
assume
A1: for a st a in X holds a is Ordinal;
then
A2: union X is epsilon-transitive epsilon-connected by Th19;
then reconsider A = succ(union X) as Ordinal;
take A;
let a be object;
assume
A3: a in X;
then reconsider B = a as Ordinal by A1;
for b be object holds b in B implies b in union X by A3,TARSKI:def 4;
then B c= union X;
hence thesis by A2,Th18;
end;
theorem Th21:
not ex X st for x holds x in X iff x is Ordinal
proof
given X such that
A1: for x holds x in X iff x is Ordinal;
A2: X is epsilon-transitive
proof
let x;
assume x in X;
then
A3: x is Ordinal by A1;
thus thesis
proof
let a be object;
assume a in x;
then a is Ordinal by A3,Th9;
hence thesis by A1;
end;
end;
X is epsilon-connected
proof
let x,y;
assume x in X & y in X;
then x is Ordinal & y is Ordinal by A1;
hence thesis by Th10;
end;
then X in X by A1,A2;
hence contradiction;
end;
theorem Th22:
not ex X st for A holds A in X
proof
defpred P[object] means $1 is Ordinal;
given X such that
A1: A in X;
consider Y such that
A2: for a being object holds a in Y iff a in X & P[a] from XBOOLE_0:sch 1;
for x st x is Ordinal holds x in Y by A1,A2;
then x in Y iff x is Ordinal by A2;
hence contradiction by Th21;
end;
theorem
for X ex A st not A in X & for B st not B in X holds A c= B
proof
let X;
defpred P[object] means not $1 in X;
consider B such that
A1: not B in X by Th22;
consider Y such that
A2: for a being object holds a in Y iff a in succ B & P[a]
from XBOOLE_0:sch 1;
for a be object holds a in Y implies a in succ B by A2;
then
A3: Y c= succ B;
B in succ B by Th2;
then Y <> {} by A1,A2;
then consider A such that
A4: A in Y and
A5: for B st B in Y holds A c= B by A3,Th16;
A in succ B by A2,A4;
then
A6: A c= succ B by Def2;
take A;
thus not A in X by A2,A4;
let C;
assume
A7: not C in X;
assume
A8: not A c= C;
then not A in C by Def2;
then C in A by A8,Th10;
then C in Y by A2,A7,A6;
hence contradiction by A5,A8;
end;
::
:: 8. Limit ordinals
::
definition
let A be set;
attr A is limit_ordinal means
A = union A;
end;
theorem Th24:
for A holds A is limit_ordinal iff for C st C in A holds succ C in A
proof
let A;
thus A is limit_ordinal implies for C st C in A holds succ C in A
proof
assume A is limit_ordinal;
then
A1: A = union A;
let C;
assume C in A;
then consider z such that
A2: C in z and
A3: z in A by A1,TARSKI:def 4;
for b be object holds b in { C } implies b in z by A2,TARSKI:def 1;
then
A4: { C } c= z;
A5: z is Ordinal by A3,Th9;
then C c= z by A2,Def2;
then succ C c= z by A4,XBOOLE_1:8;
then succ C = z or succ C c< z;
then
A6: succ C = z or succ C in z by A5,Th7;
z c= A by A3,Def2;
hence thesis by A3,A6;
end;
assume
A7: for C st C in A holds succ C in A;
now
let a be object;
reconsider aa=a as set by TARSKI:1;
assume
A8: a in A;
then a is Ordinal by Th9;
then
A9: succ aa in A by A7,A8;
a in succ aa by Th2;
hence a in union A by A9,TARSKI:def 4;
end;
then
A10: A c= union A;
now
let a be object;
assume a in union A;
then consider z such that
A11: a in z and
A12: z in A by TARSKI:def 4;
z c= A by A12,Def2;
hence a in A by A11;
end;
then union A c= A;
then A = union A by A10;
hence thesis;
end;
theorem
not A is limit_ordinal iff ex B st A = succ B
proof
thus not A is limit_ordinal implies ex B st A = succ B
proof
assume not A is limit_ordinal;
then consider B such that
A1: B in A and
A2: not succ B in A by Th24;
take B;
assume
A3: A <> succ B;
succ B c= A by A1,Th17;
then succ B c< A by A3;
hence contradiction by A2,Th7;
end;
given B such that
A4: A = succ B;
B in A & not succ B in A by A4,Th2;
hence thesis by Th24;
end;
reserve F,G for Function;
::
:: 9. Transfinite sequences
::
definition
let IT be set;
attr IT is Sequence-like means
:Def7:
proj1 IT is ordinal;
end;
registration
cluster empty -> Sequence-like for set;
coherence;
end;
definition
mode Sequence is Sequence-like Function;
end;
registration
let Z;
cluster Z-valued for Sequence;
existence
proof
take {};
thus rng {} c= Z;
end;
end;
definition
let Z;
mode Sequence of Z is Z-valued Sequence;
end;
theorem
{} is Sequence of Z
proof
rng {} c= Z;
hence thesis by RELAT_1:def 19;
end;
reserve L,L1 for Sequence;
theorem
dom F is Ordinal implies F is Sequence of rng F by Def7,RELAT_1:def 19;
registration
let L;
cluster dom L -> ordinal;
coherence by Def7;
end;
theorem
X c= Y implies for L being Sequence of X holds L is Sequence of Y
proof
assume
A1: X c= Y;
let L be Sequence of X;
rng L c= X by RELAT_1:def 19;
then rng L c= Y by A1;
hence thesis by RELAT_1:def 19;
end;
registration
let L,A;
cluster L|A -> rng L-valued Sequence-like;
coherence
proof
A1: rng(L|A) c= rng L by RELAT_1:70;
A c= dom L implies dom(L|A) = A by RELAT_1:62;
hence thesis by A1,RELAT_1:68;
end;
end;
theorem
for L being Sequence of X for A holds L|A is Sequence of X;
definition
let IT be set;
attr IT is c=-linear means
:Def8:
for x,y being set st x in IT & y in IT holds x,y are_c=-comparable;
end;
theorem
(for a st a in X holds a is Sequence) & X is c=-linear implies
union X is Sequence
proof
assume that
A1: for a st a in X holds a is Sequence and
A2: X is c=-linear;
union X is Relation-like Function-like
proof
thus for a being object st a in union X
ex b,c being object st [b,c] = a
proof let a be object;
assume a in union X;
then consider x such that
A3: a in x and
A4: x in X by TARSKI:def 4;
reconsider x as Sequence by A1,A4;
for a being object st a in x
ex b,c being object st [b,c] = a by RELAT_1:def 1;
hence thesis by A3;
end;
let a,b,c be object;
assume that
A5: [a,b] in union X and
A6: [a,c] in union X;
consider y such that
A7: [a,c] in y and
A8: y in X by A6,TARSKI:def 4;
reconsider y as Sequence by A1,A8;
consider x such that
A9: [a,b] in x and
A10: x in X by A5,TARSKI:def 4;
reconsider x as Sequence by A1,A10;
x,y are_c=-comparable by A2,A10,A8;
then x c= y or y c= x;
hence thesis by A9,A7,FUNCT_1:def 1;
end;
then reconsider F = union X as Function;
defpred P[object,object] means $1 in X & for L st L = $1 holds dom L = $2;
A11: for a,b,c being object st P[a,b] & P[a,c] holds b = c
proof
let a,b,c be object;
assume that
A12: a in X and
A13: for L st L = a holds dom L = b and
a in X and
A14: for L st L = a holds dom L = c;
reconsider a as Sequence by A1,A12;
dom a = b by A13;
hence thesis by A14;
end;
consider G such that
A15: for a,b being object holds [a,b] in G iff a in X & P[a,b]
from FUNCT_1:sch 1(A11);
A16: for a,b being object holds [a,b] in G implies b is Ordinal
proof let a,b be object;
assume
A17: [a,b] in G;
then a in X by A15;
then reconsider a as Sequence by A1;
dom a = b by A15,A17;
hence thesis;
end;
a in rng G implies a is Ordinal
proof
assume a in rng G;
then consider b being object such that
A18: b in dom G & a = G.b by FUNCT_1:def 3;
[b,a] in G by A18,FUNCT_1:1;
hence thesis by A16;
end;
then consider A such that
A19: rng G c= A by Th20;
defpred P[Ordinal] means for B st B in rng G holds B c= $1;
for B st B in rng G holds B c= A by A19,Def2;
then
A20: ex A st P[A];
consider A such that
A21: P[A] & for C st P[C] holds A c= C from OrdinalMin(A20);
dom F = A
proof
thus for a be object holds a in dom F implies a in A
proof let a be object;
assume a in dom F;
then consider b being object such that
A22: [a,b] in F by XTUPLE_0:def 12;
consider x such that
A23: [a,b] in x and
A24: x in X by A22,TARSKI:def 4;
reconsider x as Sequence by A1,A24;
for L st L = x holds dom L = dom x;
then [x,dom x] in G by A15,A24;
then x in dom G & dom x = G.x by FUNCT_1:1;
then dom x in rng G by FUNCT_1:def 3;
then
A25: dom x c= A by A21;
a in dom x by A23,XTUPLE_0:def 12;
hence thesis by A25;
end;
let a be object;
assume
A26: a in A;
then reconsider a9 = a as Ordinal by Th9;
now
assume
A27: for L st L in X holds not a9 in dom L;
now
let B;
assume B in rng G;
then consider c being object such that
A28: c in dom G & B = G.c by FUNCT_1:def 3;
A29: [c,B] in G by A28,FUNCT_1:1;
then c in X by A15;
then reconsider c as Sequence by A1;
c in X & dom c = B by A15,A29;
hence B c= a9 by A27,Th12;
end;
then
A30: A c= a9 by A21;
a9 c= A by A26,Def2;
then A: A = a by A30,XBOOLE_0:def 10;
reconsider aa = a as set by TARSKI:1;
not aa in aa;
hence contradiction by A,A26;
end;
then consider L such that
A31: L in X & a in dom L;
L c= F & ex b being object st [a,b] in L
by A31,XTUPLE_0:def 12,ZFMISC_1:74;
hence thesis by XTUPLE_0:def 12;
end;
hence thesis by Def7;
end;
::
:: 10. Schemes of definability by transfinite induction
::
scheme
TSUniq { A()->Ordinal, H(Sequence)->set, L1, L2() -> Sequence } :
L1() = L2()
provided
A1: dom L1() = A() & for B,L st B in A() & L = L1()|B holds L1().B = H(L) and
A2: dom L2() = A() & for B,L st B in A() & L = L2()|B holds L2().B = H(L)
proof
defpred P[object] means L1().$1 <> L2().$1;
consider X such that
A3: for x being object holds x in X iff x in A() & P[x] from XBOOLE_0:sch 1;
for b be object holds b in X implies b in A() by A3;
then
A4: X c= A();
assume L1() <> L2();
then ex a being object st a in A() & L1().a <> L2().a by A1,A2;
then X <> {} by A3;
then consider B such that
A5: B in X and
A6: for C st C in X holds B c= C by A4,Th16;
A7: B in A() by A3,A5;
then
A8: B c= A() by Def2;
then
A9: dom(L1()|B) = B by A1,RELAT_1:62;
A10: dom(L2()|B) = B by A2,A8,RELAT_1:62;
A11: now
let C;
assume
A12: C in B;
then not C in X by A6,Th1;
hence L1().C = L2().C by A3,A8,A12;
end;
now
let a be object;
assume
A13: a in B;
then reconsider a9 = a as Ordinal by Th9;
L1().a9 = L2().a9 & L1()|B.a = L1().a by A11,A9,A13,FUNCT_1:47;
hence L1()|B.a = L2()|B.a by A10,A13,FUNCT_1:47;
end;
then
A14: L1()|B = L2()|B by A9,A10;
L1().B = H(L1()|B) & L2().B = H(L2()|B) by A1,A2,A7;
hence contradiction by A3,A5,A14;
end;
scheme
TSExist { A()->Ordinal,H(Sequence)->set } : ex L st dom L = A() & for B,L1
st B in A() & L1 = L|B holds L.B = H(L1) proof
defpred S[Ordinal] means ex L st dom L = $1 & for B st B in $1 holds L.B = H
(L|B);
A1: for B st for C st C in B holds S[C] holds S[B]
proof
defpred P[object,object] means
$1 is Ordinal & $2 is Sequence & for A,L st A =
$1 & L = $2 holds dom L = A & for B st B in A holds L.B = H(L|B);
let B such that
A2: for C st C in B ex L st dom L = C & for D st D in C holds L.D = H( L|D);
A3: for a,b,c being object st P[a,b] & P[a,c] holds b = c
proof
let a,b,c be object;
assume that
A4: a is Ordinal and
A5: b is Sequence and
A6: for A,L st A = a & L = b holds dom L = A & for B st B in A holds
L.B = H(L|B) and
a is Ordinal and
A7: c is Sequence and
A8: for A,L st A = a & L = c holds dom L = A & for B st B in A holds
L.B = H(L|B);
reconsider c as Sequence by A7;
reconsider a as Ordinal by A4;
A9: dom c = a & for B,L st B in a & L=c|B holds c.B = H(L) by A8;
reconsider b as Sequence by A5;
A10: dom b = a & for B,L st B in a & L=b|B holds b.B = H(L) by A6;
b = c from TSUniq(A10,A9);
hence thesis;
end;
consider G such that
A11: for a,b being object holds [a,b] in G iff a in B & P[a,b]
from FUNCT_1:sch 1(A3);
defpred R[object,object] means ex L st L = G.$1 & $2 = H(L);
A12: dom G = B
proof
thus for a be object holds a in dom G implies a in B
proof let a be object;
assume a in dom G;
then ex b being object st [a,b] in G by XTUPLE_0:def 12;
hence thesis by A11;
end;
let a be object;
assume
A13: a in B;
then reconsider a9 = a as Ordinal by Th9;
consider L such that
A14: dom L = a9 & for D st D in a9 holds L.D = H(L|D) by A2,A13;
for A holds for K be Sequence holds A = a9 & K = L implies dom K
= A & for B holds B in A implies K.B = H(K|B) by A14;
then [a9,L] in G by A11,A13;
hence thesis by XTUPLE_0:def 12;
end;
A15: for a being object st a in B ex b being object st R[a,b]
proof
let a be object;
assume a in B;
then consider c being object such that
A16: [a,c] in G by A12,XTUPLE_0:def 12;
reconsider L = c as Sequence by A11,A16;
take H(L), L;
thus L = G.a by A16,FUNCT_1:1;
thus thesis;
end;
A17: for a,b,c being object st a in B & R[a,b] & R[a,c] holds b = c;
consider F such that
A18: dom F = B & for a being object st a in B holds R[a,F.a] from FUNCT_1
:sch 2(A17,A15);
reconsider L = F as Sequence by A18,Def7;
take L;
thus dom L = B by A18;
let D;
assume
A19: D in B;
then consider K being Sequence such that
A20: K = G.D and
A21: F.D = H(K) by A18;
A22: [D,K] in G by A12,A19,A20,FUNCT_1:1;
then
A23: dom K = D by A11;
A24: now
let C;
assume
A25: C in D;
A26: now
let A,L such that
A27: A = C and
A28: L = K|C;
A29: C c= D by A25,Def2;
hence
A30: dom L = A by A23,A27,A28,RELAT_1:62;
let B;
assume
A31: B in A;
then B c= A by Def2;
then
A32: K|B = L|B by A27,A28,FUNCT_1:51;
K.B = H(K|B) by A11,A22,A27,A29,A31;
hence L.B = H(L|B) by A28,A30,A31,A32,FUNCT_1:47;
end;
C in B by A19,A25,Th6;
then [C,K|C] in G by A11,A26;
hence G.C = K|C by FUNCT_1:1;
end;
A33: now
let a be object;
assume
A34: a in D;
then reconsider A = a as Ordinal by Th9;
A35: G.A = K|A & L|D.A = L.A by A24,A34,FUNCT_1:49;
ex J being Sequence st J = G.A & F.A = H(J) by A18,A19,A34,Th6;
hence L|D.a = K.a by A11,A22,A34,A35;
end;
D c= dom L by A18,A19,Def2;
then dom(L|D) = D by RELAT_1:62;
hence thesis by A21,A23,A33,FUNCT_1:2;
end;
for A holds S[A] from TransfiniteInd(A1);
then consider L such that
A36: dom L = A() and
A37: for B st B in A() holds L.B = H(L|B);
take L;
thus dom L = A() by A36;
let B,L1;
thus thesis by A37;
end;
scheme
FuncTS { L() -> Sequence, F(Ordinal)->set, H(Sequence)->set } :
for B st B in dom L() holds L().B = H(L()|B)
provided
A1: for A,a holds a = F(A) iff ex L st a = H(L) & dom L = A & for B st B
in A holds L.B = H(L|B) and
A2: for A st A in dom L() holds L().A = F(A);
consider L such that
F(dom L()) = H(L) and
A3: dom L = dom L() and
A4: for B st B in dom L() holds L.B = H(L|B) by A1;
now
let b be object;
assume
A5: b in dom L;
then reconsider B = b as Ordinal by Th9;
now
take K = L|B;
thus H(L|B) = H(K);
A6: B c= dom L by A5,Def2;
hence dom K = B by RELAT_1:62;
let C;
assume
A7: C in B;
then C c= B by Def2;
then
A8: L|C = K|C by FUNCT_1:51;
K.C = L.C by A7,FUNCT_1:49;
hence K.C = H(K|C) by A3,A4,A6,A7,A8;
end;
then F(B) = H(L|B) by A1
.= L.B by A3,A4,A5;
hence L().b = L.b by A2,A3,A5;
end;
then L() = L by A3;
hence thesis by A4;
end;
theorem
A c< B or A = B or B c< A
proof
assume that
A1: not A c< B & not A = B and
A2: not B c< A;
not A c= B by A1;
hence contradiction by A2;
end;
begin :: Addenda
:: moved from ORDINAL2, 2006.06.22, A.T.
definition
let X;
func On X -> set means
:Def9:
for x being object holds x in it iff x in X & x is Ordinal;
existence
proof
defpred P[object] means $1 is Ordinal;
thus ex Y being set st
for x being object holds x in Y iff x in X & P[x] from XBOOLE_0:sch 1;
end;
uniqueness
proof
defpred P[object] means $1 in X & $1 is Ordinal;
let Y,Z such that
A1: for x being object holds x in Y iff P[x] and
A2: for x being object holds x in Z iff P[x];
thus Y = Z from XBOOLE_0:sch 2(A1,A2);
end;
func Lim X -> set means
for x being object holds x in it iff
x in X & ex A st x = A & A is limit_ordinal;
existence
proof
defpred P[object] means ex A st $1 = A & A is limit_ordinal;
thus ex Y being set st
for x being object holds x in Y iff x in X & P[x] from XBOOLE_0:sch 1;
end;
uniqueness
proof
defpred P[object] means $1 in X & ex A st $1 = A & A is limit_ordinal;
let Y,Z such that
A3: for x being object holds x in Y iff P[x] and
A4: for x being object holds x in Z iff P[x];
thus Y = Z from XBOOLE_0:sch 2(A3,A4);
end;
end;
::$N Generalized Axiom of Infinity
theorem Th32:
for D ex A st D in A & A is limit_ordinal
proof
let D;
consider Field being set such that
A1: D in Field and
A2: for X,Y holds X in Field & Y c= X implies Y in Field and
A3: for X holds X in Field implies bool X in Field and
for X holds X c= Field implies X,Field are_equipotent or X in Field
by ZFMISC_1:112;
for X st X in On Field holds X is Ordinal & X c= On Field
proof
let X;
assume
A4: X in On Field;
then reconsider A = X as Ordinal by Def9;
A5: A in Field by A4,Def9;
thus X is Ordinal by A4,Def9;
let y be object;
assume
A6: y in X;
then y in A;
then reconsider B = y as Ordinal by Th9;
B c= A by A6,Def2;
then B in Field by A2,A5;
hence thesis by Def9;
end;
then reconsider ON = On Field as epsilon-transitive epsilon-connected set
by Th15;
take ON;
thus D in ON by A1,Def9;
A in ON implies succ A in ON
proof
A7: succ A c= bool A
proof
let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in succ A;
then x in A or x = A by Th4;
then xx c= A by Def2;
hence thesis;
end;
assume A in ON;
then A in Field by Def9;
then bool A in Field by A3;
then succ A in Field by A2,A7;
hence thesis by Def9;
end;
hence thesis by Th24;
end;
definition
func omega -> set means
:Def11:
{} in it & it is limit_ordinal & it is ordinal &
for A st {} in A & A is limit_ordinal holds it c= A;
existence
proof
defpred P[Ordinal] means {} in $1 & $1 is limit_ordinal;
A1: ex A st P[A] by Th32;
ex C st P[C] & for A st P[A] holds C c= A from OrdinalMin(A1);
hence thesis;
end;
uniqueness;
end;
registration
cluster omega -> non empty ordinal;
coherence by Def11;
end;
definition
let A be object;
attr A is natural means
:Def12:
A in omega;
end;
registration
cluster natural for Number;
existence
proof
take the Element of omega;
thus thesis;
end;
cluster natural for set;
existence
proof
take the Element of omega;
thus thesis;
end;
end;
definition
mode Nat is natural number;
end;
registration
sethood of Nat
proof
take omega;
let y be Nat;
thus y in omega by Def12;
end;
end;
:: from ARYTM_3, 2006.05.26
registration
let A be Ordinal;
cluster -> ordinal for Element of A;
coherence
proof
let x be Element of A;
A is empty or A is non empty;
hence thesis by Th9,SUBSET_1:def 1;
end;
end;
:: missing, 2006.06.25, A.T.
registration
cluster natural -> ordinal for number;
coherence;
end;
:: from ZF_REFLE, 2007,03.13, A.T.
scheme
ALFA { D() -> non empty set, P[object,object] }:
ex F st dom F = D() & for d being
Element of D() ex A st A = F.d & P[d,A] & for B st P[d,B] holds A c= B
provided
A1: for d being Element of D() ex A st P[d,A]
proof
defpred Q[object,object] means
ex A st A = $2 & P[$1,A] & for B st P[$1,B] holds A
c= B;
A2: for x being object st x in D() ex y being object st Q[x,y]
proof
let x be object;
assume x in D();
then reconsider d = x as Element of D();
defpred Q[Ordinal] means P[d,$1];
A3: ex A st Q[A] by A1;
consider A such that
A4: Q[A] & for B st Q[B] holds A c= B from OrdinalMin(A3);
reconsider y = A as set;
take y,A;
thus thesis by A4;
end;
A5: for x,y,z being object st x in D() & Q[x,y] & Q[x,z] holds y = z
proof
let x,y,z being object such that
x in D();
given A1 being Ordinal such that
A6: A1 = y and
A7: ( P[x,A1])& for B st P[x,B] holds A1 c= B;
given A2 being Ordinal such that
A8: A2 = z and
A9: ( P[x,A2])& for B st P[x,B] holds A2 c= B;
A1 c= A2 & A2 c= A1 by A7,A9;
hence thesis by A6,A8,XBOOLE_0:def 10;
end;
consider F such that
A10: dom F = D() &
for x being object st x in D() holds Q[x,F.x] from FUNCT_1:sch 2(
A5, A2);
take F;
thus dom F = D() by A10;
let d be Element of D();
thus thesis by A10;
end;
:: from CARD_4, 2007.08.06, A.T.
theorem
succ X \ {X} = X
proof
thus succ X \ {X} c= X
proof
let x be object;
assume
A1: x in succ X \ {X};
then
A2: not x in {X} by XBOOLE_0:def 5;
x in X or x = X by A1,Th4;
hence thesis by A2,TARSKI:def 1;
end;
let x be object;
assume
A3: x in X; then
reconsider xx = x as set;
not xx in xx;
then x <> X by A3;
then
A4: not x in {X} by TARSKI:def 1;
x in succ X by A3,Th4;
hence thesis by A4,XBOOLE_0:def 5;
end;
:: from ARYTM_3, 2007.09.16, A.T.
registration
cluster empty -> natural for number;
coherence
by Def11;
cluster -> natural for Element of omega;
coherence;
end;
registration
cluster non empty natural for number;
existence
proof
take succ{};
thus succ{} is non empty;
omega is limit_ordinal & {} in omega by Def11;
hence succ{} in omega by Th24;
end;
end;
:: from ARYTM_3, 2007.10.23, A.T.
registration
let a be natural Ordinal;
cluster succ a -> natural;
coherence
proof
omega is limit_ordinal & a in omega by Def11,Def12;
hence succ a in omega by Th24;
end;
end;
:: from DILWORTH, 2011.07.31,A.T.
registration
cluster empty -> c=-linear for set;
coherence;
end;
registration let X be c=-linear set;
cluster -> c=-linear for Subset of X;
coherence
by Def8;
end;
::$CT
definition
func 0 -> number equals {};
coherence;
end;
registration
cluster 0 -> natural;
coherence;
end;
definition
let x be Number;
attr x is zero means
:Def14: x = 0;
end;
registration
cluster 0 -> zero;
coherence;
cluster zero for Number;
existence
proof
take 0;
thus 0 = 0;
end;
cluster zero for set;
existence
proof
take 0;
thus 0 = 0;
end;
end;
registration
cluster zero -> natural for Number;
coherence;
end;
registration
cluster non zero for Number;
existence
proof
take {0};
thus {0} <> 0;
end;
end;
registration
cluster zero -> trivial for set;
coherence;
cluster non trivial -> non zero for set;
coherence;
end;
definition let R be Relation;
attr R is non-zero means
:Def15: not 0 in rng R;
end;
definition let X be set;
attr X is with_zero means
:Def16: 0 in X;
end;
notation let X be set;
antonym X is without_zero for X is with_zero;
end;
registration
cluster empty -> without_zero for set;
coherence;
end;
registration
cluster empty -> non-zero for Relation;
coherence;
end;
registration
cluster without_zero non empty for set;
existence
proof
take {{0}};
thus not 0 in {{0}} by TARSKI:def 1;
thus thesis;
end;
end;
registration let X be without_zero non empty set;
cluster -> non zero for Element of X;
coherence by Def16;
end;
registration
cluster non-zero for Relation;
existence
proof
take {};
thus not 0 in rng {};
end;
cluster non non-zero for Relation;
existence
proof
take R = {[0,0]};
[0,0] in R by TARSKI:def 1;
hence 0 in rng R by XTUPLE_0:def 13;
end;
end;
registration let R be non-zero Relation;
cluster rng R -> without_zero;
coherence by Def15;
end;
registration let R be non non-zero Relation;
cluster rng R -> with_zero;
coherence by Def15;
end;
registration let R be non-zero Relation, S be Relation;
cluster S*R -> non-zero;
coherence
proof
rng(S*R) c= rng R by RELAT_1:26;
hence not 0 in rng(S*R);
end;
end;
:: to be removed
registration
cluster without_zero -> with_non-empty_elements for set;
coherence
proof let X be set;
assume X is without_zero;
hence not {} in X;
end;
cluster with_zero -> non with_non-empty_elements for set;
coherence
proof let X be set;
assume X is with_zero;
hence {} in X;
end;
cluster with_non-empty_elements -> without_zero for set;
coherence;
cluster non with_non-empty_elements -> with_zero for set;
coherence;
end;
definition let o be object;
func Segm o -> set equals o;
coherence by TARSKI:1;
end;
registration let n be Ordinal;
cluster Segm n -> ordinal;
coherence;
end;
registration let n be zero Ordinal;
cluster Segm n -> empty;
coherence by Def14;
end;