Theorem trsuc

Description: A set whose successor belongs to a transitive class also belongs. (Contributed by NM, 5-Sep-2003) (Proof shortened by Andrew Salmon, 12-Aug-2011)

	Ref	Expression
Assertion	trsuc	$$⊢\left(\mathrm{Tr}A\wedge \mathrm{suc}B\in A\right)\to B\in A$$

Proof

Step	Hyp	Ref	Expression
1		trel	$$⊢\mathrm{Tr}A\to \left(\left(B\in \mathrm{suc}B\wedge \mathrm{suc}B\in A\right)\to B\in A\right)$$
2		sssucid	$$⊢B\subseteq \mathrm{suc}B$$
3		ssexg	$$⊢\left(B\subseteq \mathrm{suc}B\wedge \mathrm{suc}B\in A\right)\to B\in \mathrm{V}$$
4	2 3	mpan	$$⊢\mathrm{suc}B\in A\to B\in \mathrm{V}$$
5		sucidg	$$⊢B\in \mathrm{V}\to B\in \mathrm{suc}B$$
6	4 5	syl	$$⊢\mathrm{suc}B\in A\to B\in \mathrm{suc}B$$
7	6	ancri	$$⊢\mathrm{suc}B\in A\to \left(B\in \mathrm{suc}B\wedge \mathrm{suc}B\in A\right)$$
8	1 7	impel	$$⊢\left(\mathrm{Tr}A\wedge \mathrm{suc}B\in A\right)\to B\in A$$