let A, B, C be Ordinal; :: thesis: ( A is_cofinal_with B & B is_cofinal_with C implies A is_cofinal_with C )
given xi1 being Ordinal-Sequence such that A1: dom xi1 = B and
A2: rng xi1 c= A and
A3: xi1 is increasing and
A4: A = sup xi1 ; :: according to ORDINAL2:def 17 :: thesis: ( not B is_cofinal_with C or A is_cofinal_with C )
given xi2 being Ordinal-Sequence such that A5: dom xi2 = C and
A6: rng xi2 c= B and
A7: xi2 is increasing and
A8: B = sup xi2 ; :: according to ORDINAL2:def 17 :: thesis:
consider xi being Ordinal-Sequence such that
A9: xi = xi1 * xi2 and
A10: xi is increasing by A3, A7, Th13;
take xi ; :: according to ORDINAL2:def 17 :: thesis: ( dom xi = C & rng xi c= A & xi is increasing & A = sup xi )
thus A11: dom xi = C by ; :: thesis: ( rng xi c= A & xi is increasing & A = sup xi )
rng xi c= rng xi1 by ;
hence A12: ( rng xi c= A & xi is increasing ) by ; :: thesis: A = sup xi
thus A c= sup xi :: according to XBOOLE_0:def 10 :: thesis: sup xi c= A
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in sup xi )
assume A13: a in A ; :: thesis: a in sup xi
then reconsider a = a as Ordinal ;
consider b being Ordinal such that
A14: b in rng xi1 and
A15: a c= b by ;
consider e being object such that
A16: e in B and
A17: b = xi1 . e by ;
reconsider e = e as Ordinal by A16;
consider c being Ordinal such that
A18: c in rng xi2 and
A19: e c= c by ;
consider u being object such that
A20: u in C and
A21: c = xi2 . u by ;
reconsider u = u as Ordinal by A20;
A22: xi1 . c = xi . u by ;
xi . u in rng xi by ;
then A23: xi . u in sup xi by ORDINAL2:19;
xi1 . e c= xi1 . c by A1, A3, A6, A18, A19, Th9;
hence a in sup xi by ; :: thesis: verum
end;
sup (rng xi) c= sup A by ;
hence sup xi c= A by ORDINAL2:18; :: thesis: verum