Theorem ordsssuc

Description: An ordinal is a subset of another ordinal if and only if it belongs to its successor. (Contributed by NM, 28-Nov-2003)

	Ref	Expression
Assertion	ordsssuc	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\leftrightarrow A\in \mathrm{suc}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
2		ordsseleq	$$⊢\left(\mathrm{Ord}A\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$
3	1 2	sylan	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$
4		elsucg	$$⊢A\in \mathrm{On}\to \left(A\in \mathrm{suc}B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$
5	4	adantr	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{Ord}B\right)\to \left(A\in \mathrm{suc}B\leftrightarrow \left(A\in B\vee A=B\right)\right)$$
6	3 5	bitr4d	$$⊢\left(A\in \mathrm{On}\wedge \mathrm{Ord}B\right)\to \left(A\subseteq B\leftrightarrow A\in \mathrm{suc}B\right)$$