Theorem onsucssi

Description: A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of TakeutiZaring p. 42 and its converse. (Contributed by NM, 16-Sep-1995)

	Ref	Expression
Hypotheses	onssi.1	$$⊢A\in \mathrm{On}$$
	onsucssi.2	$$⊢B\in \mathrm{On}$$
Assertion	onsucssi	$$⊢A\in B\leftrightarrow \mathrm{suc}A\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		onssi.1	$$⊢A\in \mathrm{On}$$
2		onsucssi.2	$$⊢B\in \mathrm{On}$$
3	2	onordi	$$⊢\mathrm{Ord}B$$
4		ordelsuc	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{Ord}B\right)\to \left(A\in B\leftrightarrow \mathrm{suc}A\subseteq B\right)$$
5	1 3 4	mp2an	$$⊢A\in B\leftrightarrow \mathrm{suc}A\subseteq B$$