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


begin

definition
let X be set ;
attrX is ordinal-membered  means :Def1: :: ORDINAL6:def 1
 ex a being ordinal number 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 number 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
proofend;
let X be set ;
cluster On X ->  ordinal-membered ;
coherence
 On X is ordinal-membered
proofend;
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 )
proofend;

registration
cluster ordinal-membered for set ;
existence
 ex b1 being set st b1 is ordinal-membered
proofend;
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
proofend;
end;

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

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

theorem Th4: :: ORDINAL6:4
for a, b being ordinal number holds
( a c= b iff b nin a )
proofend;

theorem :: ORDINAL6:5
for a, b being ordinal number
for x being set holds
( x in a \ b iff ( b c= x & x in a ) )
proofend;

registration
let a, b be ordinal number ;
clustera \ b ->  ordinal-membered ;
coherence
 a \ b is ordinal-membered
proofend;
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 )
proofend;

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

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

theorem Th9: :: ORDINAL6:9
for f1, f2 being T-Sequence holds f1 c= f1 ^ f2
proofend;

theorem Th10: :: ORDINAL6:10
for f1, f2 being T-Sequence holds rng (f1 ^ f2) = (rng f1) \/ (rng f2)
proofend;

theorem Th11: :: ORDINAL6:11
for a, b being ordinal number holds
( a c= b iff epsilon_ a c= epsilon_ b )
proofend;

theorem Th12: :: ORDINAL6:12
for a, b being ordinal number holds
( a in b iff epsilon_ a in epsilon_ b )
proofend;

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

registration
let f be Ordinal-yielding Function;
cluster rng f ->  ordinal-membered ;
coherence
 rng f is ordinal-membered
proofend;
end;

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

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

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

registration
cluster Relation-like Function-like T-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 )
proofend;
end;

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

:: deftheorem Def2 defines normal ORDINAL6:def_2_:_
 for f being T-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 ) ) by Def2;
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 T-Sequence-like normal  ->  Ordinal-yielding for set ;
coherence
 for b1 being T-Sequence st b1 is normal holds
b1 is Ordinal-yielding by Def2;
cluster Relation-like Function-like T-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 ) by Def2;
cluster Relation-like Function-like T-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 by Def2;
end;

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

theorem Th13: :: ORDINAL6:13
for a being ordinal number
for f being Ordinal-Sequence st f is non-decreasing holds
f | a is non-decreasing
proofend;

definition
let X be set ;
func ord-type X ->  ordinal number  equals :: ORDINAL6:def 4
 order_type_of (RelIncl (On X));
coherence
 order_type_of (RelIncl (On X)) is ordinal number ;
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 number 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
proofend;
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
proofend;
end;

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

theorem :: ORDINAL6:15
for a being ordinal number holds ord-type {a} = 1
proofend;

theorem :: ORDINAL6:16
for a, b being ordinal number st a <> b holds
ord-type {a,b} = 2
proofend;

theorem :: ORDINAL6:17
for a being ordinal number 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
proofend;
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 &amp; rng (numbering X) = On X )
proofend;

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

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

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

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

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

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

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

registration
let X be ordinal-membered set ;
let Y be set ;
clusterX \ Y ->  ordinal-membered ;
coherence
 X \ Y is ordinal-membered
proofend;
end;

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

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

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

begin

theorem Th27: :: ORDINAL6:27
for x being set
for f being Function st x is_a_fixpoint_of f holds
x in rng f
proofend;

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

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

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  }  &amp; rng (criticals f) c= rng f )
proofend;

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

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

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

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

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

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

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

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

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

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

begin

