Metamath Proof Explorer

Theorem limsuc

Description: The successor of a member of a limit ordinal is also a member. (Contributed by NM, 3-Sep-2003)

Ref Expression
Assertion limsuc ${⊢}\mathrm{Lim}{A}\to \left({B}\in {A}↔\mathrm{suc}{B}\in {A}\right)$

Proof

Step Hyp Ref Expression
1 dflim4 ${⊢}\mathrm{Lim}{A}↔\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)$
2 suceq ${⊢}{x}={B}\to \mathrm{suc}{x}=\mathrm{suc}{B}$
3 2 eleq1d ${⊢}{x}={B}\to \left(\mathrm{suc}{x}\in {A}↔\mathrm{suc}{B}\in {A}\right)$
4 3 rspccv ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\to \left({B}\in {A}\to \mathrm{suc}{B}\in {A}\right)$
5 4 3ad2ant3 ${⊢}\left(\mathrm{Ord}{A}\wedge \varnothing \in {A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\mathrm{suc}{x}\in {A}\right)\to \left({B}\in {A}\to \mathrm{suc}{B}\in {A}\right)$
6 1 5 sylbi ${⊢}\mathrm{Lim}{A}\to \left({B}\in {A}\to \mathrm{suc}{B}\in {A}\right)$
7 limord ${⊢}\mathrm{Lim}{A}\to \mathrm{Ord}{A}$
8 ordtr ${⊢}\mathrm{Ord}{A}\to \mathrm{Tr}{A}$
9 trsuc ${⊢}\left(\mathrm{Tr}{A}\wedge \mathrm{suc}{B}\in {A}\right)\to {B}\in {A}$
10 9 ex ${⊢}\mathrm{Tr}{A}\to \left(\mathrm{suc}{B}\in {A}\to {B}\in {A}\right)$
11 7 8 10 3syl ${⊢}\mathrm{Lim}{A}\to \left(\mathrm{suc}{B}\in {A}\to {B}\in {A}\right)$
12 6 11 impbid ${⊢}\mathrm{Lim}{A}\to \left({B}\in {A}↔\mathrm{suc}{B}\in {A}\right)$