# Metamath Proof Explorer

## Theorem limensuci

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

Ref Expression
Hypothesis limensuci.1 ${⊢}\mathrm{Lim}{A}$
Assertion limensuci ${⊢}{A}\in {V}\to {A}\approx \mathrm{suc}{A}$

### Proof

Step Hyp Ref Expression
1 limensuci.1 ${⊢}\mathrm{Lim}{A}$
2 1 limenpsi ${⊢}{A}\in {V}\to {A}\approx \left({A}\setminus \left\{\varnothing \right\}\right)$
3 2 ensymd ${⊢}{A}\in {V}\to \left({A}\setminus \left\{\varnothing \right\}\right)\approx {A}$
4 0ex ${⊢}\varnothing \in \mathrm{V}$
5 en2sn ${⊢}\left(\varnothing \in \mathrm{V}\wedge {A}\in {V}\right)\to \left\{\varnothing \right\}\approx \left\{{A}\right\}$
6 4 5 mpan ${⊢}{A}\in {V}\to \left\{\varnothing \right\}\approx \left\{{A}\right\}$
7 incom ${⊢}\left({A}\setminus \left\{\varnothing \right\}\right)\cap \left\{\varnothing \right\}=\left\{\varnothing \right\}\cap \left({A}\setminus \left\{\varnothing \right\}\right)$
8 disjdif ${⊢}\left\{\varnothing \right\}\cap \left({A}\setminus \left\{\varnothing \right\}\right)=\varnothing$
9 7 8 eqtri ${⊢}\left({A}\setminus \left\{\varnothing \right\}\right)\cap \left\{\varnothing \right\}=\varnothing$
10 limord ${⊢}\mathrm{Lim}{A}\to \mathrm{Ord}{A}$
11 1 10 ax-mp ${⊢}\mathrm{Ord}{A}$
12 ordirr ${⊢}\mathrm{Ord}{A}\to ¬{A}\in {A}$
13 11 12 ax-mp ${⊢}¬{A}\in {A}$
14 disjsn ${⊢}{A}\cap \left\{{A}\right\}=\varnothing ↔¬{A}\in {A}$
15 13 14 mpbir ${⊢}{A}\cap \left\{{A}\right\}=\varnothing$
16 unen ${⊢}\left(\left(\left({A}\setminus \left\{\varnothing \right\}\right)\approx {A}\wedge \left\{\varnothing \right\}\approx \left\{{A}\right\}\right)\wedge \left(\left({A}\setminus \left\{\varnothing \right\}\right)\cap \left\{\varnothing \right\}=\varnothing \wedge {A}\cap \left\{{A}\right\}=\varnothing \right)\right)\to \left(\left({A}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)\approx \left({A}\cup \left\{{A}\right\}\right)$
17 9 15 16 mpanr12 ${⊢}\left(\left({A}\setminus \left\{\varnothing \right\}\right)\approx {A}\wedge \left\{\varnothing \right\}\approx \left\{{A}\right\}\right)\to \left(\left({A}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)\approx \left({A}\cup \left\{{A}\right\}\right)$
18 3 6 17 syl2anc ${⊢}{A}\in {V}\to \left(\left({A}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}\right)\approx \left({A}\cup \left\{{A}\right\}\right)$
19 0ellim ${⊢}\mathrm{Lim}{A}\to \varnothing \in {A}$
20 1 19 ax-mp ${⊢}\varnothing \in {A}$
21 4 snss ${⊢}\varnothing \in {A}↔\left\{\varnothing \right\}\subseteq {A}$
22 20 21 mpbi ${⊢}\left\{\varnothing \right\}\subseteq {A}$
23 undif ${⊢}\left\{\varnothing \right\}\subseteq {A}↔\left\{\varnothing \right\}\cup \left({A}\setminus \left\{\varnothing \right\}\right)={A}$
24 22 23 mpbi ${⊢}\left\{\varnothing \right\}\cup \left({A}\setminus \left\{\varnothing \right\}\right)={A}$
25 uncom ${⊢}\left\{\varnothing \right\}\cup \left({A}\setminus \left\{\varnothing \right\}\right)=\left({A}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$
26 24 25 eqtr3i ${⊢}{A}=\left({A}\setminus \left\{\varnothing \right\}\right)\cup \left\{\varnothing \right\}$
27 df-suc ${⊢}\mathrm{suc}{A}={A}\cup \left\{{A}\right\}$
28 18 26 27 3brtr4g ${⊢}{A}\in {V}\to {A}\approx \mathrm{suc}{A}$