Metamath Proof Explorer


Theorem cardalephex

Description: Every transfinite cardinal is an aleph and vice-versa. Theorem 8A(b) of Enderton p. 213 and its converse. (Contributed by NM, 5-Nov-2003)

Ref Expression
Assertion cardalephex ωAcardA=AxOnA=x

Proof

Step Hyp Ref Expression
1 simpl ωAcardA=AωA
2 cardaleph ωAcardA=AA=yOn|Ay
3 2 sseq2d ωAcardA=AωAωyOn|Ay
4 alephgeom yOn|AyOnωyOn|Ay
5 3 4 bitr4di ωAcardA=AωAyOn|AyOn
6 1 5 mpbid ωAcardA=AyOn|AyOn
7 fveq2 x=yOn|Ayx=yOn|Ay
8 7 rspceeqv yOn|AyOnA=yOn|AyxOnA=x
9 6 2 8 syl2anc ωAcardA=AxOnA=x
10 9 ex ωAcardA=AxOnA=x
11 alephcard cardx=x
12 fveq2 A=xcardA=cardx
13 id A=xA=x
14 11 12 13 3eqtr4a A=xcardA=A
15 14 rexlimivw xOnA=xcardA=A
16 10 15 impbid1 ωAcardA=AxOnA=x