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

begin

definition

let X be set ;
attr X is ordinal-membered means :SS: :: ORDINAL6:def 1
ex a being ordinal number st X c= a;

end;

:: deftheorem SS 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 set ;
coherence
for b₁ being set st b₁ is ordinal holds
b₁ is ordinal-membered

proof end;

let X be set ;
cluster On X -> ordinal-membered ;
coherence
On X is ordinal-membered

proof end;

end;

theorem EXCH9: :: 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 set ;
existence
ex b₁ being set st b₁ is ordinal-membered

proof end;

end;

registration

let X be ordinal-membered set ;
cluster -> ordinal Element of X;
coherence
for b₁ being Element of X holds b₁ is ordinal

proof end;

end;

theorem EXCH10: :: 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

proof end;

theorem EXCH1: :: ORDINAL6:4

for a, b being ordinal number holds
( a c= b iff b nin a )

proof end;

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

proof end;

registration

let a, b be ordinal number ;
cluster a \ b -> ordinal-membered ;
coherence
a \ b is ordinal-membered

proof end;

end;

theorem Lem1: :: 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 Lem3: :: ORDINAL6:8

for x, y, X being set st [x,y] in RelIncl X holds
x c= y

proof end;

theorem Lem4: :: ORDINAL6:9

for f1, f2 being T-Sequence holds f1 c= f1 ^ f2

proof end;

theorem ORDINAL4th2: :: ORDINAL6:10

for f1, f2 being T-Sequence holds rng (f1 ^ f2) = (rng f1) \/ (rng f2)

proof end;

theorem LemE1: :: ORDINAL6:11

for a, b being ordinal number holds
( a c= b iff epsilon_ a c= epsilon_ b )

proof end;

theorem LemE2: :: ORDINAL6:12

for a, b being ordinal number 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 proj2 f -> ordinal-membered ;
coherence
rng f is ordinal-membered

proof end;

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 )

proof end;

end;

registration

let a be ordinal number ;
cluster id a -> increasing Ordinal-Sequence;
coherence
for b₁ being Ordinal-Sequence st b₁ = id a holds
b₁ is increasing

proof end;

end;

registration

let a be ordinal number ;
cluster id a -> continuous 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 T-Sequence-like non empty Ordinal-yielding increasing continuous 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 T-Sequence;
attr f is normal means :NORM: :: ORDINAL6:def 2
f is increasing continuous Ordinal-Sequence;

end;

:: deftheorem NORM 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 NORM;

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 set ;
coherence
for b₁ being T-Sequence st b₁ is normal holds
b₁ is Ordinal-yielding by NORM;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding normal -> increasing continuous set ;
coherence
for b₁ being Ordinal-Sequence st b₁ is normal holds
( b₁ is increasing & b₁ is continuous ) by NORM;
cluster Relation-like Function-like T-Sequence-like Ordinal-yielding increasing continuous -> normal set ;
coherence
for b₁ being Ordinal-Sequence st b₁ is increasing & b₁ is continuous holds
b₁ is normal by NORM;

end;

registration

cluster Relation-like Function-like T-Sequence-like non empty normal set ;
existence
ex b₁ being T-Sequence st
( not b₁ is empty & b₁ is normal )

proof end;

end;

theorem ThND: :: ORDINAL6:13

for a being ordinal number
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 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 b₁ being ordinal number holds
( b₁ = ord-type X iff b₁ = order_type_of (RelIncl X) ) by EXCH10;

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:9, 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 number holds ord-type {a} = 1

proof end;

theorem :: ORDINAL6:16

for a, b being ordinal number st a <> b holds
ord-type {a,b} = 2

proof end;

theorem :: ORDINAL6:17

for a being ordinal number holds ord-type a = a by ORDERS_1:198;

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 ThN1: :: ORDINAL6:18

for X being set holds
( dom (numbering X) = ord-type X & rng (numbering X) = On X )

proof end;

theorem ThN1a: :: 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 ThN3: :: ORDINAL6:21

for X being set holds numbering X is_isomorphism_of RelIncl (ord-type X), RelIncl (On X)

proof end;

theorem ThN4: :: 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 ThN5: :: 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 ThN6: :: 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 ThN7: :: 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;

begin

theorem LemF1: :: ORDINAL6:27

for x being set
for f being Function st x is_a_fixpoint_of f holds
x in rng f

proof end;

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 Th01: :: 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 Th02: :: 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 Th03: :: 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 Th05: :: ORDINAL6:32

for f being Ordinal-Sequence holds dom (criticals f) c= dom f

proof end;

theorem Th06: :: 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) & b = (criticals f) . a )

proof end;

theorem :: ORDINAL6:34

for a, b being ordinal number
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 number
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 Th08a: :: 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 Th08: :: 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 Th19: :: 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) & 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 Th09: :: 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 Th0A: :: ORDINAL6:40

