let A be Ordinal; :: thesis: ex M being Cardinal st
( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds
M c= B ) )
defpred S₁[ Ordinal] means ( $1 c= card A & A is_cofinal_with $1 );
A1: ex B being Ordinal st S₁[B] by Th8;
consider C being Ordinal such that
A2: S₁[C] and
A3: for B being Ordinal st S₁[B] holds
C c= B from ORDINAL1:sch 1(A1);
take M = card C; :: thesis: ( M c= card A & A is_cofinal_with M & ( for B being Ordinal st A is_cofinal_with B holds
M c= B ) )
consider B being Ordinal such that
A4: B c= M and
A5: C is_cofinal_with B by Th8;
A6: M c= C by CARD_1:8;
then A7: B c= C by A4;
then B c= card A by A2, XBOOLE_1:1;
then C c= B by A2, A3, A5, ORDINAL4:37;
then A8: C = B by A7;
hence ( M c= card A & A is_cofinal_with M ) by A2, A4, A6, XBOOLE_0:def 10; :: thesis: for B being Ordinal st A is_cofinal_with B holds
M c= B
let B be Ordinal; :: thesis: ( A is_cofinal_with B implies M c= B )
assume that
A9: A is_cofinal_with B and
A10: not M c= B ; :: thesis: contradiction
A11: C = M by A4, A6, A8;
then not B c= card A by A3, A9, A10;
hence contradiction by A2, A11, A10, XBOOLE_1:1; :: thesis: verum