:: Veblen Hierarchy
:: by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010-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 ORDINAL6, CARD_1, RELAT_1, FUNCT_1, CLASSES2, NUMBERS, TARSKI,
XBOOLE_0, SUBSET_1, ORDINAL1, ORDINAL2, WELLORD1, WELLORD2, ABIAN,
CARD_3, MATROID0, ORDINAL4, NAT_1, ARYTM_3, CLASSES1, VALUED_0, AFINSQ_1,
ORDINAL5, ZFMISC_1, FINSET_1, MESFUNC8, NAGATA_1, ORDINAL3, PRE_TOPC,
AOFA_000;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1,
FUNCT_2, FINSET_1, ORDINAL1, ORDINAL2, XCMPLX_0, NAT_1, ORDINAL3, ABIAN,
WELLORD1, WELLORD2, CARD_1, ORDINAL4, CARD_3, AFINSQ_1, CLASSES1,
CLASSES2, NUMBERS, ORDINAL5;
constructors WELLORD1, WELLORD2, CLASSES1, ABIAN, CARD_3, AFINSQ_1, ORDINAL3,
ORDINAL5, NAT_1, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, RELSET_1, FUNCT_1, FINSET_1, FUNCT_2,
ORDINAL1, ORDINAL2, CARD_1, WELLORD2, ORDINAL3, CLASSES2, CARD_5,
ORDINAL4, CARD_LAR, ORDINAL5, CLASSES1, AFINSQ_1, SUBSET_1;
requirements SUBSET, BOOLE, NUMERALS;
definitions TARSKI, XBOOLE_0, FUNCT_1, WELLORD1, ABIAN, ORDINAL1, ORDINAL2,
CARD_3, ORDINAL5;
equalities ORDINAL1, ORDINAL2, ORDINAL4, CARD_3;
expansions TARSKI, XBOOLE_0, FUNCT_1, WELLORD1, ABIAN, ORDINAL1, ORDINAL2,
ORDINAL5;
theorems XBOOLE_1, ZFMISC_1, RELAT_1, FUNCT_1, ORDINAL1, ORDINAL2, ORDINAL3,
FUNCT_3, WELLORD1, WELLORD2, ORDERS_1, CARD_2, CARD_5, FUNCT_2, ORDINAL4,
XBOOLE_0, TARSKI, ORDINAL5, NAT_1, CLASSES1, CLASSES2, CARD_1, AFINSQ_1,
NAT_2, GRFUNC_1;
schemes NAT_1, ORDINAL1, ORDINAL2, ORDINAL4, TREES_2;
begin :: Preliminaries
reserve a,b,c,d for Ordinal;
reserve l for non empty limit_ordinal Ordinal;
reserve u for Element of l;
reserve A for non empty Ordinal;
reserve e for Element of A;
reserve X,Y,x,y,z for set;
reserve n,m for Nat;
definition
let X be set;
attr X is ordinal-membered means :Def1:
ex a st X c= a;
end;
registration
cluster ordinal -> ordinal-membered for set;
coherence;
let X;
cluster On X -> ordinal-membered;
coherence
proof
take sup X;
thus thesis by ORDINAL2:def 3;
end;
end;
theorem Th1:
X is ordinal-membered iff for x st x in X holds x is ordinal
proof
thus X is ordinal-membered implies for x st x in X holds x is ordinal;
assume
A1: for x st x in X holds x is ordinal;
take a = sup X;
let x be object; assume
A2: x in X; then
x is Ordinal by A1;
hence thesis by A2,ORDINAL2:19;
end;
registration
cluster ordinal-membered for set;
existence
proof
take 0,0;
thus 0 c= 0;
end;
end;
registration
let X be ordinal-membered set;
cluster -> ordinal for Element of X;
coherence
proof
let a be Element of X;
per cases;
suppose X is empty;
hence thesis;
end;
suppose X is non empty;
hence thesis by Th1;
end;
end;
end;
theorem Th2:
X is ordinal-membered iff On X = X
proof
hereby assume
A1: X is ordinal-membered;
thus On X = X
proof thus On X c= X by ORDINAL2:7;
let x be object;
thus thesis by A1,ORDINAL1:def 9;
end;
end;
thus thesis;
end;
theorem
for X being ordinal-membered set holds X c= sup X
by ORDINAL2:19;
theorem Th4:
a c= b iff b nin a
proof
a c= b & b in a implies b in b;
hence thesis by ORDINAL1:16;
end;
theorem
x in a\b iff b c= x & x in a
proof
x in a\b iff x nin b & x in a by XBOOLE_0:def 5;
hence thesis by Th4;
end;
registration let a,b;
cluster a\b -> ordinal-membered;
coherence;
end;
theorem Th6:
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y
for x,y st x in X & y in X holds x c= y iff f.x c= f.y
proof
let f be Function; assume
A1: f is_isomorphism_of RelIncl X, RelIncl Y;
let x,y such that
A2: x in X & y in X;
A3: field RelIncl X = X & field RelIncl Y = Y by WELLORD2:def 1; then
dom f = X & rng f = Y by A1; then
A4: f.x in Y & f.y in Y by A2,FUNCT_1:def 3;
x c= y iff [x,y] in RelIncl X by A2,WELLORD2:def 1; then
x c= y iff [f.x,f.y] in RelIncl Y by A1,A2,A3;
hence thesis by A4,WELLORD2:def 1;
end;
theorem
for X,Y being ordinal-membered set
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y
for x,y st x in X & y in X holds x in y iff f.x in f.y
proof
let X,Y be ordinal-membered set;
let f be Function; assume
A1: f is_isomorphism_of RelIncl X, RelIncl Y;
let x,y;
assume
A2: x in X & y in X;
field RelIncl X = X & field RelIncl Y = Y by WELLORD2:def 1; then
dom f = X & rng f = Y by A1; then
f.x in Y & f.y in Y by A2,FUNCT_1:def 3; then
reconsider a=f.x,b=f.y,x,y as Ordinal by A2;
y c= x iff b c= a by A1,A2,Th6;
hence thesis by Th4;
end;
theorem Th8:
[x,y] in RelIncl X implies x c= y
proof assume
A1: [x,y] in RelIncl X;
field RelIncl X = X by WELLORD2:def 1; then
x in X & y in X by A1,RELAT_1:15;
hence x c= y by A1,WELLORD2:def 1;
end;
theorem Th9:
for f1,f2 being Sequence holds f1 c= f1^f2
proof
let f1,f2 be Sequence;
dom(f1^f2) = (dom f1)+^dom f2 by ORDINAL4:def 1; then
A1: dom f1 c= dom(f1^f2) by ORDINAL3:24;
for x being object st x in dom f1 holds f1.x = (f1^f2).x
by ORDINAL4:def 1;
hence f1 c= f1^f2 by A1,GRFUNC_1:2;
end;
::$CT
Th10:
for f1,f2 being Sequence holds rng(f1^f2) = rng f1 \/ rng f2
by ORDINAL4:2;
theorem Th11:
a c= b iff epsilon_a c= epsilon_b
proof
hereby assume
a c= b; then
a = b or a c< b; then
a = b or epsilon_a in epsilon_b by ORDINAL1:11,ORDINAL5:44;
hence epsilon_a c= epsilon_b by ORDINAL1:def 2;
end;
assume
A1: epsilon_a c= epsilon_b;
assume a c/= b; then
epsilon_b in epsilon_a by ORDINAL1:16,ORDINAL5:44; then
epsilon_b in epsilon_b by A1;
hence thesis;
end;
theorem Th12:
a in b iff epsilon_a in epsilon_b
proof
b c/= a iff epsilon_b c/= epsilon_a by Th11;
hence thesis by Th4;
end;
registration
let X be ordinal-membered set;
cluster union X -> ordinal;
coherence
proof
ex a st X c= a by Def1;
hence thesis by ORDINAL3:4;
end;
end;
registration
let f be Ordinal-yielding Function;
cluster rng f -> ordinal-membered;
coherence
by ORDINAL2:def 4;
end;
registration
let a;
cluster id a -> Sequence-like Ordinal-yielding;
coherence;
end;
registration
let a;
cluster id a -> increasing for Ordinal-Sequence;
coherence
proof
let f be Ordinal-Sequence such that
A1: f = id a;
let b,c; assume
A2: b in c & c in dom f; then
b in dom f & dom f = a by A1,ORDINAL1:10; then
f.b = b & f.c = c by A1,A2,FUNCT_1:18;
hence thesis by A2;
end;
end;
registration
let a;
cluster id a -> continuous for Ordinal-Sequence;
coherence
proof
let f be Ordinal-Sequence such that
A1: f = id a;
let b,c; assume
A2: b in dom f & b <> 0 & b is limit_ordinal & c = f.b;
set g = f|b;
A3: dom f = a & dom id b = b by A1;
A4: c = b by A1,A2,FUNCT_1:18;
b c= a by A2,A3,ORDINAL1:def 2; then
A5: g = id b by A1,FUNCT_3:1;
per cases;
case c = 0;
hence thesis by A2,A1,FUNCT_1:18;
end;
case c <> 0;
let B,C be Ordinal; assume
A6: B in c & c in C;
take D = succ B;
thus D in dom g by A2,A4,A5,A6,ORDINAL1:28;
let E be Ordinal; assume
A7: D c= E & E in dom g; then
g.E = E by A5,FUNCT_1:18;
hence B in g.E & g.E in C by A4,A5,A6,A7,ORDINAL1:10,21;
end;
end;
end;
registration
cluster non empty increasing continuous for Ordinal-Sequence;
existence
proof
set A = the non empty Ordinal;
take id A;
thus thesis;
end;
end;
definition
let f be Sequence;
attr f is normal means
f is increasing continuous Ordinal-Sequence;
end;
definition
let f be Ordinal-Sequence;
redefine attr f is normal means :: redefines normal (ORDINAL6, definition)
f is increasing continuous;
compatibility;
end;
registration
cluster normal -> Ordinal-yielding for Sequence;
coherence;
cluster normal -> increasing continuous for Ordinal-Sequence;
coherence;
cluster increasing continuous -> normal for Ordinal-Sequence;
coherence;
end;
registration
cluster non empty normal for Sequence;
existence
proof
set A = the non empty Ordinal;
take id A;
thus thesis;
end;
end;
theorem Th13:
for f being Ordinal-Sequence holds
f is non-decreasing implies f|a is non-decreasing
proof let f be Ordinal-Sequence;
assume
A1: for b,c st b in c & c in dom f holds f.b c= f.c;
let b,c; assume
A2: b in c & c in dom(f|a); then
A3: c in dom f & c in a by RELAT_1:57; then
(f|a).b = f.b & (f|a).c = f.c by A2,FUNCT_1:49,ORDINAL1:10;
hence thesis by A1,A2,A3;
end;
definition
let X;
func ord-type X -> Ordinal equals
order_type_of RelIncl On X;
coherence;
end;
definition
let X be ordinal-membered set;
redefine func ord-type X equals order_type_of RelIncl X; :: redefines ord-type (ORDINAL6, definition)
compatibility by Th2;
end;
registration
let X be ordinal-membered set;
cluster RelIncl X -> well-ordering;
coherence
proof
ex a st X c= a by Def1;
hence thesis by WELLORD2:8;
end;
end;
registration
let E be empty set;
cluster On E -> empty;
coherence by ORDINAL2:7,XBOOLE_1:3;
end;
registration
let E be empty set;
cluster order_type_of E -> empty;
coherence
proof
RelIncl E = E;
hence thesis by ORDERS_1:88;
end;
end;
theorem
ord-type {} = 0;
theorem
ord-type {a} = 1
proof
a in succ a by ORDINAL1:6; then
A1: {a} c= succ a by ZFMISC_1:31; then
order_type_of RelIncl {a} = 1 by CARD_5:37;
hence thesis by A1,ORDINAL3:6;
end;
theorem
a <> b implies ord-type {a,b} = 2
proof
assume a <> b; then
A1: card {a,b} = 2 by CARD_2:57;
a c= a\/b & b c= a\/b by XBOOLE_1:7; then
a in succ(a\/b) & b in succ(a\/b) by ORDINAL1:22; then
A2: {a,b} c= succ(a\/b) by ZFMISC_1:32; then
On {a,b} = {a,b} by ORDINAL3:6;
hence thesis by A1,A2,CARD_5:36;
end;
theorem
ord-type a = a by ORDERS_1:88;
definition
let X;
func numbering X -> Ordinal-Sequence equals
canonical_isomorphism_of(RelIncl ord-type X, RelIncl On X);
coherence
proof
set R1 = RelIncl ord-type X;
set R2 = RelIncl On X;
set f = canonical_isomorphism_of(R1, R2);
consider a such that
A1: On X c= a by Def1;
ex phi being Ordinal-Sequence st phi = f &
phi is increasing & dom phi = ord-type X & rng phi = On X
by A1,CARD_5:5;
hence thesis;
end;
end;
theorem Th18:
dom numbering X = ord-type X & rng numbering X = On X
proof
set R1 = RelIncl ord-type X;
set R2 = RelIncl On X;
set f = canonical_isomorphism_of(R1, R2);
consider a such that
A1: On X c= a by Def1;
ex phi being Ordinal-Sequence st phi = f &
phi is increasing & dom phi = ord-type X & rng phi = On X
by A1,CARD_5:5;
hence thesis;
end;
theorem Th19:
for X being ordinal-membered set holds rng numbering X = X
proof
let X be ordinal-membered set;
thus rng numbering X = On X by Th18 .= X by Th2;
end;
theorem
card dom numbering X = card On X
proof
dom numbering X = ord-type X &
ex a st On X c= a by Th18,Def1;
hence thesis by CARD_5:7;
end;
theorem Th21:
numbering X is_isomorphism_of RelIncl ord-type X, RelIncl On X
proof
set R1 = RelIncl ord-type X;
set R2 = RelIncl On X;
R2,R1 are_isomorphic by WELLORD2:def 2; then
R1,R2 are_isomorphic by WELLORD1:40;
hence thesis by WELLORD1:def 9;
end;
reserve f for Ordinal-Sequence;
theorem Th22:
f = numbering X & x in dom f & y in dom f implies (x c= y iff f.x c= f.y)
proof assume
A1: f = numbering X & x in dom f & y in dom f; then
dom f = ord-type X &
f is_isomorphism_of RelIncl ord-type X, RelIncl On X by Th18,Th21;
hence thesis by A1,Th6;
end;
theorem Th23:
f = numbering X & x in dom f & y in dom f implies (x in y iff f.x in f.y)
proof assume
A1: f = numbering X & x in dom f & y in dom f; then
y c= x iff f.y c= f.x by Th22;
hence thesis by A1,Th4;
end;
registration
let X;
cluster numbering X -> increasing;
coherence
proof
set R1 = RelIncl ord-type X;
set R2 = RelIncl On X;
set f = canonical_isomorphism_of(R1, R2);
consider a such that
A1: On X c= a by Def1;
ex phi being Ordinal-Sequence st phi = f &
phi is increasing & dom phi = ord-type X & rng phi = On X
by A1,CARD_5:5;
hence thesis;
end;
end;
registration
let X,Y be ordinal-membered set;
cluster X \/ Y -> ordinal-membered;
coherence
proof
consider a such that
A1: X c= a by Def1;
consider b such that
A2: Y c= b by Def1;
take a \/ b;
thus thesis by A1,A2,XBOOLE_1:13;
end;
end;
registration
let X be ordinal-membered set, Y be set;
cluster X \ Y -> ordinal-membered;
coherence
proof
consider a such that
A1: X c= a by Def1;
take a;
thus thesis by A1;
end;
end;
theorem Th24:
for X,Y being ordinal-membered set
st for x,y st x in X & y in Y holds x in y
holds (numbering X)^(numbering Y) is_isomorphism_of
RelIncl ((ord-type X)+^(ord-type Y)), RelIncl (X \/ Y)
proof
let X,Y be ordinal-membered set; assume
A1: for x,y st x in X & y in Y holds x in y;
set f = numbering X, g = numbering Y;
set a = ord-type X, b = ord-type Y;
set R = RelIncl(a+^b), Q = RelIncl(X\/Y);
set R1 = RelIncl a, Q1 = RelIncl(X);
set R2 = RelIncl b, Q2 = RelIncl(Y);
A2: dom(f^g) = (dom f)+^dom g by ORDINAL4:def 1;
A3: dom f = a & dom g = b by Th18;
A4: rng f = X & rng g = Y by Th19;
A5: f is_isomorphism_of RelIncl a, RelIncl On X &
g is_isomorphism_of RelIncl b, RelIncl On Y by Th21; then
A6: f is one-to-one & g is one-to-one;
thus
A7: dom(f^g) = (dom f)+^dom g by ORDINAL4:def 1
.= field R by A3,WELLORD2:def 1;
thus rng(f^g) = (rng f)\/rng g by Th10
.= field Q by A4,WELLORD2:def 1; then
A8: rng(f^g) = X\/Y by WELLORD2:def 1;
A9: On X = X & On Y = Y by Th2;
thus f^g is one-to-one
proof
let x,y be object; assume
A10: x in dom(f^g) & y in dom(f^g) & (f^g).x = (f^g).y; then
reconsider a = x, b = y as Ordinal;
per cases by ORDINAL1:16;
suppose
A11: x in dom f & y in dom f; then
(f^g).x = f.x & (f^g).y = f.y by ORDINAL4:def 1;
hence thesis by A6,A10,A11;
end;
suppose
A12: x in dom f & dom f c= b; then
A13: (dom f)+^(b-^dom f) = y by ORDINAL3:def 5; then
A14: b-^dom f in dom g by A2,A10,ORDINAL3:22; then
(f^g).x = f.x & (f^g).y = g.(b-^dom f) by A12,A13,ORDINAL4:def 1; then
f.x in X & f.x in Y by A4,A10,A12,A14,FUNCT_1:def 3; then
f.x in f.x by A1;
hence thesis;
end;
suppose
A15: dom f c= a & y in dom f; then
A16: (dom f)+^(a-^dom f) = x by ORDINAL3:def 5; then
A17: a-^dom f in dom g by A2,A10,ORDINAL3:22; then
(f^g).y = f.y & (f^g).x = g.(a-^dom f) by A15,A16,ORDINAL4:def 1; then
f.y in X & f.y in Y by A4,A10,A15,A17,FUNCT_1:def 3; then
f.y in f.y by A1;
hence thesis;
end;
suppose dom f c= a & dom f c= b; then
A18: (dom f)+^(a-^dom f) = x & (dom f)+^(b-^dom f) = y
by ORDINAL3:def 5; then
A19: a-^dom f in dom g & b-^dom f in dom g by A2,A10,ORDINAL3:22; then
(f^g).y = g.(b-^dom f) & (f^g).x = g.(a-^dom f) by A18,ORDINAL4:def 1;
hence thesis by A6,A10,A18,A19;
end;
end;
let x,y be object;
A20: field R = a+^b by WELLORD2:def 1;
hereby assume
A21: [x,y] in R;
hence
A22: x in field R & y in field R by RELAT_1:15;
reconsider xx=x, yy=y as set by TARSKI:1;
A23: xx c= yy by A21,A20,WELLORD2:def 1,A22;
A24: (f^g).x in X\/Y & (f^g).y in X\/Y by A7,A8,A22,FUNCT_1:def 3;
thus [(f^g).x,(f^g).y] in Q
proof
reconsider x,y as Ordinal by A20,A22;
per cases by ORDINAL1:16;
suppose
A25: x in dom f & y in dom f; then
A26: [x,y] in RelIncl a by A3,A23,WELLORD2:def 1;
(f^g).x = f.x & (f^g).y = f.y by A25,ORDINAL4:def 1; then
A27: [(f^g).x, (f^g).y] in Q1 by A9,A5,A26; then
(f^g).x in field Q1 & (f^g).y in field Q1 by RELAT_1:15; then
(f^g).x in X & (f^g).y in X by WELLORD2:def 1; then
(f^g).x c= (f^g).y by A27,WELLORD2:def 1;
hence thesis by A24,WELLORD2:def 1;
end;
suppose
A28: x in dom f & dom f c= y; then
A29: (dom f)+^(y-^dom f) = y by ORDINAL3:def 5; then
A30: y-^dom f in dom g by A3,A20,A22,ORDINAL3:22; then
(f^g).x = f.x & (f^g).y = g.(y-^dom f) by A28,A29,ORDINAL4:def 1;
then
(f^g).x in X & (f^g).y in Y by A4,A28,A30,FUNCT_1:def 3; then
(f^g).x in (f^g).y by A1; then
(f^g).x c= (f^g).y by ORDINAL1:def 2;
hence thesis by A24,WELLORD2:def 1;
end;
suppose
dom f c= x & y in dom f; then
y in x; then
y in y by A23;
hence thesis;
end;
suppose dom f c= x & dom f c= y; then
A31: (dom f)+^(x-^dom f) = x & (dom f)+^(y-^dom f) = y
by ORDINAL3:def 5; then
A32: x-^dom f in dom g & y-^dom f in dom g by A3,A20,A22,ORDINAL3:22;
x-^a c= y-^a by A23,ORDINAL3:59; then
A33: [x-^a,y-^a] in RelIncl b by A32,A3,WELLORD2:def 1;
(f^g).y = g.(y-^dom f) & (f^g).x = g.(x-^dom f)
by A31,A32,ORDINAL4:def 1; then
A34: [(f^g).x, (f^g).y] in Q2 by A9,A3,A5,A33; then
(f^g).x in field Q2 & (f^g).y in field Q2 by RELAT_1:15; then
(f^g).x in Y & (f^g).y in Y by WELLORD2:def 1; then
(f^g).x c= (f^g).y by A34,WELLORD2:def 1;
hence thesis by A24,WELLORD2:def 1;
end;
end;
end;
assume
A35: x in field R & y in field R & [(f^g).x,(f^g).y] in Q; then
A36: (f^g).x c= (f^g).y by Th8;
reconsider x,y as Ordinal by A20,A35;
per cases by ORDINAL1:16;
suppose
A37: x in dom f & y in dom f; then
A38: (f^g).x = f.x & (f^g).y = f.y by ORDINAL4:def 1;
f.x in X & f.y in X by A4,A37,FUNCT_1:def 3; then
[f.x, f.y] in Q1 by A38,A36,WELLORD2:def 1; then
[x,y] in R1 by A9,A37,A5; then
x c= y by Th8;
hence thesis by A20,A35,WELLORD2:def 1;
end;
suppose
x in dom f & dom f c= y; then
x c= y by ORDINAL1:def 2;
hence thesis by A20,A35,WELLORD2:def 1;
end;
suppose
A39: dom f c= x & y in dom f; then
A40: (f^g).y = f.y by ORDINAL4:def 1;
A41: f.y in X by A4,A39,FUNCT_1:def 3;
A42: (dom f)+^(x-^dom f) = x by A39,ORDINAL3:def 5; then
A43: x-^dom f in dom g by A3,A20,A35,ORDINAL3:22; then
A44: (f^g).x = g.(x-^dom f) by A42,ORDINAL4:def 1;
g.(x-^dom f) in Y by A4,A43,FUNCT_1:def 3; then
(f^g).y in (f^g).x by A40,A41,A44,A1; then
(f^g).y in (f^g).y by A36;
hence thesis;
end;
suppose dom f c= x & dom f c= y; then
A45: (dom f)+^(x-^dom f) = x & (dom f)+^(y-^dom f) = y
by ORDINAL3:def 5; then
A46: x-^dom f in dom g & y-^dom f in dom g by A3,A20,A35,ORDINAL3:22; then
A47: g.(y-^dom f) in Y & g.(x-^dom f) in Y by A4,FUNCT_1:def 3;
(f^g).y = g.(y-^dom f) & (f^g).x = g.(x-^dom f)
by A45,A46,ORDINAL4:def 1; then
[g.(x-^dom f), g.(y-^dom f)] in Q2
by A47,A36,WELLORD2:def 1; then
[(x-^dom f), (y-^dom f)] in R2 by A9,A5,A46; then
x-^dom f c= y-^dom f by Th8; then
x c= y by A45,ORDINAL3:18;
hence thesis by A20,A35,WELLORD2:def 1;
end;
end;
theorem Th25:
for X,Y being ordinal-membered set
st for x,y st x in X & y in Y holds x in y
holds numbering(X \/ Y) = (numbering X)^(numbering Y)
proof
let X,Y be ordinal-membered set; assume
A1: for x,y st x in X & y in Y holds x in y;
set f = numbering X, g = numbering Y, h = numbering(X\/Y);
set a = ord-type X, b = ord-type Y;
set P = RelIncl(a+^b), Q = RelIncl(X\/Y);
set R = RelIncl ord-type(X\/Y);
A2: On(X\/Y) = X\/Y & On X = X & On Y = Y by Th2; then
A3: h is_isomorphism_of R,Q by Th21;
A4: f^g is_isomorphism_of P,Q by A1,Th24; then
A5: P,Q are_isomorphic & R,Q are_isomorphic by A3; then
Q,R are_isomorphic by WELLORD1:40; then
a+^b = ord-type(X\/Y) by A5,WELLORD1:42,WELLORD2:10;
hence numbering(X \/ Y) = (numbering X)^(numbering Y)
by A2,A4,A5,WELLORD1:def 9;
end;
theorem
for X,Y being ordinal-membered set
st for x,y st x in X & y in Y holds x in y
holds ord-type(X \/ Y) = (ord-type X)+^(ord-type Y)
proof
let X,Y be ordinal-membered set;
assume for x,y st x in X & y in Y holds x in y; then
A1: numbering(X \/ Y) = (numbering X)^(numbering Y) by Th25;
thus ord-type(X \/ Y) = dom numbering(X \/ Y) by Th18
.= (dom numbering X)+^(dom numbering Y) by A1,ORDINAL4:def 1
.= (ord-type X)+^(dom numbering Y) by Th18
.= (ord-type X)+^(ord-type Y) by Th18;
end;
begin :: Fixpoints of a Normal Function
theorem Th27:
for f being Function st x is_a_fixpoint_of f holds x in rng f
by FUNCT_1:def 3;
definition
let f be Ordinal-Sequence;
func criticals f -> Ordinal-Sequence equals
numbering {a where a is Element of dom f: a is_a_fixpoint_of f};
coherence;
end;
theorem Th28:
On {a where a is Element of dom f: a is_a_fixpoint_of f}
= {a where a is Element of dom f: a is_a_fixpoint_of f}
proof
set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
now
let x;
assume x in X; then
ex a being Element of dom f st x = a & a is_a_fixpoint_of f;
hence x is ordinal;
end; then
X is ordinal-membered by Th1;
hence thesis by Th2;
end;
theorem Th29:
x in dom criticals f implies (criticals f).x is_a_fixpoint_of f
proof set a = x;
set X = {b where b is Element of dom f: b is_a_fixpoint_of f};
set g = criticals f;
assume a in dom g; then
g.a in rng g by FUNCT_1:def 3; then
g.a in On X by Th18; then
g.a in X by Th28; then
ex b being Element of dom f st g.a = b & b is_a_fixpoint_of f;
hence thesis;
end;
theorem Th30:
rng criticals f = {a where a is Element of dom f: a is_a_fixpoint_of f} &
rng criticals f c= rng f
proof
set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
On X = X by Th28;
hence
A1: rng criticals f = X by Th18;
let x be object; assume x in rng criticals f; then
ex a being Element of dom f st x = a & a is_a_fixpoint_of f by A1;
hence thesis by Th27;
end;
registration let f;
cluster criticals f -> increasing;
coherence;
end;
theorem
x in dom criticals f implies x c= (criticals f).x by ORDINAL4:10;
theorem Th32:
dom criticals f c= dom f
proof let x be Ordinal;
set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
assume
A1: x in dom criticals f; then
(criticals f).x in rng criticals f by FUNCT_1:def 3; then
(criticals f).x in On X by Th18; then
(criticals f).x in X by Th28; then
consider a being Element of dom f such that
A2: (criticals f).x = a & a is_a_fixpoint_of f;
x c= a & a in dom f & a = f.a by A1,A2,ORDINAL4:10;
hence thesis by ORDINAL1:12;
end;
theorem Th33:
b is_a_fixpoint_of f implies
ex a st a in dom criticals f & b = (criticals f).a
proof
set X = {a where a is Element of dom f: a is_a_fixpoint_of f};
assume
A1: b is_a_fixpoint_of f;
b in X by A1; then
b in rng criticals f by Th30; then
ex x being object st x in dom criticals f & b = (criticals f).x
by FUNCT_1:def 3;
hence thesis;
end;
theorem
a in dom criticals f & b is_a_fixpoint_of f & (criticals f).a in b
implies succ a in dom criticals f
proof set g = criticals f;
assume that
A1: a in dom g and
A2: b is_a_fixpoint_of f and
A3: g.a in b;
consider c such that
A4: c in dom g & b = g.c by A2,Th33;
a in c by A1,A3,A4,Th23; then
succ a c= c by ORDINAL1:21;
hence succ a in dom criticals f by A4,ORDINAL1:12;
end;
theorem
succ a in dom criticals f & b is_a_fixpoint_of f & (criticals f).a in b
implies (criticals f).succ a c= b
proof set g = criticals f;
set Y = {c where c is Element of dom f: c is_a_fixpoint_of f};
set X = ord-type Y;
assume
A1: succ a in dom g & b is_a_fixpoint_of f & g.a in b; then
consider c such that
A2: c in dom g & b = g.c by Th33;
a in succ a by ORDINAL1:6; then
A3: a in dom g & g.a in g.succ a by A1,ORDINAL1:10,ORDINAL2:def 12;
On Y = Y by Th28; then
A4: g is_isomorphism_of RelIncl X, RelIncl Y by Th21;
A5: dom g = X by Th18;
b c/= g.a by A1,Th4; then
c c/= a by A2,A3,A4,A5,Th6; then
a in c by Th4; then
succ a c= c by ORDINAL1:21;
hence g.succ a c= b by A2,ORDINAL4:9;
end;
theorem Th36:
f is normal & union X in dom f & X is non empty &
(for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f)
implies union X = f.union X
proof assume that
A1: f is normal and
A2: union X in dom f & X is non empty and
A3: for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f;
reconsider l = union X as Ordinal by A2;
per cases;
suppose
ex a st a in X & for b st b in X holds b c= a; then
consider a such that
A4: a in X & for b st b in X holds b c= a;
now
let x; assume
x in X; then
consider y such that
A5: x c= y & y in X & y is_a_fixpoint_of f by A3;
y c= a by A4,A5;
hence x c= a by A5;
end; then
union X c= a & a c= union X by A4,ZFMISC_1:74,76; then
A6: union X = a; then
consider y such that
A7: union X c= y & y in X & y is_a_fixpoint_of f by A3,A4;
y c= union X by A6,A7,A4; then
y = union X by A7;
hence union X = f.union X by A7;
end;
suppose
A8: not ex a st a in X & for b st b in X holds b c= a;
set y0 = the Element of X;
consider x0 being set such that
A9: y0 c= x0 & x0 in X & x0 is_a_fixpoint_of f by A2,A3;
consider b such that
A10: b in X & b c/= x0 by A9,A8;
now
let a; assume a in l; then
consider x such that
A11: a in x & x in X by TARSKI:def 4;
consider y such that
A12: x c= y & y in X & y is_a_fixpoint_of f by A3,A11;
consider b such that
A13: b in X & b c/= y by A8,A12;
succ a c= y & y in b by A11,A12,A13,Th4,ORDINAL1:21; then
succ a in b by ORDINAL1:12;
hence succ a in l by A13,TARSKI:def 4;
end; then
reconsider l as non empty limit_ordinal Ordinal
by A10,ORDINAL1:28,TARSKI:def 4;
thus union X c= f.union X by A2,A1,ORDINAL4:10;
reconsider g = f|l as increasing Ordinal-Sequence by A1,ORDINAL4:15;
l c= dom f by A2,ORDINAL1:def 2; then
A14: dom g = l by RELAT_1:62; then
A15: Union g is_limes_of g by ORDINAL5:6;
f.l is_limes_of g by A1,A2,ORDINAL2:def 13; then
A16: f.l = lim g & Union g = lim g by A15,ORDINAL2:def 10;
let x be object; assume x in f.union X; then
consider z being object such that
A17: z in dom g & x in g.z by A16,CARD_5:2;
consider y such that
A18: z in y & y in X by A14,A17,TARSKI:def 4;
consider t being set such that
A19: y c= t & t in X & t is_a_fixpoint_of f by A18,A3;
A20: t in dom f & t = f.t by A19; then
reconsider z,t as Ordinal by A17;
f.z = g.z & z in t by A17,A18,A19,FUNCT_1:47; then
g.z in t by A1,A20,ORDINAL2:def 12; then
x in t by A17,ORDINAL1:10;
hence x in union X by A19,TARSKI:def 4;
end;
end;
theorem Th37:
f is normal & union X in dom f & X is non empty &
(for x st x in X holds x is_a_fixpoint_of f)
implies union X = f.union X
proof assume that
A1: f is normal and
A2: union X in dom f & X is non empty and
A3: for x st x in X holds x is_a_fixpoint_of f;
for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f by A3;
hence thesis by A1,A2,Th36;
end;
theorem Th38:
l c= dom criticals f & a is_a_fixpoint_of f &
(for x st x in l holds (criticals f).x in a)
implies l in dom criticals f
proof set g = criticals f;
assume that
A1: l c= dom g and
A2: a is_a_fixpoint_of f and
A3: for x st x in l holds g.x in a;
consider b such that
A4: b in dom g & a = g.b by A2,Th33;
l c= b
proof
let x be Ordinal; assume x in l; then
x in dom g & g.x in g.b by A1,A3,A4;
hence x in b by A4,Th23;
end;
hence l in dom criticals f by A4,ORDINAL1:12;
end;
theorem Th39:
f is normal & l in dom criticals f implies
(criticals f).l = Union ((criticals f)|l)
proof set g = criticals f;
reconsider h = g|l as increasing Ordinal-Sequence by ORDINAL4:15;
set X = rng h;
assume
A1: f is normal & l in dom g; then
g.l is_a_fixpoint_of f by Th29; then
A2: g.l in dom f & f.(g.l) = g.l;
A3: l c= dom g by A1,ORDINAL1:def 2; then
A4: dom h = l by RELAT_1:62;
A5: for x st x in X holds x is_a_fixpoint_of f
proof
let x; assume x in X; then
consider y being object such that
A6: y in dom h & x = h.y by FUNCT_1:def 3;
x = g.y & y in dom g by A3,A4,A6,FUNCT_1:47;
hence thesis by Th29;
end;
reconsider u = union X as Ordinal;
A7: h <> {} by A4;
now
let x; assume x in X; then
consider y being object such that
A8: y in dom h & x = h.y by FUNCT_1:def 3;
x = g.y & y in dom g by A3,A4,A8,FUNCT_1:47; then
x in g.l by A1,A4,A8,ORDINAL2:def 12;
hence x c= g.l by ORDINAL1:def 2;
end; then
A9: union X c= g.l by ZFMISC_1:76; then
A10: u in dom f by A2,ORDINAL1:12;
u = f.u by A1,A5,A7,A9,Th37,A2,ORDINAL1:12; then
u is_a_fixpoint_of f by A10; then
consider a such that
A11: a in dom g & u = g.a by Th33;
a = l
proof
thus a c= l by A1,A11,A9,Th22;
let x be Ordinal; assume
A12: x in l; then
A13: succ x in l by ORDINAL1:28; then
A14: g.x = h.x & g.succ x = h.succ x & h.succ x in X
by A4,A12,FUNCT_1:47,def 3;
x in succ x by ORDINAL1:6; then
h.x in h.succ x by A4,A13,ORDINAL2:def 12; then
g.x in u by A14,TARSKI:def 4; then
g.a c/= g.x & x in dom g by A3,A11,A12,Th4; then
a c/= x by A11,Th22;
hence thesis by Th4;
end;
hence thesis by A11;
end;
registration
let f be normal Ordinal-Sequence;
cluster criticals f -> continuous;
coherence
proof set g = criticals f;
let a,b;
reconsider h = g|a as increasing Ordinal-Sequence by ORDINAL4:15;
assume
A1: a in dom g & a <> 0 & a is limit_ordinal & b = g.a; then
A2: b = Union h by Th39;
a c= dom g by A1,ORDINAL1:def 2; then
dom h = a by RELAT_1:62;
hence b is_limes_of g|a by A1,A2,ORDINAL5:6;
end;
end;
theorem Th40:
for f1,f2 being Ordinal-Sequence st f1 c= f2
holds criticals f1 c= criticals f2
proof
let f1,f2 be Ordinal-Sequence;
assume
A1: f1 c= f2; then
A2: dom f1 c= dom f2 by GRFUNC_1:2;
set X = {a where a is Element of dom f1: a is_a_fixpoint_of f1};
set Z = {a where a is Element of dom f2: a is_a_fixpoint_of f2};
On X = X & On Z = Z by Th28; then
reconsider X,Z as ordinal-membered set;
set Y = Z\X;
A3: now let x,y; assume x in X; then
consider a being Element of dom f1 such that
A4: x = a & a is_a_fixpoint_of f1;
assume y in Y; then
A5: y in Z & not y in X by XBOOLE_0:def 5; then
consider b being Element of dom f2 such that
A6: y = b & b is_a_fixpoint_of f2;
now assume
A7: b in dom f1; then
f1.b = f2.b by A1,GRFUNC_1:2 .= b by A6; then
b is_a_fixpoint_of f1 by A7;
hence contradiction by A5,A6;
end; then
dom f1 c= b & x in dom f1 by A4,Th4;
hence x in y by A6;
end;
X c= Z
proof
let x be object; assume x in X; then
consider a being Element of dom f1 such that
A8: x = a & a is_a_fixpoint_of f1;
a in dom f1 & a = f1.a by A8; then
a in dom f2 & a = f2.a by A1,A2,GRFUNC_1:2; then
a is_a_fixpoint_of f2;
hence thesis by A8;
end; then
X\/Y = Z by XBOOLE_1:45; then
criticals f2 = (criticals f1)^numbering Y by A3,Th25;
hence criticals f1 c= criticals f2 by Th9;
end;
begin :: Fixpoints in a Universal Set
reserve U,W for Universe;
registration
let U;
cluster normal for Ordinal-Sequence of U;
existence
proof
reconsider F = id On U as Ordinal-Sequence of U;
take F;
thus thesis;
end;
end;
definition
let U,a;
mode Ordinal-Sequence of a,U is Function of a, On U;
end;
registration
let U,a;
cluster -> Sequence-like Ordinal-yielding for Ordinal-Sequence of a,U;
coherence
by FUNCT_2:def 1,RELAT_1:def 19;
end;
definition
let U,a;
let f be Ordinal-Sequence of a,U;
let x;
redefine func f.x -> Ordinal of U; :: redefines . (FUNCT_1, definition)
coherence
proof
per cases by FUNCT_1:def 2;
suppose
x in dom f; then
x in a by FUNCT_2:def 1; then
f.x in On U by FUNCT_2:5;
hence thesis by ORDINAL1:def 9;
end;
suppose
f.x = 0;
hence thesis by CLASSES2:56;
end;
end;
end;
theorem Th41:
a in U implies for f being Ordinal-Sequence of a,U holds Union f in U
proof assume
A1: a in U;
let f be Ordinal-Sequence of a,U;
dom f = a by FUNCT_2:def 1; then
card dom f in card U & card rng f c= card dom f & rng f c= On U & On U c= U
by A1,CARD_2:61,CLASSES2:1,ORDINAL2:7,RELAT_1:def 19; then
card rng f in card U & rng f c= U by ORDINAL1:12; then
rng f in U by CLASSES1:1;
hence Union f in U by CLASSES2:59;
end;
theorem Th42:
a in U implies for f being Ordinal-Sequence of a,U holds sup f in U
proof assume
A1: a in U;
let f be Ordinal-Sequence of a,U;
reconsider u = Union f as Ordinal of U by Th41,A1;
On rng f = rng f by Th2; then
sup f c= succ u by ORDINAL3:72;
hence sup f in U by CLASSES1:def 1;
end;
scheme CriticalNumber2
{U() -> Universe, a() -> Ordinal of U(),
f() -> Ordinal-Sequence of omega, U(),
phi(Ordinal) -> Ordinal}:
a() c= Union f() & phi(Union f()) = Union f() &
for b st a() c= b & b in U() & phi(b) = b holds Union f() c= b
provided
A1: omega in U()
and
A2: for a st a in U() holds phi(a) in U()
and
A3: for a,b st a in b & b in U() holds phi(a) in phi(b)
and
A4: for a being Ordinal of U() st a is non empty limit_ordinal
for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi
and
A5: f().0 = a()
and
A6: for a st a in omega holds f().(succ a) = phi(f().a)
proof
A7:dom f() = omega by FUNCT_2:def 1;
A8: a() in rng f() by A5,A7,FUNCT_1:def 3;
hence a() c= Union f() by ZFMISC_1:74;
set phi = f();
A9: now
defpred P[Ordinal] means $1 in U() & $1 c/= phi($1);
assume
A10: ex a st P[a];
consider a such that
A11: P[a] and
A12: for b st P[b] holds a c= b from ORDINAL1:sch 1(A10);
phi(phi(a)) in phi(a) by A3,A11,ORDINAL1:16; then
phi(a) c/= phi(phi(a)) by ORDINAL1:5;
hence contradiction by A2,A11,A12;
end; then
a() c= phi(a()); then
A13: a() c< phi(a()) or a() = phi(a());
per cases by A13,ORDINAL1:11;
suppose
A14: phi(a()) = a();
A15: for a be set st a in omega holds f().a = a()
proof
let a be set; assume a in omega; then
reconsider a as Element of omega;
defpred P[Nat] means f().$1 = a();
A16: P[0] by A5;
A17: now let n be Nat; assume
A18: P[n];
A19: Segm(n+1) = succ Segm n by NAT_1:38;
n in omega by ORDINAL1:def 12; then
f().succ n = phi(a()) by A6,A18;
hence P[n+1] by A14,A19;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A16,A17); then
P[a];
hence thesis;
end;
rng f() = {a()}
proof
thus rng f() c= {a()}
proof
let x be object; assume x in rng f(); then
consider a being object such that
A20: a in dom f() & x = f().a by FUNCT_1:def 3;
x = a() by A15,A20,A7;
hence thesis by TARSKI:def 1;
end;
thus thesis by A8,ZFMISC_1:31;
end; then
Union f() = a() by ZFMISC_1:25;
hence phi(Union f()) = Union f() &
for b st a() c= b & b in U() & phi(b) = b holds Union f() c= b by A14;
end;
suppose
A21: a() in phi(a());
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,Sequence) = {};
A22: now let a such that
A23: succ a in omega;
a in succ a by ORDINAL1:6;
hence phi.(succ a) = F(a,phi.a) by A6,A23,ORDINAL1:10;
end;
A24: for a st a in omega holds a() c= phi.a & phi.a in phi.succ a
proof let a; assume a in omega; then
reconsider a as Element of omega;
defpred N[Nat] means a() c= phi.$1 & phi.$1 in phi.succ Segm $1;
A25: N[0] by A21,A5,A6;
A26: now
let n be Nat; assume
A27: N[n];
A28: Segm(n+1) = succ Segm n & Segm(n+1+1) = succ Segm(n+1) &
n+1 in omega & n+1+1 in omega by NAT_1:38; then
phi.(n+1) = phi(phi.n) & phi.(n+1+1) = phi(phi.(n+1)) by A22; then
phi.n c= phi.(n+1) & phi.(n+1) in phi.(n+1+1) by A3,A9,A27,A28;
hence N[n+1] by A27,XBOOLE_1:1,A28;
end;
for n being Nat holds N[n] from NAT_1:sch 2(A25,A26); then
N[a];
hence thesis;
end;
deffunc phi(Ordinal) = phi($1);
consider fi being Ordinal-Sequence such that
A29: dom fi = Union phi & for a st a in Union phi holds fi.a = phi(a)
from ORDINAL2:sch 3;
1 = succ 0; then
f().1 = phi(a()) by A5,A6; then
phi(a()) in rng phi by A7,FUNCT_1:def 3; then
A30: phi(a()) c= Union phi by ZFMISC_1:74;
A31: Union phi in U() by A1,Th41;
now
let c; assume c in Union phi; then
consider x being object such that
A32: x in dom phi & c in phi.x by CARD_5:2;
reconsider x as Element of omega by A32,FUNCT_2:def 1;
succ c c= phi.x & phi.x in phi.succ x by A24,A32,ORDINAL1:21; then
succ c in phi.succ x & succ x in omega by ORDINAL1:12,def 12;
hence succ c in Union phi by A7,CARD_5:2;
end; then
A33: Union phi is limit_ordinal by ORDINAL1:28; then
A34: phi(Union phi) is_limes_of fi by A4,A21,A29,A30,A31;
fi is increasing
proof
let a,b;
assume
A35: a in b & b in dom fi; then
fi.a = phi(a) & fi.b = phi(b) & b in U() by A31,A29,ORDINAL1:10;
hence thesis by A3,A35;
end; then
A36: sup fi = lim fi by A21,A29,A30,A33,ORDINAL4:8
.= phi(Union phi) by A34,ORDINAL2:def 10;
thus phi(Union phi) c= Union phi
proof
let x be Ordinal;
assume
A37: x in phi(Union phi);
reconsider A = x as Ordinal;
consider b such that
A38: b in rng fi & A c= b by A36,A37,ORDINAL2:21;
consider y being object such that
A39: y in dom fi & b = fi.y by A38,FUNCT_1:def 3;
reconsider y as Ordinal by A39;
consider z being object such that
A40: z in dom phi & y in phi.z by A29,A39,CARD_5:2;
reconsider z as Ordinal by A40;
set c = phi.z;
succ z in omega by A7,A40,ORDINAL1:28; then
A41: phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
by A7,A22,A29,A39,FUNCT_1:def 3;
b in phi(c) & phi(c) c= Union phi by A41,A3,A40,ZFMISC_1:74;
hence thesis by A38,ORDINAL1:12;
end;
thus Union f() c= phi(Union f()) by A9,A1,Th41;
let b; assume
A42: a() c= b & b in U() & phi(b) = b;
rng f() c= b
proof
let x be object; assume x in rng f(); then
consider a being object such that
A43: a in dom f() & x = f().a by FUNCT_1:def 3;
reconsider a as Element of omega by A43,FUNCT_2:def 1;
defpred P[Nat] means f().$1 in b;
a() <> b by A21,A42; then
a() c< b by A42; then
A44: P[0] by A5,ORDINAL1:11;
A45: now let n be Nat; assume P[n]; then
phi(f().n) in b & n in omega by A3,A42,ORDINAL1:def 12; then
A46: f().succ n in b by A6;
Segm(n+1) = succ Segm n by NAT_1:38;
hence P[n+1] by A46;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A44,A45); then
P[a];
hence thesis by A43;
end; then
Union f() c= union b & union b c= b by ORDINAL2:5,ZFMISC_1:77;
hence Union f() c= b;
end;
end;
scheme CriticalNumber3
{U() -> Universe, a() -> Ordinal of U(), phi(Ordinal) -> Ordinal}:
ex a being Ordinal of U() st a() in a & phi(a) = a
provided
A1: omega in U()
and
A2: for a st a in U() holds phi(a) in U()
and
A3: for a,b st a in b & b in U() holds phi(a) in phi(b)
and
A4: for a being Ordinal of U() st a is non empty limit_ordinal
for phi being Ordinal-Sequence
st dom phi = a & for b st b in a holds phi.b = phi(b)
holds phi(a) is_limes_of phi
proof assume
A5: not thesis;
deffunc F(Ordinal,Ordinal) = phi($2);
deffunc G(Ordinal,Sequence) = {};
consider phi being Ordinal-Sequence such that
A6: dom phi = omega and
A7: 0 in omega implies phi.0 = succ a() and
A8: for a st succ a in omega holds phi.(succ a) = F(a,phi.a) and
for a st a in omega & a <> 0 & a is limit_ordinal
holds phi.a = G(a,phi|a) from ORDINAL2:sch 11;
A9: rng phi c= On U()
proof
let y be object; assume y in rng phi; then
consider x being object such that
A10: x in dom phi & y = phi.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A6,A10;
defpred P[Nat] means phi.$1 in On U();
A11: P[0] by A7,ORDINAL1:def 9;
A12: P[n] implies P[n+1]
proof assume P[n]; then
A13: phi.n in U() by ORDINAL1:def 9;
A14: Segm(n+1) = succ Segm n by NAT_1:38;
phi.(n+1) = phi(phi.n) & phi(phi.n) in U() by A8,A14,A13,A2;
hence P[n+1] by ORDINAL1:def 9;
end;
P[n] from NAT_1:sch 2(A11,A12); then P[x];
hence thesis by A10;
end; then
reconsider phi as Ordinal-Sequence of omega,U() by A6,FUNCT_2:2;
A15: now
defpred P[Ordinal] means $1 in U() & $1 c/= phi($1);
assume
A16: ex a st P[a];
consider a such that
A17: P[a] and
A18: for b st P[b] holds a c= b from ORDINAL1:sch 1(A16);
phi(phi(a)) in phi(a) by A3,A17,ORDINAL1:16; then
phi(a) c/= phi(phi(a)) by ORDINAL1:5;
hence contradiction by A17,A18,A2;
end;
A19:now
let a;
assume a() in a & a in U(); then
a c= phi(a) & a <> phi(a) by A5,A15; then
a c< phi(a);
hence a in phi(a) by ORDINAL1:11;
end;
A20: for a st a in omega holds a() in phi.a
proof let a; assume a in omega; then
reconsider a as Element of omega;
defpred N[Nat] means a() in phi.$1;
A21: N[0] by A7,ORDINAL1:6;
A22: now
let n be Nat; assume
A23: N[n];
Segm(n+1) = succ Segm n & n+1 in omega by NAT_1:38; then
phi.(n+1) = phi(phi.n) by A8; then
phi.n in phi.(n+1) by A23,A19;
hence N[n+1] by A23,ORDINAL1:10;
end;
for n being Nat holds N[n] from NAT_1:sch 2(A21,A22); then
N[a];
hence thesis;
end;
A24:phi is increasing
proof
let a,b;
assume
A25: a in b & b in dom phi; then
A26: ex c st b = a+^c & c <> {} by ORDINAL3:28;
defpred R[Ordinal] means
a+^$1 in omega & $1 <> {} implies phi.a in phi.(a+^$1);
A27: R[0];
A28: for c st R[c] holds R[succ c]
proof
let c such that
A29: a+^c in omega & c <> {} implies phi.a in phi.(a+^c) and
A30: a+^succ c in omega & succ c <> {};
A31: a+^c in succ(a+^c) & a+^succ c = succ(a+^c) by ORDINAL1:6,ORDINAL2:28;
reconsider d = phi.(a+^c) as Ordinal;
a+^c in omega by A30,A31,ORDINAL1:10; then
phi.(a+^succ c) = phi(d) & d in phi(d) & a+^({} qua Ordinal) = a
by A8,A19,A30,A31,A20,ORDINAL2:27;
hence thesis by A29,A30,A31,ORDINAL1:10;
end;
A32: for b st b <> 0 & b is limit_ordinal & for c st c in b holds R[c]
holds R[b]
proof
let b such that
A33: b <> 0 & b is limit_ordinal and
for c st c in b holds a+^c in omega & c <> {} implies
phi.a in phi.(a+^c) and
A34: a+^b in omega & b <> {};
a+^b is limit_ordinal & {} in a+^b by A33,ORDINAL3:8,29;
hence thesis by A34;
end;
for c holds R[c] from ORDINAL2:sch 1(A27,A28,A32);
hence thesis by A6,A25,A26;
end;
A35: sup phi in U() by A1,Th42;
deffunc phi(Ordinal) = phi($1);
consider fi being Ordinal-Sequence such that
A36: dom fi = sup phi & for a st a in sup phi holds fi.a = phi(a)
from ORDINAL2:sch 3;
succ a() in rng phi & sup rng phi = sup phi
by A6,A7,FUNCT_1:def 3; then
A37: sup phi <> {} & sup phi is limit_ordinal
by A6,A24,ORDINAL2:19,ORDINAL4:16; then
A38: phi(sup phi) is_limes_of fi by A35,A4,A36;
fi is increasing
proof
let a,b;
assume
A39: a in b & b in dom fi; then
fi.a = phi(a) & fi.b = phi(b) & b in U() by A35,A36,ORDINAL1:10;
hence thesis by A3,A39;
end; then
A40: sup fi = lim fi by A36,A37,ORDINAL4:8
.= phi(sup phi) by A38,ORDINAL2:def 10;
A41: sup fi c= sup phi
proof
let x be Ordinal;
assume
A42: x in sup fi;
reconsider A = x as Ordinal;
consider b such that
A43: b in rng fi & A c= b by A42,ORDINAL2:21;
consider y being object such that
A44: y in dom fi & b = fi.y by A43,FUNCT_1:def 3;
reconsider y as Ordinal by A44;
consider c such that
A45: c in rng phi & y c= c by A36,A44,ORDINAL2:21;
A46: c in U() by A9,A45,ORDINAL1:def 9;
consider z being object such that
A47: z in dom phi & c = phi.z by A45,FUNCT_1:def 3;
reconsider z as Ordinal by A47;
succ z in omega by A6,A47,ORDINAL1:28; then
A48: phi.succ z = phi(c) & phi.succ z in rng phi & b = phi(y)
by A6,A8,A36,A44,A47,FUNCT_1:def 3;
y c< c iff y <> c & y c= c; then
phi(y) in phi(c) or y = c by A46,A3,A45,ORDINAL1:11; then
b c= phi(c) & phi(c) in sup phi by A48,ORDINAL1:def 2,ORDINAL2:19; then
b in sup phi by ORDINAL1:12;
hence thesis by A43,ORDINAL1:12;
end;
phi.0 in rng phi by A6,FUNCT_1:def 3; then
a() in phi.0 & phi.0 in sup phi by A20,ORDINAL2:19; then
a() in sup phi by ORDINAL1:10;
hence contradiction by A35,A19,A40,A41,ORDINAL1:5;
end;
reserve F,phi for normal Ordinal-Sequence of W;
theorem Th43:
omega in W & b in W implies ex a st b in a & a is_a_fixpoint_of phi
proof assume that
A1: omega in W and
A2: b in W;
reconsider b1 = b as Ordinal of W by A2;
A3: dom phi = On W by FUNCT_2:def 1;
deffunc phi(set) = phi.$1;
A4: for a st a in W holds phi(a) in W;
A5: for a,b st a in b & b in W holds phi(a) in phi(b)
proof
let a,b;
b in W implies b in dom phi by A3,ORDINAL1:def 9;
hence thesis by ORDINAL2:def 12;
end;
A6: for a being Ordinal of W st a is non empty limit_ordinal
for f being Ordinal-Sequence
st dom f = a & for b st b in a holds f.b = phi(b)
holds phi(a) is_limes_of f
proof let a be Ordinal of W;
assume
A7: a is non empty limit_ordinal;
let f be Ordinal-Sequence such that
A8: dom f = a and
A9: for b st b in a holds f.b = phi(b);
A10: a in dom phi by A3,ORDINAL1:def 9; then
a c= dom phi by ORDINAL1:def 2; then
A11: dom (phi|a) = a by RELAT_1:62;
now let x be object; assume
A12: x in a;
reconsider xx = x as set by TARSKI:1;
thus (phi|a).x = phi(xx) by A12,FUNCT_1:49 .= f.x by A12,A9;
end; then
f = phi|a by A8,A11;
hence phi(a) is_limes_of f by A7,A10,ORDINAL2:def 13;
end;
consider a being Ordinal of W such that
A13: b1 in a & phi(a) = a from CriticalNumber3(A1,A4,A5,A6);
take a;
thus b in a & a in dom phi & a = phi.a by A3,A13,ORDINAL1:def 9;
end;
theorem Th44:
omega in W implies criticals F is Ordinal-Sequence of W
proof assume
A1: omega in W;
set G = criticals F;
A2: dom F = On W & rng F c= On W by FUNCT_2:def 1,RELAT_1:def 19;
A3: rng G c= rng F by Th30; then
A4: rng G c= On W by A2;
dom G = On W
proof
thus dom G c= On W by A2,Th32;
let a; assume a in On W; then
A5: a in W by ORDINAL1:def 9;
defpred P[Ordinal] means $1 in W implies $1 in dom G;
consider a0 being Ordinal such that
A6: 0-element_of W in a0 & a0 is_a_fixpoint_of F by A1,Th43;
consider a1 being Ordinal such that
A7: a1 in dom G & a0 = G.a1 by A6,Th33;
A8: P[0] by A7,ORDINAL1:12,XBOOLE_1:2;
A9: for a st P[a] holds P[succ a]
proof
let a; assume
A10: P[a] & succ a in W;
A11: a c= succ a by ORDINAL3:1; then
G.a in rng G by A10,CLASSES1:def 1,FUNCT_1:def 3; then
G.a in W by A4,ORDINAL1:def 9; then
consider b such that
A12: G.a in b & b is_a_fixpoint_of F by A1,Th43;
consider c such that
A13: c in dom G & b = G.c by A12,Th33;
a in c by A10,A11,A12,A13,Th23,CLASSES1:def 1; then
succ a c= c by ORDINAL1:21;
hence thesis by A13,ORDINAL1:12;
end;
A14: for a st a <> 0 & a is limit_ordinal &
for b st b in a holds P[b] holds P[a]
proof
let a such that
A15: a <> 0 & a is limit_ordinal and
A16: for b st b in a holds P[b] and
A17: a in W;
set X = G.:a;
card X c= card a & card a c= a by CARD_1:8,67; then
card X c= a; then
card X in W by A17,CLASSES1:def 1; then
card X in On W by ORDINAL1:def 9; then
A18: card X in card W by CLASSES2:9;
A19: X c= rng G by RELAT_1:111; then
A20: X c= On W by A4;
reconsider u = union X as Ordinal by A19,A4,ORDINAL3:4,XBOOLE_1:1;
On W c= W by ORDINAL2:7; then
X c= W by A20; then
X in W by A18,CLASSES1:1; then
u in W by CLASSES2:59; then
consider b such that
A21: u in b & b is_a_fixpoint_of F by A1,Th43;
A22: a c= dom G
proof
let c; assume
A23: c in a; then
c in W by A17,ORDINAL1:10;
hence thesis by A16,A23;
end;
now
let x; assume
x in a; then
G.x in X by A22,FUNCT_1:def 6; then
G.x is Ordinal & G.x c= u by ZFMISC_1:74;
hence G.x in b by A21,ORDINAL1:12;
end;
hence thesis by A15,A22,A21,Th38;
end;
P[b] from ORDINAL2:sch 1(A8,A9,A14);
hence thesis by A5;
end;
hence thesis by A3,A2,FUNCT_2:2,XBOOLE_1:1;
end;
theorem Th45:
f is normal implies
for a st a in dom criticals f holds f.a c= (criticals f).a
proof assume
A1: f is normal;
set g = criticals f;
A2: dom g c= dom f by Th32;
defpred P[Ordinal] means $1 in dom g implies f.$1 c= g.$1;
A3: P[0]
proof
assume 0 in dom g; then
g.0 is_a_fixpoint_of f by Th29; then
f.(g.0) = g.0 & g.0 in dom f;
hence thesis by A1,ORDINAL4:9,XBOOLE_1:2;
end;
A4: P[a] implies P[succ a]
proof assume that
P[a] and
A5: succ a in dom g;
g.succ a is_a_fixpoint_of f by A5,Th29; then
g.succ a in dom f & f.(g.succ a) = g.succ a;
hence f.succ a c= g.succ a by A1,A5,ORDINAL4:9,10;
end;
A6: for a st a <> 0 & a is limit_ordinal & for b st b in a holds P[b]
holds P[a]
proof
let a such that
A7: a <> 0 & a is limit_ordinal and
A8: for b st b in a holds P[b] and
A9: a in dom g;
f.a is_limes_of (f|a) & g.a is_limes_of (g|a)
by A1,A2,A7,A9,ORDINAL2:def 13; then
A10: f.a = lim(f|a) & g.a = lim(g|a) by ORDINAL2:def 10;
A11: f|a is increasing & g|a is increasing by A1,ORDINAL4:15;
A12: a c= dom f & a c= dom g by A2,A9,ORDINAL1:def 2; then
A13: dom (f|a) = a & dom (g|a) = a by RELAT_1:62; then
Union(f|a) is_limes_of (f|a) & Union(g|a) is_limes_of (g|a)
by A7,A11,ORDINAL5:6; then
A14: f.a = Union(f|a) & g.a = Union(g|a) by A10,ORDINAL2:def 10;
let b; assume b in f.a; then
consider x being object such that
A15: x in a & b in (f|a).x by A13,A14,CARD_5:2;
(f|a).x = f.x & (g|a).x = g.x & f.x c= g.x by A12,A8,A15,FUNCT_1:49;
hence b in g.a by A15,A13,A14,CARD_5:2;
end;
thus P[a] from ORDINAL2:sch 1(A3,A4,A6);
end;
begin :: Sequences of Sequences of Ordinals
definition
let U;
let a,b be Ordinal of U;
redefine func exp(a,b) -> Ordinal of U; :: redefines exp (ORDINAL2, definition)
coherence
proof
per cases by ORDINAL3:8;
suppose a = 0 & b = 0; then
exp(a,b) = 1-element_of U by ORDINAL2:43;
hence thesis;
end;
suppose a = 0 & b <> 0;
hence thesis;
end;
suppose
A1: 0 in a;
defpred P[Ordinal] means $1 in U implies exp(a,$1) in U;
exp(a,0) = succ 0 by ORDINAL2:43; then
A2: P[0] by CLASSES2:5;
A3: for b holds P[b] implies P[succ b]
proof
let b such that
A4: P[b] and
A5: succ b in U;
b in succ b by ORDINAL1:6; then
reconsider b as Ordinal of U by A5,ORDINAL1:10;
reconsider ab = exp(a,b) as Ordinal of U by A4;
exp(a,succ b) = a*^ab by ORDINAL2:44;
hence thesis;
end;
A6: for b st b <> 0 & b is limit_ordinal & for c st c in b holds P[c]
holds P[b]
proof
let b such that
A7: b <> 0 & b is limit_ordinal and
A8: for c st c in b holds P[c] and
A9: b in U;
deffunc F(Ordinal) = exp(a,$1);
consider f such that
A10: dom f = b & for c st c in b holds f.c = F(c) from ORDINAL2:sch 3;
rng f c= On U
proof
let x be object; assume x in rng f; then
consider y being object such that
A11: y in b & x = f.y by A10,FUNCT_1:def 3;
reconsider y as Ordinal by A11;
P[y] & y in U & x = F(y) by A9,A8,A10,A11,ORDINAL1:10;
hence thesis by ORDINAL1:def 9;
end; then
reconsider f as Ordinal-Sequence of b,U by A10,FUNCT_2:2;
A12: exp(a,b) = lim f by A7,A10,ORDINAL2:45;
f is non-decreasing by A1,A10,ORDINAL5:8; then
Union f is_limes_of f by A7,ORDINAL5:6; then
exp(a,b) = Union f by A12,ORDINAL2:def 10;
hence thesis by A9,Th41;
end;
for b holds P[b] from ORDINAL2:sch 1(A2,A3,A6);
hence thesis;
end;
end;
end;
definition
let U,a such that
A1: a in U;
func U exp a -> Ordinal-Sequence of U means: Def8:
for b being Ordinal of U holds it.b = exp(a,b);
existence
proof
reconsider a as Ordinal of U by A1;
deffunc F(Ordinal of U) = exp(a,$1);
ex f being Ordinal-Sequence of U st
for b being Ordinal of U holds f.b = F(b) from ORDINAL4:sch 2;
hence thesis;
end;
uniqueness
proof let f1,f2 be Ordinal-Sequence of U such that
A2: for b being Ordinal of U holds f1.b = exp(a,b) and
A3: for b being Ordinal of U holds f2.b = exp(a,b);
now
let x be Element of On U;
x in U by ORDINAL1:def 9; then
f1.x = exp(a,x) & f2.x = exp(a,x) by A2,A3;
hence f1.x = f2.x;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
cluster omega -> non trivial;
coherence;
end;
registration
let U;
cluster non trivial finite for Ordinal of U;
existence
proof
succ(1-element_of U) is non trivial by NAT_2:def 1;
hence thesis;
end;
end;
registration
cluster non trivial finite for Ordinal;
existence
proof
2 is non trivial by NAT_2:def 1;
hence thesis;
end;
end;
registration
let U;
let a be non trivial Ordinal of U;
cluster U exp a -> normal;
coherence
proof set f = U exp a;
A1: dom f = On U by FUNCT_2:def 1;
A2: 0 in a by ORDINAL3:8;
succ 0 c= a; then
1 c< a; then
A3: 1 in a by ORDINAL1:11;
A4: now
let b; assume b in dom f; then
b in U by A1,ORDINAL1:def 9;
hence f.b = exp(a,b) by Def8;
end;
hence f is increasing by A3,ORDINAL5:10;
let b,c; assume
A5: b in dom f & b <> 0 & b is limit_ordinal & c = f.b; then
b c= dom f by ORDINAL1:def 2; then
A6: dom (f|b) = b by RELAT_1:62;
A7: f|b is increasing by A4,A3,ORDINAL4:15,ORDINAL5:10;
A8: b in U by A1,A5,ORDINAL1:def 9; then
A9: f.b = exp(a,b) by Def8;
f.b = Union(f|b)
proof
thus f.b c= Union(f|b)
proof
let c; assume c in f.b; then
consider d such that
A10: d in b & c in exp(a,d) by A2,A5,A9,ORDINAL5:11;
d in U by A8,A10,ORDINAL1:10; then
exp(a,d) = f.d by Def8 .= (f|b).d by A10,FUNCT_1:49;
hence c in Union(f|b) by A6,A10,CARD_5:2;
end;
let c; assume c in Union(f|b); then
consider x being object such that
A11: x in b & c in (f|b).x by A6,CARD_5:2;
reconsider x as Ordinal by A11;
x in U by A8,A11,ORDINAL1:10; then
exp(a,x) = f.x by Def8 .= (f|b).x by A11,FUNCT_1:49;
hence thesis by A2,A11,A5,A9,ORDINAL5:11;
end;
hence thesis by A5,A7,A6,ORDINAL5:6;
end;
end;
definition
let g be Function;
attr g is Ordinal-Sequence-valued means :Def9:
x in rng g implies x is Ordinal-Sequence;
end;
registration
let f be Ordinal-Sequence;
cluster <%f%> -> Ordinal-Sequence-valued;
coherence
proof
let x; assume x in rng <%f%>; then
x in {f} by AFINSQ_1:33;
hence thesis by TARSKI:def 1;
end;
end;
definition ::: MESFUNC8:def 1 generalized
let f be Function;
attr f is with_the_same_dom means
rng f is with_common_domain;
end;
registration
let f be Function;
cluster {f} -> with_common_domain;
coherence
proof
let g,h be Function;
assume g in {f} & h in {f}; then
g = f & h = f by TARSKI:def 1;
hence thesis;
end;
end;
registration
let f be Function;
cluster <%f%> -> with_the_same_dom;
coherence
proof
rng <%f%> = {f} by AFINSQ_1:33;
hence rng <%f%> is with_common_domain;
end;
end;
registration
cluster non empty Ordinal-Sequence-valued with_the_same_dom for Sequence;
existence
proof
set f = the Ordinal-Sequence; take <%f%>; thus thesis;
end;
end;
registration
let g be Ordinal-Sequence-valued Function;
let x be object;
cluster g.x -> Relation-like Function-like;
coherence
proof
per cases by FUNCT_1:def 2;
suppose g.x = {};
hence thesis;
end;
suppose x in dom g; then
g.x in rng g by FUNCT_1:def 3;
hence thesis by Def9;
end;
end;
end;
registration
let g be Ordinal-Sequence-valued Function;
let x;
cluster g.x -> Sequence-like Ordinal-yielding;
coherence
proof
per cases by FUNCT_1:def 2;
suppose g.x = {};
hence thesis;
end;
suppose x in dom g; then
g.x in rng g by FUNCT_1:def 3;
hence thesis by Def9;
end;
end;
end;
registration
let g be Sequence;
let a;
cluster g|a -> Sequence-like;
coherence;
end;
registration
let g be Ordinal-Sequence-valued Function;
let X;
cluster g|X -> Ordinal-Sequence-valued;
coherence
proof
let x;
rng(g|X) c= rng g by RELAT_1:70;
hence thesis by Def9;
end;
end;
registration
let a,b;
cluster -> Ordinal-yielding Sequence-like for Function of a,b;
coherence
proof
let f be Function of a,b;
rng f c= b by RELAT_1:def 19;
hence ex c st rng f c= c;
b = {} implies f = {};
hence dom f is epsilon-transitive epsilon-connected by FUNCT_2:def 1;
end;
end;
definition
let g be Ordinal-Sequence-valued Sequence;
func criticals g -> Ordinal-Sequence equals
numbering {a where a is Element of dom(g.0): a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f};
coherence;
end;
reserve g for Ordinal-Sequence-valued Sequence;
theorem Th46:
for g holds
{a where a is Element of dom(g.0): a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f} is ordinal-membered
proof let g;
now let x;
assume x in {a where a is Element of dom(g.0): a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f};
then ex a being Element of dom(g.0) st x = a & a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f;
hence x is ordinal;
end;
hence thesis by Th1;
end;
theorem Th47:
a in dom g & b in dom criticals g
implies (criticals g).b is_a_fixpoint_of g.a
proof
assume that
A1: a in dom g and
A2: b in dom criticals g;
set h = criticals g;
set X = {c where c is Element of dom(g.0): c in dom(g.0) &
for f st f in rng g holds c is_a_fixpoint_of f};
X is ordinal-membered by Th46; then
rng h = X by Th19; then
h.b in X by A2,FUNCT_1:def 3; then
consider c being Element of dom(g.0) such that
A3: h.b = c & c in dom(g.0) & for f st f in rng g holds c is_a_fixpoint_of f;
g.a in rng g by A1,FUNCT_1:def 3;
hence (criticals g).b is_a_fixpoint_of g.a by A3;
end;
theorem
x in dom criticals g implies x c= (criticals g).x by ORDINAL4:10;
theorem Th49:
f in rng g implies dom criticals g c= dom f
proof assume
A1: f in rng g;
let x be Ordinal;
set X = {a where a is Element of dom(g.0): a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f};
assume
A2: x in dom criticals g; then
(criticals g).x in rng criticals g by FUNCT_1:def 3; then
(criticals g).x in On X & X is ordinal-membered by Th18,Th46; then
(criticals g).x in X by Th2; then
consider a being Element of dom(g.0) such that
A3: (criticals g).x = a & a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f;
a is_a_fixpoint_of f by A1,A3; then
x c= a & a in dom f & a = f.a by A2,A3,ORDINAL4:10;
hence thesis by ORDINAL1:12;
end;
theorem Th50:
dom g <> {} & (for c st c in dom g holds b is_a_fixpoint_of g.c) implies
ex a st a in dom criticals g & b = (criticals g).a
proof
reconsider X = {a where a is Element of dom(g.0): a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f} as ordinal-membered set
by Th46;
assume that
A1: dom g <> {} and
A2: for c st c in dom g holds b is_a_fixpoint_of g.c;
b is_a_fixpoint_of g.0 by A2,A1,ORDINAL3:8; then
A3: b in dom(g.0);
now
let f; assume f in rng g;
then ex x being object st x in dom g & f = g.x by FUNCT_1:def 3;
hence b is_a_fixpoint_of f by A2;
end; then
b in X by A3; then
b in rng criticals g by Th19; then
ex x being object st x in dom criticals g & b = (criticals g).x
by FUNCT_1:def 3;
hence thesis;
end;
theorem
dom g <> {} & l c= dom criticals g &
(for f st f in rng g holds a is_a_fixpoint_of f) &
(for x st x in l holds (criticals g).x in a)
implies l in dom criticals g
proof set h = criticals g;
assume that
A1: dom g <> {} and
A2: l c= dom h and
A3: for f st f in rng g holds a is_a_fixpoint_of f and
A4: for x st x in l holds h.x in a;
now
let c; assume
c in dom g; then
g.c in rng g by FUNCT_1:def 3;
hence a is_a_fixpoint_of g.c by A3;
end; then
consider b such that
A5: b in dom h & a = h.b by A1,Th50;
l c= b
proof
let x be Ordinal; assume x in l; then
x in dom h & h.x in h.b by A2,A4,A5;
hence x in b by A5,Th23;
end;
hence l in dom criticals g by A5,ORDINAL1:12;
end;
theorem Th52:
for g st dom g <> {} & for a st a in dom g holds g.a is normal
holds l in dom criticals g implies
(criticals g).l = Union ((criticals g)|l)
proof let F be Ordinal-Sequence-valued Sequence such that
A1: dom F <> {};
set g = criticals F;
reconsider h = g|l as increasing Ordinal-Sequence by ORDINAL4:15;
set X = rng h;
assume
A2: (for a st a in dom F holds F.a is normal) & l in dom g;
A3: now
let a; set f = F.a;
assume a in dom F; then
g.l is_a_fixpoint_of F.a by A2,Th47;
hence g.l in dom f & f.(g.l) = g.l;
end;
A4: l c= dom g by A2,ORDINAL1:def 2; then
A5: dom h = l by RELAT_1:62;
A6: for a,x st a in dom F & x in X holds x is_a_fixpoint_of F.a
proof
let a,x; assume
A7: a in dom F & x in X; then
consider y being object such that
A8: y in dom h & x = h.y by FUNCT_1:def 3;
x = g.y & y in dom g by A4,A5,A8,FUNCT_1:47;
hence thesis by A7,Th47;
end;
reconsider u = union X as Ordinal;
A9: h <> {} by A5;
now
let x; assume x in X; then
consider y being object such that
A10: y in dom h & x = h.y by FUNCT_1:def 3;
x = g.y & y in dom g by A4,A5,A10,FUNCT_1:47; then
x in g.l by A2,A5,A10,ORDINAL2:def 12;
hence x c= g.l by ORDINAL1:def 2;
end; then
A11: u c= g.l by ZFMISC_1:76;
now let c; set f = F.c;
assume
A12: c in dom F; then
A13: g.l in dom f by A3; then
A14: u in dom f by A11,ORDINAL1:12;
A15: f is normal by A2,A12;
for x st x in X holds x is_a_fixpoint_of f by A6,A12; then
u = f.u by A9,A13,A15,Th37,A11,ORDINAL1:12;
hence u is_a_fixpoint_of f by A14;
end; then
consider a such that
A16: a in dom g & u = g.a by A1,Th50;
a = l
proof
thus a c= l by A2,A16,A11,Th22;
let x be Ordinal; assume
A17: x in l; then
A18: succ x in l by ORDINAL1:28; then
A19: g.x = h.x & g.succ x = h.succ x & h.succ x in X
by A5,A17,FUNCT_1:47,def 3;
x in succ x by ORDINAL1:6; then
h.x in h.succ x by A5,A18,ORDINAL2:def 12; then
g.x in u by A19,TARSKI:def 4; then
g.a c/= g.x & x in dom g by A4,A16,A17,Th4; then
a c/= x by A16,Th22;
hence thesis by Th4;
end;
hence thesis by A16;
end;
theorem Th53:
for g st dom g <> {} & for a st a in dom g holds g.a is normal
holds criticals g is continuous
proof
let g;
assume A1: dom g <> {};
assume A2: for a st a in dom g holds g.a is normal;
set f = criticals g;
let a,b;
reconsider h = f|a as increasing Ordinal-Sequence by ORDINAL4:15;
assume
A3: a in dom f & a <> 0 & a is limit_ordinal & b = f.a; then
A4: b = Union h by A1,A2,Th52;
a c= dom f by A3,ORDINAL1:def 2; then
dom h = a by RELAT_1:62;
hence b is_limes_of f|a by A3,A4,ORDINAL5:6;
end;
theorem Th54:
for g st dom g <> {} & for a st a in dom g holds g.a is normal
for a,f st a in dom criticals g & f in rng g holds f.a c= (criticals g).a
proof let F be Ordinal-Sequence-valued Sequence such that
A1: dom F <> {} and
A2: for a st a in dom F holds F.a is normal;
let a,f such that
A3: a in dom criticals F and
A4: f in rng F;
consider x being object such that
A5: x in dom F & f = F.x by A4,FUNCT_1:def 3;
A6: f is normal by A5,A2;
set g = criticals F;
A7: dom g c= dom f by A4,Th49;
defpred P[Ordinal] means $1 in dom g implies f.$1 c= g.$1;
A8: P[0]
proof
assume 0 in dom g; then
g.0 is_a_fixpoint_of f by A5,Th47; then
f.(g.0) = g.0 & g.0 in dom f;
hence thesis by A6,ORDINAL4:9,XBOOLE_1:2;
end;
A9: for a holds P[a] implies P[succ a]
proof let a such that
P[a] and
A10: succ a in dom g;
g.succ a is_a_fixpoint_of f by A5,A10,Th47; then
g.succ a in dom f & f.(g.succ a) = g.succ a;
hence f.succ a c= g.succ a by A6,A10,ORDINAL4:9,10;
end;
A11: for a st a <> 0 & a is limit_ordinal & for b st b in a holds P[b]
holds P[a]
proof
let a such that
A12: a <> 0 & a is limit_ordinal and
A13: for b st b in a holds P[b] and
A14: a in dom g;
g is continuous by A1,A2,Th53; then
f.a is_limes_of (f|a) & g.a is_limes_of (g|a)
by A6,A7,A12,A14,ORDINAL2:def 13; then
A15: f.a = lim(f|a) & g.a = lim(g|a) by ORDINAL2:def 10;
A16: f|a is increasing & g|a is increasing by A6,ORDINAL4:15;
A17: a c= dom f & a c= dom g by A7,A14,ORDINAL1:def 2; then
A18: dom (f|a) = a & dom (g|a) = a by RELAT_1:62; then
Union(f|a) is_limes_of (f|a) & Union(g|a) is_limes_of (g|a)
by A12,A16,ORDINAL5:6; then
A19: f.a = Union(f|a) & g.a = Union(g|a) by A15,ORDINAL2:def 10;
let b; assume b in f.a; then
consider x being object such that
A20: x in a & b in (f|a).x by A18,A19,CARD_5:2;
(f|a).x = f.x & (g|a).x = g.x & f.x c= g.x by A17,A13,A20,FUNCT_1:49;
hence b in g.a by A20,A18,A19,CARD_5:2;
end;
for a holds P[a] from ORDINAL2:sch 1(A8,A9,A11);
hence thesis by A3;
end;
theorem Th55:
for g1,g2 being Ordinal-Sequence-valued Sequence
st dom g1 = dom g2 & dom g1 <> {} & for a st a in dom g1 holds g1.a c= g2.a
holds criticals g1 c= criticals g2
proof
let g1,g2 be Ordinal-Sequence-valued Sequence;
assume
A1: dom g1 = dom g2;
assume
A2: dom g1 <> {};
assume
A3: for a st a in dom g1 holds g1.a c= g2.a;
set f1 = g1.0, f2 = g2.0;
0 in dom g1 by A2,ORDINAL3:8; then
f1 c= f2 & f1 in rng g1 & f2 in rng g2 by A1,A3,FUNCT_1:def 3; then
A4: dom f1 c= dom f2 by GRFUNC_1:2;
set X = {a where a is Element of dom f1: a in dom f1 &
for f st f in rng g1 holds a is_a_fixpoint_of f};
set Z = {a where a is Element of dom f2: a in dom f2 &
for f st f in rng g2 holds a is_a_fixpoint_of f};
reconsider X,Z as ordinal-membered set by Th46;
set Y = Z\X;
A5: now let x,y; assume x in X; then
consider a being Element of dom f1 such that
A6: x = a & a in dom f1 & for f st f in rng g1 holds a is_a_fixpoint_of f;
assume y in Y; then
A7: y in Z & not y in X by XBOOLE_0:def 5; then
consider b being Element of dom f2 such that
A8: y = b & b in dom f2 & for f st f in rng g2 holds b is_a_fixpoint_of f;
assume not x in y; then
A9: b c= a by A6,A8,ORDINAL1:16; then
A10: b in dom f1 by A6,ORDINAL1:12;
now
let f; assume
A11: f in rng g1; then
consider z being object such that
A12: z in dom g1 & f = g1.z by FUNCT_1:def 3;
reconsider z as set by TARSKI:1;
A13: f c= g2.z by A3,A12;
g2.z in rng g2 by A1,A12,FUNCT_1:def 3; then
A14: b is_a_fixpoint_of g2.z by A8;
a is_a_fixpoint_of f by A6,A11; then
a in dom f; then
A15: b in dom f by A9,ORDINAL1:12; then
f.b = g2.z.b by A13,GRFUNC_1:2 .= b by A14;
hence b is_a_fixpoint_of f by A15;
end;
hence contradiction by A7,A8,A10;
end;
X c= Z
proof
let x be object; assume x in X; then
consider a being Element of dom f1 such that
A16: x = a & a in dom f1 & for f st f in rng g1 holds a is_a_fixpoint_of f;
now let f; assume
f in rng g2; then
consider z being object such that
A17: z in dom g2 & f = g2.z by FUNCT_1:def 3;
reconsider z as set by TARSKI:1;
A18: g1.z c= f by A1,A3,A17; then
A19: dom(g1.z) c= dom f by GRFUNC_1:2;
g1.z in rng g1 by A1,A17,FUNCT_1:def 3; then
a is_a_fixpoint_of g1.z by A16; then
a in dom(g1.z) & a = g1.z.a; then
a in dom f & a = f.a by A18,A19,GRFUNC_1:2;
hence a is_a_fixpoint_of f;
end;
hence thesis by A16,A4;
end; then
X\/Y = Z by XBOOLE_1:45; then
criticals g2 = (criticals g1)^numbering Y by A5,Th25;
hence criticals g1 c= criticals g2 by Th9;
end;
definition
let g be Ordinal-Sequence-valued Sequence;
func lims g -> Ordinal-Sequence means :Def12:
dom it = dom (g.0) & for a st a in dom it holds
it.a = union {g.b.a where b is Element of dom g: b in dom g};
existence
proof
deffunc X(Ordinal) = {g.b.$1 where b is Element of dom g: b in dom g};
deffunc F(Ordinal) = union On X($1);
consider f such that
A1: dom f = dom(g.0) & for a st a in dom(g.0) holds f.a = F(a)
from ORDINAL2:sch 3;
take f; thus dom f = dom(g.0) by A1;
let a; assume a in dom f; then
A2: f.a = F(a) by A1;
now
let x; assume x in X(a); then
ex b being Element of dom g st x = g.b.a & b in dom g;
hence x is ordinal;
end; then
X(a) is ordinal-membered by Th1;
hence thesis by A2,Th2;
end;
uniqueness
proof
let f1,f2 be Ordinal-Sequence such that
A3: dom f1 = dom (g.0) & for a st a in dom f1 holds f1.a =
union {g.b.a where b is Element of dom g: b in dom g} and
A4: dom f2 = dom (g.0) & for a st a in dom f2 holds f2.a =
union {g.b.a where b is Element of dom g: b in dom g};
thus dom f1 = dom f2 by A3,A4;
let x be object; assume
A5: x in dom f1; then
f1.x = union {g.b.x where b is Element of dom g: b in dom g} by A3;
hence thesis by A3,A4,A5;
end;
end;
theorem Th56:
for g being Ordinal-Sequence-valued Sequence
st dom g <> {} & dom g in U &
for a st a in dom g holds g.a is Ordinal-Sequence of U
holds lims g is Ordinal-Sequence of U
proof
let g be Ordinal-Sequence-valued Sequence;
assume
A1: dom g <> {} & dom g in U;
assume
A2: for a st a in dom g holds g.a is Ordinal-Sequence of U;
reconsider g0 = g.0 as Ordinal-Sequence of U by A2,A1,ORDINAL3:8;
A3: dom lims g = dom g0 by Def12 .= On U by FUNCT_2:def 1;
rng lims g c= On U
proof
let x be object; assume x in rng lims g; then
consider y being object such that
A4: y in dom lims g & x = (lims g).y by FUNCT_1:def 3;
reconsider y as Ordinal by A4;
set X = {g.b.y where b is Element of dom g: b in dom g};
A5: x = union X by A4,Def12;
reconsider a = dom g as non empty Ordinal of U by A1;
deffunc F(set) = g.$1.y;
A6: card {F(b) where b is Element of a: b in a} c= card a from TREES_2:sch 2;
card a c= a by CARD_1:8; then
card X c= a by A6; then
card X in U by CLASSES1:def 1; then
card X in On U by ORDINAL1:def 9; then
A7: card X in card U by CLASSES2:9;
A8: X c= On U
proof
let z be object; assume z in X; then
consider b being Element of a such that
A9: z = g.b.y & b in a;
reconsider f = g.b as Ordinal-Sequence of U by A2;
z = f.y by A9;
hence thesis by ORDINAL1:def 9;
end; then
reconsider u = union X as Ordinal by ORDINAL3:4;
On U c= U by ORDINAL2:7; then
X c= U by A8; then
X in U by A7,CLASSES1:1; then
u in U by CLASSES2:59;
hence thesis by A5,ORDINAL1:def 9;
end;
hence lims g is Ordinal-Sequence of U by A3,FUNCT_2:2;
end;
begin :: Veblen Hierarchy
definition
let x;
func OS@ x -> Ordinal-Sequence equals: Def13:
x if x is Ordinal-Sequence otherwise the Ordinal-Sequence;
correctness;
func OSV@ x -> Ordinal-Sequence-valued Sequence equals: Def14:
x if x is Ordinal-Sequence-valued Sequence
otherwise the Ordinal-Sequence-valued Sequence;
correctness;
end;
definition
let U;
func U-Veblen -> Ordinal-Sequence-valued Sequence means: Def15:
dom it = On U & it.0 = U exp omega &
(for b st succ b in On U holds it.succ b = criticals (it.b)) &
(for l st l in On U holds it.l = criticals (it|l));
existence
proof
reconsider o = omega as non trivial Ordinal;
deffunc C(set,set) = criticals OS@ $2;
deffunc D(set,set) = criticals OSV@ $2;
consider L being Sequence such that
A1: dom L = On U and
A2: 0 in On U implies L.0 = U exp o and
A3: for b st succ b in On U holds L.(succ b) = C(b,L.b) and
A4: for b st b in On U & b <> 0 & b is limit_ordinal holds L.b = D(b,L|b)
from ORDINAL2:sch 5;
defpred P[Ordinal] means
$1 in On U implies L.$1 is Ordinal-Sequence;
A5: P[0] by A2;
A6: P[b] implies P[succ b]
proof assume that
A7: P[b] and
A8: succ b in On U;
b in succ b by ORDINAL1:6; then
reconsider f = L.b as Ordinal-Sequence by A7,A8,ORDINAL1:10;
L.(succ b) = C(b,f) by A3,A8 .= criticals f by Def13;
hence thesis;
end;
A9: for b st b <> 0 & b is limit_ordinal & for c st c in b holds P[c]
holds P[b]
proof
let b; assume that
A10: b <> 0 & b is limit_ordinal and
for c st c in b holds P[c] and
A11: b in On U;
L.b = D(b,L|b) by A4,A10,A11;
hence thesis;
end;
A12: P[b] from ORDINAL2:sch 1(A5,A6,A9);
L is Ordinal-Sequence-valued
proof
let x; assume x in rng L; then
ex y being object st y in dom L & x = L.y by FUNCT_1:def 3;
hence thesis by A1,A12;
end; then
reconsider L as Ordinal-Sequence-valued Sequence;
take L;
0-element_of U in On U by ORDINAL1:def 9;
hence dom L = On U & L.0 = U exp omega by A1,A2;
hereby
let b; assume
A13: succ b in On U;
reconsider f = L.b as Ordinal-Sequence;
thus L.succ b = C(b,f) by A13,A3 .= criticals (L.b) by Def13;
end;
let l; assume l in On U;
hence L.l = D(l,L|l) by A4 .= criticals(L|l) by Def14;
end;
uniqueness
proof let g1,g2 be Ordinal-Sequence-valued Sequence such that
A14: dom g1 = On U and
A15: g1.0 = U exp omega and
A16: (for b st succ b in On U holds g1.succ b = criticals (g1.b)) and
A17: (for l st l in On U holds g1.l = criticals(g1|l)) and
A18: dom g2 = On U and
A19: g2.0 = U exp omega and
A20: (for b st succ b in On U holds g2.succ b = criticals (g2.b)) and
A21: (for l st l in On U holds g2.l = criticals(g2|l));
deffunc C(set,Ordinal-Sequence) = criticals $2;
deffunc D(set,Ordinal-Sequence-valued Sequence) = criticals $2;
A22: 0 in On U implies g1.0 = U exp omega by A15;
A23: for b st succ b in On U holds g1.succ b = C(b,g1.b) by A16;
A24: for a st a in On U & a <> 0 & a is limit_ordinal
holds g1.a = D(a,g1|a) by A17;
A25: 0 in On U implies g2.0 = U exp omega by A19;
A26: for b st succ b in On U holds g2.succ b = C(b,g2.b) by A20;
A27: for a st a in On U & a <> 0 & a is limit_ordinal
holds g2.a = D(a,g2|a) by A21;
thus g1 = g2 from ORDINAL2:sch 4(A14,A22,A23,A24,A18,A25,A26,A27);
end;
end;
registration
cluster uncountable for Universe;
existence
proof
take U = Tarski-Class omega;
omega in U by CLASSES1:2; then
card omega in card U by CLASSES2:1;
hence card U c/= omega;
end;
end;
theorem Th57:
for U being Universe holds U is uncountable iff omega in U
proof
let U be Universe;
thus U is uncountable implies omega in U
proof assume
card U c/= omega; then
omega in card U by Th4; then
omega in On U by CLASSES2:9;
hence omega in U by ORDINAL1:def 9;
end;
assume omega in U; then
card omega in card U by CLASSES2:1;
hence card U c/= omega;
end;
theorem Th58:
a in b & b in U & omega in U & c in dom(U-Veblen.b)
implies U-Veblen.b.c is_a_fixpoint_of U-Veblen.a
proof assume
A1: a in b & b in U & omega in U;
set F = U-Veblen;
defpred P[Ordinal] means $1 in U implies
for a,c st a in $1 & c in dom(F.$1) holds F.$1.c is_a_fixpoint_of F.a;
A2: P[0];
A3: for b st P[b] holds P[succ b]
proof
let b such that
A4: P[b] and
A5: succ b in U;
A6: b in succ b by ORDINAL1:6;
let a,c;
assume a in succ b; then
A7: a in b or a in {b} by XBOOLE_0:def 3;
succ b in On U by A5,ORDINAL1:def 9; then
A8: F.succ b = criticals(F.b) by Def15;
assume c in dom(F.succ b); then
F.(succ b).c is_a_fixpoint_of F.b by A8,Th29; then
F.(succ b).c in dom(F.b) & F.(succ b).c = F.b.(F.(succ b).c);
hence thesis by A4,A5,A6,A7,ORDINAL1:10,TARSKI:def 1;
end;
A9: dom F = On U by Def15;
A10: for b st b <> 0 & b is limit_ordinal & for d st d in b holds P[d]
holds P[b]
proof
let b such that
A11: b <> 0 & b is limit_ordinal and
for d st d in b holds P[d] and
A12: b in U;
A13: b in On U by A12,ORDINAL1:def 9; then
A14: F.b = criticals(F|b) by A11,Def15;
b c= On U by A13,ORDINAL1:def 2; then
A15: dom(F|b) = b by A9,RELAT_1:62;
let a,c; assume
A16: a in b; then
A17: F.a = (F|b).a by FUNCT_1:49;
set g = F|b;
set X = {z where z is Element of dom(g.0): z in dom(g.0) &
for f st f in rng g holds z is_a_fixpoint_of f};
now
let x; assume x in X; then
ex a being Element of dom(g.0) st x = a & a in dom(g.0) &
for f st f in rng g holds a is_a_fixpoint_of f;
hence x is ordinal;
end; then
reconsider X as ordinal-membered set by Th1;
assume
c in dom(F.b); then
F.b.c in rng (F.b) by FUNCT_1:def 3; then
F.b.c in X by A14,Th19; then
consider z being Element of dom(g.0) such that
A18: F.b.c = z & z in dom(g.0) &
for f st f in rng g holds z is_a_fixpoint_of f;
F.a in rng g by A15,A17,A16,FUNCT_1:def 3;
hence thesis by A18;
end;
for b holds P[b] from ORDINAL2:sch 1(A2,A3,A10);
hence thesis by A1;
end;
theorem
l in U & (for c st c in l holds a is_a_fixpoint_of U-Veblen.c)
implies a is_a_fixpoint_of lims(U-Veblen|l)
proof
assume
A1: l in U;
assume
A2: for c st c in l holds a is_a_fixpoint_of U-Veblen.c;
set F = U-Veblen; set g = F|l;
set X = {g.d.a where d is Element of dom g: d in dom g};
set u = union X;
A3: 0 in l by ORDINAL3:8; then
omega c= l by ORDINAL1:def 11; then
reconsider o = omega as non trivial Ordinal of U by A1,CLASSES1:def 1;
F.0 = U exp o by Def15; then
reconsider f0 = F.0 as normal Ordinal-Sequence of U;
A4: f0 = g.0 by FUNCT_1:49,ORDINAL3:8; then
A5: dom lims g = dom f0 & dom f0 = On U by Def12,FUNCT_2:def 1;
A6: a is_a_fixpoint_of f0 by A2,ORDINAL3:8; then
A7: a in On U & a = f0.a by A5;
A8: dom F = On U by Def15;
l in On U by A1,ORDINAL1:def 9; then
l c= dom F by A8,ORDINAL1:def 2; then
A9: dom g = l by RELAT_1:62;
set lg = lims g;
thus a in dom lims g by A5,A6;
A10: lg.a = u by A5,A7,Def12;
{a} = X
proof
a in X by A3,A9,A7,A4;
hence {a} c= X by ZFMISC_1:31;
let x be object; assume x in X; then
consider d being Element of dom g such that
A11: x = g.d.a & d in dom g;
g.d = F.d by A11,FUNCT_1:47; then
a is_a_fixpoint_of g.d by A2,A9; then
x = a by A11;
hence thesis by TARSKI:def 1;
end;
hence a = (lims g).a by A10,ZFMISC_1:25;
end;
theorem Th60:
a c= b & b in U & omega in U & c in dom(U-Veblen.b) &
(for c st c in b holds U-Veblen.c is normal)
implies U-Veblen.a.c c= U-Veblen.b.c
proof assume
A1: a c= b & b in U & omega in U & c in dom(U-Veblen.b);
set F = U-Veblen;
defpred P[Ordinal] means
for a,c st a c= $1 & $1 in U & c in dom(F.$1) &
for c st c in $1 holds U-Veblen.c is normal holds F.a.c c= F.$1.c;
A2: P[0];
A3: for b st P[b] holds P[succ b]
proof
let b such that
A4: P[b];
let a,c such that
A5: a c= succ b and
A6: succ b in U and
A7: c in dom(F.succ b);
assume
A8: for c st c in succ b holds U-Veblen.c is normal;
succ b in On U by A6,ORDINAL1:def 9; then
A9: F.succ b = criticals (F.b) by Def15; then
A10: dom(F.succ b) c= dom(F.b) by Th32;
A11: b in succ b by ORDINAL1:6; then
A12: b in U by A6,ORDINAL1:10;
F.b is normal by A8,ORDINAL1:6; then
A13: F.b.c c= F.succ b.c by A7,A9,Th45;
A14: for c st c in b holds F.c is normal by A8,A11,ORDINAL1:10;
per cases by A5,ORDINAL5:1;
suppose a = succ b;
hence thesis;
end;
suppose a c= b; then
F.a.c c= F.b.c by A4,A7,A10,A12,A14;
hence thesis by A13;
end;
end;
A15: for b st b <> 0 & b is limit_ordinal & for d st d in b holds P[d]
holds P[b]
proof
let b;
assume
A16: b <> 0 & b is limit_ordinal;
assume for d st d in b holds P[d];
let a,c;
assume
A17: a c= b;
per cases by A17;
suppose a = b;
hence thesis;
end;
suppose
A18: a c< b; then
A19: a in b by ORDINAL1:11;
assume
b in U; then
A20: b in On U by ORDINAL1:def 9; then
A21: F.b = criticals(F|b) by A16,Def15;
dom F = On U by Def15; then
b c= dom F by A20,ORDINAL1:def 2; then
A22: dom(F|b) = b by RELAT_1:62;
assume
A23: c in dom(F.b);
assume
A24: for c st c in b holds U-Veblen.c is normal;
A25: now let c; assume c in dom(F|b); then
c in b & (F|b).c = F.c by A22,FUNCT_1:49;
hence (F|b).c is normal by A24;
end;
A26: (F|b).a in rng(F|b) by A19,A22,FUNCT_1:def 3;
(F|b).a = F.a by A18,FUNCT_1:49,ORDINAL1:11;
hence F.a.c c= F.b.c by A19,A21,A22,A23,A25,A26,Th54;
end;
end;
for b holds P[b] from ORDINAL2:sch 1(A2,A3,A15);
hence thesis by A1;
end;
theorem Th61:
l in U & a in U & b in l &
(for c st c in l holds U-Veblen.c is normal Ordinal-Sequence of U)
implies (lims(U-Veblen|l)).a is_a_fixpoint_of U-Veblen.b
proof assume that
A1: l in U and
A2: a in U and
A3: b in l and
A4: for c st c in l holds U-Veblen.c is normal Ordinal-Sequence of U;
set F = U-Veblen;
set g = F|l;
set X = {g.d.a where d is Element of dom g: d in dom g};
set u = union X;
A5: 0 in l by ORDINAL3:8;
reconsider f0 = F.0, f = F.b as normal Ordinal-Sequence of U
by A3,A4,ORDINAL3:8;
A6: f0 = g.0 & f = g.b by A3,FUNCT_1:49,ORDINAL3:8; then
A7: dom lims g = dom f0 by Def12 .= On U by FUNCT_2:def 1;
A8: dom F = On U by Def15;
l in On U by A1,ORDINAL1:def 9; then
l c= dom F by A8,ORDINAL1:def 2; then
A9: dom g = l by RELAT_1:62; then
A10: g.b.a in X by A3;
now
let c; assume
A11: c in dom g; then
g.c = F.c by FUNCT_1:47;
hence g.c is Ordinal-Sequence of U by A9,A11,A4;
end; then
reconsider lg = lims g as Ordinal-Sequence of U by A1,A9,Th56;
A12: a in On U by A2,ORDINAL1:def 9; then
A13: lg.a = u by A7,Def12;
A14: dom f = On U & dom f0 = On U by FUNCT_2:def 1;
A15: for x st x in X ex y st x c= y & y in X & y is_a_fixpoint_of f
proof let x; assume
A16: x in X; then
consider d being Element of dom g such that
A17: x = g.d.a & d in dom g;
reconsider f2 = F.d as normal Ordinal-Sequence of U by A4,A9;
A18: f2 = g.d by A9,FUNCT_1:49;
A19: dom f2 = On U by FUNCT_2:def 1;
omega c= l by A5,ORDINAL1:def 11; then
A20: d in U & omega in U by A9,A1,CLASSES1:def 1,ORDINAL1:10;
A21: b in U by A1,A3,ORDINAL1:10;
A22: for c st c in b holds U-Veblen.c is normal by A4,A3,ORDINAL1:10;
per cases by ORDINAL1:16;
suppose
d c= b; then
A23: x c= g.b.a by A12,A6,A14,A17,A18,A20,A21,A22,Th60;
take y = g.(succ b).a;
A24: b in succ b & succ b in l by A3,ORDINAL1:6,28; then
reconsider f1 = F.succ b as normal Ordinal-Sequence of U by A4;
A25: f1 = g.succ b by A24,FUNCT_1:49;
succ b in U by A24,A1,ORDINAL1:10; then
succ b in On U by ORDINAL1:def 9; then
A26: f1 = criticals f & dom f1 = On U by Def15,FUNCT_2:def 1; then
f.a c= y by A12,A25,Th45;
hence x c= y by A23,A6;
thus y in X by A9,A24;
thus thesis by A12,A25,A26,Th29;
end;
suppose
A27: b in d;
take y = x;
thus x c= y & y in X by A16;
thus thesis by A12,A17,A27,A18,A19,A20,Th58;
end;
end;
thus (lims(U-Veblen|l)).a in dom(U-Veblen.b) by A13,A14,ORDINAL1:def 9;
hence thesis by A13,A10,A15,Th36;
end;
Lm1:
omega in U implies U-Veblen.0 is normal Ordinal-Sequence of U
proof
assume omega in U;
then reconsider o = omega as non trivial Ordinal of U;
U-Veblen.0 = U exp o by Def15;
hence U-Veblen.0 is normal Ordinal-Sequence of U;
end;
Lm2:
omega in U & a in U & U-Veblen.a is normal Ordinal-Sequence of U
implies U-Veblen.succ a is normal Ordinal-Sequence of U
proof assume that
A1: omega in U and
A2: a in U;
assume U-Veblen.a is normal Ordinal-Sequence of U;
then reconsider f = U-Veblen.a as normal Ordinal-Sequence of U;
succ a in U by A2,CLASSES2:5;
then succ a in On U by ORDINAL1:def 9;
then U-Veblen.succ a = criticals f by Def15;
hence U-Veblen.succ a is normal Ordinal-Sequence of U
by A1,Th44;
end;
Lm3:
l in U & (for a st a in l holds U-Veblen.a is normal Ordinal-Sequence of U)
implies U-Veblen.l is normal Ordinal-Sequence of U
proof
assume
A1: l in U;
assume
A2: for a st a in l holds U-Veblen.a is normal Ordinal-Sequence of U;
A3: l in On U by A1,ORDINAL1:def 9; then
A4: U-Veblen.l = criticals(U-Veblen|l) by Def15;
A5: dom(U-Veblen) = On U by Def15;
l c= On U by A3,ORDINAL1:def 2; then
A6: dom(U-Veblen|l) = l by A5,RELAT_1:62;
A7: dom (U-Veblen.l) = On U
proof set F = U-Veblen; set G = F.l;
A8: 0 in l by ORDINAL3:8;
reconsider f0 = F.0 as normal Ordinal-Sequence of U by A2,ORDINAL3:8;
A9: dom f0 = On U by FUNCT_2:def 1;
A10: f0 = (F|l).0 by FUNCT_1:49,ORDINAL3:8; then
f0 in rng (F|l) by A6,A8,FUNCT_1:def 3;
hence dom G c= On U by A4,A9,Th49;
now
let c; assume
A11: c in dom (F|l); then
(F|l).c = F.c by FUNCT_1:47;
hence (F|l).c is Ordinal-Sequence of U by A6,A11,A2;
end; then
reconsider lg = lims (F|l) as Ordinal-Sequence of U by A1,A6,Th56;
A12: dom lg = On U by FUNCT_2:def 1;
rng lg c= rng G
proof let y be object;
assume y in rng lg; then
consider x being object such that
A13: x in dom lg & y = lg.x by FUNCT_1:def 3;
reconsider x as Ordinal by A13;
y = lg.x by A13;
then
A14: x in U & y in On U by A12,A13,ORDINAL1:def 9;
set Y = {a where a is Element of dom((F|l).0): a in dom((F|l).0) &
for f st f in rng(F|l) holds a is_a_fixpoint_of f};
A15: Y is ordinal-membered by Th46;
now let f;
assume f in rng(F|l); then
consider z being object such that
A16: z in l & f = (F|l).z by A6,FUNCT_1:def 3;
f = F.z by A16,FUNCT_1:49;
hence y is_a_fixpoint_of f by A1,A2,A16,A13,A14,Th61;
end; then
y in Y by A9,A10,A14;
hence thesis by A4,A15,Th19;
end; then
A17: Union lg c= Union G by ZFMISC_1:77;
On U c= Union lg
proof
let a; assume
A18: a in On U;
A19: a in succ a by ORDINAL1:6;
set X = {(F|l).b.succ a where b is Element of dom(F|l):b in dom(F|l)};
On U is limit_ordinal by CLASSES2:51; then
A20: succ a in On U by A18,ORDINAL1:28; then
A21: lg.succ a = union X by A12,Def12;
A22: f0.succ a in X by A10,A6,A8;
A23: f0.a in f0.succ a by A19,A20,A9,ORDINAL2:def 12;
a c= f0.a by A9,A18,ORDINAL4:10; then
a in f0.succ a by A23,ORDINAL1:12; then
a in lg.succ a by A21,A22,TARSKI:def 4;
hence thesis by A12,A20,CARD_5:2;
end; then
A24: On U c= Union G by A17;
A25: rng G c= U
proof let x be object;
reconsider xx=x as set by TARSKI:1;
assume x in rng G; then
consider y being object such that
A26: y in dom G & x = G.y by FUNCT_1:def 3;
x is_a_fixpoint_of f0 by A4,A6,A8,A10,A26,Th47; then
xx in dom f0 & xx = f0.xx;
hence thesis;
end;
assume On U c/= dom G; then
dom G in On U by ORDINAL1:16; then
reconsider d = dom G as Ordinal of U by ORDINAL1:def 9;
A27: card d in card U by CLASSES2:1;
card rng G c= card d by CARD_1:12; then
card rng G in card U by A27,ORDINAL1:12; then
reconsider r = rng G as Element of U by A25,CLASSES1:1;
union r in U; then
Union G in On U by ORDINAL1:def 9; then
Union G in Union G by A24;
hence thesis;
end;
A28: rng (U-Veblen.l) c= On U
proof
let x be object; assume x in rng(U-Veblen.l); then
consider y being object such that
A29: y in dom (U-Veblen.l) & x = (U-Veblen.l).y by FUNCT_1:def 3;
reconsider y as Ordinal by A29;
A30: 0 in l by ORDINAL3:8; then
x is_a_fixpoint_of (U-Veblen|l).0 by A4,A29,A6,Th47; then
x in dom ((U-Veblen|l).0); then
x in dom (U-Veblen.0) & U-Veblen.0 is Ordinal-Sequence of U
by A2,A30,FUNCT_1:49;
hence thesis by FUNCT_2:def 1;
end;
now let a;
assume
A31: a in l; then
(U-Veblen|l).a = U-Veblen.a by FUNCT_1:49;
hence (U-Veblen|l).a is normal by A2,A31;
end; then
U-Veblen.l is continuous by A4,A6,Th53;
hence U-Veblen.l is normal Ordinal-Sequence of U by A4,A7,A28,FUNCT_2:2;
end;
theorem Th62:
omega in U & a in U implies U-Veblen.a is normal Ordinal-Sequence of U
proof assume
A1: omega in U;
defpred P[Ordinal] means
$1 in U implies U-Veblen.$1 is normal Ordinal-Sequence of U;
A2: P[0] by A1,Lm1;
A3: P[b] implies P[succ b]
proof
b in succ b by ORDINAL1:6;
then succ b in U implies b in U by ORDINAL1:10;
hence thesis by A1,Lm2;
end;
A4: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
proof assume that
A5: b <> 0 & b is limit_ordinal and
A6: for c st c in b holds P[c] and
A7: b in U;
now
let a; assume
A8: a in b;
then a in U by A7,ORDINAL1:10;
hence U-Veblen.a is normal Ordinal-Sequence of U by A6,A8;
end;
hence thesis by A5,A7,Lm3;
end;
P[b] from ORDINAL2:sch 1(A2,A3,A4);
hence thesis;
end;
theorem Th63:
omega in U & U c= W & a in U implies U-Veblen.a c= W-Veblen.a
proof assume
A1: omega in U & U c= W; then
A2: On U c= On W by ORDINAL2:9;
defpred P[Ordinal] means
$1 in U implies U-Veblen.$1 c= W-Veblen.$1;
A3: U-Veblen.0 = U exp omega & W-Veblen.0 = W exp omega by Def15;
A4: dom (U exp omega) = On U & dom (W exp omega) = On W by FUNCT_2:def 1;
now let x be object; assume
x in On U; then
reconsider a = x as Ordinal of U by ORDINAL1:def 9;
reconsider b = a as Ordinal of W by A1;
(U exp omega).a = exp(omega,b) by A1,Def8;
hence (U exp omega).x = (W exp omega).x by A1,Def8;
end; then
A5: P[0] by A2,A3,A4,GRFUNC_1:2;
A6: P[b] implies P[succ b]
proof assume
A7: P[b]; assume
A8: succ b in U;
A9: b in succ b by ORDINAL1:6;
succ b in On U & succ b in On W by A1,A8,ORDINAL1:def 9; then
U-Veblen.succ b = criticals (U-Veblen.b) &
W-Veblen.succ b = criticals (W-Veblen.b) by Def15;
hence thesis by A7,A9,Th40,A8,ORDINAL1:10;
end;
A10: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
proof assume that
A11: b <> 0 & b is limit_ordinal and
A12: for c st c in b holds P[c] and
A13: b in U;
set g1 = U-Veblen|b, g2 = W-Veblen|b;
A14: b in On U & b in On W by A1,A13,ORDINAL1:def 9; then
A15: U-Veblen.b = criticals g1 & W-Veblen.b = criticals g2 by A11,Def15;
dom(U-Veblen) = On U & dom(W-Veblen) = On W by Def15; then
b c= dom(U-Veblen) & b c= dom(W-Veblen) by A14,ORDINAL1:def 2; then
A16: dom g1 = b & dom g2 = b by RELAT_1:62;
now
let a; assume
A17: a in dom g1; then
A18: g1.a = U-Veblen.a & g2.a = W-Veblen.a by A16,FUNCT_1:47;
a in U by A13,A16,A17,ORDINAL1:10;
hence g1.a c= g2.a by A12,A16,A17,A18;
end;
hence thesis by A11,A15,A16,Th55;
end;
P[b] from ORDINAL2:sch 1(A5,A6,A10);
hence thesis;
end;
theorem Th64:
omega in U & a in U & b in U & omega in W & a in W & b in W implies
U-Veblen.b.a = W-Veblen.b.a
proof assume
A1: omega in U & a in U & b in U & omega in W & a in W & b in W; then
A2: a in On U & a in On W by ORDINAL1:def 9;
W-Veblen.b is Ordinal-Sequence of W &
U-Veblen.b is Ordinal-Sequence of U by A1,Th62; then
A3: dom(U-Veblen.b) = On U & dom(W-Veblen.b) = On W by FUNCT_2:def 1;
U c= W or W in U by CLASSES2:53; then
U c= W or W c= U by ORDINAL1:def 2; then
U-Veblen.b c= W-Veblen.b or W-Veblen.b c= U-Veblen.b by A1,Th63;
hence thesis by A2,A3,GRFUNC_1:2;
end;
theorem
l in U & (for a st a in l holds
U-Veblen.a is normal Ordinal-Sequence of U)
implies lims(U-Veblen|l) is non-decreasing continuous Ordinal-Sequence of U
proof set G = U-Veblen;
assume that
A1: l in U and
A2: for a st a in l holds G.a is normal Ordinal-Sequence of U;
0 in l by ORDINAL3:8; then
omega c= l by ORDINAL1:def 11; then
A3: omega in U & l in On U by A1,CLASSES1:def 1,ORDINAL1:def 9; then
A4: G.l = criticals(G|l) & dom G = On U by Def15;
l c= On U by A3,ORDINAL1:def 2; then
A5: dom(G|l) = l by A4,RELAT_1:62;
set g = G|l;
now let a; assume
A6: a in dom g; then
g.a = G.a by A5,FUNCT_1:49;
hence g.a is Ordinal-Sequence of U by A2,A5,A6;
end; then
reconsider f = lims g as Ordinal-Sequence of U by A1,A5,Th56;
g.0 = G.0 by FUNCT_1:49,ORDINAL3:8; then
reconsider g0 = g.0 as Ordinal-Sequence of U by A2,ORDINAL3:8;
A7: dom f = On U by FUNCT_2:def 1;
deffunc X(object) = {g.b.$1 where b is Element of dom g: b in dom g};
A8: f is non-decreasing
proof
let a,b; assume
A9: a in b & b in dom f; then
a in dom f by ORDINAL1:10; then
A10: f.a = union X(a) & f.b = union X(b) by A9,Def12;
let c; assume c in f.a; then
consider x such that
A11: c in x & x in X(a) by A10,TARSKI:def 4;
consider xa being Element of dom g such that
A12: x = g.xa.a & xa in dom g by A11;
g.xa = G.xa by A5,FUNCT_1:49; then
reconsider h = g.xa as increasing Ordinal-Sequence of U by A2,A5;
dom h = On U by FUNCT_2:def 1; then
h.a in h.b by A7,A9,ORDINAL2:def 12; then
h.a c= h.b by ORDINAL1:def 2; then
c in h.b & h.b in X(b) by A11,A12;
hence c in f.b by A10,TARSKI:def 4;
end;
f is continuous
proof let a,b; assume
A13: a in dom f & a <> 0 & a is limit_ordinal & b = f.a; then
A14: b = union X(a) by Def12;
A15: a c= dom f by A13,ORDINAL1:def 2; then
A16: dom(f|a) = a by RELAT_1:62;
A17: b = Union(f|a)
proof
thus b c= Union(f|a)
proof
let c; assume c in b; then
consider x such that
A18: c in x & x in X(a) by A14,TARSKI:def 4;
consider xa being Element of dom g such that
A19: x = g.xa.a & xa in dom g by A18;
g.xa = G.xa by A5,FUNCT_1:49; then
reconsider h = g.xa as normal Ordinal-Sequence of U
by A2,A5;
A20: dom h = On U by FUNCT_2:def 1; then
A21: h.a is_limes_of h|a by A7,A13,ORDINAL2:def 13;
A22: h|a is increasing by ORDINAL4:15;
A23: dom(h|a) = a by A7,A15,A20,RELAT_1:62; then
Union(h|a) is_limes_of h|a by A13,A22,ORDINAL5:6; then
lim(h|a) = Union(h|a) by ORDINAL2:def 10; then
h.a = Union(h|a) by A21,ORDINAL2:def 10; then
consider y being object such that
A24: y in a & c in (h|a).y by A18,A19,A23,CARD_5:2;
A25: y in On U by A7,A13,A24,ORDINAL1:10;
(h|a).y = h.y by A24,FUNCT_1:49; then
(h|a).y in X(y) by A19; then
c in union X(y) by A24,TARSKI:def 4; then
c in f.y by A7,A25,Def12; then
c in (f|a).y by A24,FUNCT_1:49;
hence thesis by A16,A24,CARD_5:2;
end;
let c; assume c in Union(f|a); then
consider x being object such that
A26: x in dom(f|a) & c in (f|a).x by CARD_5:2;
A27: (f|a).x = f.x by A16,A26,FUNCT_1:49;
x in dom f by A26,RELAT_1:57; then
f.x = union X(x) by Def12; then
consider y such that
A28: c in y & y in X(x) by A26,A27,TARSKI:def 4;
consider z being Element of dom g such that
A29: y = g.z.x & z in dom g by A28;
g.z = G.z by A5,FUNCT_1:49; then
reconsider h = g.z as normal Ordinal-Sequence of U
by A2,A5;
dom h = On U by FUNCT_2:def 1; then
h.x in h.a by A26,A16,A13,A7,ORDINAL2:def 12; then
h.x c= h.a by ORDINAL1:def 2; then
c in h.a & h.a in X(a) by A28,A29;
hence c in b by A14,TARSKI:def 4;
end;
f|a is non-decreasing by A8,Th13;
hence b is_limes_of f|a by A13,A16,A17,ORDINAL5:6;
end;
hence thesis by A8;
end;
registration
let a;
cluster Tarski-Class(a \/ omega) -> uncountable;
coherence
proof
set U = Tarski-Class(a \/ omega);
omega c= a \/ omega & a \/ omega in U by CLASSES1:2,XBOOLE_1:7; then
omega in U by CLASSES1:def 1;
hence thesis by Th57;
end;
end;
definition
let a,b;
func a-Veblen(b) -> Ordinal equals
(Tarski-Class(a \/ b \/ omega))-Veblen.a.b;
coherence;
end;
definition
let n,b;
redefine func n-Veblen(b) -> Ordinal equals :: redefines -Veblen (ORDINAL6, definition)
(Tarski-Class(b \/ omega))-Veblen.n.b;
coherence;
compatibility
proof
n c= omega; then
n\/omega = omega by XBOOLE_1:12;
hence thesis by XBOOLE_1:4;
end;
end;
theorem Th66:
a in Tarski-Class(a\/b\/c)
proof set U = Tarski-Class(a\/b\/c);
a c= a\/b & a\/b c= a\/b\/c by XBOOLE_1:7; then
a c= a\/b\/c & a\/b\/c in U by CLASSES1:2;
hence thesis by CLASSES1:def 1;
end;
theorem Th67:
omega in U & a in U & b in U implies b-Veblen a = U-Veblen.b.a
proof assume
A1: omega in U & a in U & b in U;
set W = Tarski-Class(b\/a\/omega);
omega in W & a in W & b in W by Th57,Th66;
hence b-Veblen a = U-Veblen.b.a by A1,Th64;
end;
theorem Th68:
0-Veblen(a) = exp(omega,a)
proof
set b = 0\/a\/omega;
set U = Tarski-Class b;
b in U by CLASSES1:2; then
A1: b in On U by ORDINAL1:def 9;
omega in On U by A1,ORDINAL1:12,XBOOLE_1:7; then
A2: omega in U by ORDINAL1:def 9;
a in On U by A1,ORDINAL1:12,XBOOLE_1:7; then
A3: a in U by ORDINAL1:def 9;
thus 0-Veblen(a) = (U exp omega).a by Def15
.= exp(omega,a) by A3,A2,Def8;
end;
theorem Th69:
b-Veblen((succ b)-Veblen a) = (succ b)-Veblen a
proof set U = Tarski-Class(b\/a\/omega);
A1: omega in U by Th57;
reconsider b1 = b as Ordinal of U by Th66;
succ b1 in On U by ORDINAL1:def 9; then
A2: U-Veblen.(succ b) = criticals (U-Veblen.b) by Def15;
reconsider f = U-Veblen.b1, g = U-Veblen.(succ b1) as
normal Ordinal-Sequence of U by A1,Th62;
A3: a in U by Th66; then
A4: a in On U by ORDINAL1:def 9;
A5: dom f = On U & dom g = On U by FUNCT_2:def 1;
set W = Tarski-Class(b\/(g.a)\/omega);
omega in U by Th57;
then
A6: (succ b1)-Veblen a = g.a & b1-Veblen(g.a) = f.(g.a) by A3,Th67; then
(succ b)-Veblen a is_a_fixpoint_of U-Veblen.b by A4,A2,A5,Th29;
hence b-Veblen((succ b)-Veblen a) = (succ b)-Veblen a by A6;
end;
theorem Th70:
b in c implies b-Veblen(c-Veblen a) = c-Veblen a
proof assume
A1: b in c;
set U = Tarski-Class(c\/a\/omega);
A2: omega in U by Th57;
A3: a in U & c in U by Th66; then
A4: b in U by A1,ORDINAL1:10; then
reconsider f = U-Veblen.b, g = U-Veblen.c as normal Ordinal-Sequence of U
by A2,Th66,Th62;
dom g = On U by FUNCT_2:def 1; then
a in dom g by A3,ORDINAL1:def 9; then
g.a is_a_fixpoint_of f by A1,A2,Th66,Th58; then
g.a = f.(g.a);
hence b-Veblen(c-Veblen a) = c-Veblen a by A2,A4,Th67;
end;
theorem Th71:
a c= b iff c-Veblen a c= c-Veblen b
proof
set U = Tarski-Class(c\/b\/omega);
set W = Tarski-Class(c\/a\/omega);
A1: n in omega & omega in U & omega in W by Th57,ORDINAL1:def 12;
A2: b in U & c in U by Th66;
A3: a in W & c in W by Th66;
reconsider f = U-Veblen.c as increasing Ordinal-Sequence of U
by A1,Th66,Th62;
reconsider g = W-Veblen.c as increasing Ordinal-Sequence of W
by A1,Th66,Th62;
A4: dom f = On U & dom g = On W by FUNCT_2:def 1;
A5: b in On U & a in On W by A2,A3,ORDINAL1:def 9;
hereby
assume
A6: a c= b; then
A7: a in U by A2,CLASSES1:def 1;
per cases by A6;
suppose a = b;
hence c-Veblen a c= c-Veblen b;
end;
suppose a c< b; then
a in b by ORDINAL1:11; then
f.a in f.b by A4,A5,ORDINAL2:def 12; then
c-Veblen a in c-Veblen b by A7,A1,A2,A3,Th64;
hence c-Veblen a c= c-Veblen b by ORDINAL1:def 2;
end;
end;
assume
A8: c-Veblen a c= c-Veblen b & a c/= b; then
A9: b in a by ORDINAL1:16; then
A10: b in W by A3,ORDINAL1:10;
g.b in g.a by A4,A5,A9,ORDINAL2:def 12; then
c-Veblen b in c-Veblen a by A1,A2,A3,A10,Th64; then
c-Veblen b in c-Veblen b by A8;
hence thesis;
end;
theorem Th72:
a in b iff c-Veblen a in c-Veblen b
proof
b c= a iff c-Veblen b c= c-Veblen a by Th71;
hence thesis by Th4;
end;
theorem
a-Veblen b in c-Veblen d iff
a = c & b in d or
a in c & b in c-Veblen d or
c in a & a-Veblen b in d
proof
hereby
assume
A1: a-Veblen b in c-Veblen d;
per cases by ORDINAL1:14;
case a = c;
hence b in d by A1,Th72;
end;
case a in c; then
a-Veblen(c-Veblen d) = c-Veblen d by Th70;
hence b in c-Veblen d by A1,Th72;
end;
case c in a; then
c-Veblen(a-Veblen b) = a-Veblen b by Th70;
hence a-Veblen b in d by A1,Th72;
end;
end;
assume
A2: a = c & b in d or a in c & b in c-Veblen d or c in a & a-Veblen b in d;
per cases by A2;
suppose a = c & b in d;
hence a-Veblen b in c-Veblen d by Th72;
end;
suppose
A3: a in c & b in c-Veblen d; then
a-Veblen(c-Veblen d) = c-Veblen d by Th70;
hence a-Veblen b in c-Veblen d by A3,Th72;
end;
suppose
A4: c in a & a-Veblen b in d; then
c-Veblen(a-Veblen b) = a-Veblen b by Th70;
hence a-Veblen b in c-Veblen d by A4,Th72;
end;
end;
begin :: Epsilon Numbers
reserve U for uncountable Universe;
theorem Th74:
U-Veblen.1 = criticals(U exp omega)
proof set o = succ(0-element_of U);
o in On U by ORDINAL1:def 9; then
U-Veblen.1 = criticals(U-Veblen.0) by Def15;
hence thesis by Def15;
end;
theorem Th75:
1-Veblen(a) is epsilon
proof set U = Tarski-Class(a\/omega);
0-Veblen(1-Veblen a) = (succ 0)-Veblen a by Th69;
hence exp(omega,1-Veblen a) = 1-Veblen a by Th68;
end;
theorem Th76:
for e being epsilon Ordinal ex a st e = 1-Veblen a
proof
let e be epsilon Ordinal;
set U = Tarski-Class(e\/omega);
A1: omega in U by Th57;
0-element_of U = 0 & 1-element_of U = 1; then
reconsider f = U-Veblen.0, g = U-Veblen.1 as
normal Ordinal-Sequence of U by A1,Th62;
A2: g = criticals(U exp omega) by Th74
.= criticals f by Def15;
A3: f.e = 0-Veblen e .= exp(omega,e) by Th68 .= e by ORDINAL5:def 5;
A4: dom f = On U by FUNCT_2:def 1;
e c= e\/omega & e\/omega in U by CLASSES1:2,XBOOLE_1:7; then
A5: e in U by CLASSES1:def 1; then
e in On U by ORDINAL1:def 9; then
e is_a_fixpoint_of f by A3,A4; then
consider a such that
A6: a in dom criticals f & e = (criticals f).a by Th33;
take a;
set W = Tarski-Class(a\/omega);
A7: a c= a\/omega & a\/omega in W by CLASSES1:2,XBOOLE_1:7;
a c= e by A6,ORDINAL4:10; then
omega in W & a in W & a in U & 1-element_of U = 1-element_of W
by A5,A7,Th57,CLASSES1:def 1;
hence e = 1-Veblen a by A1,A2,A6,Th64;
end;
Lm4:
1-Veblen 0 = epsilon_0
proof
consider b such that
A1: 1-Veblen 0 = epsilon_b by Th75,ORDINAL5:51;
consider a such that
A2: epsilon_0 = 1-Veblen a by Th76;
now assume b <> 0; then
epsilon_0 in epsilon_b by ORDINAL3:8,ORDINAL5:44;
hence contradiction by A1,A2,Th72;
end;
hence thesis by A1;
end;
Lm5:
1-Veblen a = epsilon_a implies 1-Veblen succ a = epsilon_succ a
proof
assume
A1: 1-Veblen a = epsilon_a;
consider b such that
A2: 1-Veblen succ a = epsilon_b by Th75,ORDINAL5:51;
consider c such that
A3: epsilon_succ a = 1-Veblen c by Th76;
A4: a in succ a by ORDINAL1:6;
epsilon_a in epsilon_succ a by ORDINAL1:6,ORDINAL5:44; then
a in c by A1,A3,Th72; then
succ a c= c by ORDINAL1:21;
hence 1-Veblen succ a c= epsilon_succ a by A3,Th71;
assume epsilon_succ a c/= 1-Veblen succ a; then
epsilon_b in epsilon_succ a by A2,Th4; then
b in succ a by Th12; then
b c= a by ORDINAL1:22; then
epsilon_b c= epsilon_a by Th11; then
succ a c= a by A1,A2,Th71; then
a in a by A4;
hence thesis;
end;
Lm6:
(for a st a in l holds 1-Veblen(a) = epsilon_a)
implies 1-Veblen(l) = epsilon_l
proof assume
A1: for a st a in l holds 1-Veblen(a) = epsilon_a;
set U = Tarski-Class(l\/omega);
0 in l by ORDINAL3:8; then
omega c= l by ORDINAL1:def 11; then
l\/omega = l by XBOOLE_1:12; then
A2: l in U by CLASSES1:2;
A3: omega in U by Th57;
1-element_of U = 1; then
reconsider g = U-Veblen.1 as normal Ordinal-Sequence of U
by A3,Th62;
reconsider o = omega as non trivial Ordinal of U by Th57;
set f = U exp o;
A4: g = criticals f by Th74;
A5: dom g = On U by FUNCT_2:def 1; then
A6: l in dom g by A2,ORDINAL1:def 9; then
A7: g.l = Union(g|l) by A4,Th39 .= union rng(g|l);
l c= dom g by A6,ORDINAL1:def 2; then
A8: dom(g|l) = l by RELAT_1:62;
now let x;
assume x in rng(g|l); then
consider y being object such that
A9: y in dom(g|l) & x = (g|l).y by FUNCT_1:def 3;
reconsider y as Ordinal by A9;
A10: x = g.y by A9,FUNCT_1:47;
y in dom g by A6,A8,A9,ORDINAL1:10; then
y in U & 1-element_of U in U by A5,ORDINAL1:def 9; then
x = 1-Veblen y by A3,A10,Th67; then
x = epsilon_y by A1,A8,A9; then
x in epsilon_l by A8,A9,Th12;
hence x c= epsilon_l by ORDINAL1:def 2;
end;
hence 1-Veblen(l) c= epsilon_l by A7,ZFMISC_1:76;
let a; assume a in epsilon_l; then
consider b such that
A11: b in l & a in epsilon_b by ORDINAL5:47;
epsilon_b = 1-Veblen b by A1,A11; then
epsilon_b in 1-Veblen l by A11,Th72;
hence thesis by A11,ORDINAL1:10;
end;
theorem
1-Veblen(a) = epsilon_a
proof set U = Tarski-Class(a\/omega);
defpred P[Ordinal] means 1-Veblen $1 = epsilon_$1;
A1: P[0] by Lm4;
A2: P[b] implies P[succ b] by Lm5;
A3: b <> 0 & b is limit_ordinal & (for c st c in b holds P[c]) implies P[b]
by Lm6;
P[b] from ORDINAL2:sch 1(A1,A2,A3);
hence thesis;
end;