Metamath Proof Explorer


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 ( ℵ ‘ 𝐴 ) )