:: by Grzegorz Bancerek

::

:: Received October 18, 2010

:: Copyright (c) 2010-2021 Association of Mizar Users

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

for X being set holds

( X is ordinal-membered iff ex a being Ordinal st X c= a );

registration

coherence

for b_{1} being set st b_{1} is ordinal holds

b_{1} is ordinal-membered
;

let X be set ;

coherence

On X is ordinal-membered

end;
for b

b

let X be set ;

coherence

On X is ordinal-membered

proof end;

registration

let X be ordinal-membered set ;

coherence

for b_{1} being Element of X holds b_{1} is ordinal

end;
coherence

for b

proof end;

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

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 )

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;

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

by ORDINAL4:2;

registration
end;

registration
end;

registration

let a be Ordinal;

coherence

for b_{1} being Ordinal-Sequence st b_{1} = id a holds

b_{1} is increasing

end;
coherence

for b

b

proof end;

registration

let a be Ordinal;

coherence

for b_{1} being Ordinal-Sequence st b_{1} = id a holds

b_{1} is continuous

end;
coherence

for b

b

proof end;

registration

ex b_{1} being Ordinal-Sequence st

( not b_{1} is empty & b_{1} is increasing & b_{1} is continuous )
end;

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

existence ex b

( not b

proof end;

:: deftheorem defines normal ORDINAL6:def 2 :

for f being Sequence holds

( f is normal iff f is increasing continuous Ordinal-Sequence );

for f being Sequence holds

( f is normal iff f is increasing continuous Ordinal-Sequence );

definition

let f be Ordinal-Sequence;

compatibility

( f is normal iff ( f is increasing & f is continuous ) ) ;

end;
compatibility

( f is normal iff ( f is increasing & f is continuous ) ) ;

:: deftheorem defines normal ORDINAL6:def 3 :

for f being Ordinal-Sequence holds

( f is normal iff ( f is increasing & f is continuous ) );

for f being Ordinal-Sequence holds

( f is normal iff ( f is increasing & f is continuous ) );

registration

coherence

for b_{1} being Sequence st b_{1} is normal holds

b_{1} is Ordinal-yielding
;

for b_{1} being Ordinal-Sequence st b_{1} is normal holds

( b_{1} is increasing & b_{1} is continuous )
;

for b_{1} being Ordinal-Sequence st b_{1} is increasing & b_{1} is continuous holds

b_{1} is normal
;

end;
for b

b

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

coherence for b

( b

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

coherence for b

b

registration
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

for f being Ordinal-Sequence st f is non-decreasing holds

f | a is non-decreasing

proof end;

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

for X being set holds ord-type X = order_type_of (RelIncl (On X));

for X being set holds ord-type X = order_type_of (RelIncl (On X));

definition

let X be ordinal-membered set ;

compatibility

for b_{1} being Ordinal holds

( b_{1} = ord-type X iff b_{1} = order_type_of (RelIncl X) )
by Th2;

end;
compatibility

for b

( b

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

for X being ordinal-membered set holds ord-type X = order_type_of (RelIncl X);

for X being ordinal-membered set holds ord-type X = order_type_of (RelIncl X);

registration
end;

definition

let X be set ;

canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) is Ordinal-Sequence

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

canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X))) is Ordinal-Sequence

proof end;

:: deftheorem defines numbering ORDINAL6:def 6 :

for X being set holds numbering X = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));

for X being set holds numbering X = canonical_isomorphism_of ((RelIncl (ord-type X)),(RelIncl (On X)));

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 )

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 )

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

registration
end;

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

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)

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)

x in y ) holds

ord-type (X \/ Y) = (ord-type X) +^ (ord-type Y)

proof end;

definition

let f be Ordinal-Sequence;

numbering { a where a is Element of dom f : a is_a_fixpoint_of f } is Ordinal-Sequence ;

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

numbering { a where a is Element of dom f : a is_a_fixpoint_of f } is Ordinal-Sequence ;

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

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

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 )

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

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;

for f being Ordinal-Sequence st x in dom (criticals f) holds

x c= (criticals f) . x by ORDINAL4:10;

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 )

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)

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

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)

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)

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)

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)

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 U be Universe;

ex b_{1} being Ordinal-Sequence of U st b_{1} is normal

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

proof end;

definition
end;

registration

let U be Universe;

let a be Ordinal;

for b_{1} being Ordinal-Sequence of a,U holds

( b_{1} is Sequence-like & b_{1} is Ordinal-yielding )
by FUNCT_2:def 1, RELAT_1:def 19;

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

