Theorem limsuc2

Description: Limit ordinals in the sense inclusive of zero contain all successors of their members. (Contributed by Stefan O'Rear, 20-Jan-2015)

	Ref	Expression
Assertion	limsuc2	$$⊢\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\to \left(B\in A\leftrightarrow \mathrm{suc}B\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		ordunisuc2	$$⊢\mathrm{Ord}A\to \left(A=\bigcup A\leftrightarrow \forall x\in A\mathrm{suc}x\in A\right)$$
2	1	biimpa	$$⊢\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\to \forall x\in A\mathrm{suc}x\in A$$
3		suceq	$$⊢x=B\to \mathrm{suc}x=\mathrm{suc}B$$
4	3	eleq1d	$$⊢x=B\to \left(\mathrm{suc}x\in A\leftrightarrow \mathrm{suc}B\in A\right)$$
5	4	rspccva	$$⊢\left(\forall x\in A\mathrm{suc}x\in A\wedge B\in A\right)\to \mathrm{suc}B\in A$$
6	2 5	sylan	$$⊢\left(\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\wedge B\in A\right)\to \mathrm{suc}B\in A$$
7	6	ex	$$⊢\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\to \left(B\in A\to \mathrm{suc}B\in A\right)$$
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	8 10	syl	$$⊢\mathrm{Ord}A\to \left(\mathrm{suc}B\in A\to B\in A\right)$$
12	11	adantr	$$⊢\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\to \left(\mathrm{suc}B\in A\to B\in A\right)$$
13	7 12	impbid	$$⊢\left(\mathrm{Ord}A\wedge A=\bigcup A\right)\to \left(B\in A\leftrightarrow \mathrm{suc}B\in A\right)$$