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 Th17;
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 & C is_cofinal_with B ) by Th17;
A5: M c= C by CARD_1:24;
then A6: B c= C by A4, XBOOLE_1:1;
then ( B c= card A & A is_cofinal_with B ) by A2, A4, ORDINAL4:39, XBOOLE_1:1;
then C c= B by A3;
then A7: C = B by A6, XBOOLE_0:def 10;
then A8: C = M by A4, A5, XBOOLE_0:def 10;
thus ( M c= card A & A is_cofinal_with M ) by A2, A4, A5, A7, 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 ( A is_cofinal_with B & not M c= B ) ; :: thesis: contradiction
then ( not B c= card A & B c= M ) by A3, A8;
hence contradiction by A2, A8, XBOOLE_1:1; :: thesis: verum