ORDINAL6: Veblen Hierarchy

proof end;

end;

registration

let f be Ordinal-yielding Function;

cluster rng f -> ordinal-membered ;

coherence by ORDINAL2:def 4;

end;

registration

let a be Ordinal;

cluster id a -> Sequence-like Ordinal-yielding ;

end;

registration

let a be Ordinal;

cluster id a -> increasing for Ordinal-Sequence;

proof end;

end;

registration

let a be Ordinal;

cluster id a -> continuous for Ordinal-Sequence;

proof end;

end;

registration

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

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 :

definition

let f be Ordinal-Sequence;

redefine attr f is normal means :: ORDINAL6:def 3
( f is increasing & f is continuous );

compatibility ;

end;

:: deftheorem defines normal ORDINAL6:def 3 :

registration

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

coherence ;

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

coherence ;

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

end;

registration

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

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

end;

:: deftheorem defines ord-type ORDINAL6:def 4 :

definition

let X be ordinal-membered set ;

redefine func ord-type X equals :: ORDINAL6:def 5
order_type_of (RelIncl X);

compatibility by Th2;

end;

:: deftheorem defines ord-type ORDINAL6:def 5 :

registration

let X be ordinal-membered set ;

cluster RelIncl X -> well-ordering ;

proof end;

end;

registration

let E be empty set ;

cluster On E -> empty ;

coherence by ORDINAL2:7, XBOOLE_1:3;

end;

registration

let E be empty set ;

cluster order_type_of E -> empty ;

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

proof end;

end;

:: deftheorem defines numbering ORDINAL6:def 6 :

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 ;

proof end;

end;

registration

let X, Y be ordinal-membered set ;

cluster X \/ Y -> ordinal-membered ;

proof end;

end;

registration

let X be ordinal-membered set ;
let Y be set ;

cluster X \ Y -> 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 } ;

end;

:: deftheorem defines criticals ORDINAL6:def 7 :

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 ;

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 ;

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):];

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

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

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines exp ORDINAL6:def 8 :

registration

cluster omega -> non trivial ;

end;

registration

let U be Universe;

cluster epsilon-transitive epsilon-connected ordinal non trivial finite ordinal-membered for Element of U;

proof end;

end;

registration

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

proof end;

end;

registration

let U be Universe;
let a be non trivial Ordinal of U;

cluster U exp a -> 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 :

registration

let f be Ordinal-Sequence;

cluster <%f%> -> 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 :

registration

let f be Function;

cluster {f} -> with_common_domain ;

proof end;

end;

registration

let f be Function;

cluster <%f%> -> 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 ;

proof end;

end;

registration

let g be Ordinal-Sequence-valued Function;
let x be object ;

cluster g . x -> Relation-like Function-like ;

proof end;

end;

registration

let g be Ordinal-Sequence-valued Function;
let x be set ;

cluster g . x -> Sequence-like Ordinal-yielding ;

proof end;

end;

registration

let g be Sequence;
let a be Ordinal;

cluster g | a -> Sequence-like ;

end;

registration

let g be Ordinal-Sequence-valued Function;
let X be set ;

cluster g | X -> 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:];

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

end;

:: deftheorem defines criticals ORDINAL6:def 11 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines lims ORDINAL6:def 12 :

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 ;

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 ;

end;

:: deftheorem Def13 defines OS@ ORDINAL6:def 13 :

:: deftheorem Def14 defines OSV@ ORDINAL6:def 14 :

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines -Veblen ORDINAL6:def 15 :

registration

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

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 ;

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;