This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem alephislim

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

Ref Expression
Assertion alephislim ⊢ A ∈ On ↔ Lim ⁡ ℵ ⁡ A

Proof

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