:: Veblen Hierarchy
:: by Grzegorz Bancerek
::
:: Received October 18, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users


definition
let X be set ;
attr X is ordinal-membered means :Def1: :: ORDINAL6:def 1
ex a being Ordinal st X c= a;
end;

:: deftheorem Def1 defines ordinal-membered ORDINAL6:def 1 :
for X being set holds
( X is ordinal-membered iff ex a being Ordinal st X c= a );

registration
cluster ordinal -> ordinal-membered for set ;
coherence
for b1 being set st b1 is ordinal holds
b1 is ordinal-membered
;
let X be set ;
cluster On X -> ordinal-membered ;
coherence
On X is ordinal-membered
proof end;
end;

theorem Th1: :: ORDINAL6:1
for X being set holds
( X is ordinal-membered iff for x being set st x in X holds
x is ordinal )
proof end;

registration
cluster ordinal-membered for set ;
existence
ex b1 being set st b1 is ordinal-membered
proof end;
end;

registration
let X be ordinal-membered set ;
cluster -> ordinal for Element of X;
coherence
for b1 being Element of X holds b1 is ordinal
proof end;
end;

theorem Th2: :: ORDINAL6:2
for X being set holds
( X is ordinal-membered iff On X = X )
proof end;

theorem :: ORDINAL6:3
for X being ordinal-membered set holds X c= sup X by ORDINAL2:19;

theorem Th4: :: ORDINAL6:4
for a, b being Ordinal holds
( a c= b iff b nin a )
proof end;

theorem :: ORDINAL6:5
for a, b being Ordinal
for x being set holds
( x in a \ b iff ( b c= x & x in a ) )
proof end;

registration
let a, b be Ordinal;
cluster a \ b -> ordinal-membered ;
coherence
a \ b is ordinal-membered
;
end;

theorem Th6: :: ORDINAL6:6
for X, Y being set
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y holds
for x, y being set st x in X & y in X holds
( x c= y iff f . x c= f . y )
proof end;

theorem :: ORDINAL6:7
for X, Y being ordinal-membered set
for f being Function st f is_isomorphism_of RelIncl X, RelIncl Y holds
for x, y being set st x in X & y in X holds
( x in y iff f . x in f . y )
proof end;

theorem Th8: :: ORDINAL6:8
for X, x, y being set st [x,y] in RelIncl X holds
x c= y
proof end;

theorem Th9: :: ORDINAL6:9
for f1, f2 being Sequence holds f1 c= f1 ^ f2
proof end;

theorem :: ORDINAL6:10
canceled;

Th10: for f1, f2 being Sequence holds rng (f1 ^ f2) = (rng f1) \/ (rng f2)
by ORDINAL4:2;

theorem Th11: :: ORDINAL6:11
for a, b being Ordinal holds
( a c= b iff epsilon_ a c= epsilon_ b )
proof end;

theorem Th12: :: ORDINAL6:12
for a, b being Ordinal holds
( a in b iff epsilon_ a in epsilon_ b )
proof end;

registration
let X be ordinal-membered set ;
cluster union X -> ordinal ;
coherence
union X is ordinal
proof end;
end;

registration
let f be Ordinal-yielding Function;
cluster rng f -> ordinal-membered ;
coherence
rng f is ordinal-membered
by ORDINAL2:def 4;
end;

registration
let a be Ordinal;
cluster id a -> Sequence-like Ordinal-yielding ;
coherence
( id a is Sequence-like & id a is Ordinal-yielding )
;
end;

registration
let a be Ordinal;
cluster id a -> increasing for Ordinal-Sequence;
coherence
for b1 being Ordinal-Sequence st b1 = id a holds
b1 is increasing
proof end;
end;

registration
let a be Ordinal;
cluster id a -> continuous for Ordinal-Sequence;
coherence
for b1 being Ordinal-Sequence st b1 = id a holds
b1 is continuous
proof end;
end;

registration
cluster Relation-like Function-like Sequence-like non empty Ordinal-yielding increasing continuous for set ;
existence
ex b1 being Ordinal-Sequence st
( not b1 is empty & b1 is increasing & b1 is continuous )
proof end;
end;

