Theorem alephislim

Description: Every aleph is a limit ordinal. (Contributed by NM, 11-Nov-2003)

	Ref	Expression
Assertion	alephislim	$$⊢A\in \mathrm{On}\leftrightarrow \mathrm{Lim}\aleph \left(A\right)$$

Proof

Step	Hyp	Ref	Expression
1		alephgeom	$$⊢A\in \mathrm{On}\leftrightarrow \mathrm{\omega }\subseteq \aleph \left(A\right)$$
2		cardlim	$$⊢\mathrm{\omega }\subseteq \mathrm{card}\left(\aleph \left(A\right)\right)\leftrightarrow \mathrm{Lim}\mathrm{card}\left(\aleph \left(A\right)\right)$$
3		alephcard	$$⊢\mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)$$
4	3	sseq2i	$$⊢\mathrm{\omega }\subseteq \mathrm{card}\left(\aleph \left(A\right)\right)\leftrightarrow \mathrm{\omega }\subseteq \aleph \left(A\right)$$
5		limeq	$$⊢\mathrm{card}\left(\aleph \left(A\right)\right)=\aleph \left(A\right)\to \left(\mathrm{Lim}\mathrm{card}\left(\aleph \left(A\right)\right)\leftrightarrow \mathrm{Lim}\aleph \left(A\right)\right)$$
6	3 5	ax-mp	$$⊢\mathrm{Lim}\mathrm{card}\left(\aleph \left(A\right)\right)\leftrightarrow \mathrm{Lim}\aleph \left(A\right)$$
7	2 4 6	3bitr3i	$$⊢\mathrm{\omega }\subseteq \aleph \left(A\right)\leftrightarrow \mathrm{Lim}\aleph \left(A\right)$$
8	1 7	bitri	$$⊢A\in \mathrm{On}\leftrightarrow \mathrm{Lim}\aleph \left(A\right)$$