registration
let U be Universe;
cluster Relation-like On U -defined On U -valued Function-like T-Sequence-like non empty V26( On U) V30( 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
proofend;
end;

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

registration
let U be Universe;
let a be ordinal number ;
cluster Function-like V30(a, On U)  ->  T-Sequence-like Ordinal-yielding for Element of bool [:a,(On U):];
coherence
 for b1 being Ordinal-Sequence of a,U holds
( b1 is T-Sequence-like &amp; b1 is Ordinal-yielding )
proofend;
end;

definition
let U be Universe;
let a be ordinal number ;
let f be Ordinal-Sequence of a,U;
let x be set ;
:: original:.
redefine funcf . x ->  Ordinal of U;
coherence
 f . x is Ordinal of U
proofend;
end;

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

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

scheme :: ORDINAL6:sch 1
CriticalNumber2{ F1() ->  Universe, F2() ->  Ordinal of F1(), F3() ->  Ordinal-Sequence of omega,F1(), F4( Ordinal) ->  Ordinal } :
 ( F2() c= Union F3() &amp; F4((Union F3())) = Union F3() &amp; ( for b being ordinal number st F2() c= b &amp; b in F1() &amp; F4(b) = b holds
Union F3() c= b ) )
provided
A1: omega in F1() and
A2: for a being ordinal number st a in F1() holds
F4(a) in F1() and
A3: for a, b being ordinal number st a in b &amp; b in F1() holds
F4(a) in F4(b) and
A4: for a being Ordinal of F1() st not a is empty &amp; a is limit_ordinal holds
for phi being Ordinal-Sequence st dom phi = a &amp; ( for b being ordinal number 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 number st a in omega holds
F3() . (succ a) = F4((F3() . a))
proofend;

Lm1:  {} in omega
by ORDINAL1:def_11;

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

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

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

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

begin

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

definition
let U be Universe;
let a be ordinal number ;
assume AA: a in U ;
funcU 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)
proofend;
uniqueness
 for b1, b2 being Ordinal-Sequence of U st ( for b being Ordinal of U holds b1 . b = exp (a,b) ) &amp; ( for b being Ordinal of U holds b2 . b = exp (a,b) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines exp ORDINAL6:def_8_:_
 for U being Universe
for a being ordinal number 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 &amp; b1 is finite )
proofend;
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 &amp; b1 is finite )
proofend;
end;

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

definition
let g be Function;
attrg 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
proofend;
end;

definition
let f be Function;
attrf 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
proofend;
end;

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

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

registration
let g be Ordinal-Sequence-valued Function;
let x be set ;
clusterg . x ->  Relation-like Function-like ;
coherence
 ( g . x is Relation-like &amp; g . x is Function-like )
proofend;
end;

registration
let g be Ordinal-Sequence-valued Function;
let x be set ;
clusterg . x ->  T-Sequence-like Ordinal-yielding ;
coherence
 ( g . x is T-Sequence-like &amp; g . x is Ordinal-yielding )
proofend;
end;

registration
let g be T-Sequence;
let a be ordinal number ;
clusterg | a ->  T-Sequence-like ;
coherence
 g | a is T-Sequence-like ;
end;

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

registration
let a, b be ordinal number ;
cluster Function-like V30(a,b)  ->  T-Sequence-like Ordinal-yielding for Element of bool [:a,b:];
coherence
 for b1 being Function of a,b holds
( b1 is Ordinal-yielding &amp; b1 is T-Sequence-like )
proofend;
end;

definition
let g be Ordinal-Sequence-valued T-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) &amp; ( 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) &amp; ( 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 T-Sequence holds criticals g = numbering  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) &amp; ( 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 T-Sequence holds  {  a where a is Element of dom (g . 0) : ( a in dom (g . 0) &amp; ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) )  }  is ordinal-membered
proofend;

theorem Th47: :: ORDINAL6:47
for a, b being ordinal number
for g being Ordinal-Sequence-valued T-Sequence st a in dom g &amp; b in dom (criticals g) holds
(criticals g) . b is_a_fixpoint_of g . a
proofend;

theorem :: ORDINAL6:48
for x being set
for g being Ordinal-Sequence-valued T-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 T-Sequence st f in rng g holds
dom (criticals g) c= dom f
proofend;

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

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

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

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

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

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