definition
let f be Sequence;
attr f is normal means :: ORDINAL6:def 2
f is increasing continuous Ordinal-Sequence;
end;

:: deftheorem defines normal ORDINAL6:def 2 :
for f being Sequence holds
( f is normal iff f is increasing continuous Ordinal-Sequence );

definition
let f be Ordinal-Sequence;
redefine attr f is normal means :: ORDINAL6:def 3
( f is increasing & f is continuous );
compatibility
( f is normal iff ( f is increasing & f is continuous ) )
;
end;

:: deftheorem defines normal ORDINAL6:def 3 :
for f being Ordinal-Sequence holds
( f is normal iff ( f is increasing & f is continuous ) );

registration
cluster Relation-like Function-like Sequence-like normal -> Ordinal-yielding for set ;
coherence
for b1 being Sequence st b1 is normal holds
b1 is Ordinal-yielding
;
cluster Relation-like Function-like Sequence-like Ordinal-yielding normal -> increasing continuous for set ;
coherence
for b1 being Ordinal-Sequence st b1 is normal holds
( b1 is increasing & b1 is continuous )
;
cluster Relation-like Function-like Sequence-like Ordinal-yielding increasing continuous -> normal for set ;
coherence
for b1 being Ordinal-Sequence st b1 is increasing & b1 is continuous holds
b1 is normal
;
end;

registration
cluster Relation-like Function-like Sequence-like non empty normal for set ;
existence
ex b1 being Sequence st
( not b1 is empty & b1 is normal )
proof end;
end;

theorem Th13: :: ORDINAL6:13
for a being Ordinal
for f being Ordinal-Sequence st f is non-decreasing holds
f | a is non-decreasing
proof end;

definition
let X be set ;
func ord-type X -> Ordinal equals :: ORDINAL6:def 4
order_type_of (RelIncl (On X));
coherence
order_type_of (RelIncl (On X)) is Ordinal
;
end;

:: deftheorem defines ord-type ORDINAL6:def 4 :
for X being set holds ord-type X = order_type_of (RelIncl (On X));

definition
let X be ordinal-membered set ;
redefine func ord-type X equals :: ORDINAL6:def 5
order_type_of (RelIncl X);
compatibility
for b1 being Ordinal holds
( b1 = ord-type X iff b1 = order_type_of (RelIncl X) )
by Th2;
end;

:: deftheorem defines ord-type ORDINAL6:def 5 :
for X being ordinal-membered set holds ord-type X = order_type_of (RelIncl X);

registration
let X be ordinal-membered set ;
cluster RelIncl X -> well-ordering ;
coherence
RelIncl X is well-ordering
proof end;
end;

registration
let E be empty set ;
cluster On E -> empty ;
coherence
On E is empty
by ORDINAL2:7, XBOOLE_1:3;
end;

registration
let E be empty set ;
cluster order_type_of E -> empty ;
coherence
order_type_of E is empty
proof end;
end;

theorem :: ORDINAL6:14
ord-type {} = 0 ;

theorem :: ORDINAL6:15
for a being Ordinal holds ord-type {a} = 1
proof end;

theorem :: ORDINAL6:16
for a, b being Ordinal st a <> b holds
ord-type {a,b} = 2
proof end;

theorem :: ORDINAL6:17
for a being Ordinal holds ord-type a = a by ORDERS_1:88;

definition
let X be set ;
func numbering X -> Ordinal-Sequence equals :: ORDINAL6:def 6
canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));
coherence
canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) is Ordinal-Sequence
proof end;
end;

:: deftheorem defines numbering ORDINAL6:def 6 :
for X being set holds numbering X = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));

theorem Th18: :: ORDINAL6:18
for X being set holds
( dom (numbering X) = ord-type X & rng (numbering X) = On X )
proof end;

theorem Th19: :: ORDINAL6:19
for X being ordinal-membered set holds rng (numbering X) = X
proof end;

theorem :: ORDINAL6:20
for X being set holds card (dom (numbering X)) = card (On X)
proof end;

