Theorem alephislim

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

	Ref	Expression
Assertion	alephislim	⊢ ( 𝐴 ∈ On ↔ Lim ( ℵ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		alephgeom	⊢ ( 𝐴 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )
2		cardlim	⊢ ( ω ⊆ ( card ‘ ( ℵ ‘ 𝐴 ) ) ↔ Lim ( card ‘ ( ℵ ‘ 𝐴 ) ) )
3		alephcard	⊢ ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 )
4	3	sseq2i	⊢ ( ω ⊆ ( card ‘ ( ℵ ‘ 𝐴 ) ) ↔ ω ⊆ ( ℵ ‘ 𝐴 ) )
5		limeq	⊢ ( ( card ‘ ( ℵ ‘ 𝐴 ) ) = ( ℵ ‘ 𝐴 ) → ( Lim ( card ‘ ( ℵ ‘ 𝐴 ) ) ↔ Lim ( ℵ ‘ 𝐴 ) ) )
6	3 5	ax-mp	⊢ ( Lim ( card ‘ ( ℵ ‘ 𝐴 ) ) ↔ Lim ( ℵ ‘ 𝐴 ) )
7	2 4 6	3bitr3i	⊢ ( ω ⊆ ( ℵ ‘ 𝐴 ) ↔ Lim ( ℵ ‘ 𝐴 ) )
8	1 7	bitri	⊢ ( 𝐴 ∈ On ↔ Lim ( ℵ ‘ 𝐴 ) )