:: The Ordinal Numbers. Transfinite Induction and Defining by Transfinite Induction :: by Grzegorz Bancerek :: :: Received March 20, 1989 :: Copyright (c) 1990-2015 Association of Mizar Users
A1:
( dom F3() = F1() & ( for B being Ordinal for L being Sequence st B in F1() & L = F3() | B holds F3() . B = F2(L) ) )
and A2:
( dom F4() = F1() & ( for B being Ordinal for L being Sequence st B in F1() & L = F4() | B holds F4() . B = F2(L) ) )
for B being Ordinal st B indom F1() holds F1() . B = F3((F1() | B))
provided
A1:
for A being Ordinal for a being object holds ( a = F2(A) iff ex L being Sequence st ( a = F3(L) & dom L = A & ( for B being Ordinal st B in A holds L . B = F3((L | B)) ) ) )
and A2:
for A being Ordinal st A indom F1() holds F1() . A = F2(A)
ex F being Function st ( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st ( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds A c= B ) ) ) )
provided
A1:
for d being Element of F1() ex A being Ordinal st P1[d,A]