( b

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

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

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

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

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_{1}() -> Universe, F_{2}() -> Ordinal of F_{1}(), F_{3}() -> Ordinal-Sequence of omega,F_{1}(), F_{4}( Ordinal) -> Ordinal } :

CriticalNumber2{ F

( F_{2}() c= Union F_{3}() & F_{4}((Union F_{3}())) = Union F_{3}() & ( for b being Ordinal st F_{2}() c= b & b in F_{1}() & F_{4}(b) = b holds

Union F_{3}() c= b ) )

providedUnion F

A1:
omega in F_{1}()
and

A2: for a being Ordinal st a in F_{1}() holds

F_{4}(a) in F_{1}()
and

A3: for a, b being Ordinal st a in b & b in F_{1}() holds

F_{4}(a) in F_{4}(b)
and

A4: for a being Ordinal of F_{1}() 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_{4}(b) ) holds

F_{4}(a) is_limes_of phi
and

A5: F_{3}() . 0 = F_{2}()
and

A6: for a being Ordinal st a in omega holds

F_{3}() . (succ a) = F_{4}((F_{3}() . a))

A2: for a being Ordinal st a in F

F

A3: for a, b being Ordinal st a in b & b in F

F

A4: for a being Ordinal of F

for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds

phi . b = F

F

A5: F

A6: for a being Ordinal st a in omega holds

F

proof end;

scheme :: ORDINAL6:sch 2

CriticalNumber3{ F_{1}() -> Universe, F_{2}() -> Ordinal of F_{1}(), F_{3}( Ordinal) -> Ordinal } :

provided

CriticalNumber3{ F

provided

A1:
omega in F_{1}()
and

A2: for a being Ordinal st a in F_{1}() holds

F_{3}(a) in F_{1}()
and

A3: for a, b being Ordinal st a in b & b in F_{1}() holds

F_{3}(a) in F_{3}(b)
and

A4: for a being Ordinal of F_{1}() 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_{3}(b) ) holds

F_{3}(a) is_limes_of phi

A2: for a being Ordinal st a in F

F

A3: for a, b being Ordinal st a in b & b in F

F

A4: for a being Ordinal of F

for phi being Ordinal-Sequence st dom phi = a & ( for b being Ordinal st b in a holds

phi . b = F

F

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 )

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

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

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

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

definition

let U be Universe;

let a be Ordinal;

assume A1: a in U ;

ex b_{1} being Ordinal-Sequence of U st

for b being Ordinal of U holds b_{1} . b = exp (a,b)

for b_{1}, b_{2} being Ordinal-Sequence of U st ( for b being Ordinal of U holds b_{1} . b = exp (a,b) ) & ( for b being Ordinal of U holds b_{2} . b = exp (a,b) ) holds

b_{1} = b_{2}

end;
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 for b being Ordinal of U holds it . b = exp (a,b);

ex b

for b being Ordinal of U holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines exp ORDINAL6:def 8 :

for U being Universe

for a being Ordinal st a in U holds

for b_{3} being Ordinal-Sequence of U holds

( b_{3} = U exp a iff for b being Ordinal of U holds b_{3} . b = exp (a,b) );

for U being Universe

for a being Ordinal st a in U holds

for b

( b

registration

let U be Universe;

ex b_{1} being Ordinal of U st

( not b_{1} is trivial & b_{1} is finite )

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

existence ex b

( not b

proof end;

registration
end;

registration
end;

definition

let g be Function;

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

for x being set st x in rng g holds

x is Ordinal-Sequence;

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

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

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

for f being Function holds

( f is with_the_same_dom iff rng f is with_common_domain );

registration

ex b_{1} being Sequence st

( not b_{1} is empty & b_{1} is Ordinal-Sequence-valued & b_{1} is with_the_same_dom )
end;

cluster Relation-like Function-like Sequence-like non empty Ordinal-Sequence-valued with_the_same_dom for set ;

existence ex b

( not b

proof end;

registration

let g be Ordinal-Sequence-valued Function;

let x be object ;

coherence

( g . x is Relation-like & g . x is Function-like )

end;
let x be object ;

coherence

( g . x is Relation-like & g . x is Function-like )

proof end;

registration

let g be Ordinal-Sequence-valued Function;

let x be set ;

coherence

( g . x is Sequence-like & g . x is Ordinal-yielding )

end;
let x be set ;

coherence

( g . x is Sequence-like & g . x is Ordinal-yielding )

proof end;

registration

let g be Ordinal-Sequence-valued Function;

let X be set ;

coherence

g | X is Ordinal-Sequence-valued

end;
let X be set ;

coherence

g | X is Ordinal-Sequence-valued

proof end;

registration

let a, b be Ordinal;

coherence

for b_{1} being Function of a,b holds

( b_{1} is Ordinal-yielding & b_{1} is Sequence-like )

end;
coherence

for b

( b

proof end;

definition

let g be Ordinal-Sequence-valued Sequence;

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

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 ;

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

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

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

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;

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

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 )

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)

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)

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

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

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

g1 . a c= g2 . a ) holds