theorem Th21: :: ORDINAL6:21
for X being set holds numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X)
proof end;

theorem Th22: :: ORDINAL6:22
for X, x, y being set
for f being Ordinal-Sequence st f = numbering X & x in dom f & y in dom f holds
( x c= y iff f . x c= f . y )
proof end;

theorem Th23: :: ORDINAL6:23
for X, x, y being set
for f being Ordinal-Sequence st f = numbering X & x in dom f & y in dom f holds
( x in y iff f . x in f . y )
proof end;

registration
let X be set ;
cluster numbering X -> increasing ;
coherence
numbering X is increasing
proof end;
end;

registration
let X, Y be ordinal-membered set ;
cluster X \/ Y -> ordinal-membered ;
coherence
X \/ Y is ordinal-membered
proof end;
end;

registration
let X be ordinal-membered set ;
let Y be set ;
cluster X \ Y -> ordinal-membered ;
coherence
X \ Y is ordinal-membered
proof end;
end;

theorem Th24: :: ORDINAL6:24
for X, Y being ordinal-membered set st ( for x, y being set 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 end;

theorem Th25: :: ORDINAL6:25
for X, Y being ordinal-membered set st ( for x, y being set st x in X & y in Y holds
x in y ) holds
numbering (X \/ Y) = (numbering X) ^ (numbering Y)
proof end;

theorem :: ORDINAL6:26
for X, Y being ordinal-membered set st ( for x, y being set st x in X & y in Y holds
x in y ) holds
ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y)
proof end;

theorem Th27: :: ORDINAL6:27
for x being set
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 :: ORDINAL6:def 7
numbering { a where a is Element of dom f : a is_a_fixpoint_of f } ;
coherence
numbering { a where a is Element of dom f : a is_a_fixpoint_of f } is Ordinal-Sequence
;
end;

:: deftheorem defines criticals ORDINAL6:def 7 :
for f being Ordinal-Sequence holds criticals f = numbering { a where a is Element of dom f : a is_a_fixpoint_of f } ;

theorem Th28: :: ORDINAL6:28
for f being Ordinal-Sequence holds 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 end;

theorem Th29: :: ORDINAL6:29
for x being set
for f being Ordinal-Sequence st x in dom (criticals f) holds
(criticals f) . x is_a_fixpoint_of f
proof end;

theorem Th30: :: ORDINAL6:30
for f being Ordinal-Sequence holds
( rng (criticals f) = { a where a is Element of dom f : a is_a_fixpoint_of f } & rng (criticals f) c= rng f )
proof end;

registration
let f be Ordinal-Sequence;
cluster criticals f -> increasing ;
coherence
criticals f is increasing
;
end;

theorem :: ORDINAL6:31
for x being set
for f being Ordinal-Sequence st x in dom (criticals f) holds
x c= (criticals f) . x by ORDINAL4:10;

theorem Th32: :: ORDINAL6:32
for f being Ordinal-Sequence holds dom (criticals f) c= dom f
proof end;

theorem Th33: :: ORDINAL6:33
for b being Ordinal
for f being Ordinal-Sequence st b is_a_fixpoint_of f holds
ex a being Ordinal st
( a in dom (criticals f) & b = (criticals f) . a )
proof end;

theorem :: ORDINAL6:34
for a, b being Ordinal
for f being Ordinal-Sequence st a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
succ a in dom (criticals f)
proof end;

theorem :: ORDINAL6:35
for a, b being Ordinal
for f being Ordinal-Sequence st succ a in dom (criticals f) & b is_a_fixpoint_of f & (criticals f) . a in b holds
(criticals f) . (succ a) c= b
proof end;

theorem Th36: :: ORDINAL6:36
for X being set
for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) holds
union X = f . (union X)
proof end;

theorem Th37: :: ORDINAL6:37
for X being set
for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
x is_a_fixpoint_of f ) holds
union X = f . (union X)
proof end;

theorem Th38: :: ORDINAL6:38
for a being Ordinal
for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
proof end;

theorem Th39: :: ORDINAL6:39
for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st f is normal & l in dom (criticals f) holds
(criticals f) . l = Union ((criticals f) | l)
proof end;