for f1, f2 being Ordinal-Sequence st f1 c= f2 holds
criticals f1 c= criticals f2

proof end;

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) V27( On U, On U) Ordinal-yielding normal 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 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 V27(a, On U) -> T-Sequence-like Ordinal-yielding Element of bool [:a,(On U):];
coherence
for b₁ being Ordinal-Sequence of a,U holds
( b₁ is T-Sequence-like & b₁ is Ordinal-yielding )

proof end;

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 func f . x -> Ordinal of U;
coherence
f . x is Ordinal of U

proof end;

end;

theorem ThC1: :: 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

proof end;

theorem ThC2: :: 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

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 number st F₂() c= b & b in F₁() & F₄(b) = b holds
Union F₃() c= b ) )

provided

A0: omega in F₁() and
P0: for a being ordinal number st a in F₁() holds
F₄(a) in F₁() and
A1: for a, b being ordinal number st a in b & b in F₁() holds
F₄(a) in F₄(b) and
A2: 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 number st b in a holds
phi . b = F₄(b) ) holds
F₄(a) is_limes_of phi and
F1: F₃() . 0 = F₂() and
F2: for a being ordinal number st a in omega holds
F₃() . (succ a) = F₄((F₃() . a))

proof end;

Lm1: {} in omega
by ORDINAL1:def 12;

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

A0: omega in F₁() and
P0: for a being ordinal number st a in F₁() holds
F₃(a) in F₁() and
A1: for a, b being ordinal number st a in b & b in F₁() holds
F₃(a) in F₃(b) and
A2: 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 number st b in a holds
phi . b = F₃(b) ) holds
F₃(a) is_limes_of phi

proof end;

theorem Th38: :: ORDINAL6:43

for b being ordinal number
for W being Universe
for phi being normal Ordinal-Sequence of W st omega in W & b in W holds
ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi )

proof end;

theorem Th39: :: 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 Th40: :: 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

proof end;

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

proof end;

end;

definition

let U be Universe;
let a be ordinal number ;
assume AA: a in U ;
func U exp a -> Ordinal-Sequence of U means :EXP: :: 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 EXP defines exp ORDINAL6:def 8 :
for U being Universe
for a being ordinal number 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

proof end;

end;

registration

let U be Universe;
cluster epsilon-transitive epsilon-connected ordinal non trivial finite ordinal-membered 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 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 :OSV: :: ORDINAL6:def 9
for x being set st x in rng g holds
x is Ordinal-Sequence;

end;

:: deftheorem OSV 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 T-Sequence-like non empty Ordinal-Sequence-valued with_the_same_dom set ;
existence
ex b₁ being T-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 set ;
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 -> T-Sequence-like Ordinal-yielding ;
coherence
( g . x is T-Sequence-like & g . x is Ordinal-yielding )

proof end;

end;

registration

let g be T-Sequence;
let a be ordinal number ;
cluster g | a -> T-Sequence-like ;
coherence
g | a is T-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 number ;
cluster Function-like V27(a,b) -> T-Sequence-like Ordinal-yielding Element of bool [:a,b:];
coherence
for b₁ being Function of a,b holds
( b₁ is Ordinal-yielding & b₁ is T-Sequence-like )

proof end;

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) & ( 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 T-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 ThA1: :: 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) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } is ordinal-membered

proof end;

theorem ThA2: :: ORDINAL6:47

for a, b being ordinal number
for g being Ordinal-Sequence-valued T-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 T-Sequence st x in dom (criticals g) holds
x c= (criticals g) . x by ORDINAL4:10;

theorem ThA5: :: 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

proof end;

theorem ThA6: :: ORDINAL6:50

for b being ordinal number
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( 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) & b = (criticals g) . a )

proof end;

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 <> {} & 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 ThA9: :: ORDINAL6:52

for l being limit_ordinal non empty Ordinal
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for a being ordinal number 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 ThAA: :: ORDINAL6:53

for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( for a being ordinal number st a in dom g holds
g . a is normal ) holds
criticals g is continuous

proof end;

theorem ThAB: :: ORDINAL6:54

for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & ( 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) & f in rng g holds
f . a c= (criticals g) . a

proof end;

theorem ThAC: :: ORDINAL6:55

