let fi, psi be Ordinal-Sequence; :: thesis: for C being Ordinal st {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) holds
sup psi = C +^ (sup fi)
let C be Ordinal; :: thesis: ( {} <> dom fi & dom fi = dom psi & ( for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ) implies sup psi = C +^ (sup fi) )
assume that
A1: {} <> dom fi and
A2: dom fi = dom psi and
A3: for A, B being Ordinal st A in dom fi & B = fi . A holds
psi . A = C +^ B ; :: thesis: sup psi = C +^ (sup fi)
set z = the Element of dom fi;
reconsider z9 = fi . the Element of dom fi as Ordinal ;
A4: C +^ (sup (rng fi)) c= sup (rng psi)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in C +^ (sup (rng fi)) or x in sup (rng psi) )
assume A5: x in C +^ (sup (rng fi)) ; :: thesis: x in sup (rng psi)
then reconsider A = x as Ordinal ;
A6: now :: thesis: ( ex B being Ordinal st
( B in sup (rng fi) & A = C +^ B ) implies A in sup (rng psi) )
given B being Ordinal such that A7: B in sup (rng fi) and
A8: A = C +^ B ; :: thesis: A in sup (rng psi)
consider D being Ordinal such that
A9: D in rng fi and
A10: B c= D by A7, ORDINAL2:21;
consider x being object such that
A11: x in dom fi and
A12: D = fi . x by A9, FUNCT_1:def 3;
reconsider x = x as Ordinal by A11;
psi . x = C +^ D by A3, A11, A12;
then C +^ D in rng psi by A2, A11, FUNCT_1:def 3;
then C +^ D in sup (rng psi) by ORDINAL2:19;
hence A in sup (rng psi) by A8, A10, ORDINAL1:12, ORDINAL2:33; :: thesis: verum
end;
now :: thesis: ( A in C implies A in sup (rng psi) )
C +^ z9 = psi . the Element of dom fi by A1, A3;
then C +^ z9 in rng psi by A1, A2, FUNCT_1:def 3;
then A13: C +^ z9 in sup (rng psi) by ORDINAL2:19;
assume A14: A in C ; :: thesis: A in sup (rng psi)
C c= C +^ z9 by Th24;
then A c= C +^ z9 by A14, ORDINAL1:def 2;
hence A in sup (rng psi) by A13, ORDINAL1:12; :: thesis: verum
end;
hence x in sup (rng psi) by A5, A6, Th38; :: thesis: verum
end;
sup (rng psi) c= C +^ (sup (rng fi))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in sup (rng psi) or x in C +^ (sup (rng fi)) )
assume A15: x in sup (rng psi) ; :: thesis: x in C +^ (sup (rng fi))
then reconsider A = x as Ordinal ;
consider B being Ordinal such that
A16: B in rng psi and
A17: A c= B by A15, ORDINAL2:21;
consider y being object such that
A18: y in dom psi and
A19: B = psi . y by A16, FUNCT_1:def 3;
reconsider y = y as Ordinal by A18;
reconsider y9 = fi . y as Ordinal ;
y9 in rng fi by A2, A18, FUNCT_1:def 3;
then A20: y9 in sup (rng fi) by ORDINAL2:19;
B = C +^ y9 by A2, A3, A18, A19;
then B in C +^ (sup (rng fi)) by A20, ORDINAL2:32;
hence x in C +^ (sup (rng fi)) by A17, ORDINAL1:12; :: thesis: verum
end;
hence sup psi = C +^ (sup fi) by A4; :: thesis: verum