registration
let f be normal Ordinal-Sequence;
cluster criticals f -> continuous ;
coherence
criticals f is continuous
proof end;
end;

theorem Th40: :: ORDINAL6:40
for f1, f2 being Ordinal-Sequence st f1 c= f2 holds
criticals f1 c= criticals f2
proof end;

registration
let U be Universe;
cluster Relation-like On U -defined On U -valued Function-like Sequence-like non empty V28( On U) V32( On U, On U) Ordinal-yielding normal for Element of bool [:(On U),(On U):];
existence
ex b1 being Ordinal-Sequence of U st b1 is normal
proof end;
end;

definition
let U be Universe;
let a be Ordinal;
mode Ordinal-Sequence of a,U is Function of a,(On U);
end;

registration
let U be Universe;
let a be Ordinal;
cluster Function-like V32(a, On U) -> Sequence-like Ordinal-yielding for Element of bool [:a,(On U):];
coherence
for b1 being Ordinal-Sequence of a,U holds
( b1 is Sequence-like & b1 is Ordinal-yielding )
by FUNCT_2:def 1, RELAT_1:def 19;
end;

definition
let U be Universe;
let a be Ordinal;
let f be Ordinal-Sequence of a,U;
let x be set ;
:: original: .
redefine func f . x -> Ordinal of U;
coherence
f . x is Ordinal of U
proof end;
end;

theorem Th41: :: ORDINAL6:41
for a being Ordinal
for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds Union f in U
proof end;

theorem Th42: :: ORDINAL6:42
for a being Ordinal
for U being Universe st a in U holds
for f being Ordinal-Sequence of a,U holds sup f in U
proof end;

scheme :: ORDINAL6:sch 1
CriticalNumber2{ F1() -> Universe, F2() -> Ordinal of F1(), F3() -> Ordinal-Sequence of omega,F1(), F4( Ordinal) -> Ordinal } :
( F2() c= Union F3() & F4((Union F3())) = Union F3() & ( for b being Ordinal st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )
provided
A1: omega in F1() and
A2: for a being Ordinal st a in F1() holds
F4(a) in F1() and
A3: for a, b being Ordinal st a in b & b in F1() holds
F4(a) in F4(b) and
A4: for a being Ordinal of F1() st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = F4(b) ) holds
F4(a) is_limes_of phi and
A5: F3() . 0 = F2() and
A6: for a being Ordinal st a in omega holds
F3() . (succ a) = F4((F3() . a))
proof end;

scheme :: ORDINAL6:sch 2
CriticalNumber3{ F1() -> Universe, F2() -> Ordinal of F1(), F3( Ordinal) -> Ordinal } :
ex a being Ordinal of F1() st
( F2() in a & F3(a) = a )
provided
A1: omega in F1() and
A2: for a being Ordinal st a in F1() holds
F3(a) in F1() and
A3: for a, b being Ordinal st a in b & b in F1() holds
F3(a) in F3(b) and
A4: for a being Ordinal of F1() st not a is empty & a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds
phi . b = F3(b) ) holds
F3(a) is_limes_of phi
proof end;

theorem Th43: :: ORDINAL6:43
for b being Ordinal
for W being Universe
for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being Ordinal st
( b in a & a is_a_fixpoint_of phi )
proof end;

theorem Th44: :: ORDINAL6:44
for W being Universe
for F being normal Ordinal-Sequence of W st omega in W holds
criticals F is Ordinal-Sequence of W
proof end;

theorem Th45: :: ORDINAL6:45
for f being Ordinal-Sequence st f is normal holds
for a being Ordinal st a in dom (criticals f) holds
f . a c= (criticals f) . a
proof end;

definition
let U be Universe;
let a, b be Ordinal of U;
:: original: exp
redefine func exp (a,b) -> Ordinal of U;
coherence
exp (a,b) is Ordinal of U
proof end;
end;