criticals g1 c= criticals g2

proof end;

definition

let g be Ordinal-Sequence-valued Sequence;

ex b_{1} being Ordinal-Sequence st

( dom b_{1} = dom (g . 0) & ( for a being Ordinal st a in dom b_{1} holds

b_{1} . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) )

for b_{1}, b_{2} being Ordinal-Sequence st dom b_{1} = dom (g . 0) & ( for a being Ordinal st a in dom b_{1} holds

b_{1} . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) & dom b_{2} = dom (g . 0) & ( for a being Ordinal st a in dom b_{2} holds

b_{2} . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) holds

b_{1} = b_{2}

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

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines lims ORDINAL6:def 12 :

for g being Ordinal-Sequence-valued Sequence

for b_{2} being Ordinal-Sequence holds

( b_{2} = lims g iff ( dom b_{2} = dom (g . 0) & ( for a being Ordinal st a in dom b_{2} holds

b_{2} . a = union { ((g . b) . a) where b is Element of dom g : b in dom g } ) ) );

for g being Ordinal-Sequence-valued Sequence

for b

( b

b

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

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 ;

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_{1} being Ordinal-Sequence holds verum;

;

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_{1} being Ordinal-Sequence-valued Sequence holds verum;

;

end;
func OS@ x -> Ordinal-Sequence equals :Def13: :: ORDINAL6:def 13

x if x is Ordinal-Sequence

otherwise the Ordinal-Sequence;

correctness x if x is Ordinal-Sequence

otherwise the Ordinal-Sequence;

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

;

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 x if x is Ordinal-Sequence-valued Sequence

otherwise the Ordinal-Sequence-valued Sequence;

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

;

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

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

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;

ex b_{1} being Ordinal-Sequence-valued Sequence st

( dom b_{1} = On U & b_{1} . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds

b_{1} . (succ b) = criticals (b_{1} . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds

b_{1} . l = criticals (b_{1} | l) ) )

for b_{1}, b_{2} being Ordinal-Sequence-valued Sequence st dom b_{1} = On U & b_{1} . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds

b_{1} . (succ b) = criticals (b_{1} . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds

b_{1} . l = criticals (b_{1} | l) ) & dom b_{2} = On U & b_{2} . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds

b_{2} . (succ b) = criticals (b_{2} . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds

b_{2} . l = criticals (b_{2} | l) ) holds

b_{1} = b_{2}

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

ex b

( dom b

b

b

proof end;

uniqueness for b

b

b

b

b

b

proof end;

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

for U being Universe

for b_{2} being Ordinal-Sequence-valued Sequence holds

( b_{2} = U -Veblen iff ( dom b_{2} = On U & b_{2} . 0 = U exp omega & ( for b being Ordinal st succ b in On U holds

b_{2} . (succ b) = criticals (b_{2} . b) ) & ( for l being limit_ordinal non empty Ordinal st l in On U holds

b_{2} . l = criticals (b_{2} | l) ) ) );

for U being Universe

for b

( b

b

b

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

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)

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

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

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

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

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

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

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;

definition

let a, b be Ordinal;

(((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b is Ordinal ;

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

(((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b is Ordinal ;

:: deftheorem defines -Veblen ORDINAL6:def 16 :

for a, b being Ordinal holds a -Veblen b = (((Tarski-Class ((a \/ b) \/ omega)) -Veblen) . a) . b;

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;

n -Veblen b is Ordinal ;

compatibility

for b_{1} being Ordinal holds

( b_{1} = n -Veblen b iff b_{1} = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b )

end;
let b be Ordinal;

:: original: -Veblen

redefine func n -Veblen b -> Ordinal equals :: ORDINAL6:def 17

(((Tarski-Class (b \/ omega)) -Veblen) . n) . b;

coherence redefine func n -Veblen b -> Ordinal equals :: ORDINAL6:def 17

(((Tarski-Class (b \/ omega)) -Veblen) . n) . b;

n -Veblen b is Ordinal ;

compatibility

for b

( b

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

for n being Nat

for b being Ordinal holds n -Veblen b = (((Tarski-Class (b \/ omega)) -Veblen) . n) . b;

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

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

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

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;