Description: Every aleph is a limit ordinal. (Contributed by NM, 11-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Assertion | alephislim | ⊢ ( 𝐴 ∈ On ↔ Lim ( ℵ ‘ 𝐴 ) ) |
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 ( ℵ ‘ 𝐴 ) ) |