definition
let U be Universe;
let a be Ordinal;
assume A1: a in U ;
func U exp a -> Ordinal-Sequence of U means :Def8: :: ORDINAL6:def 8
for b being Ordinal of U holds it . b = exp (a,b);
existence
ex b1 being Ordinal-Sequence of U st
for b being Ordinal of U holds b1 . b = exp (a,b)
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence of U st ( for b being Ordinal of U holds b1 . b = exp (a,b) ) & ( for b being Ordinal of U holds b2 . b = exp (a,b) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines exp ORDINAL6:def 8 :
for U being Universe
for a being Ordinal st a in U holds
for b3 being Ordinal-Sequence of U holds
( b3 = U exp a iff for b being Ordinal of U holds b3 . b = exp (a,b) );

registration
cluster omega -> non trivial ;
coherence
not omega is trivial
;
end;

registration
let U be Universe;
cluster epsilon-transitive epsilon-connected ordinal non trivial finite ordinal-membered for Element of U;
existence
ex b1 being Ordinal of U st
( not b1 is trivial & b1 is finite )
proof end;
end;

registration
cluster epsilon-transitive epsilon-connected ordinal non trivial finite ordinal-membered for set ;
existence
ex b1 being Ordinal st
( not b1 is trivial & b1 is finite )
proof end;
end;

registration
let U be Universe;
let a be non trivial Ordinal of U;
cluster U exp a -> normal ;
coherence
U exp a is normal
proof end;
end;

definition
let g be Function;
attr g is Ordinal-Sequence-valued means :Def9: :: ORDINAL6:def 9
for x being set st x in rng g holds
x is Ordinal-Sequence;
end;

:: deftheorem Def9 defines Ordinal-Sequence-valued ORDINAL6:def 9 :
for g being Function holds
( g is Ordinal-Sequence-valued iff for x being set st x in rng g holds
x is Ordinal-Sequence );

registration
let f be Ordinal-Sequence;
cluster <%f%> -> Ordinal-Sequence-valued ;
coherence
<%f%> is Ordinal-Sequence-valued
proof end;
end;

definition
let f be Function;
attr f is with_the_same_dom means :: ORDINAL6:def 10
rng f is with_common_domain ;
end;

:: deftheorem defines with_the_same_dom ORDINAL6:def 10 :
for f being Function holds
( f is with_the_same_dom iff rng f is with_common_domain );

registration
let f be Function;
cluster {f} -> with_common_domain ;
coherence
{f} is with_common_domain
proof end;
end;

registration
let f be Function;
cluster <%f%> -> with_the_same_dom ;
coherence
<%f%> is with_the_same_dom
proof end;
end;

registration
cluster Relation-like Function-like Sequence-like non empty Ordinal-Sequence-valued with_the_same_dom for set ;
existence
ex b1 being Sequence st
( not b1 is empty & b1 is Ordinal-Sequence-valued & b1 is with_the_same_dom )
proof end;
end;

registration
let g be Ordinal-Sequence-valued Function;
let x be object ;
cluster g . x -> Relation-like Function-like ;
coherence
( g . x is Relation-like & g . x is Function-like )
proof end;
end;

registration
let g be Ordinal-Sequence-valued Function;
let x be set ;
cluster g . x -> Sequence-like Ordinal-yielding ;
coherence
( g . x is Sequence-like & g . x is Ordinal-yielding )
proof end;
end;

registration
let g be Sequence;
let a be Ordinal;
cluster g | a -> Sequence-like ;
coherence
g | a is Sequence-like
;
end;

registration
let g be Ordinal-Sequence-valued Function;
let X be set ;
cluster g | X -> Ordinal-Sequence-valued ;
coherence
g | X is Ordinal-Sequence-valued
proof end;
end;

registration
let a, b be Ordinal;
cluster Function-like V32(a,b) -> Sequence-like Ordinal-yielding for Element of bool [:a,b:];
coherence
for b1 being Function of a,b holds
( b1 is Ordinal-yielding & b1 is Sequence-like )
proof end;
end;

definition
let g be Ordinal-Sequence-valued Sequence;
func criticals g -> Ordinal-Sequence equals :: ORDINAL6:def 11
numbering { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )
}
;
coherence
numbering { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )
}
is Ordinal-Sequence
;
end;

