# Metamath Proof Explorer

## Theorem limensuc

Description: A limit ordinal is equinumerous to its successor. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion limensuc ${⊢}\left({A}\in {V}\wedge \mathrm{Lim}{A}\right)\to {A}\approx \mathrm{suc}{A}$

### Proof

Step Hyp Ref Expression
1 eleq1 ${⊢}{A}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\to \left({A}\in {V}↔if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\in {V}\right)$
2 id ${⊢}{A}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\to {A}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)$
3 suceq ${⊢}{A}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\to \mathrm{suc}{A}=\mathrm{suc}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)$
4 2 3 breq12d ${⊢}{A}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\to \left({A}\approx \mathrm{suc}{A}↔if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\approx \mathrm{suc}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\right)$
5 1 4 imbi12d ${⊢}{A}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\to \left(\left({A}\in {V}\to {A}\approx \mathrm{suc}{A}\right)↔\left(if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\in {V}\to if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\approx \mathrm{suc}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\right)\right)$
6 limeq ${⊢}{A}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\to \left(\mathrm{Lim}{A}↔\mathrm{Lim}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\right)$
7 limeq ${⊢}\mathrm{On}=if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\to \left(\mathrm{Lim}\mathrm{On}↔\mathrm{Lim}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\right)$
8 limon ${⊢}\mathrm{Lim}\mathrm{On}$
9 6 7 8 elimhyp ${⊢}\mathrm{Lim}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)$
10 9 limensuci ${⊢}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\in {V}\to if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)\approx \mathrm{suc}if\left(\mathrm{Lim}{A},{A},\mathrm{On}\right)$
11 5 10 dedth ${⊢}\mathrm{Lim}{A}\to \left({A}\in {V}\to {A}\approx \mathrm{suc}{A}\right)$
12 11 impcom ${⊢}\left({A}\in {V}\wedge \mathrm{Lim}{A}\right)\to {A}\approx \mathrm{suc}{A}$