:: 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 b₁ being set st b₁ is ordinal holds
b₁ 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 b₁ being set st b₁ is ordinal-membered

proof end;

end;

registration

let X be ordinal-membered set ;

cluster -> ordinal for Element of X;

coherence
for b₁ being Element of X holds b₁ 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 b₁ being Ordinal-Sequence st b₁ = id a holds
b₁ is increasing

proof end;

end;

registration

let a be Ordinal;

cluster id a -> continuous for Ordinal-Sequence;

coherence
for b₁ being Ordinal-Sequence st b₁ = id a holds
b₁ is continuous

proof end;

end;

registration

cluster Relation-like Function-like Sequence-like non empty Ordinal-yielding increasing continuous for set ;

existence
ex b₁ being Ordinal-Sequence st
( not b₁ is empty & b₁ is increasing & b₁ 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 b₁ being Sequence st b₁ is normal holds
b₁ is Ordinal-yielding ;

cluster Relation-like Function-like Sequence-like Ordinal-yielding normal -> increasing continuous for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is normal holds
( b₁ is increasing & b₁ is continuous ) ;

cluster Relation-like Function-like Sequence-like Ordinal-yielding increasing continuous -> normal for set ;

coherence
for b₁ being Ordinal-Sequence st b₁ is increasing & b₁ is continuous holds
b₁ is normal ;

end;

registration

cluster Relation-like Function-like Sequence-like non empty normal for set ;

existence
ex b₁ being Sequence st
( not b₁ is empty & b₁ 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 b₁ being Ordinal holds
( b₁ = ord-type X iff b₁ = 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 b₁ being Ordinal-Sequence of U st b₁ 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 b₁ being Ordinal-Sequence of a,U holds
( b₁ is Sequence-like & b₁ 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{ F₁() -> Universe, F₂() -> Ordinal of F₁(), F₃() -> Ordinal-Sequence of omega,F₁(), F₄( Ordinal) -> Ordinal } :

( F₂() c= Union F₃() & F₄((Union F₃())) = Union F₃() & ( for b being Ordinal st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) )

provided

A1: omega in F₁() and
A2: for a being Ordinal st a in F₁() holds
F₄(a) in F₁() and
A3: for a, b being Ordinal st a in b & b in F₁() holds
F₄(a) in F₄(b) and
A4: for a being Ordinal of F₁() 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 = F₄(b) ) holds
F₄(a) is_limes_of phi and
A5: F₃() . 0 = F₂() and
A6: for a being Ordinal st a in omega holds
F₃() . (succ a) = F₄((F₃() . a))

proof end;

scheme :: ORDINAL6:sch 2
CriticalNumber3{ F₁() -> Universe, F₂() -> Ordinal of F₁(), F₃( Ordinal) -> Ordinal } :

ex a being Ordinal of F₁() st
( F₂() in a & F₃(a) = a )

provided

A1: omega in F₁() and
A2: for a being Ordinal st a in F₁() holds
F₃(a) in F₁() and
A3: for a, b being Ordinal st a in b & b in F₁() holds
F₃(a) in F₃(b) and
A4: for a being Ordinal of F₁() 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 = F₃(b) ) holds
F₃(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 b₁ being Ordinal-Sequence of U st
for b being Ordinal of U holds b₁ . b = exp (a,b)

proof end;

uniqueness
for b₁, b₂ being Ordinal-Sequence of U st ( for b being Ordinal of U holds b₁ . b = exp (a,b) ) & ( for b being Ordinal of U holds b₂ . b = exp (a,b) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines exp ORDINAL6:def 8 :
for U being Universe
for a being Ordinal st a in U holds
for b₃ being Ordinal-Sequence of U holds
( b₃ = U exp a iff for b being Ordinal of U holds b₃ . 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 b₁ being Ordinal of U st
( not b₁ is trivial & b₁ is finite )

proof end;

end;

registration

cluster epsilon-transitive epsilon-connected ordinal non trivial finite ordinal-membered for set ;

existence
ex b₁ being Ordinal st
( not b₁ is trivial & b₁ 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 b₁ being Sequence st
( not b₁ is empty & b₁ is Ordinal-Sequence-valued & b₁ 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 b₁ being Function of a,b holds
( b₁ is Ordinal-yielding & b₁ 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 b₁ being Ordinal-Sequence st
( dom b₁ = dom (g . 0) & ( for a being Ordinal st a in dom b₁ holds
b₁ . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal-Sequence st dom b₁ = dom (g . 0) & ( for a being Ordinal st a in dom b₁ holds
b₁ . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) & dom b₂ = dom (g . 0) & ( for a being Ordinal st a in dom b₂ holds
b₂ . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines lims ORDINAL6:def 12 :
for g being Ordinal-Sequence-valued Sequence
for b₂ being Ordinal-Sequence holds
( b₂ = lims g iff ( dom b₂ = dom (g . 0) & ( for a being Ordinal st a in dom b₂ holds
b₂ . 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 b₁ 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 b₁ 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 b₁ being Ordinal-Sequence-valued Sequence st
( dom b₁ = On U & b₁ . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b₁ . (succ b) = criticals (b₁ . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b₁ . l = criticals (b₁ | l) ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal-Sequence-valued Sequence st dom b₁ = On U & b₁ . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b₁ . (succ b) = criticals (b₁ . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b₁ . l = criticals (b₁ | l) ) & dom b₂ = On U & b₂ . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds
b₂ . (succ b) = criticals (b₂ . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds
b₂ . l = criticals (b₂ | l) ) holds
b₁ = b₂

proof end;

end;

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

registration

cluster epsilon-transitive non empty subset-closed Tarski uncountable universal for set ;

existence
ex b₁ being Universe st b₁ 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 b₁ being Ordinal holds
( b₁ = n -Veblen b iff b₁ = (((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;