:: deftheorem defines criticals ORDINAL6:def 11 :
for g being Ordinal-Sequence-valued Sequence holds criticals g = numbering { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )
}
;

theorem Th46: :: ORDINAL6:46
for g being Ordinal-Sequence-valued Sequence holds { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )
}
is ordinal-membered
proof end;

theorem Th47: :: ORDINAL6:47
for a, b being Ordinal
for g being Ordinal-Sequence-valued Sequence st a in dom g & b in dom (criticals g) holds
(criticals g) . b is_a_fixpoint_of g . a
proof end;

theorem :: ORDINAL6:48
for x being set
for g being Ordinal-Sequence-valued Sequence st x in dom (criticals g) holds
x c= (criticals g) . x by ORDINAL4:10;

theorem Th49: :: ORDINAL6:49
for f being Ordinal-Sequence
for g being Ordinal-Sequence-valued Sequence st f in rng g holds
dom (criticals g) c= dom f
proof end;

theorem Th50: :: ORDINAL6:50
for b being Ordinal
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for c being Ordinal st c in dom g holds
b is_a_fixpoint_of g . c ) holds
ex a being Ordinal st
( a in dom (criticals g) & b = (criticals g) . a )
proof end;

theorem :: ORDINAL6:51
for a being Ordinal
for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & l c= dom (criticals g) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) & ( for x being set st x in l holds
(criticals g) . x in a ) holds
l in dom (criticals g)
proof end;

theorem Th52: :: ORDINAL6:52
for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for a being Ordinal st a in dom g holds
g . a is normal ) & l in dom (criticals g) holds
(criticals g) . l = Union ((criticals g) | l)
proof end;

theorem Th53: :: ORDINAL6:53
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for a being Ordinal st a in dom g holds
g . a is normal ) holds
criticals g is continuous
proof end;

theorem Th54: :: ORDINAL6:54
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for a being Ordinal st a in dom g holds
g . a is normal ) holds
for a being Ordinal
for f being Ordinal-Sequence st a in dom (criticals g) & f in rng g holds
f . a c= (criticals g) . a
proof end;

theorem Th55: :: ORDINAL6:55
for g1, g2 being Ordinal-Sequence-valued Sequence st dom g1 = dom g2 & dom g1 <> {} & ( for a being Ordinal st a in dom g1 holds
g1 . a c= g2 . a ) holds
criticals g1 c= criticals g2
proof end;

