let b be ordinal number ; :: thesis: 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 )
let W be Universe; :: thesis: 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 )
let phi be normal Ordinal-Sequence of W; :: thesis: ( omega in W & b in W implies ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi ) )
assume that
A1: omega in W and
A0: b in W ; :: thesis: ex a being ordinal number st
( b in a & a is_a_fixpoint_of phi )
reconsider b1 = b as Ordinal of W by A0;
A2: dom phi = On W by FUNCT_2:def 1;
deffunc H₁( set ) -> Ordinal of W = phi . $1;
P0: for a being ordinal number st a in W holds
H₁(a) in W ;
00: for a, b being ordinal number st a in b & b in W holds
H₁(a) in H₁(b)

proof

let a, b be ordinal number ; :: thesis: ( a in b & b in W implies H₁(a) in H₁(b) )
( b in W implies b in dom phi ) by A2, ORDINAL1:def 9;
hence ( a in b & b in W implies H₁(a) in H₁(b) ) by ORDINAL2:def 12; :: thesis: verum

end;

01: for a being Ordinal of W st not a is empty & a is limit_ordinal holds
for f being Ordinal-Sequence st dom f = a & ( for b being ordinal number st b in a holds
f . b = H₁(b) ) holds
H₁(a) is_limes_of f

proof

let a be Ordinal of W; :: thesis: ( not a is empty & a is limit_ordinal implies for f being Ordinal-Sequence st dom f = a & ( for b being ordinal number st b in a holds
f . b = H₁(b) ) holds
H₁(a) is_limes_of f )
assume Z0: ( not a is empty & a is limit_ordinal ) ; :: thesis: for f being Ordinal-Sequence st dom f = a & ( for b being ordinal number st b in a holds
f . b = H₁(b) ) holds
H₁(a) is_limes_of f
let f be Ordinal-Sequence; :: thesis: ( dom f = a & ( for b being ordinal number st b in a holds
f . b = H₁(b) ) implies H₁(a) is_limes_of f )
assume that
Z1: dom f = a and
Z2: for b being ordinal number st b in a holds
f . b = H₁(b) ; :: thesis: H₁(a) is_limes_of f
A3: a in dom phi by A2, ORDINAL1:def 9;
then a c= dom phi by ORDINAL1:def 2;
then A4: dom (phi | a) = a by RELAT_1:62;

now

let x be set ; :: thesis: ( x in a implies (phi | a) . x = f . x )
assume A5: x in a ; :: thesis: (phi | a) . x = f . x
hence (phi | a) . x = H₁(x) by FUNCT_1:49
.= f . x by A5, Z2 ;
:: thesis: verum

end;

then f = phi | a by Z1, A4, FUNCT_1:2;
hence H₁(a) is_limes_of f by Z0, A3, ORDINAL2:def 13; :: thesis: verum

end;

consider a being Ordinal of W such that
A6: ( b1 in a & H₁(a) = a ) from ORDINAL6:sch 2(A1, P0, 00, 01);
take a ; :: thesis: ( b in a & a is_a_fixpoint_of phi )
thus ( b in a & a in dom phi & a = phi . a ) by A2, A6, ORDINAL1:def 9; :: according to ABIAN:def 3 :: thesis: verum