for g1, g2 being Ordinal-Sequence-valued T-Sequence st dom g1 = dom g2 & dom g1 <> {} & ( for a being ordinal number 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 T-Sequence;
func lims g -> Ordinal-Sequence means :LIM: :: ORDINAL6:def 12
( dom it = dom (g . 0) & ( 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 b₁ being Ordinal-Sequence st
( dom b₁ = dom (g . 0) & ( for a being ordinal number 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 number 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 number 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 LIM defines lims ORDINAL6:def 12 :
for g being Ordinal-Sequence-valued T-Sequence
for b₂ being Ordinal-Sequence holds
( b₂ = lims g iff ( dom b₂ = dom (g . 0) & ( for a being ordinal number st a in dom b₂ holds
b₂ . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) ) );

theorem ThL1: :: ORDINAL6:56

for U being Universe
for g being Ordinal-Sequence-valued T-Sequence st dom g <> {} & dom g in U & ( 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

proof end;

begin

definition

let x be set ;
func OS@ x -> Ordinal-Sequence equals :OSc: :: 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 T-Sequence equals :OSVc: :: 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 ) & ( x is not Ordinal-Sequence-valued T-Sequence implies the Ordinal-Sequence-valued T-Sequence is Ordinal-Sequence-valued T-Sequence ) );
consistency
for b₁ being Ordinal-Sequence-valued T-Sequence holds verum;
;

end;

:: deftheorem OSc 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 OSVc defines OSV@ ORDINAL6:def 14 :
for x being set holds
( ( x is Ordinal-Sequence-valued T-Sequence implies OSV@ x = x ) & ( x is not Ordinal-Sequence-valued T-Sequence implies OSV@ x = the Ordinal-Sequence-valued T-Sequence ) );

definition

let U be Universe;
func U -Veblen -> Ordinal-Sequence-valued T-Sequence means :V: :: ORDINAL6:def 15
( dom it = On U & it . 0 = U exp omega & ( for b being ordinal number 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 T-Sequence st
( dom b₁ = On U & b₁ . 0 = U exp omega & ( for b being ordinal number 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 T-Sequence st dom b₁ = On U & b₁ . 0 = U exp omega & ( for b being ordinal number 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 number 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 V defines -Veblen ORDINAL6:def 15 :
for U being Universe
for b₂ being Ordinal-Sequence-valued T-Sequence holds
( b₂ = U -Veblen iff ( dom b₂ = On U & b₂ . 0 = U exp omega & ( for b being ordinal number 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 set ;
existence
not for b₁ being Universe holds b₁ is countable

proof end;

end;

theorem Unc1: :: ORDINAL6:57

for U being Universe holds
( not U is countable iff omega in U )

proof end;

theorem Th51: :: ORDINAL6:58

for a, b, c being ordinal number
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 number
for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( 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)

proof end;

theorem Th52: :: ORDINAL6:60

for a, b, c being ordinal number
for U being Universe st a c= b & b in U & omega in U & c in dom ((U -Veblen) . b) & ( 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

proof end;

theorem Th53: :: ORDINAL6:61

for a, b being ordinal number
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 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

proof end;

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

proof end;

Th22: for a being ordinal number
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;

Th61: for l being limit_ordinal non empty Ordinal
for U being Universe st l in U & ( 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

proof end;

theorem Th23: :: ORDINAL6:62

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

proof end;

theorem Th24: :: ORDINAL6:63

for a being ordinal number
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 Th25: :: ORDINAL6:64

for a, b being ordinal number
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 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

proof end;

registration

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

proof end;

end;

definition

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

theorem LemT: :: ORDINAL6:66

for a, b, c being ordinal number holds a in Tarski-Class ((a \/ b) \/ c)

proof end;

theorem Th26: :: ORDINAL6:67

for a, b being ordinal number
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 Th10: :: ORDINAL6:68

for a being ordinal number holds 0 -Veblen a = exp (omega,a)

proof end;

theorem Th11: :: ORDINAL6:69

for b, a being ordinal number holds b -Veblen ((succ b) -Veblen a) = (succ b) -Veblen a

proof end;

theorem Th11a: :: ORDINAL6:70

for b, c, a being ordinal number st b in c holds
b -Veblen (c -Veblen a) = c -Veblen a

proof end;

theorem Th15: :: ORDINAL6:71

for a, b, c being ordinal number holds
( a c= b iff c -Veblen a c= c -Veblen b )

proof end;

theorem Th15a: :: ORDINAL6:72

for a, b, c being ordinal number holds
( a in b iff c -Veblen a in c -Veblen b )

proof end;

theorem :: ORDINAL6:73

for a, b, c, d being ordinal number 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;

begin

theorem Th12: :: ORDINAL6:74

for U being uncountable Universe holds (U -Veblen) . 1 = criticals (U exp omega)

proof end;

theorem Th13: :: ORDINAL6:75

for a being ordinal number holds 1 -Veblen a is epsilon

proof end;

theorem Th14: :: ORDINAL6:76

for e being epsilon Ordinal ex a being ordinal number st e = 1 -Veblen a

proof end;

Th16: 1 -Veblen 0 = epsilon_ 0

proof end;

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

proof end;

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

proof end;

theorem :: ORDINAL6:77

for a being ordinal number holds 1 -Veblen a = epsilon_ a

proof end;