definition
let g be Ordinal-Sequence-valued Sequence;
func lims g -> Ordinal-Sequence means :Def12: :: ORDINAL6:def 12
( dom it = dom (g . 0) & ( for a being Ordinal st a in dom it holds
it . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) );
existence
ex b1 being Ordinal-Sequence st
( dom b1 = dom (g . 0) & ( for a being Ordinal st a in dom b1 holds
b1 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence st dom b1 = dom (g . 0) & ( for a being Ordinal st a in dom b1 holds
b1 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) & dom b2 = dom (g . 0) & ( for a being Ordinal st a in dom b2 holds
b2 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines lims ORDINAL6:def 12 :
for g being Ordinal-Sequence-valued Sequence
for b2 being Ordinal-Sequence holds
( b2 = lims g iff ( dom b2 = dom (g . 0) & ( for a being Ordinal st a in dom b2 holds
b2 . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) ) );

theorem Th56: :: ORDINAL6:56
for U being Universe
for g being Ordinal-Sequence-valued Sequence st dom g <> {} & dom g in U & ( for a being Ordinal st a in dom g holds
g . a is Ordinal-Sequence of U ) holds
lims g is Ordinal-Sequence of U
proof end;

definition
let x be set ;
func OS@ x -> Ordinal-Sequence equals :Def13: :: ORDINAL6:def 13
x if x is Ordinal-Sequence
otherwise the Ordinal-Sequence;
correctness
coherence
( ( x is Ordinal-Sequence implies x is Ordinal-Sequence ) & ( x is not Ordinal-Sequence implies the Ordinal-Sequence is Ordinal-Sequence ) )
;
consistency
for b1 being Ordinal-Sequence holds verum
;
;
func OSV@ x -> Ordinal-Sequence-valued Sequence equals :Def14: :: ORDINAL6:def 14
x if x is Ordinal-Sequence-valued Sequence
otherwise the Ordinal-Sequence-valued Sequence;
correctness
coherence
( ( x is Ordinal-Sequence-valued Sequence implies x is Ordinal-Sequence-valued Sequence ) & ( x is not Ordinal-Sequence-valued Sequence implies the Ordinal-Sequence-valued Sequence is Ordinal-Sequence-valued Sequence ) )
;
consistency
for b1 being Ordinal-Sequence-valued Sequence holds verum
;
;
end;

:: deftheorem Def13 defines OS@ ORDINAL6:def 13 :
for x being set holds
( ( x is Ordinal-Sequence implies OS@ x = x ) & ( x is not Ordinal-Sequence implies OS@ x = the Ordinal-Sequence ) );

:: deftheorem Def14 defines OSV@ ORDINAL6:def 14 :
for x being set holds
( ( x is Ordinal-Sequence-valued Sequence implies OSV@ x = x ) & ( x is not Ordinal-Sequence-valued Sequence implies OSV@ x = the Ordinal-Sequence-valued Sequence ) );

definition
let U be Universe;
func U -Veblen -> Ordinal-Sequence-valued Sequence means :Def15: :: ORDINAL6:def 15
( dom it = On U & it . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
it . (succ b) = criticals (it . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
it . l = criticals (it | l) ) );
existence
ex b1 being Ordinal-Sequence-valued Sequence st
( dom b1 = On U & b1 . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b1 . (succ b) = criticals (b1 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b1 . l = criticals (b1 | l) ) )
proof end;
uniqueness
for b1, b2 being Ordinal-Sequence-valued Sequence st dom b1 = On U & b1 . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b1 . (succ b) = criticals (b1 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b1 . l = criticals (b1 | l) ) & dom b2 = On U & b2 . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b2 . (succ b) = criticals (b2 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b2 . l = criticals (b2 | l) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines -Veblen ORDINAL6:def 15 :
for U being Universe
for b2 being Ordinal-Sequence-valued Sequence holds
( b2 = U -Veblen iff ( dom b2 = On U & b2 . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b2 . (succ b) = criticals (b2 . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b2 . l = criticals (b2 | l) ) ) );

registration
cluster epsilon-transitive non empty subset-closed Tarski uncountable universal for set ;
existence
ex b1 being Universe st b1 is uncountable
proof end;
end;

theorem Th57: :: ORDINAL6:57
for U being Universe holds
( U is uncountable iff omega in U )
proof end;

theorem Th58: :: ORDINAL6:58
for a, b, c being Ordinal
for U being Universe st a in b & b in U & omega in U & c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
proof end;

theorem :: ORDINAL6:59
for a being Ordinal
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for c being Ordinal st c in l holds
a is_a_fixpoint_of (U -Veblen) . c ) holds
a is_a_fixpoint_of lims ((U -Veblen) | l)
proof end;

theorem Th60: :: ORDINAL6:60
for a, b, c being Ordinal
for U being Universe st a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( for c being Ordinal st c in b holds
(U -Veblen) . c is normal ) holds
((U -Veblen) . a) . c c= ((U -Veblen) . b) . c
proof end;

theorem Th61: :: ORDINAL6:61
for a, b being Ordinal
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & a in U & b in l & ( for c being Ordinal st c in l holds
(U -Veblen) . c is normal Ordinal-Sequence of U ) holds
(lims ((U -Veblen) | l)) . a is_a_fixpoint_of (U -Veblen) . b
proof end;

Lm1: for U being Universe st omega in U holds
(U -Veblen) . 0 is normal Ordinal-Sequence of U

proof end;

Lm2: for a being Ordinal
for U being Universe st omega in U & a in U & (U -Veblen) . a is normal Ordinal-Sequence of U holds
(U -Veblen) . (succ a) is normal Ordinal-Sequence of U

proof end;

Lm3: for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
(U -Veblen) . l is normal Ordinal-Sequence of U

proof end;

theorem Th62: :: ORDINAL6:62
for a being Ordinal
for U being Universe st omega in U & a in U holds
(U -Veblen) . a is normal Ordinal-Sequence of U
proof end;

theorem Th63: :: ORDINAL6:63
for a being Ordinal
for U, W being Universe st omega in U & U c= W & a in U holds
(U -Veblen) . a c= (W -Veblen) . a
proof end;

theorem Th64: :: ORDINAL6:64
for a, b being Ordinal
for U, W being Universe st omega in U & a in U & b in U & omega in W & a in W & b in W holds
((U -Veblen) . b) . a = ((W -Veblen) . b) . a
proof end;

theorem :: ORDINAL6:65
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( for a being Ordinal st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
lims ((U -Veblen) | l) is continuous non-decreasing Ordinal-Sequence of U
proof end;

registration
let a be Ordinal;
cluster Tarski-Class (a \/ omega) -> uncountable ;
coherence
not Tarski-Class (a \/ omega) is countable
proof end;
end;

definition
let a, b be Ordinal;
func a -Veblen b -> Ordinal equals :: ORDINAL6:def 16
(((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b;
coherence
(((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b is Ordinal
;
end;

:: deftheorem defines -Veblen ORDINAL6:def 16 :
for a, b being Ordinal holds a -Veblen b = (((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b;

definition
let n be Nat;
let b be Ordinal;
:: original: -Veblen
redefine func n -Veblen b -> Ordinal equals :: ORDINAL6:def 17
(((Tarski-Class (b \/ omega)) -Veblen) . n) . b;
coherence
n -Veblen b is Ordinal
;
compatibility
for b1 being Ordinal holds
( b1 = n -Veblen b iff b1 = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b )
proof end;
end;

:: deftheorem defines -Veblen ORDINAL6:def 17 :
for n being Nat
for b being Ordinal holds n -Veblen b = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b;

theorem Th66: :: ORDINAL6:66
for a, b, c being Ordinal holds a in Tarski-Class ((a \/ b) \/ c)
proof end;

theorem Th67: :: ORDINAL6:67
for a, b being Ordinal
for U being Universe st omega in U & a in U & b in U holds
b -Veblen a = ((U -Veblen) . b) . a
proof end;

theorem Th68: :: ORDINAL6:68
for a being Ordinal holds 0 -Veblen a = exp (omega,a)
proof end;

theorem Th69: :: ORDINAL6:69
for a, b being Ordinal holds b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a
proof end;

theorem Th70: :: ORDINAL6:70
for a, b, c being Ordinal st b in c holds
b -Veblen (c -Veblen a) = c -Veblen a
proof end;

theorem Th71: :: ORDINAL6:71
for a, b, c being Ordinal holds
( a c= b iff c -Veblen a c= c -Veblen b )
proof end;

theorem Th72: :: ORDINAL6:72
for a, b, c being Ordinal holds
( a in b iff c -Veblen a in c -Veblen b )
proof end;

theorem :: ORDINAL6:73
for a, b, c, d being Ordinal holds
( 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 end;

theorem Th74: :: ORDINAL6:74
for U being uncountable Universe holds (U -Veblen) . 1 = criticals (U exp omega)
proof end;

theorem Th75: :: ORDINAL6:75
for a being Ordinal holds 1 -Veblen a is epsilon
proof end;

theorem Th76: :: ORDINAL6:76
for e being epsilon Ordinal ex a being Ordinal st e = 1 -Veblen a
proof end;

Lm4: 1 -Veblen 0 = epsilon_ 0
proof end;

Lm5: for a being Ordinal st 1 -Veblen a = epsilon_ a holds
1 -Veblen (succ a) = epsilon_ (succ a)

proof end;

Lm6: for l being limit_ordinal non empty Ordinal st ( for a being Ordinal st a in l holds
1 -Veblen a = epsilon_ a ) holds
1 -Veblen l = epsilon_ l

proof end;

theorem :: ORDINAL6:77
for a being Ordinal holds 1 -Veblen a = epsilon_ a
proof end;