definition
let g be Ordinal-Sequence-valued T-Sequence;
func lims g ->  Ordinal-Sequence means :Def12: :: ORDINAL6:def 12
( dom it = dom (g . 0) &amp; ( for a being ordinal number 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) &amp; ( for a being ordinal number st a in dom b1 holds
b1 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) )
proofend;
uniqueness
 for b1, b2 being Ordinal-Sequence st dom b1 = dom (g . 0) &amp; ( for a being ordinal number st a in dom b1 holds
b1 . a = union  {  ((g . b) . a) where b is Element of dom g : b in dom g  }  ) &amp; dom b2 = dom (g . 0) &amp; ( for a being ordinal number 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
proofend;
end;

:: deftheorem Def12 defines lims ORDINAL6:def_12_:_
 for g being Ordinal-Sequence-valued T-Sequence
for b2 being Ordinal-Sequence holds
( b2 = lims g iff ( dom b2 = dom (g . 0) &amp; ( for a being ordinal number 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 T-Sequence st dom g <> {} &amp; dom g in U &amp; ( for a being ordinal number st a in dom g holds
g . a is Ordinal-Sequence of U ) holds
lims g is Ordinal-Sequence of U
proofend;

begin

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 ) &amp; ( 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 T-Sequence equals :Def14: :: ORDINAL6:def 14
x if x is Ordinal-Sequence-valued T-Sequence
otherwise  the Ordinal-Sequence-valued T-Sequence;
correctness
coherence
( ( x is Ordinal-Sequence-valued T-Sequence implies x is Ordinal-Sequence-valued T-Sequence ) &amp; ( x is not Ordinal-Sequence-valued T-Sequence implies the Ordinal-Sequence-valued T-Sequence is Ordinal-Sequence-valued T-Sequence ) );
consistency
for b1 being Ordinal-Sequence-valued T-Sequence holds verum;
;
end;

:: deftheorem Def13 defines OS@ ORDINAL6:def_13_:_
 for x being set holds
( ( x is Ordinal-Sequence implies OS@ x = x ) &amp; ( 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 T-Sequence implies OSV@ x = x ) &amp; ( x is not Ordinal-Sequence-valued T-Sequence implies OSV@ x = the Ordinal-Sequence-valued T-Sequence ) );

definition
let U be Universe;
funcU -Veblen  ->  Ordinal-Sequence-valued T-Sequence means :Def15: :: ORDINAL6:def 15
( dom it = On U &amp; it . 0 = U exp omega &amp; ( for b being ordinal number st succ b in On U holds
it . (succ b) = criticals (it . b) ) &amp; ( 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 T-Sequence st
( dom b1 = On U &amp; b1 . 0 = U exp omega &amp; ( for b being ordinal number st succ b in On U holds
b1 . (succ b) = criticals (b1 . b) ) &amp; ( for l being limit_ordinal non empty Ordinal st l in On U holds
b1 . l = criticals (b1 | l) ) )
proofend;
uniqueness
 for b1, b2 being Ordinal-Sequence-valued T-Sequence st dom b1 = On U &amp; b1 . 0 = U exp omega &amp; ( for b being ordinal number st succ b in On U holds
b1 . (succ b) = criticals (b1 . b) ) &amp; ( for l being limit_ordinal non empty Ordinal st l in On U holds
b1 . l = criticals (b1 | l) ) &amp; dom b2 = On U &amp; b2 . 0 = U exp omega &amp; ( for b being ordinal number st succ b in On U holds
b2 . (succ b) = criticals (b2 . b) ) &amp; ( for l being limit_ordinal non empty Ordinal st l in On U holds
b2 . l = criticals (b2 | l) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def15 defines -Veblen ORDINAL6:def_15_:_
 for U being Universe
for b2 being Ordinal-Sequence-valued T-Sequence holds
( b2 = U -Veblen iff ( dom b2 = On U &amp; b2 . 0 = U exp omega &amp; ( for b being ordinal number st succ b in On U holds
b2 . (succ b) = criticals (b2 . b) ) &amp; ( 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
proofend;
end;

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

theorem Th58: :: ORDINAL6:58
for a, b, c being ordinal number
for U being Universe st a in b &amp; b in U &amp; omega in U &amp; c in dom ((U -Veblen) . b) holds
((U -Veblen) . b) . c is_a_fixpoint_of (U -Veblen) . a
proofend;

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

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

theorem Th61: :: ORDINAL6:61
for a, b being ordinal number
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U &amp; a in U &amp; b in l &amp; ( for c being ordinal number 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
proofend;

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

Lm3:  for a being ordinal number
for U being Universe st omega in U &amp; a in U &amp; (U -Veblen) . a is normal Ordinal-Sequence of U holds
(U -Veblen) . (succ a) is normal Ordinal-Sequence of U
proofend;

Lm4:  for l being limit_ordinal non empty Ordinal
for U being Universe st l in U &amp; ( for a being ordinal number st a in l holds
(U -Veblen) . a is normal Ordinal-Sequence of U ) holds
(U -Veblen) . l is normal Ordinal-Sequence of U
proofend;

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

theorem Th63: :: ORDINAL6:63
for a being ordinal number
for U, W being Universe st omega in U &amp; U c= W &amp; a in U holds
(U -Veblen) . a c= (W -Veblen) . a
proofend;

theorem Th64: :: ORDINAL6:64
for a, b being ordinal number
for U, W being Universe st omega in U &amp; a in U &amp; b in U &amp; omega in W &amp; a in W &amp; b in W holds
((U -Veblen) . b) . a = ((W -Veblen) . b) . a
proofend;

theorem :: ORDINAL6:65
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U &amp; ( for a being ordinal number 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
proofend;

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

definition
let a, b be ordinal number ;
funca -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 number holds a -Veblen b = (((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b;

definition
let n be Nat;
let b be ordinal number ;
:: original:-Veblen
redefine funcn -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 )
proofend;
end;

:: deftheorem  defines -Veblen ORDINAL6:def_17_:_
 for n being Nat
for b being ordinal number holds n -Veblen b = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b;

theorem Th66: :: ORDINAL6:66
for a, b, c being ordinal number holds a in Tarski-Class ((a \/ b) \/ c)
proofend;

theorem Th67: :: ORDINAL6:67
for a, b being ordinal number
for U being Universe st omega in U &amp; a in U &amp; b in U holds
b -Veblen a = ((U -Veblen) . b) . a
proofend;

theorem Th68: :: ORDINAL6:68
for a being ordinal number holds 0 -Veblen a = exp (omega,a)
proofend;

theorem Th69: :: ORDINAL6:69
for b, a being ordinal number holds b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a
proofend;

theorem Th70: :: ORDINAL6:70
for b, c, a being ordinal number st b in c holds
b -Veblen (c -Veblen a) = c -Veblen a
proofend;

theorem Th71: :: ORDINAL6:71
for a, b, c being ordinal number holds
( a c= b iff c -Veblen a c= c -Veblen b )
proofend;

theorem Th72: :: ORDINAL6:72
for a, b, c being ordinal number holds
( a in b iff c -Veblen a in c -Veblen b )
proofend;

theorem :: ORDINAL6:73
for a, b, c, d being ordinal number holds
( a -Veblen b in c -Veblen d iff ( ( a = c &amp; b in d ) or ( a in c &amp; b in c -Veblen d ) or ( c in a &amp; a -Veblen b in d ) ) )
proofend;

begin

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

theorem Th75: :: ORDINAL6:75
for a being ordinal number holds 1 -Veblen a is epsilon
proofend;

theorem Th76: :: ORDINAL6:76
for e being epsilon Ordinal ex a being ordinal number st e = 1 -Veblen a
proofend;

Lm5:  1 -Veblen 0 = epsilon_ 0
proofend;

Lm6:  for a being ordinal number st 1 -Veblen a = epsilon_ a holds
1 -Veblen (succ a) = epsilon_ (succ a)
proofend;

Lm7:  for l being limit_ordinal non empty Ordinal st ( for a being ordinal number st a in l holds
1 -Veblen a = epsilon_ a ) holds
1 -Veblen l = epsilon_ l
proofend;

theorem :: ORDINAL6:77
for a being ordinal number holds 1 -Veblen a = epsilon_ a
proofend;