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\leftrightarrow \mathrm{suc}B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dflim4	$$⊢\mathrm{Lim}A\leftrightarrow \left(\mathrm{Ord}A\wedge \varnothing \in A\wedge \forall x\in A\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\leftrightarrow \mathrm{suc}B\in A\right)$$
4	3	rspccv	$$⊢\forall x\in A\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\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\leftrightarrow \mathrm{suc}B\in A\right)$$